Theorem zred 9751

Description: An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)

Assertion

Ref	Expression
zred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem zred

Step	Hyp	Ref	Expression
1		zssre 9634	. 2 ⊢ ℤ ⊆ ℝ
2		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1, 2	sselid 3246	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2209  ℝcr 8172  ℤcz 9627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6082  df-neg 8494  df-z 9628

This theorem is referenced by:  zcnd  9752  btwnapz  9759  eluzmn  9911  eluzelre  9915  eluzadd  9934  eluzsub  9935  uzm1  9936  ltesubnnd  10153  z2ge  10211  zltaddlt1le  10393  fztri3or  10426  fznlem  10428  fzdisj  10440  fzpreddisj  10461  fznatpl1  10466  uzdisj  10483  fzm1  10490  fz0fzdiffz0  10520  elfzmlbm  10521  elfzmlbp  10522  difelfznle  10525  nn0disj  10528  elfzolt3  10548  fzonel  10551  fzouzdisj  10572  fzodisjsn  10574  fzonmapblen  10582  fzoaddel  10588  elincfzoext  10594  elfzonelfzo  10631  zsupcl  10647  zssinfcl  10648  infssuzex  10649  suprzubdc  10654  zsupssdc  10656  suprzcl2dc  10657  qtri3or  10658  exbtwnzlemstep  10665  exbtwnzlemex  10667  exbtwnz  10668  rebtwn2zlemstep  10670  rebtwn2z  10672  qbtwnrelemcalc  10673  qbtwnre  10674  apbtwnz  10692  qfraclt1  10698  qfracge0  10699  flqge  10700  flid  10702  flqltnz  10705  flqwordi  10706  flqaddz  10715  flqmulnn0  10717  btwnzge0  10718  2tnp1ge0ge0  10719  flhalf  10720  flltdivnn0lt  10722  fldiv4p1lem1div2  10723  fldiv4lem1div2uz2  10724  ceiqge  10729  ceiqm1l  10731  ceiqle  10733  flqleceil  10737  flqeqceilz  10738  intfracq  10740  modqval  10744  modqge0  10752  modqlt  10753  modqmulnn  10762  mulp1mod1  10785  modaddmodup  10807  modaddmodlo  10808  modsumfzodifsn  10816  addmodlteq  10818  frec2uzlt2d  10824  frec2uzf1od  10826  uzennn  10856  seq3split  10908  iseqf1olemkle  10917  iseqf1olemqcl  10919  iseqf1olemnab  10921  iseqf1olemab  10922  iseqf1olemqk  10927  seq3f1olemqsumkj  10931  seq3f1olemqsumk  10932  seq3f1olemqsum  10933  seqf1oglem1  10939  seqf1oglem2  10940  seqfeq4g  10951  exp3val  10961  expcanlem  11136  expcan  11137  facavg  11167  bcval4  11173  bcp1nk  11183  bcval5  11184  bcm1n  11190  zfz1isolemiso  11274  seq3coll  11277  iswrdiz  11294  ccatrn  11360  ccatalpha  11364  seq3shft  11586  resqrexlemdecn  11761  fzomaxdiflem  11861  nn0maxcl  11974  fsum3cvg3  12146  fsumm1  12166  fsum1p  12168  fsum0diaglem  12190  isumshft  12240  isumsplit  12241  divcnv  12247  geolim2  12262  cvgratnnlemabsle  12277  cvgratnnlemsumlt  12278  cvgratnnlemrate  12280  cvgratz  12282  mertenslemi1  12285  fprodntrivap  12334  prodsnf  12342  fprod1p  12349  fprodeq0  12367  zdvdsdc  12562  dvdslelemd  12593  oexpneg  12627  ltoddhalfle  12643  divalglemnqt  12670  divalglemex  12672  divalglemeuneg  12673  flodddiv4t2lthalf  12689  bitsfzolem  12704  bitsfzo  12705  bitsmod  12706  bitscmp  12708  dvdsbnd  12716  dvdslegcd  12724  gcd0id  12739  gcdneg  12742  bezoutlemsup  12769  dfgcd2  12774  uzwodc  12797  nn0seqcvgd  12802  lcmgcdlem  12838  ncoprmgcdne1b  12850  nprm  12884  prmdc  12891  prmdvdsfz  12900  isprm5lem  12902  coprm  12905  prmexpb  12912  prmfac1  12913  znege1  12939  sqrt2irrap  12941  hashdvds  12982  eulerthlemrprm  12990  eulerthlema  12991  hashgcdlem  12999  pythagtriplem13  13038  pythagtriplem16  13041  pcxcl  13073  pcaddlem  13101  pcadd  13102  pcfac  13112  qexpz  13114  4sqlem7  13146  4sqlem10  13149  4sqexercise2  13161  4sqlemsdc  13162  4sqlem11  13163  4sqlem12  13164  4sqlem15  13167  4sqlem16  13168  4sqlem17  13169  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemimin  13232  ballotfilemsgt1  13237  ballotfilemsel1i  13239  ballotfilemsi  13241  ballotfilemsima  13242  ballotfilemgun  13251  ballotfilemfrceq  13255  ballotfilemfrcn0  13256  ballotfilemirc  13258  oddennn  13266  ennnfoneleminc  13285  nninfdclemp1  13324  nninfdclemlt  13325  gzsumfzval  13694  gzsumcl  13787  mulgfng  13910  subgmulg  13974  gzsumreidx  14124  gzsumsubmcl  14125  gzsummhm  14128  gzsumsplit0  14131  gzsumshift  14132  ltexp2  16026  logblt  16047  mersenne  16094  lgsval2lem  16112  lgsvalmod  16121  lgsneg  16126  lgsdilem  16129  lgssq  16142  lgssq2  16143  gausslemma2dlem1a  16160  gausslemma2dlem3  16165  lgseisenlem2  16173  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad3  16186  2lgslem1a2  16189  2sqlem3  16219  2sqlem8  16225  supfz  17095  inffz  17096