Theorem axaddrcl 5259

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

Step	Hyp	Ref	Expression
1		elreal 5237	. 2 |- (A e. RR <-> E.x(x e. R. /\ <.x, 0R>. = A))
2		elreal 5237	. 2 |- (B e. RR <-> E.y(y e. R. /\ <.y, 0R>. = B))
3		opreq1 3965	. . 3 |- (<.x, 0R>. = A -> (<.x, 0R>. + <.y, 0R>.) = (A + <.y, 0R>.))
4	3	eleq1d 1539	. 2 |- (<.x, 0R>. = A -> ((<.x, 0R>. + <.y, 0R>.) e. RR <-> (A + <.y, 0R>.) e. RR))
5		opreq2 3966	. . 3 |- (<.y, 0R>. = B -> (A + <.y, 0R>.) = (A + B))
6	5	eleq1d 1539	. 2 |- (<.y, 0R>. = B -> ((A + <.y, 0R>.) e. RR <-> (A + B) e. RR))
7		addresr 5243	. . 3 |- ((x e. R. /\ y e. R.) -> (<.x, 0R>. + <.y, 0R>.) = <.(x +R y), 0R>.)
8		addclsr 5179	. . . 4 |- ((x e. R. /\ y e. R.) -> (x +R y) e. R.)
9		opelreal 5236	. . . 4 |- (<.(x +R y), 0R>. e. RR <-> (x +R y) e. R.)
10	8, 9	sylibr 200	. . 3 |- ((x e. R. /\ y e. R.) -> <.(x +R y), 0R>. e. RR)
11	7, 10	eqeltrd 1547	. 2 |- ((x e. R. /\ y e. R.) -> (<.x, 0R>. + <.y, 0R>.) e. RR)
12	1, 2, 4, 6, 11	2gencl 1827	1 |- ((A e. RR /\ B e. RR) -> (A + B) e. RR)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 955   e. wcel 957  <.cop 2409  (class class class)co 3960  R.cnr 4980  0Rc0r 4981   +R cplr 4984  RRcr 5220   + caddc 5224

This theorem is referenced by:  readdclt 5289  readdcl 5321  cnegextlem3 5334  cnegext 5335  peano2re 5423  resubclt 5425  0re 5427  axltadd 5492  ltaddsubt 5619  leaddsubt 5621  ltleaddt 5633  recextlem2 5670  recext 5671  recp1lt1 5863  recrecltt 5864  nnge1t 5905  nnaddm1clt 5919  avglet 6005  zaddclt 6126  uzindOLD 6170  fladdzt 6204  rpaddclt 6245  ser1recl 6286  icoshft 6359  bernneq 6602  absrelet 6831  absimlet 6832  caubnd 6892  ser1absdiflem 6895  fsumreclt 6985  fsumcmp 7008  fsumabs 7011  2climnn 7070  2climnn0 7071  climge0 7080  climaddlem3 7085  climmullem1 7089  climmullem2 7090  climmullem3 7091  climmullem4 7092  climmullem5 7093  climmullem8 7096  climcau 7125  caucvglem5 7130  caucvglem6 7131  caucvg 7132  serzf0 7140  ser1f0 7141  ser1cmp 7145  ser1cmp2lem 7147  ser1cmp2 7148  cvgcmp2lem 7151  infcvglem1 7192  infcvglem3 7194  ivthlem6 7257  ivthlem7 7258  ivthlem6OLD 7266  ivthlem7OLD 7267  efcn 7399  ruclem13 7501  metxplem3 7809  bl2in 7825  blss 7835  blssOLD 7836  bl2ioo 7894  ioo2bl 7895  blssioo 7896  tgioolem 7897  iscau3 7921  iscau4 7923  lmuni 7934  lmle 7943  lmcau 7979  bcthlem24 8005  bcthlem25 8006  readdsubg 8114  ubthlem11 8523  minveclem21 8549  minveclem27 8555  minveclem31 8559  shftefif1olem 8725  relogmult 8754  hcau2 9043  nmoptri 10018  hmopidmch 10070  hstlet 10148  stadd 10164  stadd3 10166  cdj1 10351  cdj3lem2b 10355  cdj3 10359  truni1 10480  msr4 10577  mslb1 10580  msra3 10582  iintlem1 10583  iint 10585  trdom 10586  trran 10587  trnij 10588  cnvtr 10589

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2690  ax-sep 2700  ax-nul 2707  ax-pow 2739  ax-pr 2776  ax-un 2863  ax-inf2 4612

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-reu 1650  df-rab 1651  df-v 1810  df-sbc 1940  df-csb 2000  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-pss 2053  df-nul 2279  df-if 2360  df-pw 2400  df-sn 2410  df-pr 2411  df-tp 2413  df-op 2414  df-uni 2501  df-int 2531  df-iun 2565  df-br 2617  df-opab 2664  df-tr 2678  df-eprel 2829  df-id 2832  df-po 2837  df-so 2847  df-fr 2914  df-we 2931  df-ord 2948  df-on 2949  df-lim 2950  df-suc 2951  df-om 3129  df-xp 3181  df-rel 3182  df-cnv 3183  df-co 3184  df-dm 3185  df-rn 3186  df-res 3187  df-ima 3188  df-fun 3189  df-fn 3190  df-f 3191  df-fv 3195  df-rdg 3929  df-opr 3962  df-oprab 3963  df-1st 4076  df-2nd 4077  df-1o 4130  df-oadd 4132  df-omul 4133  df-er 4258  df-ec 4260  df-qs 4263  df-ni 4987  df-pli 4988  df-mi 4989  df-lti 4990  df-plpq 5022  df-mpq 5023  df-enq 5024  df-nq 5025  df-plq 5026  df-mq 5027  df-rq 5028  df-ltq 5029  df-1q 5030  df-np 5073  df-1p 5074  df-plp 5075  df-ltp 5077  df-plpr 5151  df-enr 5153  df-nr 5154  df-plr 5155  df-0r 5158  df-c 5227  df-r 5231  df-plus 5232

Copyright terms: Public domain