Theorem 0re 6399

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

Assertion

Ref	Expression
0re	|- 0 e. RR

Proof of Theorem 0re

Step	Hyp	Ref	Expression
1		0cn 6277	. . . 4 |- 0 e. CC
2		axcnre 6235	. . . 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 1944	. . . 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		exsimpl 1299	. . . 4 |- (E.x(x e. RR /\ E.y e. RR 0 = (x + (_i x. y))) -> E.x x e. RR)
6	4, 5	sylbi 215	. . 3 |- (E.x e. RR E.y e. RR 0 = (x + (_i x. y)) -> E.x x e. RR)
7	3, 6	ax-mp 7	. 2 |- E.x x e. RR
8		axrnegex 6232	. . . 4 |- (x e. RR -> E.y e. RR (x + y) = 0)
9		pm3.27 348	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ (x + y) = 0) -> (x + y) = 0)
10		readdcl 6251	. . . . . . . 8 |- ((x e. RR /\ y e. RR) -> (x + y) e. RR)
11	10	adantr 423	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ (x + y) = 0) -> (x + y) e. RR)
12	9, 11	eqeltrrd 1809	. . . . . 6 |- (((x e. RR /\ y e. RR) /\ (x + y) = 0) -> 0 e. RR)
13	12	ex 400	. . . . 5 |- ((x e. RR /\ y e. RR) -> ((x + y) = 0 -> 0 e. RR))
14	13	r19.23adva 2050	. . . 4 |- (x e. RR -> (E.y e. RR (x + y) = 0 -> 0 e. RR))
15	8, 14	mpd 29	. . 3 |- (x e. RR -> 0 e. RR)
16	15	19.23aiv 1512	. 2 |- (E.x x e. RR -> 0 e. RR)
17	7, 16	ax-mp 7	1 |- 0 e. RR

Syntax hints:   /\ wa 239   = wceq 1136   e. wcel 1138  E.wex 1164  E.wrex 1940  (class class class)co 4695  CCcc 6180  RRcr 6181  0cc0 6182  _ici 6184   + caddc 6185   x. cmul 6187

This theorem is referenced by:  axmulgt0 6471  addgt0i 6571  addgt0iOLD 6572  addge0i 6573  addge0iOLD 6574  addgegt0i 6575  addgegt0iOLD 6576  add20i 6578  mulge0i 6583  gt0ne0i 6587  lesub0i 6588  lesub0iOLD 6589  msqgt0i 6590  msqge0i 6591  msqge0iOLD 6592  msqgt0 6593  msqge0 6594  gt0ne0 6596  ne0gt0 6597  ltadd1 6602  leadd1 6604  ltsubadd 6606  lesubadd 6608  ltmullem 6620  lt2add 6623  le2add 6624  addgt0 6627  addgt0OLD 6628  addgegt0 6629  addgegt0OLD 6630  addgtge0 6631  addge0 6633  addge0OLD 6634  ltaddpos 6635  ltneg 6640  leneg 6642  lt0neg1 6653  lt0neg2 6654  le0neg1 6655  le0neg2 6656  addge01 6657  lesub0 6663  mulge0 6664  mulge0OLD 6665  redivcl 6773  elimge0 6783  recgt0ii 6787  ltm1 6788  prodgt0lem 6791  prodgt0i 6792  prodge0i 6793  prodgt0 6799  prodge0 6801  ltmul1 6803  lemul1a 6814  lemul1aOLD 6815  ltmul12a 6818  lemul12aOLD 6820  lemul12a 6821  mulgt1 6822  lemulge11 6825  ltdiv1 6826  ltdiv1OLD 6827  gt0div 6830  ge0div 6831  ltmuldiv 6840  ltmuldivOLD 6841  lt2msqi 6859  ltrec 6862  lerec 6863  lt2msq 6864  lediv12a 6874  recgt1i 6878  recreclt 6880  le2msq 6881  halfposi 6882  ledivp1 6883  ledivp1i 6884  ltdivp1i 6885  squeeze0 6902  nnge1 6921  nngt0 6924  0nnn 6926  nnrecgt0 6932  nnleltp1 6933  halfpos 7017  rpge0 7036  rpneg 7047  0nrp 7048  xrsupsslem 7080  xrinfmsslem 7081  nn0ssre 7107  lt0nnn0 7120  nn0ge0 7121  nn0le0eq0 7123  nn0ltp1le 7131  elnnz 7149  0z 7150  elnn0z 7151  elnnz1 7159  nn0sub 7165  elnn0nn 7175  zltp1le 7185  recnz 7198  gtndiv 7200  uzindOLD 7215  qsqueeze 7256  flhalf 7282  ioopos 7357  icoshftf1olem 7374  icoun 7377  snunioo 7379  elfz2nn0 7462  cardfz 7514  seq1lem2 7518  ser1monoi 7545  expge0 7628  expordi 7640  exple1 7647  expubnd 7648  sq11 7669  le2sq2 7672  sqge0 7673  sumsqne0i 7674  sqlecan 7682  bernneq2 7695  expnbnd 7696  expnlbnd 7697  expnlbnd2 7698  discrlem1 7701  discrlem3 7703  discrlem 7704  nnesqi 7707  sqr0 7717  sqrlem1 7718  sqrlem2 7719  sqrlem5 7722  sqrlem6 7723  sqrlem8 7725  sqrlem11 7728  sqrlem12 7729  sqrlem15 7732  sqrlem19 7736  sqrlem24 7741  sqrgt0ii 7742  sqrlem26 7743  sqrthi 7744  sqrcli 7745  sqrge0i 7747  sqrmuli 7750  sqrcl 7755  sqrgt0 7756  sqrge0 7757  sqrle 7758  sqr00 7759  sqr1 7761  sqr4 7762  sqr9 7763  sqr2gt1lt2 7764  sqrsq 7767  sqsqr 7768  sqr2irrlem1 7769  sqr2irrlem4 7772  sqr2irr 7774  inelr 7780  cru 7783  crne0i 7784  rimul 7789  nthruz 7791  re0 7865  im0 7866  rei 7869  imi 7870  cj0 7871  absgt0i 7889  absrpcl 7901  absid 7908  leabs 7910  absor 7911  absexp 7914  leabsi 7919  abslt 7927  absle 7928  abs1mi 7951  abs3lem 7954  facdiv 7989  facwordi 7991  faclbnd3 7994  faclbnd4lem1 7995  bcval4 8008  bcpasci 8016  bccl2 8018  fsumcmp0 8096  serzcmp0 8110  climrecl 8165  climge0 8167  iserzcmp0 8198  ser1cmp0i 8230  cvgcmpi 8240  cvgcmpubi 8241  cvgcmp3cetlem1 8244  cvgcmp3cetlem2 8245  iserzgt0 8267  reccnv 8274  arisumi 8282  expcnvlem2 8284  expcnvlem6 8288  georeclim 8297  geoisumr 8300  0.999... 8303  cvgratlem4 8310  cvgratlem5 8311  reefcl 8375  erelem2 8377  erelem3 8378  efaddlem12 8406  efaddlem20 8414  efaddlem25 8419  eftabsi 8432  ef01tllem2 8441  ef01tllem2OLD 8442  ef01tlubi 8443  absef01tlubi 8445  abspef01tlubi 8455  efgt1i 8463  efgt0i 8464  efgt0 8465  reef11 8469  absefm1lei 8472  eflegeolem2 8474  eflegeo 8476  reeff1olem1 8484  reeff1o 8486  reefiso 8488  sin0 8504  cos0 8506  sinbnd 8526  cosbnd 8527  sin01bndlem1 8528  sin01bndlem2 8529  sin01bndlem3 8530  cos01bndlem2 8531  cos01bndlem3 8532  cos1bnd 8535  cos2bnd 8536  sin01gt0 8537  cos01gt0 8538  sin02gt0 8539  sincos1sgn 8540  sincos2sgn 8541  sin4lt0 8542  absefib 8545  efieq1re 8546  znnenlem 8565  znnen 8566  ruclem8 8581  ruclem39 8612  metgt0 8892  metxp 8906  dscmet 8991  lmnn 9008  gxnval 9178  readdsubg 9232  nvm1 9419  nvz0 9423  nvmtri 9426  nv1 9431  sm1cnilem 9481  ipid 9497  nmosetn0 9562  nmoge0 9564  nmo0 9586  0blo 9587  nmlno0lem 9588  nmlnoubi 9591  nmlnogt0 9592  nmblolbii 9594  blocnilem 9599  siilem2 9648  ubthlem10 9676  ubthlem12 9678  ubthlem12OLD 9679  ubthlem13 9680  ubthlem13OLD 9681  minveclem10 9694  minveclem14 9698  minveclem16 9700  minveclem21 9705  minveclem25 9709  minveclem35 9719  minveclem38 9722  minveceu 9723  htthlem10 9771  pilem1 9815  pilem2 9816  pilem3 9817  sinhalfpilem 9823  sinperlem1 9830  sincosq1lem 9847  sincosq1sgn 9848  sincosq2sgn 9849  sinq12gt0t 9852  sinq34lt0t 9853  sincos4thpi 9855  sincos6thpi 9856  coskpi 9859  sineq0 9860  sineq0OLD 9861  sineq0re 9862  cosh111lem1 9863  cosh111 9866  efif 9870  efifolem1 9871  efifolem2 9872  efifolem3 9873  efifolem4 9874  efifolem5 9875  efifolem6 9876  efifolem7 9877  efif1lem1 9879  efif1lem2 9880  efif1lem3 9881  efif1lem5 9883  efif1lem6 9884  efif1lem7 9885  circgrp 9889  resslogrn 9902  log1 9915  pilog 9917  hiidge0 10389  his6 10390  normlem6 10406  normlem7tALT 10410  normgt0OLD 10418  normgt0 10419  norm-i 10421  norm-ii.i 10429  normsubi 10433  normpyc 10438  normpar2i 10448  bcsiALT 10471  hlimcauii 10531  norm1 10546  occllem7 10604  projlem1 10611  projlem2 10612  projlem4 10614  projlem5 10615  projlem6 10616  projlem7 10617  projlem8 10618  projlem13 10623  projlem18 10628  projlem28 10638  pjthlem10 10653  pjthlem11 10654  osumlem3 11007  pjneli 11095  nmopsetn0 11221  nmfnsetn0 11234  nmopge0 11264  nmopgt0 11265  nmfnge0 11280  nmop0 11339  nmfn0 11340  0bdop 11347  nmlnop0iALT 11349  unopbd 11369  nmbdoplbi 11378  nmcopexlem3 11382  nmcopexlem5 11384  nmcoplbi 11387  lnopconi 11392  nmbdfnlbi 11407  nmbdfnlb 11408  nmcfnexlem3 11411  nmcfnexlem5 11413  nmcfnlbi 11416  lnfnconi 11419  cnlnadjlem7 11435  nmopcoi 11457  unierri 11466  branmfn 11467  branmfnOLD 11468  leoprf2 11490  leoprf 11491  leopmul 11497  nmopleid 11502  pjbdlni 11512  hmopidmchlem 11514  pjnormssi 11532  hstle1 11590  stle0i 11603  strlem1 11614  strlem3a 11616  strlem5 11619  jplem1 11632  cdj3lem1 11798  elnn00nn 13394  nn0lt10b 13395  fnn0ind 13403  nn0seqcvgd 13451  dvdslelem 13484  divalglem1 13489  divalglem5 13492  divalglem6 13493  divalglem7 13494  gcdn0gt0 13520  algcvgblem 13537  algcvga 13539  mulgcdlem2 13549  mulgcdlem7 13554  zgt1b1 13563  isprm3 13568  nndivlub 13989  cntrsetlem 14709  iintlem1 14720  lvsovso 14734  epos 15047  reconnlem4 15131  reconnlem5 15132  add20 15459  fz10 15470  rddif 15480  absrdbnd 15481  elnnr 15485  fsumltisumii 15504  fsumltisumi 15505  fsumleisumii 15507  fsumleisumi 15508  fsumlt1 15513  csbrni 15514  trirn 15516  geomcau 15531  iiuni 15550  dfii2 15551  dfii3 15552  iirev 15553  iihalf1 15554  iihalf2 15555  iimulcl 15556  lincmb01cmp 15560  lincmb01icc 15561  txmet 15607  totbndbnd 15626  heiborlem18 15654  heiborlem32 15668  heiborlem35 15671  bfplem9 15688  bfp 15691  recms 15692  rrndm 15697  rrntotbnd 15704  iicmp 15710  phtpyid 15731  phtpycom 15732  phtpycolem1 15733  phtpycolem2 15734  phtpycolem3 15735  phtpycolem4 15736  phtpycolem5 15737  phtpyco 15738  reparphtlem2 15746  reparpht 15747  pcoval1 15756  pcoval2 15757  pcocn 15758  pco0 15759  pcohtpylem1 15762  pcohtpylem2 15763  pcohtpylem3 15764  pcohtpy 15765  pcopt 15766  pcoass 15767  pcorevlem 15768  pcorev 15769  pi1gp 15777

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601  ax-inf2 5540

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-reu 1945  df-rab 1946  df-v 2127  df-sbc 2287  df-csb 2374  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-int 3037  df-iun 3079  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-fv 3825  df-opr 4697  df-oprab 4698  df-1st 4831  df-2nd 4832  df-rdg 4951  df-1o 4988  df-oadd 4990  df-omul 4991  df-er 5129  df-ec 5131  df-qs 5134  df-ni 5948  df-pli 5949  df-mi 5950  df-lti 5951  df-plpq 5983  df-mpq 5984  df-enq 5985  df-nq 5986  df-plq 5987  df-mq 5988  df-rq 5989  df-ltq 5990  df-1q 5991  df-np 6034  df-1p 6035  df-plp 6036  df-mp 6037  df-ltp 6038  df-plpr 6112  df-mpr 6113  df-enr 6114  df-nr 6115  df-plr 6116  df-mr 6117  df-0r 6119  df-1r 6120  df-m1r 6121  df-c 6188  df-0 6189  df-1 6190  df-i 6191  df-r 6192  df-plus 6193  df-mul 6194

Copyright terms: Public domain