Theorem 0re 5363

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

Assertion

Ref	Expression
0re	|- 0 e. RR

Proof of Theorem 0re

Step	Hyp	Ref	Expression
1		0cn 5251	. . . 4 |- 0 e. CC
2		axcnre 5209	. . . 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 1626	. . . 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 1016	. . . 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 5206	. . . 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 5195	. . . . . . . 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 1525	. . . . . 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 1723	. . . 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 1277	. 2 |- (E.x x e. RR -> 0 e. RR)
18	8, 17	ax-mp 7	1 |- 0 e. RR

Syntax hints:   /\ wa 223  E.wex 956   = wceq 1099   e. wcel 1105  E.wrex 1622  (class class class)co 3902  CCcc 5155  RRcr 5156  0cc0 5157  ici 5159   + caddc 5160   x. cmul 5162

This theorem is referenced by:  axmulgt0 5429  addgt0 5523  addge0 5524  addgegt0 5525  add20 5527  mulge0 5532  gt0ne0 5536  lesub0 5537  msqgt0 5538  msqge0 5539  msqgt0t 5540  msqge0t 5541  gt0ne0t 5543  ne0gt0t 5544  ltadd1t 5548  leadd1t 5550  ltsubaddt 5552  lesubaddt 5554  ltmullem 5565  lt2addt 5568  le2addt 5569  addgt0t 5571  addgegt0t 5572  addge0t 5574  ltaddpost 5575  ltnegt 5579  lenegt 5581  lt0neg1t 5592  lt0neg2t 5593  le0neg1t 5594  le0neg2t 5595  addge01t 5596  lesub0t 5602  mulge0t 5603  redivclt 5707  elimge0 5717  recgt0i 5721  ltm1t 5722  prodgt0lem 5725  prodgt0 5726  prodge0 5727  prodgt0t 5733  prodge0t 5735  ltmul1t 5737  lemul1it 5744  lemul1itOLD 5745  ltmul12it 5748  lemul12itOLD 5750  lemul12it 5751  mulgt1t 5752  lemulge11t 5755  ltdiv1t 5756  gt0divt 5758  ge0divt 5759  ltmuldivt 5768  lt2msq 5780  ltrect 5783  lerect 5784  lt2msqt 5785  lediv12it 5795  recgt1it 5799  recrecltt 5801  le2msqt 5802  halfpos 5803  ledivp1t 5804  ledivp1 5805  ltdivp1 5806  squeeze0 5823  nnge1t 5842  nngt0t 5845  0nnn 5847  nnrecgt0t 5851  nnleltp1t 5852  halfpost 5934  xrsupsslem 5974  xrinfmsslem 5975  nn0ssre 6001  lt0nnn0 6014  nn0ge0t 6015  nn0le0eq0t 6017  nn0ltp1let 6025  elnnz 6043  0z 6044  elnn0z 6045  elnnz1 6053  nn0subt 6059  elnn0nn 6069  zltp1let 6079  recnzt 6089  gtndivt 6091  uzindOLD 6107  flhalft 6140  qsqueeze 6169  rpge0t 6176  0nrp 6181  seq1lem2 6198  ser1mono 6225  ioopos 6277  icoshftf1olem 6294  icoun 6297  snunioo 6299  elfz2nn0t 6378  expge0t 6473  expordit 6482  exple1t 6489  expubndt 6490  sq11t 6511  le2sqit 6514  sqge0t 6515  sumsqne0 6516  sqlecant 6523  bernneq2 6535  expnbndt 6536  discrlem1 6537  discrlem3 6539  discrlem 6540  nnesq 6543  sqr0 6553  sqrlem1 6554  sqrlem2 6555  sqrlem5 6558  sqrlem6 6559  sqrlem8 6561  sqrlem11 6564  sqrlem12 6565  sqrlem15 6568  sqrlem19 6572  sqrlem24 6577  sqrgt0i 6578  sqrlem26 6579  sqrth 6580  sqrcl 6581  sqrge0 6583  sqrmul 6586  sqrclt 6591  sqrgt0t 6592  sqrge0t 6593  sqrlet 6594  sqr00t 6595  sqr1 6597  sqr4 6598  sqr9 6599  sqr2gt1lt2 6600  sqrsqt 6603  sqsqrt 6604  sqr2irrlem1 6605  sqr2irrlem4 6608  sqr2irr 6610  inelr 6616  crut 6619  crne0 6621  rimul 6626  nthruz 6628  reret 6685  re0 6706  im0 6707  rei 6710  imi 6711  cj0 6712  absgt0 6729  absrpclt 6741  absidt 6748  leabst 6750  absort 6751  absexpt 6754  leabs 6758  absltt 6768  abslttOLD 6769  abslet 6770  abs1m 6792  abs3lemt 6795  facdivt 6830  facwordit 6832  faclbnd3 6835  faclbnd4lem1 6836  bcval4t 6850  bcpasc 6858  bccl2t 6860  fsumcmp0 6930  serzcmp0 6944  climrecl 6998  climge0 7000  iserzcmp0 7030  ser1cmp0 7062  cvgcmp 7071  cvgcmpub 7072  cvgcmp3cetlem1 7075  cvgcmp3cetlem2 7076  iserzgt0 7097  reccnv 7104  fnsmnt 7112  expcnvlem2 7114  expcnvlem6 7118  georeclim 7126  geoisumr 7129  0.999... 7132  cvgratlem4 7139  cvgratlem5 7140  reefclt 7211  erelem2 7213  erelem3 7214  efaddlem12 7242  efaddlem20 7250  efaddlem25 7255  eftabs 7268  ef01tllem2 7277  ef01tlub 7278  absef01tlub 7280  abspef01tlub 7287  efgt1 7295  efgt0 7296  efgt0t 7297  absefm1le 7303  eflegeolem2 7305  eflegeot 7307  reeff1olem1 7315  reeff1olem1OLD 7317  reeff1o 7319  reefiso 7321  sin0 7337  cos0 7339  sinbndt 7358  cosbndt 7359  sin01bndlem1 7360  sin01bndlem2 7361  sin01bndlem3 7362  cos01bndlem2 7363  cos01bndlem3 7364  cos1bnd 7367  cos2bnd 7368  sin01gt0 7369  cos01gt0 7370  sin02gt0 7371  sincos1sgn 7372  sincos2sgn 7373  sin4lt0 7374  znnenlem 7394  znnenlemOLD 7395  znnen 7396  ruclem8 7411  ruclem39 7442  metgt0 7709  metxp 7722  dscmet 7804  lmnn 7821  readdsubg 8014  nvm1 8168  nvz0 8172  nvmtri 8175  nv1 8180  sm1cnilem 8216  ipid 8232  nmosetn0 8295  nmoge0 8297  nmo0 8318  0blo 8319  nmlno0lem 8320  nmlnoubi 8323  nmlnogt0 8324  nmblolbii 8325  blocnilem 8330  siilem2 8378  ubthlem10 8404  ubthlem12 8406  ubthlem13 8407  minveclem10 8420  minveclem14 8424  minveclem16 8426  minveclem21 8431  minveclem25 8435  minveclem35 8445  minveclem38 8448  minveceu 8449  htthlem10 8493  pilem1 8503  pilem2 8504  pilem3 8505  sinhalfpilem 8511  sinperlem1 8518  sincosq1lem 8533  sincosq1sgn 8534  sincosq2sgn 8535  sinq12gt0t 8538  sincos4thpi 8540  sincos6thpi 8541  cosh111lem1 8542  cosh111t 8545  efif 8549  efifolem1 8550  efifolem2 8551  efifolem3 8552  efifolem4 8553  efifolem5 8554  efifolem6 8555  efifolem7 8556  efif1lem1 8558  efif1lem2 8559  efif1lem3 8560  efif1lem5 8562  efif1lem6 8563  efif1lem7 8564  circgrpOLD 8571  circgrp 8573  resslogrn 8588  log1 8601  pilog 8603  log1OLD 8620  iintlem1 8826  hiidge0t 9113  his6t 9114  normlem6 9130  normlem7tALT 9134  normgt0tOLD 9142  normgt0t 9143  norm-it 9145  norm-ii 9153  normsub 9157  normpyct 9162  normpar2 9172  bcsALT 9195  hlimcaui 9257  norm1t 9272  occllem7 9309  projlem1 9316  projlem2 9317  projlem4 9319  projlem5 9320  projlem6 9321  projlem7 9322  projlem8 9323  projlem13 9328  projlem18 9333  projlem28 9343  pjthlem10 9357  pjthlem11 9358  osumlem3 9711  pjnel 9799  nmopsetn0 9923  nmfnsetn0 9936  nmopge0t 9965  nmopgt0t 9966  nmfnge0t 9981  nmop0 10040  nmfn0 10041  0bdop 10047  nmlnop0ALT 10049  unopbdt 10069  nmbdoplb 10078  nmcopexlem3 10082  nmcopexlem5 10084  nmcoplb 10087  lnopcon 10092  nmbdfnlb 10107  nmbdfnlbt 10108  nmcfnexlem3 10111  nmcfnexlem5 10113  nmcfnlb 10116  lnfncon 10119  cnlnadjlem7 10135  nmopco 10156  unierr 10164  branmfnt 10165  leoprf2t 10186  leoprft 10187  leopmult 10193  nmopleidt 10197  pjbdln 10201  hmopidmchlem 10203  pjnormss 10221  hstle1t 10277  stle0 10290  strlem1 10301  strlem3a 10303  strlem5 10306  jplem1 10319  cdj3lem1 10480

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-mp 5012  df-ltp 5013  df-plpr 5087  df-mpr 5088  df-enr 5089  df-nr 5090  df-plr 5091  df-mr 5092  df-0r 5094  df-1r 5095  df-m1r 5096  df-c 5163  df-0 5164  df-1 5165  df-i 5166  df-r 5167  df-plus 5168  df-mul 5169

Copyright terms: Public domain