Theorem axaddcl 5263

Description: Closure law for addition of complex numbers. Axiom 5 of 25 for real and complex numbers, derived from ZF set theory.

Assertion

Ref	Expression
axaddcl	⊢ ((A ∈ ℂ ⋀ B ∈ ℂ) → (A + B) ∈ ℂ)

Proof of Theorem axaddcl

Step	Hyp	Ref	Expression
1		axaddopr 5257	. 2 ⊢ + :(ℂ × ℂ)–→ℂ
2	1	foprcl 4017	1 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ) → (A + B) ∈ ℂ)

Syntax hints:   → wi 3   ⋀ wa 223   ∈ wcel 956  (class class class)co 3965  ℂcc 5224   + caddc 5229

This theorem is referenced by:  addclt 5293  adddirt 5311  addcl 5312  add4t 5330  peano2cn 5336  cnegextlem3 5339  cnegext 5340  0cnALT 5342  negeu 5347  addsubasst 5375  2addsubt 5381  muladdt 5413  muladd11t 5414  nppcan2t 5462  addsub4t 5465  mulsubt 5469  ppncant 5473  recext 5677  muleqaddt 5689  conjmult 5773  halfaddsubcl 6007  halfaddsubt 6008  uzindOLD 6176  shftval2t 6304  shftval5t 6307  2shft 6309  ser0cl1 6516  bernneq 6603  crret 6722  crretOLD 6723  crimt 6724  crimtOLD 6725  recjt 6773  imcjt 6774  sqabsaddt 6803  absreimsqt 6811  absreimt 6812  ser1absdiflem 6886  fsumclt 6973  fsumadd 6980  binomlem5 7028  climaddlem3 7072  serzf0 7125  ser1f0 7126  fnsmnt 7181  cosclt 7394  efi4pt 7397  resin4pt 7398  recos4pt 7399  efivalt 7409  addsint 7419  demoivre 7446  ioo2bl 7876  addcn 7948  4ipval2 8321  4ipval3 8325  ipcj 8330  cnph 8438  minveclem18 8522  minveclem27 8531  cosco 8622  efgh 8668  effoi 8701  effoiOLD 8702  hhssnv 9108  hoadddirt 9705  golem1 10171  superpos 10252  mslb1 10545  2wsms 10546

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 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2865  ax-inf2 4617

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 2500  df-int 2530  df-iun 2564  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2829  df-id 2832  df-po 2839  df-so 2849  df-fr 2916  df-we 2933  df-ord 2950  df-on 2951  df-lim 2952  df-suc 2953  df-om 3132  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194  df-fv 3198  df-rdg 3934  df-opr 3967  df-oprab 3968  df-1st 4080  df-2nd 4081  df-1o 4134  df-oadd 4136  df-omul 4137  df-er 4262  df-ec 4264  df-qs 4267  df-ni 4992  df-pli 4993  df-mi 4994  df-lti 4995  df-plpq 5027  df-mpq 5028  df-enq 5029  df-nq 5030  df-plq 5031  df-mq 5032  df-rq 5033  df-ltq 5034  df-1q 5035  df-np 5078  df-plp 5080  df-ltp 5082  df-plpr 5156  df-enr 5158  df-nr 5159  df-plr 5160  df-c 5232  df-plus 5237

Copyright terms: Public domain