Theorem nndivred 11694

Description: A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
nndivred.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
nndivred.2	⊢ (𝜑 → 𝐵 ∈ ℕ)

Assertion

Ref	Expression
nndivred	⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)

Proof of Theorem nndivred

Step	Hyp	Ref	Expression
1		nndivred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		nndivred.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℕ)
3		nndivre 11681	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 586	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7158  ℝcr 10538   / cdiv 11299  ℕcn 11640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-nn 11641

This theorem is referenced by:  bcp1nk  13680  reeftcl  15430  efcllem  15433  eftlub  15464  eirrlem  15559  dvdsmod  15680  bitsfzo  15786  bitsmod  15787  bitscmp  15789  bitsuz  15825  bezoutlem3  15891  hashdvds  16114  prmdiv  16124  odzdvds  16134  pcfaclem  16236  pcfac  16237  pcbc  16238  pockthlem  16243  prmreclem4  16257  odmod  18676  zringlpirlem3  20635  prmirredlem  20642  lebnumii  23572  ovoliunlem1  24105  uniioombllem4  24189  dyadss  24197  dyaddisjlem  24198  dyadmaxlem  24200  opnmbllem  24204  mbfi1fseqlem1  24318  mbfi1fseqlem3  24320  mbfi1fseqlem4  24321  mbfi1fseqlem5  24322  mbfi1fseqlem6  24323  aaliou3lem9  24941  taylthlem2  24964  advlogexp  25240  leibpilem2  25521  leibpi  25522  leibpisum  25523  birthdaylem3  25533  amgmlem  25569  fsumharmonic  25591  lgamgulmlem2  25609  lgamgulmlem3  25610  lgamgulmlem4  25611  lgamgulmlem6  25613  regamcl  25640  basellem4  25663  dvdsflf1o  25766  fsumfldivdiaglem  25768  logexprlim  25803  pcbcctr  25854  bcp1ctr  25857  bposlem2  25863  bposlem6  25867  lgseisenlem4  25956  lgseisen  25957  lgsquadlem1  25958  lgsquadlem2  25959  chebbnd1lem3  26049  chtppilimlem1  26051  vmadivsum  26060  vmadivsumb  26061  rplogsumlem1  26062  rplogsumlem2  26063  rpvmasumlem  26065  dchrisumlem1  26067  dchrvmasumlem1  26073  dchrvmasum2lem  26074  dchrvmasum2if  26075  dchrvmasumlem2  26076  dchrvmasumlem3  26077  dchrvmasumiflem1  26079  dchrvmasumiflem2  26080  rpvmasum2  26090  dchrisum0lem1  26094  dchrmusumlem  26100  dirith2  26106  mudivsum  26108  mulogsumlem  26109  mulogsum  26110  mulog2sumlem1  26112  mulog2sumlem2  26113  mulog2sumlem3  26114  vmalogdivsum2  26116  vmalogdivsum  26117  2vmadivsumlem  26118  selberglem1  26123  selberglem2  26124  selbergb  26127  selberg2b  26130  logdivbnd  26134  selberg3lem1  26135  selberg3  26137  selberg4lem1  26138  selberg4  26139  pntrsumo1  26143  pntrsumbnd  26144  pntrsumbnd2  26145  selbergr  26146  selberg3r  26147  selberg4r  26148  pntsf  26151  pntsval2  26154  pntrlog2bndlem2  26156  pntrlog2bndlem4  26158  pntrlog2bndlem5  26159  pntrlog2bndlem6  26161  pntpbnd1  26164  pntpbnd2  26165  pntibndlem2  26169  pntlemn  26178  pntlemj  26181  pntlemk  26184  pntlemo  26185  ostth2lem2  26212  subfacval2  32436  subfaclim  32437  cvmliftlem6  32539  cvmliftlem7  32540  cvmliftlem8  32541  cvmliftlem9  32542  cvmliftlem10  32543  faclimlem1  32977  faclimlem2  32978  faclim2  32982  poimirlem29  34923  opnmbllem0  34930  pellexlem2  39434  hashnzfz2  40660  hashnzfzclim  40661  stoweidlem11  42303  stoweidlem26  42318  stoweidlem42  42334  stoweidlem59  42351  etransclem23  42549