Theorem nnrpd 9694

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

Hypothesis

Ref	Expression
nnrpd.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnrpd	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Proof of Theorem nnrpd

Step	Hyp	Ref	Expression
1		nnrpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnrp 9663	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2148  ℕcn 8919  ℝ⁺crp 9653

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-in1 614  ax-in2 615  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-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908  ax-0lt1 7917  ax-0id 7919  ax-rnegex 7920  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-lttrn 7925  ax-pre-ltadd 7927

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2740  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-br 4005  df-opab 4066  df-xp 4633  df-cnv 4635  df-iota 5179  df-fv 5225  df-ov 5878  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998  df-inn 8920  df-rp 9654

This theorem is referenced by:  zgt1rpn0n1  9695  qtri3or  10243  qbtwnrelemcalc  10256  qbtwnre  10257  flqdiv  10321  addmodlteq  10398  nnesq  10640  bcpasc  10746  cvg1nlemcxze  10991  cvg1nlemcau  10993  cvg1nlemres  10994  resqrexlemnmsq  11026  resqrexlemnm  11027  resqrexlemcvg  11028  climrecvg1n  11356  climcvg1nlem  11357  cvgratnnlembern  11531  cvgratnnlemfm  11537  mertenslemi1  11543  mertenslem2  11544  efcllemp  11666  ege2le3  11679  eftlub  11698  effsumlt  11700  efgt1p2  11703  eirraplem  11784  prmind2  12120  isprm5lem  12141  sqrt2irrlem  12161  sqrt2irraplemnn  12179  sqrt2irrap  12180  modprmn0modprm0  12256  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  4sqlem7  12382  logbrec  14381  logbgcd1irr  14388  logbgcd1irraplemexp  14389  logbgcd1irraplemap  14390  lgseisenlem1  14453  2sqlem8  14473  cvgcmp2nlemabs  14783  trilpolemlt1  14792