Theorem 0re 10908

Description: The number 0 is real. Remark: the first step could also be ax-icn 10861. See also 0reALT 11248. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 11-Oct-2022.)

Assertion

Ref	Expression
0re	⊢ 0 ∈ ℝ

Proof of Theorem 0re

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1cn 10860	. 2 ⊢ 1 ∈ ℂ
2		cnre 10903	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 10873	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 10885	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2826	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 244	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3212	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3209	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∃wrex 3064  (class class class)co 7255  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803  ici 10804   + caddc 10805   · cmul 10807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addrcl 10863  ax-rnegex 10873  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069

This theorem is referenced by:  0red  10909  0xr  10953  axmulgt0  10980  ne0gt0  11010  00id  11080  mul02lem1  11081  mul02lem2  11082  mul02  11083  addid1  11085  ltaddneg  11120  addgt0  11391  addgegt0  11392  addgtge0  11393  addge0  11394  ltaddpos  11395  ltneg  11405  leneg  11408  lt0neg1  11411  lt0neg2  11412  le0neg1  11413  le0neg2  11414  addge01  11415  suble0  11419  mulge0  11423  msqge0  11426  0le1  11428  relin01  11429  gt0ne0i  11440  gt0ne0d  11469  lt0ne0d  11470  elimge0  11744  ltm1  11747  recgt0  11751  prodgt0  11752  lemul1a  11759  ltmul12a  11761  lemul12a  11763  mulgt1  11764  gt0div  11771  ge0div  11772  mulge0b  11775  lediv12a  11798  recgt1i  11802  recreclt  11804  ledivp1  11807  squeeze0  11808  recgt0ii  11811  ledivp1i  11830  ltdivp1i  11831  fimaxre2  11850  inelr  11893  crne0  11896  nnge1  11931  nngt0  11934  nnnle0  11936  nnne0  11937  nnrecgt0  11946  0le0  12004  neg1lt0  12020  halfge0  12120  nn0ssre  12167  nn0ge0  12188  nn0nlt0  12189  nn0le0eq0  12191  0mnnnnn0  12195  elnnnn0b  12207  elnnnn0c  12208  nn0sub  12213  elnnz  12259  0z  12260  elnn0z  12262  elnnz1  12276  recnz  12325  gtndiv  12327  fnn0ind  12349  10re  12385  rpge0  12672  rpneg  12691  0nrp  12694  0ltpnf  12787  mnflt0  12790  qsqueeze  12864  xneg0  12875  xaddid1  12904  xnn0xadd0  12910  xmulpnf1  12937  xlemul1a  12951  xadddi  12958  xrsupsslem  12970  xrinfmsslem  12971  elrege0  13115  0e0icopnf  13119  elicc01  13127  0elunit  13130  unitssre  13160  0nelfz1  13204  fzpreddisj  13234  fz0to4untppr  13288  nn0p1elfzo  13358  ico01fl0  13467  rpsup  13514  modelico  13529  0mod  13550  1mod  13551  le2sq2  13782  expubnd  13823  sqlecan  13853  bernneq2  13873  expnbnd  13875  expnlbnd  13876  expmulnbnd  13878  discr1  13882  discr  13883  faclbnd  13932  faclbnd3  13934  faclbnd6  13941  bcval4  13949  bcval5  13960  bcpasc  13963  hasheq0  14006  hashneq0  14007  hashnn0n0nn  14034  hashgt12el  14065  hashgt12el2  14066  hashge2el2dif  14122  lsw0  14196  swrdccatin2  14370  pfxccatin12lem3  14373  reim0  14757  re0  14791  im0  14792  rei  14795  imi  14796  cj0  14797  sqeqd  14805  rennim  14878  cnpart  14879  sqr0lem  14880  sqrlem4  14885  resqrex  14890  sqrtgt0  14898  sqrt00  14903  sqrtneglem  14906  sqrt9  14913  sqrt2gt1lt2  14914  leabs  14939  absor  14940  max0add  14950  eqsqrt2d  15008  sqrtpclii  15022  rlimconst  15181  rlimrege0  15216  lo1mul  15265  iserge0  15300  fsum00  15438  isumless  15485  arisum2  15501  georeclim  15512  geo2sum  15513  geoisumr  15518  0.999...  15521  cvgrat  15523  fprodge0  15631  bpoly4  15697  cos0  15787  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  cos2bnd  15825  sin01gt0  15827  cos01gt0  15828  sincos2sgn  15831  sin4lt0  15832  absef  15834  absefib  15835  efieq1re  15836  epos  15844  rpnnen2lem2  15852  rpnnen2lem3  15853  rpnnen2lem4  15854  rpnnen2lem9  15859  ruclem6  15872  dvdslelem  15946  divalglem1  16031  divalglem5  16034  divalglem6  16035  flodddiv4  16050  sadcadd  16093  gcdn0gt0  16153  nn0seqcvgd  16203  algcvgblem  16210  algcvga  16212  pythagtriplem12  16455  pythagtriplem13  16456  pythagtriplem14  16457  pythagtriplem16  16459  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  1arith  16556  ramz  16654  mulgnegnn  18629  subgmulg  18684  srgbinomlem4  19694  isabvd  19995  abvtrivd  20015  xrs1mnd  20548  xrs10  20549  rge0srg  20581  psgnodpmr  20707  re0g  20729  psrbaglesupp  21037  psrbaglesuppOLD  21038  mnfnei  22280  imasdsf1olem  23434  ssblps  23483  ssbl  23484  xmeter  23494  dscmet  23634  dscopn  23635  nmoi  23798  nmoeq0  23806  0nghm  23811  idnghm  23813  cnbl0  23843  xrsxmet  23878  metdseq0  23923  iicmp  23955  iiconn  23956  iihalf1  24000  iihalf1cn  24001  elii1  24004  icopnfcnv  24011  icopnfhmeo  24012  iccpnfcnv  24013  xrhmeo  24015  xrhmph  24016  htpycc  24049  reparphti  24066  pcoval1  24082  pco0  24083  pcoval2  24085  pcocn  24086  pcohtpylem  24088  pcopt  24091  pcopt2  24092  pcoass  24093  pcorevlem  24095  reust  24450  recusp  24451  rrx0el  24467  minveclem4c  24494  minveclem2  24495  minveclem3b  24497  minveclem4  24501  minveclem7  24504  pjthlem1  24506  cniccbdd  24530  ovolunnul  24569  ovoliunnul  24576  ovolicc1  24585  ovolre  24594  iccvolcl  24636  ovolioo  24637  ioovolcl  24639  ioorcl  24646  vitalilem4  24680  vitalilem5  24681  vitali  24682  ismbf  24697  mbfmulc2lem  24716  mbfpos  24720  mbfposr  24721  i1f0  24756  i1f1  24759  itg1addlem2  24766  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1flimlem  24792  xrge0f  24801  itg2ge0  24805  itg2const  24810  itg2mulc  24817  itg2splitlem  24818  itg2gt0  24830  itg2cnlem1  24831  ibl0  24856  iblrelem  24860  iblposlem  24861  iblpos  24862  iblre  24863  itgreval  24866  itgneg  24873  iblss  24874  i1fibl  24877  itgitg1  24878  itgle  24879  itgeqa  24883  itgless  24886  iblconst  24887  itgconst  24888  ibladdlem  24889  itgaddlem2  24893  iblabslem  24897  iblabsr  24899  iblmulc2  24900  itgmulc2lem2  24902  itgabs  24904  itgsplit  24905  bddmulibl  24908  dvferm1  25054  dvferm2  25056  dvferm  25057  dvlip  25062  c1lip1  25066  dveq0  25069  dv11cn  25070  dvne0  25080  ftc1lem4  25108  ply1divex  25206  dgrco  25341  plyrecj  25345  vieta1lem2  25376  aalioulem2  25398  aalioulem3  25399  pserulm  25486  psercnlem2  25488  psercnlem1  25489  psercn  25490  abelth  25505  reeff1olem  25510  reeff1o  25511  pilem2  25516  pilem3  25517  pipos  25522  sinhalfpilem  25525  sincosq1sgn  25560  sincosq2sgn  25561  coseq00topi  25564  coseq0negpitopi  25565  tangtx  25567  tanabsge  25568  sinq12ge0  25570  sinq34lt0t  25571  cosq14ge0  25573  sincos4thpi  25575  sincos6thpi  25577  pige3ALT  25581  sineq0  25585  cosordlem  25591  cosord  25592  cos0pilt1  25593  cos11  25594  sinord  25595  recosf1o  25596  resinf1o  25597  tanord1  25598  tanord  25599  tanregt0  25600  efif1olem4  25606  efifo  25608  relogrn  25622  log1  25646  logneg  25648  argregt0  25670  argrege0  25671  argimgt0  25672  logneg2  25675  logdivlti  25680  logdivlt  25681  ellogdm  25699  logdmn0  25700  logdmnrp  25701  logcnlem3  25704  dvloglem  25708  logdmopn  25709  logf1o2  25710  dvlog2lem  25712  efopnlem1  25716  logtayl  25720  recxpcl  25735  cxpge0  25743  cxple2  25757  cxple2a  25759  cxpsqrtlem  25762  cxpcn3  25806  cxpaddlelem  25809  cxpaddle  25810  loglesqrt  25816  logbrec  25837  ang180lem3  25866  ang180lem4  25867  asinneg  25941  asin1  25949  reasinsin  25951  acosbnd  25955  atan0  25963  atanrecl  25966  atanlogaddlem  25968  atanlogsublem  25970  atanlogsub  25971  atantan  25978  atanbnd  25981  atan1  25983  atans2  25986  ressatans  25989  log2cnv  25999  log2tlbnd  26000  log2ub  26004  log2le1  26005  rlimcnp  26020  rlimcnp2  26021  o1cxp  26029  jensen  26043  amgm  26045  emgt0  26061  harmonicbnd3  26062  harmoniclbnd  26063  harmonicbnd4  26065  zetacvg  26069  eldmgm  26076  lgamgulmlem2  26084  basellem3  26137  basellem8  26142  efnnfsumcl  26157  ppisval  26158  vmage0  26175  chpge0  26180  efchtdvds  26213  ppiltx  26231  ppiub  26257  chpeq0  26261  chteq0  26262  chtleppi  26263  chpchtsum  26272  chpub  26273  dchr1re  26316  bcmono  26330  efexple  26334  bposlem1  26337  bposlem4  26340  bposlem5  26341  bposlem7  26343  bposlem8  26344  bposlem9  26345  lgsval2lem  26360  lgsval4a  26372  lgsneg  26374  lgsdilem  26377  lgsdir2lem1  26378  2lgsoddprmlem3a  26463  2lgsoddprmlem3b  26464  2lgsoddprmlem3c  26465  2lgsoddprmlem3d  26466  rplogsumlem2  26538  rpvmasumlem  26540  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0fno1  26564  rplogsum  26580  logdivsum  26586  mulog2sumlem2  26588  selberg2lem  26603  logdivbnd  26609  pntrsumo1  26618  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntpbnd1  26639  pntpbnd2  26640  pntlem3  26662  pntleml  26664  ostth2  26690  trgcgrg  26780  ttgcontlem1  27155  axlowdimlem1  27213  axlowdimlem6  27218  axlowdimlem7  27219  axlowdimlem10  27222  axlowdim1  27230  axlowdim2  27231  axlowdim  27232  elntg2  27256  umgrislfupgrlem  27395  lfgrnloop  27398  lfuhgr1v0e  27524  usgrexmplef  27529  pthdlem2  28037  crctcshwlkn0lem7  28082  rusgrnumwwlks  28240  clwwlkn0  28293  konigsberg  28522  ex-po  28700  ex-sqrt  28719  ex-gcd  28722  nvz0  28931  0blo  29055  nmlno0lem  29056  nmblolbii  29062  siilem2  29115  minvecolem2  29138  minvecolem3  29139  minvecolem4c  29142  minvecolem4  29143  minvecolem5  29144  minvecolem7  29146  htthlem  29180  hiidge0  29361  normlem6  29378  normgt0  29390  norm-i  29392  normpyc  29409  bcsiALT  29442  pjhthlem1  29654  pjneli  29986  nmlnop0iALT  30258  unopbd  30278  nmbdoplbi  30287  nmcoplbi  30291  nmbdfnlbi  30312  nmbdfnlb  30313  nmcfnlbi  30315  cnlnadjlem7  30336  nmopcoi  30358  branmfn  30368  leopmul  30397  nmopleid  30402  pjbdlni  30412  pjnormssi  30431  stle0i  30502  cdj3lem1  30697  xaddeq0  30978  pr01ssre  31040  dp20u  31054  dp20h  31055  dp2clq  31057  dp2lt10  31060  dp2lt  31061  dp0u  31077  dplti  31081  dpexpp1  31084  xdiv0  31105  xrge0slmod  31450  unitdivcld  31753  sqsscirc1  31760  xrge0iifcnv  31785  xrge0iifiso  31787  rezh  31821  indf  31883  indfval  31884  esumcvgsum  31956  voliune  32097  volfiniune  32098  sibfinima  32206  sitmcl  32218  0rrv  32318  coinfliprv  32349  ballotlem2  32355  ballotlem4  32365  ballotlemi1  32369  ballotlemic  32373  sgnclre  32406  sgnnbi  32412  sgnpbi  32413  plymulx0  32426  signsply0  32430  signswch  32440  signstf  32445  signstf0  32447  signstfveq0  32456  signlem0  32466  signshf  32467  itgexpif  32486  hgt750lemd  32528  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  iisconn  33114  iillysconn  33115  cvmliftlem10  33156  fz0n  33602  logi  33606  bcneg1  33608  nn0prpwlem  34438  dnizeq0  34582  dnizphlfeqhlf  34583  knoppndvlem13  34631  cnndvlem1  34644  bj-pinftyccb  35319  bj-minftyccb  35323  bj-pinftynminfty  35325  taupilemrplb  35418  irrdiff  35424  sin2h  35694  tan2h  35696  ptrecube  35704  poimirlem16  35720  poimirlem17  35721  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem29  35733  poimirlem31  35735  poimir  35737  heicant  35739  mblfinlem2  35742  ismblfin  35745  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  mbfposadd  35751  itg2addnclem  35755  itg2addnclem2  35756  ibladdnclem  35760  itgaddnclem2  35763  iblabsnclem  35767  iblmulc2nc  35769  itgmulc2nclem2  35771  itgabsnc  35773  ftc1cnnclem  35775  ftc1anclem5  35781  ftc1anclem8  35784  asindmre  35787  dvasin  35788  areacirclem4  35795  areacirc  35797  isbnd3  35869  ssbnd  35873  prdsbnd  35878  bfplem2  35908  bfp  35909  renegclALT  36904  2xp3dxp2ge1d  40090  factwoffsmonot  40091  0cnALT3  40211  sn-1ne2  40216  oexpreposd  40242  sn-00idlem2  40303  sn-00idlem3  40304  sn-00id  40305  rei4  40326  sn-0tie0  40342  sn-ltaddpos  40344  relt0neg1  40346  sn-0lt1  40353  sn-inelr  40356  itrere  40357  retire  40358  pellexlem6  40572  elpell14qr2  40600  oddcomabszz  40682  zindbi  40684  jm2.24  40701  acongeq  40721  arearect  40962  areaquad  40963  reabsifneg  41129  reabsifnpos  41130  reabsifpos  41131  reabsifnneg  41132  imsqrtvalex  41143  relexp01min  41210  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2lem1  41669  imo72b2  41672  dvconstbi  41841  binomcxplemnn0  41856  binomcxplemdvbinom  41860  binomcxplemcvg  41861  binomcxplemnotnn0  41863  sineq0ALT  42446  halffl  42725  ren0  42832  sqrlearg  42981  limsup10ex  43204  dvnmptdivc  43369  dvnmul  43374  itgsin0pilem1  43381  itgsinexplem1  43385  itgsinexp  43386  iblempty  43396  stoweidlem17  43448  stoweidlem36  43467  stoweidlem55  43486  wallispilem1  43496  wallispilem2  43497  wallispilem4  43499  stirlinglem4  43508  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  stirlingr  43521  dirker2re  43523  dirkerdenne0  43524  dirkerre  43526  dirkertrigeqlem1  43529  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem11  43549  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem41  43579  fourierdlem42  43580  fourierdlem48  43585  fourierdlem62  43599  fourierdlem66  43603  fourierdlem79  43616  fourierdlem83  43620  fourierdlem94  43631  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fourierdlem114  43651  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  etransclem23  43688  etransclem44  43709  etransclem46  43711  salexct3  43771  salgensscntex  43773  sge0rnn0  43796  sge00  43804  0ome  43957  ovn0lem  43993  ovnhoilem1  44029  smfmullem1  44212  smfmullem2  44213  smfmullem3  44214  smfmullem4  44215  zm1nn  44682  sqrtnegnre  44687  m1mod0mod1  44709  fmtnoprmfac2lem1  44906  31prm  44937  mod42tp1mod8  44942  nfermltl2rev  45083  tgblthelfgott  45155  altgsumbcALT  45577  expnegico01  45747  dignnld  45837  eenglngeehlnmlem1  45971  line2ylem  45985  line2y  45989  itsclc0yqsollem2  45997  icccldii  46100  i0oii  46101  sepfsepc  46109  ex-gt  46316