Theorem nndivred 12269

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 12256	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2144  (class class class)co 7398  ℝcr 11074   / cdiv 11846  ℕcn 12212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847  df-nn 12213

This theorem is referenced by:  bcp1nk  14332  reeftcl  16106  efcllem  16109  eftlub  16143  eirrlem  16238  dvdsmod  16365  bitsfzo  16471  bitsmod  16472  bitscmp  16474  bitsuz  16510  bezoutlem3  16577  hashdvds  16812  prmdiv  16822  odzdvds  16833  pcfaclem  16936  pcfac  16937  pcbc  16938  pockthlem  16943  prmreclem4  16957  odmod  19588  zringlpirlem3  21518  prmirredlem  21526  lebnumii  25030  ovoliunlem1  25566  uniioombllem4  25650  dyadss  25658  dyaddisjlem  25659  dyadmaxlem  25661  opnmbllem  25665  mbfi1fseqlem1  25779  mbfi1fseqlem3  25781  mbfi1fseqlem4  25782  mbfi1fseqlem5  25783  mbfi1fseqlem6  25784  aaliou3lem9  26416  taylthlem2  26439  advlogexp  26722  leibpilem2  27008  leibpi  27009  leibpisum  27010  birthdaylem3  27020  amgmlem  27056  fsumharmonic  27078  lgamgulmlem2  27096  lgamgulmlem3  27097  lgamgulmlem4  27098  lgamgulmlem6  27100  regamcl  27127  basellem4  27150  dvdsflf1o  27253  fsumfldivdiaglem  27255  logexprlim  27291  pcbcctr  27342  bcp1ctr  27345  bposlem2  27351  bposlem6  27355  lgseisenlem4  27444  lgseisen  27445  lgsquadlem1  27446  lgsquadlem2  27447  chebbnd1lem3  27537  chtppilimlem1  27539  vmadivsum  27548  vmadivsumb  27549  rplogsumlem1  27550  rplogsumlem2  27551  rpvmasumlem  27553  dchrisumlem1  27555  dchrvmasumlem1  27561  dchrvmasum2lem  27562  dchrvmasum2if  27563  dchrvmasumlem2  27564  dchrvmasumlem3  27565  dchrvmasumiflem1  27567  dchrvmasumiflem2  27568  rpvmasum2  27578  dchrisum0lem1  27582  dchrmusumlem  27588  dirith2  27594  mudivsum  27596  mulogsumlem  27597  mulogsum  27598  mulog2sumlem1  27600  mulog2sumlem2  27601  mulog2sumlem3  27602  vmalogdivsum2  27604  vmalogdivsum  27605  2vmadivsumlem  27606  selberglem1  27611  selberglem2  27612  selbergb  27615  selberg2b  27618  logdivbnd  27622  selberg3lem1  27623  selberg3  27625  selberg4lem1  27626  selberg4  27627  pntrsumo1  27631  pntrsumbnd  27632  pntrsumbnd2  27633  selbergr  27634  selberg3r  27635  selberg4r  27636  pntsf  27639  pntsval2  27642  pntrlog2bndlem2  27644  pntrlog2bndlem4  27646  pntrlog2bndlem5  27647  pntrlog2bndlem6  27649  pntpbnd1  27652  pntpbnd2  27653  pntibndlem2  27657  pntlemn  27666  pntlemj  27669  pntlemk  27672  pntlemo  27673  ostth2lem2  27700  subfacval2  35542  subfaclim  35543  cvmliftlem6  35645  cvmliftlem7  35646  cvmliftlem8  35647  cvmliftlem9  35648  cvmliftlem10  35649  faclimlem1  36098  faclimlem2  36099  faclim2  36103  poimirlem29  38153  opnmbllem0  38160  pellexlem2  43412  hashnzfz2  44902  hashnzfzclim  44903  stoweidlem11  46590  stoweidlem26  46605  stoweidlem42  46621  stoweidlem59  46638  etransclem23  46836