Theorem 0re 10632

Description: The number 0 is real. Remark: the first step could also be ax-icn 10585. See also 0reALT 10972. (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 10584	. 2 ⊢ 1 ∈ ℂ
2		cnre 10627	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 10597	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 10609	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2877	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 248	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3243	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 484	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3240	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃wrex 3107  (class class class)co 7135  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527  ici 10528   + caddc 10529   · cmul 10531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-addrcl 10587  ax-rnegex 10597  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112

This theorem is referenced by:  0red  10633  0xr  10677  axmulgt0  10704  ne0gt0  10734  00id  10804  mul02lem1  10805  mul02lem2  10806  mul02  10807  addid1  10809  ltaddneg  10844  addgt0  11115  addgegt0  11116  addgtge0  11117  addge0  11118  ltaddpos  11119  ltneg  11129  leneg  11132  lt0neg1  11135  lt0neg2  11136  le0neg1  11137  le0neg2  11138  addge01  11139  suble0  11143  mulge0  11147  msqge0  11150  0le1  11152  relin01  11153  gt0ne0i  11164  gt0ne0d  11193  lt0ne0d  11194  elimge0  11468  ltm1  11471  recgt0  11475  prodgt0  11476  lemul1a  11483  ltmul12a  11485  lemul12a  11487  mulgt1  11488  gt0div  11495  ge0div  11496  mulge0b  11499  lediv12a  11522  recgt1i  11526  recreclt  11528  ledivp1  11531  squeeze0  11532  recgt0ii  11535  ledivp1i  11554  ltdivp1i  11555  fimaxre2  11574  inelr  11615  crne0  11618  nnge1  11653  nngt0  11656  nnnle0  11658  nnne0  11659  nnrecgt0  11668  0le0  11726  neg1lt0  11742  halfge0  11842  nn0ssre  11889  nn0ge0  11910  nn0nlt0  11911  nn0le0eq0  11913  0mnnnnn0  11917  elnnnn0b  11929  elnnnn0c  11930  nn0sub  11935  elnnz  11979  0z  11980  elnn0z  11982  elnnz1  11996  recnz  12045  gtndiv  12047  fnn0ind  12069  10re  12105  rpge0  12390  rpneg  12409  0nrp  12412  0ltpnf  12505  mnflt0  12508  qsqueeze  12582  xneg0  12593  xaddid1  12622  xnn0xadd0  12628  xmulpnf1  12655  xlemul1a  12669  xadddi  12676  xrsupsslem  12688  xrinfmsslem  12689  elrege0  12832  0e0icopnf  12836  elicc01  12844  0elunit  12847  unitssre  12877  0nelfz1  12921  fzpreddisj  12951  fz0to4untppr  13005  nn0p1elfzo  13075  ico01fl0  13184  rpsup  13229  modelico  13244  0mod  13265  1mod  13266  le2sq2  13496  expubnd  13537  sqlecan  13567  bernneq2  13587  expnbnd  13589  expnlbnd  13590  expmulnbnd  13592  discr1  13596  discr  13597  faclbnd  13646  faclbnd3  13648  faclbnd6  13655  bcval4  13663  bcval5  13674  bcpasc  13677  hasheq0  13720  hashneq0  13721  hashnn0n0nn  13748  hashgt12el  13779  hashgt12el2  13780  hashge2el2dif  13834  lsw0  13908  swrdccatin2  14082  pfxccatin12lem3  14085  reim0  14469  re0  14503  im0  14504  rei  14507  imi  14508  cj0  14509  sqeqd  14517  rennim  14590  cnpart  14591  sqr0lem  14592  sqrlem4  14597  resqrex  14602  sqrtgt0  14610  sqrt00  14615  sqrtneglem  14618  sqrt9  14625  sqrt2gt1lt2  14626  leabs  14651  absor  14652  max0add  14662  eqsqrt2d  14720  sqrtpclii  14734  rlimconst  14893  rlimrege0  14928  lo1mul  14976  iserge0  15009  fsum00  15145  isumless  15192  arisum2  15208  georeclim  15220  geo2sum  15221  geoisumr  15226  0.999...  15229  cvgrat  15231  fprodge0  15339  bpoly4  15405  cos0  15495  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  cos2bnd  15533  sin01gt0  15535  cos01gt0  15536  sincos2sgn  15539  sin4lt0  15540  absef  15542  absefib  15543  efieq1re  15544  epos  15552  rpnnen2lem2  15560  rpnnen2lem3  15561  rpnnen2lem4  15562  rpnnen2lem9  15567  ruclem6  15580  dvdslelem  15651  divalglem1  15735  divalglem5  15738  divalglem6  15739  flodddiv4  15754  sadcadd  15797  gcdn0gt0  15856  nn0seqcvgd  15904  algcvgblem  15911  algcvga  15913  pythagtriplem12  16153  pythagtriplem13  16154  pythagtriplem14  16155  pythagtriplem16  16157  prmreclem4  16245  prmreclem5  16246  prmreclem6  16247  1arith  16253  ramz  16351  mulgnegnn  18230  subgmulg  18285  srgbinomlem4  19286  isabvd  19584  abvtrivd  19604  xrs1mnd  20129  xrs10  20130  rge0srg  20162  psgnodpmr  20279  re0g  20301  psrbaglesupp  20606  mnfnei  21826  imasdsf1olem  22980  ssblps  23029  ssbl  23030  xmeter  23040  dscmet  23179  dscopn  23180  nmoi  23334  nmoeq0  23342  0nghm  23347  idnghm  23349  cnbl0  23379  xrsxmet  23414  metdseq0  23459  iicmp  23491  iiconn  23492  iihalf1  23536  iihalf1cn  23537  elii1  23540  icopnfcnv  23547  icopnfhmeo  23548  iccpnfcnv  23549  xrhmeo  23551  xrhmph  23552  htpycc  23585  reparphti  23602  pcoval1  23618  pco0  23619  pcoval2  23621  pcocn  23622  pcohtpylem  23624  pcopt  23627  pcopt2  23628  pcoass  23629  pcorevlem  23631  reust  23985  recusp  23986  rrx0el  24002  minveclem4c  24029  minveclem2  24030  minveclem3b  24032  minveclem4  24036  minveclem7  24039  pjthlem1  24041  cniccbdd  24065  ovolunnul  24104  ovoliunnul  24111  ovolicc1  24120  ovolre  24129  iccvolcl  24171  ovolioo  24172  ioovolcl  24174  ioorcl  24181  vitalilem4  24215  vitalilem5  24216  vitali  24217  ismbf  24232  mbfmulc2lem  24251  mbfpos  24255  mbfposr  24256  i1f0  24291  i1f1  24294  itg1addlem2  24301  itg1addlem4  24303  itg1addlem5  24304  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  mbfi1flimlem  24326  xrge0f  24335  itg2ge0  24339  itg2const  24344  itg2mulc  24351  itg2splitlem  24352  itg2gt0  24364  itg2cnlem1  24365  ibl0  24390  iblrelem  24394  iblposlem  24395  iblpos  24396  iblre  24397  itgreval  24400  itgneg  24407  iblss  24408  i1fibl  24411  itgitg1  24412  itgle  24413  itgeqa  24417  itgless  24420  iblconst  24421  itgconst  24422  ibladdlem  24423  itgaddlem2  24427  iblabslem  24431  iblabsr  24433  iblmulc2  24434  itgmulc2lem2  24436  itgabs  24438  itgsplit  24439  bddmulibl  24442  dvferm1  24588  dvferm2  24590  dvferm  24591  dvlip  24596  c1lip1  24600  dveq0  24603  dv11cn  24604  dvne0  24614  ftc1lem4  24642  ply1divex  24737  dgrco  24872  plyrecj  24876  vieta1lem2  24907  aalioulem2  24929  aalioulem3  24930  pserulm  25017  psercnlem2  25019  psercnlem1  25020  psercn  25021  abelth  25036  reeff1olem  25041  reeff1o  25042  pilem2  25047  pilem3  25048  pipos  25053  sinhalfpilem  25056  sincosq1sgn  25091  sincosq2sgn  25092  coseq00topi  25095  coseq0negpitopi  25096  tangtx  25098  tanabsge  25099  sinq12ge0  25101  sinq34lt0t  25102  cosq14ge0  25104  sincos4thpi  25106  sincos6thpi  25108  pige3ALT  25112  sineq0  25116  cosordlem  25122  cosord  25123  cos0pilt1  25124  cos11  25125  sinord  25126  recosf1o  25127  resinf1o  25128  tanord1  25129  tanord  25130  tanregt0  25131  efif1olem4  25137  efifo  25139  relogrn  25153  log1  25177  logneg  25179  argregt0  25201  argrege0  25202  argimgt0  25203  logneg2  25206  logdivlti  25211  logdivlt  25212  ellogdm  25230  logdmn0  25231  logdmnrp  25232  logcnlem3  25235  dvloglem  25239  logdmopn  25240  logf1o2  25241  dvlog2lem  25243  efopnlem1  25247  logtayl  25251  recxpcl  25266  cxpge0  25274  cxple2  25288  cxple2a  25290  cxpsqrtlem  25293  cxpcn3  25337  cxpaddlelem  25340  cxpaddle  25341  loglesqrt  25347  logbrec  25368  ang180lem3  25397  ang180lem4  25398  asinneg  25472  asin1  25480  reasinsin  25482  acosbnd  25486  atan0  25494  atanrecl  25497  atanlogaddlem  25499  atanlogsublem  25501  atanlogsub  25502  atantan  25509  atanbnd  25512  atan1  25514  atans2  25517  ressatans  25520  log2cnv  25530  log2tlbnd  25531  log2ub  25535  log2le1  25536  rlimcnp  25551  rlimcnp2  25552  o1cxp  25560  jensen  25574  amgm  25576  emgt0  25592  harmonicbnd3  25593  harmoniclbnd  25594  harmonicbnd4  25596  zetacvg  25600  eldmgm  25607  lgamgulmlem2  25615  basellem3  25668  basellem8  25673  efnnfsumcl  25688  ppisval  25689  vmage0  25706  chpge0  25711  efchtdvds  25744  ppiltx  25762  ppiub  25788  chpeq0  25792  chteq0  25793  chtleppi  25794  chpchtsum  25803  chpub  25804  dchr1re  25847  bcmono  25861  efexple  25865  bposlem1  25868  bposlem4  25871  bposlem5  25872  bposlem7  25874  bposlem8  25875  bposlem9  25876  lgsval2lem  25891  lgsval4a  25903  lgsneg  25905  lgsdilem  25908  lgsdir2lem1  25909  2lgsoddprmlem3a  25994  2lgsoddprmlem3b  25995  2lgsoddprmlem3c  25996  2lgsoddprmlem3d  25997  rplogsumlem2  26069  rpvmasumlem  26071  dchrisum0flblem1  26092  dchrisum0flblem2  26093  dchrisum0fno1  26095  rplogsum  26111  logdivsum  26117  mulog2sumlem2  26119  selberg2lem  26134  logdivbnd  26140  pntrsumo1  26149  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntpbnd1  26170  pntpbnd2  26171  pntlem3  26193  pntleml  26195  ostth2  26221  trgcgrg  26309  ttgcontlem1  26679  axlowdimlem1  26736  axlowdimlem6  26741  axlowdimlem7  26742  axlowdimlem10  26745  axlowdim1  26753  axlowdim2  26754  axlowdim  26755  elntg2  26779  umgrislfupgrlem  26915  lfgrnloop  26918  lfuhgr1v0e  27044  usgrexmplef  27049  pthdlem2  27557  crctcshwlkn0lem7  27602  rusgrnumwwlks  27760  clwwlkn0  27813  konigsberg  28042  ex-po  28220  ex-sqrt  28239  ex-gcd  28242  nvz0  28451  0blo  28575  nmlno0lem  28576  nmblolbii  28582  siilem2  28635  minvecolem2  28658  minvecolem3  28659  minvecolem4c  28662  minvecolem4  28663  minvecolem5  28664  minvecolem7  28666  htthlem  28700  hiidge0  28881  normlem6  28898  normgt0  28910  norm-i  28912  normpyc  28929  bcsiALT  28962  pjhthlem1  29174  pjneli  29506  nmlnop0iALT  29778  unopbd  29798  nmbdoplbi  29807  nmcoplbi  29811  nmbdfnlbi  29832  nmbdfnlb  29833  nmcfnlbi  29835  cnlnadjlem7  29856  nmopcoi  29878  branmfn  29888  leopmul  29917  nmopleid  29922  pjbdlni  29932  pjnormssi  29951  stle0i  30022  cdj3lem1  30217  xaddeq0  30503  pr01ssre  30566  dp20u  30580  dp20h  30581  dp2clq  30583  dp2lt10  30586  dp2lt  30587  dp0u  30603  dplti  30607  dpexpp1  30610  xdiv0  30631  xrge0slmod  30968  unitdivcld  31254  sqsscirc1  31261  xrge0iifcnv  31286  xrge0iifiso  31288  rezh  31322  indf  31384  indfval  31385  esumcvgsum  31457  voliune  31598  volfiniune  31599  sibfinima  31707  sitmcl  31719  0rrv  31819  coinfliprv  31850  ballotlem2  31856  ballotlem4  31866  ballotlemi1  31870  ballotlemic  31874  sgnclre  31907  sgnnbi  31913  sgnpbi  31914  plymulx0  31927  signsply0  31931  signswch  31941  signstf  31946  signstf0  31948  signstfveq0  31957  signlem0  31967  signshf  31968  itgexpif  31987  hgt750lemd  32029  hgt750lem  32032  hgt750lem2  32033  hgt750leme  32039  iisconn  32612  iillysconn  32613  cvmliftlem10  32654  fz0n  33075  logi  33079  bcneg1  33081  nn0prpwlem  33783  dnizeq0  33927  dnizphlfeqhlf  33928  knoppndvlem13  33976  cnndvlem1  33989  bj-pinftyccb  34636  bj-minftyccb  34640  bj-pinftynminfty  34642  bj-isrvec  34708  taupilemrplb  34734  irrdiff  34740  sin2h  35047  tan2h  35049  ptrecube  35057  poimirlem16  35073  poimirlem17  35074  poimirlem20  35077  poimirlem22  35079  poimirlem23  35080  poimirlem29  35086  poimirlem31  35088  poimir  35090  heicant  35092  mblfinlem2  35095  ismblfin  35098  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  mbfposadd  35104  itg2addnclem  35108  itg2addnclem2  35109  ibladdnclem  35113  itgaddnclem2  35116  iblabsnclem  35120  iblmulc2nc  35122  itgmulc2nclem2  35124  itgabsnc  35126  ftc1cnnclem  35128  ftc1anclem5  35134  ftc1anclem8  35137  asindmre  35140  dvasin  35141  areacirclem4  35148  areacirc  35150  isbnd3  35222  ssbnd  35226  prdsbnd  35231  bfplem2  35261  bfp  35262  renegclALT  36259  2xp3dxp2ge1d  39387  factwoffsmonot  39388  0cnALT3  39461  sn-1ne2  39466  oexpreposd  39487  sn-00idlem2  39537  sn-00idlem3  39538  sn-00id  39539  rei4  39560  sn-0tie0  39576  sn-ltaddpos  39578  relt0neg1  39580  sn-0lt1  39587  sn-inelr  39590  itrere  39591  retire  39592  pellexlem6  39775  elpell14qr2  39803  oddcomabszz  39885  zindbi  39887  jm2.24  39904  acongeq  39924  arearect  40165  areaquad  40166  reabsifneg  40332  reabsifnpos  40333  reabsifpos  40334  reabsifnneg  40335  imsqrtvalex  40346  relexp01min  40414  imo72b2lem0  40869  imo72b2lem2  40871  imo72b2lem1  40874  imo72b2  40878  dvconstbi  41038  binomcxplemnn0  41053  binomcxplemdvbinom  41057  binomcxplemcvg  41058  binomcxplemnotnn0  41060  sineq0ALT  41643  halffl  41928  ren0  42039  sqrlearg  42190  limsup10ex  42415  dvnmptdivc  42580  dvnmul  42585  itgsin0pilem1  42592  itgsinexplem1  42596  itgsinexp  42597  iblempty  42607  stoweidlem17  42659  stoweidlem36  42678  stoweidlem55  42697  wallispilem1  42707  wallispilem2  42708  wallispilem4  42710  stirlinglem4  42719  stirlinglem13  42728  stirlinglem14  42729  stirlinglem15  42730  stirlingr  42732  dirker2re  42734  dirkerdenne0  42735  dirkerre  42737  dirkertrigeqlem1  42740  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem11  42760  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem41  42790  fourierdlem42  42791  fourierdlem48  42796  fourierdlem62  42810  fourierdlem66  42814  fourierdlem79  42827  fourierdlem83  42831  fourierdlem94  42842  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  fourierdlem114  42862  sqwvfoura  42870  sqwvfourb  42871  fourierswlem  42872  fouriersw  42873  etransclem23  42899  etransclem44  42920  etransclem46  42922  salexct3  42982  salgensscntex  42984  sge0rnn0  43007  sge00  43015  0ome  43168  ovn0lem  43204  ovnhoilem1  43240  smfmullem1  43423  smfmullem2  43424  smfmullem3  43425  smfmullem4  43426  zm1nn  43859  sqrtnegnre  43864  m1mod0mod1  43886  fmtnoprmfac2lem1  44083  31prm  44114  mod42tp1mod8  44120  nfermltl2rev  44261  tgblthelfgott  44333  altgsumbcALT  44755  expnegico01  44927  dignnld  45017  eenglngeehlnmlem1  45151  line2ylem  45165  line2y  45169  itsclc0yqsollem2  45177  ex-gt  45254