Theorem nnrecred 12293

Description: The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

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

Assertion

Ref	Expression
nnrecred	⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)

Proof of Theorem nnrecred

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnrecre 12284	. 2 ⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈ ℝ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2099  (class class class)co 7420  ℝcr 11137  1c1 11139   / cdiv 11901  ℕcn 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-er 8724  df-en 8964  df-dom 8965  df-sdom 8966  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243

This theorem is referenced by:  trireciplem  15840  trirecip  15841  geo2sum  15851  geo2lim  15853  bpolydiflem  16030  ege2le3  16066  eftlub  16085  eirrlem  16180  prmreclem4  16887  prmreclem6  16889  lmnn  25190  bcthlem5  25255  opnmbllem  25529  mbfi1fseqlem4  25647  taylthlem2  26308  taylthlem2OLD  26309  logtayl  26593  leibpi  26873  amgmlem  26921  emcllem1  26927  emcllem2  26928  emcllem3  26929  emcllem5  26931  harmoniclbnd  26940  harmonicubnd  26941  harmonicbnd4  26942  fsumharmonic  26943  lgamgulmlem1  26960  lgamgulmlem2  26961  lgamgulmlem3  26962  lgamgulmlem5  26964  lgamucov  26969  ftalem4  27007  ftalem5  27008  basellem6  27017  basellem7  27018  basellem9  27020  chpchtsum  27151  logfaclbnd  27154  rplogsumlem2  27417  rpvmasumlem  27419  dchrmusum2  27426  dchrvmasumlem3  27431  dchrisum0fno1  27443  mulogsumlem  27463  mulogsum  27464  mulog2sumlem1  27466  vmalogdivsum2  27470  logdivbnd  27488  pntrsumo1  27497  pntrlog2bndlem2  27510  pntrlog2bndlem5  27513  pntrlog2bndlem6  27515  pntpbnd2  27519  padicabvf  27563  nrt2irr  30282  minvecolem3  30685  minvecolem4  30689  subfacval3  34799  cvmliftlem13  34906  poimirlem29  37122  opnmbllem0  37129  heiborlem7  37290  fltne  42068  irrapxlem4  42245  hashnzfz2  43758  hashnzfzclim  43759  stoweidlem30  45418  stoweidlem38  45426  stoweidlem44  45432  vonioolem1  46068  smflimlem3  46161  amgmlemALT  48236