Theorem zred 9377

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 9262	. 2 ⊢ ℤ ⊆ ℝ
2		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1, 2	sselid 3155	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7812  ℤcz 9255

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-rab 2464  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880  df-neg 8133  df-z 9256

This theorem is referenced by:  zcnd  9378  btwnapz  9385  eluzelre  9540  eluzadd  9558  eluzsub  9559  uzm1  9560  z2ge  9828  zltaddlt1le  10009  fztri3or  10041  fznlem  10043  fzdisj  10054  fzpreddisj  10073  fznatpl1  10078  uzdisj  10095  fzm1  10102  fz0fzdiffz0  10132  elfzmlbm  10133  elfzmlbp  10134  difelfznle  10137  nn0disj  10140  elfzolt3  10159  fzonel  10162  fzouzdisj  10182  fzonmapblen  10189  fzoaddel  10194  elfzonelfzo  10232  qtri3or  10245  exbtwnzlemstep  10250  exbtwnzlemex  10252  exbtwnz  10253  rebtwn2zlemstep  10255  rebtwn2z  10257  qbtwnrelemcalc  10258  qbtwnre  10259  apbtwnz  10276  qfraclt1  10282  qfracge0  10283  flqge  10284  flid  10286  flqltnz  10289  flqwordi  10290  flqaddz  10299  flqmulnn0  10301  btwnzge0  10302  2tnp1ge0ge0  10303  flhalf  10304  flltdivnn0lt  10306  fldiv4p1lem1div2  10307  ceiqge  10311  ceiqm1l  10313  ceiqle  10315  flqleceil  10319  flqeqceilz  10320  intfracq  10322  modqval  10326  modqge0  10334  modqlt  10335  modqmulnn  10344  mulp1mod1  10367  modaddmodup  10389  modaddmodlo  10390  modsumfzodifsn  10398  addmodlteq  10400  frec2uzlt2d  10406  frec2uzf1od  10408  uzennn  10438  seq3split  10481  iseqf1olemkle  10486  iseqf1olemqcl  10488  iseqf1olemnab  10490  iseqf1olemab  10491  iseqf1olemqk  10496  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  exp3val  10524  expcanlem  10697  expcan  10698  facavg  10728  bcval4  10734  bcp1nk  10744  bcval5  10745  zfz1isolemiso  10821  seq3coll  10824  seq3shft  10849  resqrexlemdecn  11023  fzomaxdiflem  11123  fsum3cvg3  11406  fsumm1  11426  fsum1p  11428  fsum0diaglem  11450  isumshft  11500  isumsplit  11501  divcnv  11507  geolim2  11522  cvgratnnlemabsle  11537  cvgratnnlemsumlt  11538  cvgratnnlemrate  11540  cvgratz  11542  mertenslemi1  11545  fprodntrivap  11594  prodsnf  11602  fprod1p  11609  fprodeq0  11627  zdvdsdc  11821  dvdslelemd  11851  oexpneg  11884  ltoddhalfle  11900  divalglemnqt  11927  divalglemex  11929  divalglemeuneg  11930  flodddiv4t2lthalf  11944  zsupcl  11950  zssinfcl  11951  infssuzex  11952  suprzubdc  11955  zsupssdc  11957  suprzcl2dc  11958  dvdsbnd  11959  dvdslegcd  11967  gcd0id  11982  gcdneg  11985  bezoutlemsup  12012  dfgcd2  12017  uzwodc  12040  nn0seqcvgd  12043  lcmgcdlem  12079  ncoprmgcdne1b  12091  nprm  12125  prmdc  12132  prmdvdsfz  12141  isprm5lem  12143  coprm  12146  prmexpb  12153  prmfac1  12154  znege1  12180  sqrt2irrap  12182  hashdvds  12223  eulerthlemrprm  12231  eulerthlema  12232  hashgcdlem  12240  pythagtriplem13  12278  pythagtriplem16  12281  pcxcl  12313  pcaddlem  12340  pcadd  12341  pcfac  12350  qexpz  12352  4sqlem7  12384  4sqlem10  12387  oddennn  12395  ennnfoneleminc  12414  nninfdclemp1  12453  nninfdclemlt  12454  mulgfng  12992  subgmulg  13053  ltexp2  14399  logblt  14419  lgsval2lem  14450  lgsvalmod  14459  lgsneg  14464  lgsdilem  14467  lgssq  14480  lgssq2  14481  lgseisenlem2  14490  2sqlem3  14503  2sqlem8  14509  supfz  14857  inffz  14858