Theorem 0re 5412

Description: 0 is a real number. Proved without referencing 1re 5407. (Contributed by Eric Schmidt, 21-May-2007.)

Assertion

Ref	Expression
0re	|- 0 e. RR

Proof of Theorem 0re

Step	Hyp	Ref	Expression
1		0cn 5300	. . . 4 |- 0 e. CC
2		axcnre 5258	. . . 4 |- (0 e. CC -> E.x e. RR E.y e. RR 0 = (x + (i x. y)))
3	1, 2	ax-mp 7	. . 3 |- E.x e. RR E.y e. RR 0 = (x + (i x. y))
4		df-rex 1642	. . . 4 |- (E.x e. RR E.y e. RR 0 = (x + (i x. y)) <-> E.x(x e. RR /\ E.y e. RR 0 = (x + (i x. y))))
5		pm3.26 319	. . . . 5 |- ((x e. RR /\ E.y e. RR 0 = (x + (i x. y))) -> x e. RR)
6	5	19.22i 1036	. . . 4 |- (E.x(x e. RR /\ E.y e. RR 0 = (x + (i x. y))) -> E.x x e. RR)
7	4, 6	sylbi 199	. . 3 |- (E.x e. RR E.y e. RR 0 = (x + (i x. y)) -> E.x x e. RR)
8	3, 7	ax-mp 7	. 2 |- E.x x e. RR
9		axrnegex 5255	. . . 4 |- (x e. RR -> E.y e. RR (x + y) = 0)
10		pm3.27 323	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ (x + y) = 0) -> (x + y) = 0)
11		axaddrcl 5244	. . . . . . . 8 |- ((x e. RR /\ y e. RR) -> (x + y) e. RR)
12	11	adantr 389	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ (x + y) = 0) -> (x + y) e. RR)
13	10, 12	eqeltrrd 1541	. . . . . 6 |- (((x e. RR /\ y e. RR) /\ (x + y) = 0) -> 0 e. RR)
14	13	ex 373	. . . . 5 |- ((x e. RR /\ y e. RR) -> ((x + y) = 0 -> 0 e. RR))
15	14	r19.23adva 1739	. . . 4 |- (x e. RR -> (E.y e. RR (x + y) = 0 -> 0 e. RR))
16	9, 15	mpd 26	. . 3 |- (x e. RR -> 0 e. RR)
17	16	19.23aiv 1290	. 2 |- (E.x x e. RR -> 0 e. RR)
18	8, 17	ax-mp 7	1 |- 0 e. RR

Syntax hints:   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977  E.wrex 1638  (class class class)co 3948  CCcc 5204  RRcr 5205  0cc0 5206  ici 5208   + caddc 5209   x. cmul 5211

This theorem is referenced by:  axmulgt0 5478  addgt0 5572  addge0 5573  addgegt0 5574  add20 5576  mulge0 5581  gt0ne0 5585  lesub0 5586  msqgt0 5587  msqge0 5588  msqgt0t 5589  msqge0t 5590  gt0ne0t 5592  ne0gt0t 5593  ltadd1t 5597  leadd1t 5599  ltsubaddt 5601  lesubaddt 5603  ltmullem 5614  lt2addt 5617  le2addt 5618  addgt0t 5620  addgegt0t 5621  addge0t 5623  ltaddpost 5624  ltnegt 5628  lenegt 5630  lt0neg1t 5641  lt0neg2t 5642  le0neg1t 5643  le0neg2t 5644  addge01t 5645  lesub0t 5651  mulge0t 5652  redivclt 5756  elimge0 5766  recgt0i 5770  ltm1t 5771  prodgt0lem 5774  prodgt0 5775  prodge0 5776  prodgt0t 5782  prodge0t 5784  ltmul1t 5786  lemul1it 5793  lemul1itOLD 5794  ltmul12it 5797  lemul12itOLD 5799  lemul12it 5800  mulgt1t 5801  lemulge11t 5804  ltdiv1t 5805  gt0divt 5807  ge0divt 5808  ltmuldivt 5817  lt2msq 5829  ltrect 5832  lerect 5833  lt2msqt 5834  lediv12it 5844  recgt1it 5848  recrecltt 5850  le2msqt 5851  halfpos 5852  ledivp1t 5853  ledivp1 5854  ltdivp1 5855  squeeze0 5872  nnge1t 5891  nngt0t 5894  0nnn 5896  nnrecgt0t 5900  nnleltp1t 5901  halfpost 5983  xrsupsslem 6023  xrinfmsslem 6024  nn0ssre 6050  lt0nnn0 6063  nn0ge0t 6064  nn0le0eq0t 6066  nn0ltp1let 6074  elnnz 6092  0z 6093  elnn0z 6094  elnnz1 6102  nn0subt 6108  elnn0nn 6118  zltp1let 6128  recnzt 6138  gtndivt 6140  uzindOLD 6156  flhalft 6189  qsqueeze 6218  rpge0t 6225  0nrp 6230  seq1lem2 6247  ser1mono 6274  ioopos 6326  icoshftf1olem 6343  icoun 6346  snunioo 6348  elfz2nn0t 6427  expge0t 6522  expordit 6531  exple1t 6538  expubndt 6539  sq11t 6560  le2sqit 6563  sqge0t 6564  sumsqne0 6565  sqlecant 6572  bernneq2 6584  expnbndt 6585  discrlem1 6586  discrlem3 6588  discrlem 6589  nnesq 6592  sqr0 6602  sqrlem1 6603  sqrlem2 6604  sqrlem5 6607  sqrlem6 6608  sqrlem8 6610  sqrlem11 6613  sqrlem12 6614  sqrlem15 6617  sqrlem19 6621  sqrlem24 6626  sqrgt0i 6627  sqrlem26 6628  sqrth 6629  sqrcl 6630  sqrge0 6632  sqrmul 6635  sqrclt 6640  sqrgt0t 6641  sqrge0t 6642  sqrlet 6643  sqr00t 6644  sqr1 6646  sqr4 6647  sqr9 6648  sqr2gt1lt2 6649  sqrsqt 6652  sqsqrt 6653  sqr2irrlem1 6654  sqr2irrlem4 6657  sqr2irr 6659  inelr 6665  crut 6668  crne0 6670  rimul 6675  nthruz 6677  reret 6734  re0 6755  im0 6756  rei 6759  imi 6760  cj0 6761  absgt0 6778  absrpclt 6790  absidt 6797  leabst 6799  absort 6800  absexpt 6803  leabs 6807  absltt 6817  abslttOLD 6818  abslet 6819  abs1m 6841  abs3lemt 6844  facdivt 6879  facwordit 6881  faclbnd3 6884  faclbnd4lem1 6885  bcval4t 6899  bcpasc 6907  bccl2t 6909  fsumcmp0 6979  serzcmp0 6993  climrecl 7047  climge0 7049  iserzcmp0 7079  ser1cmp0 7111  cvgcmp 7120  cvgcmpub 7121  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  iserzgt0 7146  reccnv 7153  fnsmnt 7161  expcnvlem2 7163  expcnvlem6 7167  georeclim 7175  geoisumr 7178  0.999... 7181  cvgratlem4 7188  cvgratlem5 7189  reefclt 7260  erelem2 7262  erelem3 7263  efaddlem12 7291  efaddlem20 7299  efaddlem25 7304  eftabs 7317  ef01tllem2 7326  ef01tlub 7327  absef01tlub 7329  abspef01tlub 7336  efgt1 7344  efgt0 7345  efgt0t 7346  absefm1le 7352  eflegeolem2 7354  eflegeot 7356  reeff1olem1 7364  reeff1olem1OLD 7366  reeff1o 7368  reefiso 7370  sin0 7386  cos0 7388  sinbndt 7407  cosbndt 7408  sin01bndlem1 7409  sin01bndlem2 7410  sin01bndlem3 7411  cos01bndlem2 7412  cos01bndlem3 7413  cos1bnd 7416  cos2bnd 7417  sin01gt0 7418  cos01gt0 7419  sin02gt0 7420  sincos1sgn 7421  sincos2sgn 7422  sin4lt0 7423  znnenlem 7443  znnenlemOLD 7444  znnen 7445  ruclem8 7460  ruclem39 7491  metgt0 7761  metxp 7774  dscmet 7856  lmnn 7873  readdsubg 8066  nvm1 8231  nvz0 8235  nvmtri 8238  nv1 8243  sm1cnilem 8281  ipid 8297  nmosetn0 8360  nmoge0 8362  nmo0 8383  0blo 8384  nmlno0lem 8385  nmlnoubi 8388  nmlnogt0 8389  nmblolbii 8390  blocnilem 8395  siilem2 8443  ubthlem10 8469  ubthlem12 8471  ubthlem13 8472  minveclem10 8485  minveclem14 8489  minveclem16 8491  minveclem21 8496  minveclem25 8500  minveclem35 8510  minveclem38 8513  minveceu 8514  htthlem10 8559  pilem1 8590  pilem2 8591  pilem3 8592  sinhalfpilem 8598  sinperlem1 8605  sincosq1lem 8620  sincosq1sgn 8621  sincosq2sgn 8622  sinq12gt0t 8625  sincos4thpi 8627  sincos6thpi 8628  cosh111lem1 8629  cosh111t 8632  efif 8636  efifolem1 8637  efifolem2 8638  efifolem3 8639  efifolem4 8640  efifolem5 8641  efifolem6 8642  efifolem7 8643  efif1lem1 8645  efif1lem2 8646  efif1lem3 8647  efif1lem5 8649  efif1lem6 8650  efif1lem7 8651  circgrpOLD 8658  circgrp 8660  resslogrn 8675  log1 8688  pilog 8690  log1OLD 8707  hiidge0t 8885  his6t 8886  normlem6 8902  normlem7tALT 8906  normgt0tOLD 8914  normgt0t 8915  norm-it 8917  norm-ii 8925  normsub 8929  normpyct 8934  normpar2 8944  bcsALT 8967  hlimcaui 9027  norm1t 9042  occllem7 9095  projlem1 9102  projlem2 9103  projlem4 9105  projlem5 9106  projlem6 9107  projlem7 9108  projlem8 9109  projlem13 9114  projlem18 9119  projlem28 9129  pjthlem10 9143  pjthlem11 9144  osumlem3 9497  pjnel 9585  nmopsetn0 9709  nmfnsetn0 9722  nmopge0t 9751  nmopgt0t 9752  nmfnge0t 9767  nmop0 9826  nmfn0 9827  0bdop 9833  nmlnop0ALT 9835  unopbdt 9855  nmbdoplb 9864  nmcopexlem3 9868  nmcopexlem5 9870  nmcoplb 9873  lnopcon 9878  nmbdfnlb 9893  nmbdfnlbt 9894  nmcfnexlem3 9897  nmcfnexlem5 9899  nmcfnlb 9902  lnfncon 9905  cnlnadjlem7 9921  nmopco 9942  unierr 9950  branmfnt 9951  leoprf2t 9972  leoprft 9973  leopmult 9979  nmopleidt 9983  pjbdln 9987  hmopidmchlem 9989  pjnormss 10007  hstle1t 10063  stle0 10076  strlem1 10087  strlem3a 10089  strlem5 10092  jplem1 10105  cdj3lem1 10266  iintlem1 10476

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-pss 2045  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-lim 2943  df-suc 2944  df-om 3122  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-fv 3188  df-rdg 3917  df-opr 3950  df-oprab 3951  df-1st 4063  df-2nd 4064  df-1o 4117  df-oadd 4119  df-omul 4120  df-er 4245  df-ec 4247  df-qs 4250  df-ni 4972  df-pli 4973  df-mi 4974  df-lti 4975  df-plpq 5007  df-mpq 5008  df-enq 5009  df-nq 5010  df-plq 5011  df-mq 5012  df-rq 5013  df-ltq 5014  df-1q 5015  df-np 5058  df-1p 5059  df-plp 5060  df-mp 5061  df-ltp 5062  df-plpr 5136  df-mpr 5137  df-enr 5138  df-nr 5139  df-plr 5140  df-mr 5141  df-0r 5143  df-1r 5144  df-m1r 5145  df-c 5212  df-0 5213  df-1 5214  df-i 5215  df-r 5216  df-plus 5217  df-mul 5218

Copyright terms: Public domain