Theorem 0re 5452

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

Assertion

Ref	Expression
0re	|- 0 e. RR

Proof of Theorem 0re

Step	Hyp	Ref	Expression
1		0cn 5340	. . . 4 |- 0 e. CC
2		axcnre 5298	. . . 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 1653	. . . 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 1042	. . . 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 5295	. . . 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 5284	. . . . . . . 8 |- ((x e. RR /\ y e. RR) -> (x + y) e. RR)
12	11	adantr 391	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ (x + y) = 0) -> (x + y) e. RR)
13	10, 12	eqeltrrd 1552	. . . . . 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 1750	. . . 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 1297	. 2 |- (E.x x e. RR -> 0 e. RR)
18	8, 17	ax-mp 7	1 |- 0 e. RR

Syntax hints:   /\ wa 223   = wceq 958   e. wcel 960  E.wex 982  E.wrex 1649  (class class class)co 3969  CCcc 5244  RRcr 5245  0cc0 5246  ici 5248   + caddc 5249   x. cmul 5251

This theorem is referenced by:  axmulgt0 5518  addgt0 5610  addge0 5611  addgegt0 5612  add20 5614  mulge0 5619  gt0ne0 5623  lesub0 5624  msqgt0 5625  msqge0 5626  msqgt0t 5627  msqge0t 5628  gt0ne0t 5630  ne0gt0t 5631  ltadd1t 5635  leadd1t 5637  ltsubaddt 5639  lesubaddt 5641  ltmullem 5652  lt2addt 5655  le2addt 5656  addgt0t 5659  addgegt0t 5660  addge0t 5662  ltaddpost 5663  ltnegt 5667  lenegt 5669  lt0neg1t 5680  lt0neg2t 5681  le0neg1t 5682  le0neg2t 5683  addge01t 5684  lesub0t 5690  mulge0t 5691  redivclt 5802  elimge0 5812  recgt0i 5816  ltm1t 5817  prodgt0lem 5820  prodgt0 5821  prodge0 5822  prodgt0t 5828  prodge0t 5830  ltmul1t 5832  lemul1it 5839  lemul1itOLD 5840  ltmul12it 5843  lemul12itOLD 5845  lemul12it 5846  mulgt1t 5847  lemulge11t 5850  ltdiv1t 5851  ltdiv1tOLD 5852  gt0divt 5855  ge0divt 5856  ltmuldivt 5865  ltmuldivtOLD 5866  lt2msq 5883  ltrect 5886  lerect 5887  lt2msqt 5888  lediv12it 5898  recgt1it 5902  recrecltt 5904  le2msqt 5905  halfpos 5906  ledivp1t 5907  ledivp1 5908  ltdivp1 5909  squeeze0 5926  nnge1t 5945  nngt0t 5948  0nnn 5950  nnrecgt0t 5955  nnleltp1t 5956  halfpost 6038  xrsupsslem 6078  xrinfmsslem 6079  nn0ssre 6105  lt0nnn0 6118  nn0ge0t 6119  nn0le0eq0t 6121  nn0ltp1let 6129  elnnz 6147  0z 6148  elnn0z 6149  elnnz1 6157  nn0subt 6163  elnn0nn 6173  zltp1let 6183  recnzt 6193  gtndivt 6195  uzindOLD 6210  flhalft 6248  qsqueeze 6281  rpge0t 6288  0nrp 6294  seq1lem2 6311  ser1mono 6338  ioopos 6395  icoshftf1olem 6411  icoun 6414  snunioo 6416  elfz2nn0t 6496  expge0t 6592  expordit 6601  exple1t 6608  expubndt 6609  sq11t 6630  le2sqit 6633  sqge0t 6634  sumsqne0 6635  sqlecant 6642  bernneq2 6654  expnbndt 6655  expnlbndt 6656  discrlem1 6657  discrlem3 6659  discrlem 6660  nnesq 6663  sqr0 6673  sqrlem1 6674  sqrlem2 6675  sqrlem5 6678  sqrlem6 6679  sqrlem8 6681  sqrlem11 6684  sqrlem12 6685  sqrlem15 6688  sqrlem19 6692  sqrlem24 6697  sqrgt0i 6698  sqrlem26 6699  sqrth 6700  sqrcl 6701  sqrge0 6703  sqrmul 6706  sqrclt 6711  sqrgt0t 6712  sqrge0t 6713  sqrlet 6714  sqr00t 6715  sqr1 6717  sqr4 6718  sqr9 6719  sqr2gt1lt2 6720  sqrsqt 6723  sqsqrt 6724  sqr2irrlem1 6725  sqr2irrlem4 6728  sqr2irr 6730  inelr 6736  crut 6739  crne0 6740  rimul 6745  nthruz 6747  re0 6820  im0 6821  rei 6824  imi 6825  cj0 6826  absgt0 6843  absrpclt 6855  absidt 6862  leabst 6864  absort 6865  absexpt 6868  leabs 6872  absltt 6880  abslet 6881  abs1m 6904  abs3lemt 6907  facdivt 6942  facwordit 6944  faclbnd3 6947  faclbnd4lem1 6948  bcval4t 6961  bcpasc 6969  bccl2t 6971  fsumcmp0 7041  serzcmp0 7055  climrecl 7110  climge0 7112  iserzcmp0 7143  ser1cmp0 7175  cvgcmp 7184  cvgcmpub 7185  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  iserzgt0 7211  reccnv 7218  fnsmnt 7226  expcnvlem2 7228  expcnvlem6 7232  georeclim 7240  geoisumr 7243  0.999... 7246  cvgratlem4 7253  cvgratlem5 7254  reefclt 7318  erelem2 7320  erelem3 7321  efaddlem12 7349  efaddlem20 7357  efaddlem25 7362  eftabs 7375  ef01tllem2 7384  ef01tllem2OLD 7385  ef01tlub 7386  absef01tlub 7388  abspef01tlub 7395  efgt1 7403  efgt0 7404  efgt0t 7405  reef11t 7409  absefm1le 7412  eflegeolem2 7414  eflegeot 7416  reeff1olem1 7424  reeff1o 7426  reefiso 7428  sin0 7444  cos0 7446  sinbndt 7466  cosbndt 7467  sin01bndlem1 7468  sin01bndlem2 7469  sin01bndlem3 7470  cos01bndlem2 7471  cos01bndlem3 7472  cos1bnd 7475  cos2bnd 7476  sin01gt0 7477  cos01gt0 7478  sin02gt0 7479  sincos1sgn 7480  sincos2sgn 7481  sin4lt0 7482  znnenlem 7502  znnen 7503  ruclem8 7518  ruclem39 7549  metgt0 7817  metxp 7831  dscmet 7915  lmnn 7932  readdsubg 8125  nvm1 8288  nvz0 8292  nvmtri 8295  nv1 8300  sm1cnilem 8343  ipid 8359  nmosetn0 8424  nmoge0 8426  nmo0 8447  0blo 8448  nmlno0lem 8449  nmlnoubi 8452  nmlnogt0 8453  nmblolbii 8455  blocnilem 8460  siilem2 8508  ubthlem10 8534  ubthlem12 8536  ubthlem13 8537  minveclem10 8550  minveclem14 8554  minveclem16 8556  minveclem21 8561  minveclem25 8565  minveclem35 8575  minveclem38 8578  minveceu 8579  htthlem10 8625  pilem1 8666  pilem2 8667  pilem3 8668  sinhalfpilem 8674  sinperlem1 8681  sincosq1lem 8698  sincosq1sgn 8699  sincosq2sgn 8700  sinq12gt0t 8703  sincos4thpi 8705  sincos6thpi 8706  sineq0 8708  cosh111lem1 8709  cosh111t 8712  efif 8716  efifolem1 8717  efifolem2 8718  efifolem3 8719  efifolem4 8720  efifolem5 8721  efifolem6 8722  efifolem7 8723  efif1lem1 8725  efif1lem2 8726  efif1lem3 8727  efif1lem5 8729  efif1lem6 8730  efif1lem7 8731  circgrp 8735  resslogrn 8748  log1 8761  pilog 8763  hiidge0t 8959  his6t 8960  normlem6 8976  normlem7tALT 8980  normgt0tOLD 8988  normgt0t 8989  norm-it 8991  norm-ii 8999  normsub 9003  normpyct 9008  normpar2 9018  bcsALT 9041  hlimcaui 9101  norm1t 9116  occllem7 9174  projlem1 9181  projlem2 9182  projlem4 9184  projlem5 9185  projlem6 9186  projlem7 9187  projlem8 9188  projlem13 9193  projlem18 9198  projlem28 9208  pjthlem10 9223  pjthlem11 9224  osumlem3 9575  pjnel 9663  nmopsetn0 9787  nmfnsetn0 9800  nmopge0t 9830  nmopgt0t 9831  nmfnge0t 9846  nmop0 9905  nmfn0 9906  0bdop 9913  nmlnop0ALT 9915  unopbdt 9935  nmbdoplb 9944  nmcopexlem3 9948  nmcopexlem5 9950  nmcoplb 9953  lnopcon 9958  nmbdfnlb 9973  nmbdfnlbt 9974  nmcfnexlem3 9977  nmcfnexlem5 9979  nmcfnlb 9982  lnfncon 9985  cnlnadjlem7 10001  nmopco 10023  unierr 10032  branmfnt 10033  leoprf2t 10055  leoprft 10056  leopmult 10062  nmopleidt 10067  pjbdln 10071  hmopidmchlem 10073  pjnormss 10091  hstle1t 10148  stle0 10161  strlem1 10172  strlem3a 10174  strlem5 10177  jplem1 10190  cdj3lem1 10356  nndivlub 10417  iintlem1 10603

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-int 2538  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-fv 3204  df-rdg 3938  df-opr 3971  df-oprab 3972  df-1st 4085  df-2nd 4086  df-1o 4139  df-oadd 4141  df-omul 4142  df-er 4267  df-ec 4269  df-qs 4272  df-ni 5012  df-pli 5013  df-mi 5014  df-lti 5015  df-plpq 5047  df-mpq 5048  df-enq 5049  df-nq 5050  df-plq 5051  df-mq 5052  df-rq 5053  df-ltq 5054  df-1q 5055  df-np 5098  df-1p 5099  df-plp 5100  df-mp 5101  df-ltp 5102  df-plpr 5176  df-mpr 5177  df-enr 5178  df-nr 5179  df-plr 5180  df-mr 5181  df-0r 5183  df-1r 5184  df-m1r 5185  df-c 5252  df-0 5253  df-1 5254  df-i 5255  df-r 5256  df-plus 5257  df-mul 5258

Copyright terms: Public domain