Theorem peano2re 11522

Description: A theorem for reals analogous the second Peano postulate peano2nn 12387. (Contributed by NM, 5-Jul-2005.)

Assertion

Ref	Expression
peano2re	⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11347	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11322	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 704	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7451  ℝcr 11238  1c1 11240   + caddc 11242

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rrecex 11311  ax-cnre 11312

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  lep1  12198  letrp1  12201  p1le  12202  ledivp1  12259  sup2  12313  nnssre  12379  nnge1  12406  div4p1lem1div2  12641  zltp1le  12786  suprzcl  12819  zeo  12825  peano2uz2  12827  uzind  12831  numltc  12885  uzwo  13078  ge0p1rp  13193  qbtwnxr  13370  xrsupsslem  13477  supxrunb1  13489  fznatpl1  13752  fzp1disj  13757  fzneuz  13782  fzp1nel  13785  ubmelm1fzo  13938  fllep1  13981  flflp1  13987  flhalf  14010  ltdifltdiv  14014  fldiv4p1lem1div2  14015  dfceil2  14019  ceim1l  14027  uzsup  14043  modltm1p1mod  14106  addmodlteq  14129  fsequb  14158  seqf1olem1  14224  seqf1olem2  14225  bernneq3  14416  expnbnd  14417  expmulnbnd  14420  discr1  14424  discr  14425  facwordi  14474  faclbnd  14475  hashfun  14623  seqcoll2  14651  rexuzre  15564  caubnd  15570  rlim2lt  15708  lo1bddrp  15736  rlimo1  15828  o1rlimmul  15830  o1fsum  16024  harmonic  16072  expcnv  16077  geomulcvg  16089  mertenslem1  16097  bpoly4  16269  nonsq  16979  eulerthlem2  17003  pcprendvds  17062  pcmpt  17114  pcfac  17121  vdwlem6  17208  vdwlem11  17213  chnccat  18850  chfacffsupp  23229  chfacfscmul0  23231  chfacfpmmul0  23235  tgioo  25170  zcld  25188  iocopnst  25316  cnheibor  25331  bndth  25334  cncmet  25698  pjthlem1  25813  ovolicc2lem3  25895  ovolicopnf  25900  ioorcl2  25948  dyadf  25967  dyadovol  25969  dyadss  25970  dyaddisjlem  25971  dyadmaxlem  25973  opnmbllem  25977  volsup2  25981  vitalilem2  25985  itg2const2  26117  itg2cnlem1  26137  dvfsumle  26396  dvfsumabs  26398  dvfsumlem1  26401  dvfsumlem3  26403  dvfsumrlim  26406  fta1glem2  26542  fta1lem  26683  aalioulem3  26718  ulmbdd  26782  itgulm  26792  psercnlem1  26809  abelthlem2  26816  abelthlem7  26822  reeff1olem  26830  logtayl  27045  loglesqrt  27146  atanlogsublem  27300  leibpi  27327  efrlim  27354  harmonicubnd  27394  fsumharmonic  27396  ftalem5  27461  basellem2  27466  basellem3  27467  chtnprm  27538  chpp1  27539  ppip1le  27545  ppiub  27588  logfaclbnd  27606  logfacrlim  27608  perfectlem2  27614  bcmono  27661  lgsvalmod  27700  gausslemma2dlem3  27752  lgseisen  27763  lgsquadlem1  27764  lgsquadlem2  27765  chebbnd1lem2  27854  chtppilimlem1  27857  rplogsumlem2  27869  dchrisumlema  27872  dchrisumlem1  27873  dchrisumlem3  27875  dchrisum0lem1  27900  chpdifbndlem1  27937  logdivbnd  27940  pntrmax  27948  pntrsumo1  27949  pntpbnd1a  27969  pntpbnd1  27970  pntpbnd2  27971  pntibndlem2  27975  pntlemg  27982  pntlemr  27986  pntlemj  27987  pntlemk  27990  ostth2lem1  28002  qabvle  28009  ostth2lem3  28019  ostth2lem4  28020  axlowdimlem16  29592  wwlksnredwwlkn  30541  wwlksnextproplem3  30557  wwlksext2clwwlk  30705  wwlksubclwwlk  30706  eupth2lems  30896  smcnlem  31356  minvecolem4  31539  pjhthlem1  32050  zltp1ne  36098  cvmliftlem7  36264  dnibndlem13  37571  knoppndvlem19  37611  knoppndvlem21  37613  icoreunrn  38550  relowlssretop  38554  ltflcei  38799  poimirlem1  38807  poimirlem2  38808  poimirlem4  38810  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  opnmbllem0  38842  mblfinlem1  38843  mblfinlem2  38844  mblfinlem4  38846  itg2addnclem2  38858  itg2addnclem3  38859  incsequz  38948  isbnd3  38984  rrntotbnd  39036  sn-sup2  43821  3cubeslem1  43960  3cubeslem2  43961  irrapxlem4  44098  pellexlem5  44106  pell14qrgapw  44149  pellfundgt1  44156  jm3.1lem2  44291  expdiophlem1  44294  fzuntgd  44720  zltlesub  46574  suplesup  46624  supxrunb3  46683  xrpnf  46768  fmul01lt1lem1  46869  limsupre3lem  47015  xlimxrre  47114  xlimpnfv  47121  ioodvbdlimc1lem1  47214  dvnxpaek  47225  dvnmul  47226  fourierdlem4  47394  fourierdlem11  47401  fourierdlem25  47415  fourierdlem50  47439  fourierdlem64  47453  fourierdlem65  47454  fourierdlem77  47466  fourierdlem79  47468  iinhoiicclem  47956  smfresal  48071  fmtno4prmfac  48930  lighneallem4a  48966  evenltle  49088  perfectALTVlem2  49093  logbpw2m1  50010