HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem axaddrcl 5195
Description: Closure law for addition in the real subfield of complex numbers. Axiom 6 of 25 for real and complex numbers, derived from ZF set theory.
Assertion
Ref Expression
axaddrcl |- ((A e. RR /\ B e. RR) -> (A + B) e. RR)
Proof of Theorem axaddrcl
StepHypRef Expression
1 elreal 5173 . 2 |- (A e. RR <-> E.x(x e. R. /\ <.x, 0R>. = A))
2 elreal 5173 . 2 |- (B e. RR <-> E.y(y e. R. /\ <.y, 0R>. = B))
3 opreq1 3907 . . 3 |- (<.x, 0R>. = A -> (<.x, 0R>. + <.y, 0R>.) = (A + <.y, 0R>.))
43eleq1d 1516 . 2 |- (<.x, 0R>. = A -> ((<.x, 0R>. + <.y, 0R>.) e. RR <-> (A + <.y, 0R>.) e. RR))
5 opreq2 3908 . . 3 |- (<.y, 0R>. = B -> (A + <.y, 0R>.) = (A + B))
65eleq1d 1516 . 2 |- (<.y, 0R>. = B -> ((A + <.y, 0R>.) e. RR <-> (A + B) e. RR))
7 addresr 5179 . . 3 |- ((x e. R. /\ y e. R.) -> (<.x, 0R>. + <.y, 0R>.) = <.(x +R y), 0R>.)
8 addclsr 5115 . . . 4 |- ((x e. R. /\ y e. R.) -> (x +R y) e. R.)
9 opelreal 5172 . . . 4 |- (<.(x +R y), 0R>. e. RR <-> (x +R y) e. R.)
108, 9sylibr 200 . . 3 |- ((x e. R. /\ y e. R.) -> <.(x +R y), 0R>. e. RR)
117, 10eqeltrd 1524 . 2 |- ((x e. R. /\ y e. R.) -> (<.x, 0R>. + <.y, 0R>.) e. RR)
121, 2, 4, 6, 112gencl 1804 1 |- ((A e. RR /\ B e. RR) -> (A + B) e. RR)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223   = wceq 1099   e. wcel 1105  <.cop 2382  (class class class)co 3902  R.cnr 4916  0Rc0r 4917   +R cplr 4920  RRcr 5156   + caddc 5160
This theorem is referenced by:  readdclt 5225  readdcl 5257  cnegextlem3 5270  cnegext 5271  peano2re 5359  resubclt 5361  0re 5363  axltadd 5428  ltaddsubt 5556  leaddsubt 5558  ltleaddt 5570  recextlem2 5607  recext 5608  recp1lt1 5800  recrecltt 5801  nnge1t 5842  nnaddm1clt 5856  avglet 5942  zaddclt 6063  uzindOLD 6107  fladdzt 6138  rpaddclt 6178  ser1recl 6219  icoshft 6292  bernneq 6534  absrelet 6755  absimlet 6756  caubnd 6814  ser1absdiflem 6817  fsumreclt 6906  fsumcmp 6929  fsumabs 6932  2climnn 6990  2climnn0 6991  climge0 7000  climaddlem3 7003  climmullem1 7007  climmullem2 7008  climmullem3 7009  climmullem4 7010  climmullem5 7011  climmullem8 7014  climcau 7043  caucvglem5 7048  caucvglem6 7049  caucvg 7050  serzf0 7056  ser1f0 7057  ser1cmp 7061  ser1cmp2lem 7063  ser1cmp2 7064  cvgcmp2lem 7067  infcvglem1 7107  infcvglem3 7109  ivthlem6 7172  ivthlem7 7173  ivthlem6OLD 7181  ivthlem7OLD 7182  efcn 7314  ruclem13 7416  metxplem3 7716  bl2in 7731  blss 7741  bl2ioo 7798  ioo2bl 7799  blssioo 7800  tgioolem 7801  iscau3 7824  lmuni 7834  lmle 7843  lmcau 7878  bcthlem24 7904  bcthlem25 7905  readdsubg 8014  ubthlem11 8405  minveclem21 8431  minveclem27 8437  minveclem31 8441  shftefif1olem 8574  shftefif1olemOLD 8575  relogmult 8605  logmultOLD 8623  truni1 8743  msr4 8820  mslb1 8823  msra3 8825  iintlem1 8826  iint 8828  trdom 8829  trran 8830  trnij 8831  cnvtr 8832  hcau2 9205  nmoptri 10155  hmopidmch 10204  hstlet 10281  stadd 10297  stadd3 10299  cdj1 10479  cdj3lem2b 10483  cdj3 10487
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-reu 1627  df-rab 1628  df-v 1787  df-sbc 1913  df-csb 1973  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-int 2502  df-iun 2536  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-fv 3161  df-rdg 3871  df-opr 3904  df-oprab 3905  df-1st 4017  df-2nd 4018  df-1o 4071  df-oadd 4073  df-omul 4074  df-er 4199  df-ec 4201  df-qs 4204  df-ni 4923  df-pli 4924  df-mi 4925  df-lti 4926  df-plpq 4958  df-mpq 4959  df-enq 4960  df-nq 4961  df-plq 4962  df-mq 4963  df-rq 4964  df-ltq 4965  df-1q 4966  df-np 5009  df-1p 5010  df-plp 5011  df-ltp 5013  df-plpr 5087  df-enr 5089  df-nr 5090  df-plr 5091  df-0r 5094  df-c 5163  df-r 5167  df-plus 5168
Copyright terms: Public domain