HomeRelated theorems
GIF version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Closure law for addition of complex numbers. Axiom 5 of 25 for real and complex numbers, derived from ZF set theory. |
| Ref | Expression |
|---|---|
| axaddcl | ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ) → (A + B) ∈ ℂ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axaddopr 5245 | . 2 ⊢ + :(ℂ × ℂ)–→ℂ | |
| 2 | 1 | foprcl 4006 | 1 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ) → (A + B) ∈ ℂ) |
| Colors of variables: wff set class |
| Syntax hints: → wi 3 ⋀ wa 223 ∈ wcel 956 (class class class)co 3954 ℂcc 5212 + caddc 5217 |
| This theorem is referenced by: addclt 5281 adddirt 5299 addcl 5300 add4t 5318 peano2cn 5324 cnegextlem3 5327 cnegext 5328 0cnALT 5330 negeu 5335 addsubasst 5363 2addsubt 5369 muladdt 5401 muladd11t 5402 nppcan2t 5450 addsub4t 5453 mulsubt 5457 ppncant 5461 recext 5665 muleqaddt 5677 conjmult 5761 halfaddsubcl 5995 halfaddsubt 5996 uzindOLD 6164 shftval2t 6292 shftval5t 6295 2shft 6297 ser0cl1 6504 bernneq 6591 crret 6710 crretOLD 6711 crimt 6712 crimtOLD 6713 recjt 6761 imcjt 6762 sqabsaddt 6791 absreimsqt 6799 absreimt 6800 ser1absdiflem 6874 fsumclt 6961 fsumadd 6968 binomlem5 7016 climaddlem3 7060 serzf0 7113 ser1f0 7114 fnsmnt 7169 cosclt 7382 efi4pt 7385 resin4pt 7386 recos4pt 7387 efivalt 7397 addsint 7407 demoivre 7434 ioo2bl 7864 addcn 7936 4ipval2 8305 4ipval3 8309 ipcj 8314 cnph 8422 minveclem18 8506 minveclem27 8515 cosco 8606 efgh 8652 effoi 8684 hhssnv 9073 hoadddirt 9670 golem1 10136 superpos 10218 mslb1 10509 2wsms 10510 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861 ax-inf2 4605 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2499 df-int 2529 df-iun 2563 df-br 2615 df-opab 2662 df-tr 2676 df-eprel 2827 df-id 2830 df-po 2835 df-so 2845 df-fr 2912 df-we 2929 df-ord 2946 df-on 2947 df-lim 2948 df-suc 2949 df-om 3127 df-xp 3179 df-rel 3180 df-cnv 3181 df-co 3182 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fun 3187 df-fn 3188 df-f 3189 df-fv 3193 df-rdg 3923 df-opr 3956 df-oprab 3957 df-1st 4069 df-2nd 4070 df-1o 4123 df-oadd 4125 df-omul 4126 df-er 4251 df-ec 4253 df-qs 4256 df-ni 4980 df-pli 4981 df-mi 4982 df-lti 4983 df-plpq 5015 df-mpq 5016 df-enq 5017 df-nq 5018 df-plq 5019 df-mq 5020 df-rq 5021 df-ltq 5022 df-1q 5023 df-np 5066 df-plp 5068 df-ltp 5070 df-plpr 5144 df-enr 5146 df-nr 5147 df-plr 5148 df-c 5220 df-plus 5225 |