Theorem zred 9378

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7813  ℤcz 9256

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 5881  df-neg 8134  df-z 9257

This theorem is referenced by:  zcnd  9379  btwnapz  9386  eluzelre  9541  eluzadd  9559  eluzsub  9560  uzm1  9561  z2ge  9829  zltaddlt1le  10010  fztri3or  10042  fznlem  10044  fzdisj  10055  fzpreddisj  10074  fznatpl1  10079  uzdisj  10096  fzm1  10103  fz0fzdiffz0  10133  elfzmlbm  10134  elfzmlbp  10135  difelfznle  10138  nn0disj  10141  elfzolt3  10160  fzonel  10163  fzouzdisj  10183  fzonmapblen  10190  fzoaddel  10195  elfzonelfzo  10233  qtri3or  10246  exbtwnzlemstep  10251  exbtwnzlemex  10253  exbtwnz  10254  rebtwn2zlemstep  10256  rebtwn2z  10258  qbtwnrelemcalc  10259  qbtwnre  10260  apbtwnz  10277  qfraclt1  10283  qfracge0  10284  flqge  10285  flid  10287  flqltnz  10290  flqwordi  10291  flqaddz  10300  flqmulnn0  10302  btwnzge0  10303  2tnp1ge0ge0  10304  flhalf  10305  flltdivnn0lt  10307  fldiv4p1lem1div2  10308  ceiqge  10312  ceiqm1l  10314  ceiqle  10316  flqleceil  10320  flqeqceilz  10321  intfracq  10323  modqval  10327  modqge0  10335  modqlt  10336  modqmulnn  10345  mulp1mod1  10368  modaddmodup  10390  modaddmodlo  10391  modsumfzodifsn  10399  addmodlteq  10401  frec2uzlt2d  10407  frec2uzf1od  10409  uzennn  10439  seq3split  10482  iseqf1olemkle  10487  iseqf1olemqcl  10489  iseqf1olemnab  10491  iseqf1olemab  10492  iseqf1olemqk  10497  seq3f1olemqsumkj  10501  seq3f1olemqsumk  10502  seq3f1olemqsum  10503  exp3val  10525  expcanlem  10698  expcan  10699  facavg  10729  bcval4  10735  bcp1nk  10745  bcval5  10746  zfz1isolemiso  10822  seq3coll  10825  seq3shft  10850  resqrexlemdecn  11024  fzomaxdiflem  11124  fsum3cvg3  11407  fsumm1  11427  fsum1p  11429  fsum0diaglem  11451  isumshft  11501  isumsplit  11502  divcnv  11508  geolim2  11523  cvgratnnlemabsle  11538  cvgratnnlemsumlt  11539  cvgratnnlemrate  11541  cvgratz  11543  mertenslemi1  11546  fprodntrivap  11595  prodsnf  11603  fprod1p  11610  fprodeq0  11628  zdvdsdc  11822  dvdslelemd  11852  oexpneg  11885  ltoddhalfle  11901  divalglemnqt  11928  divalglemex  11930  divalglemeuneg  11931  flodddiv4t2lthalf  11945  zsupcl  11951  zssinfcl  11952  infssuzex  11953  suprzubdc  11956  zsupssdc  11958  suprzcl2dc  11959  dvdsbnd  11960  dvdslegcd  11968  gcd0id  11983  gcdneg  11986  bezoutlemsup  12013  dfgcd2  12018  uzwodc  12041  nn0seqcvgd  12044  lcmgcdlem  12080  ncoprmgcdne1b  12092  nprm  12126  prmdc  12133  prmdvdsfz  12142  isprm5lem  12144  coprm  12147  prmexpb  12154  prmfac1  12155  znege1  12181  sqrt2irrap  12183  hashdvds  12224  eulerthlemrprm  12232  eulerthlema  12233  hashgcdlem  12241  pythagtriplem13  12279  pythagtriplem16  12282  pcxcl  12314  pcaddlem  12341  pcadd  12342  pcfac  12351  qexpz  12353  4sqlem7  12385  4sqlem10  12388  oddennn  12396  ennnfoneleminc  12415  nninfdclemp1  12454  nninfdclemlt  12455  mulgfng  12993  subgmulg  13054  ltexp2  14500  logblt  14520  lgsval2lem  14551  lgsvalmod  14560  lgsneg  14565  lgsdilem  14568  lgssq  14581  lgssq2  14582  lgseisenlem2  14591  2sqlem3  14604  2sqlem8  14610  supfz  14960  inffz  14961