Theorem nndivred 12228

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7364  ℝcr 11034   / cdiv 11804  ℕcn 12171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111  ax-pre-mulgt0 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-om 7815  df-2nd 7940  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-xr 11180  df-ltxr 11181  df-le 11182  df-sub 11376  df-neg 11377  df-div 11805  df-nn 12172

This theorem is referenced by:  bcp1nk  14276  reeftcl  16036  efcllem  16039  eftlub  16073  eirrlem  16168  dvdsmod  16295  bitsfzo  16401  bitsmod  16402  bitscmp  16404  bitsuz  16440  bezoutlem3  16507  hashdvds  16742  prmdiv  16752  odzdvds  16763  pcfaclem  16866  pcfac  16867  pcbc  16868  pockthlem  16873  prmreclem4  16887  odmod  19518  zringlpirlem3  21460  prmirredlem  21468  lebnumii  24949  ovoliunlem1  25485  uniioombllem4  25569  dyadss  25577  dyaddisjlem  25578  dyadmaxlem  25580  opnmbllem  25584  mbfi1fseqlem1  25698  mbfi1fseqlem3  25700  mbfi1fseqlem4  25701  mbfi1fseqlem5  25702  mbfi1fseqlem6  25703  aaliou3lem9  26333  taylthlem2  26357  taylthlem2OLD  26358  advlogexp  26638  leibpilem2  26924  leibpi  26925  leibpisum  26926  birthdaylem3  26936  amgmlem  26973  fsumharmonic  26995  lgamgulmlem2  27013  lgamgulmlem3  27014  lgamgulmlem4  27015  lgamgulmlem6  27017  regamcl  27044  basellem4  27067  dvdsflf1o  27170  fsumfldivdiaglem  27172  logexprlim  27208  pcbcctr  27259  bcp1ctr  27262  bposlem2  27268  bposlem6  27272  lgseisenlem4  27361  lgseisen  27362  lgsquadlem1  27363  lgsquadlem2  27364  chebbnd1lem3  27454  chtppilimlem1  27456  vmadivsum  27465  vmadivsumb  27466  rplogsumlem1  27467  rplogsumlem2  27468  rpvmasumlem  27470  dchrisumlem1  27472  dchrvmasumlem1  27478  dchrvmasum2lem  27479  dchrvmasum2if  27480  dchrvmasumlem2  27481  dchrvmasumlem3  27482  dchrvmasumiflem1  27484  dchrvmasumiflem2  27485  rpvmasum2  27495  dchrisum0lem1  27499  dchrmusumlem  27505  dirith2  27511  mudivsum  27513  mulogsumlem  27514  mulogsum  27515  mulog2sumlem1  27517  mulog2sumlem2  27518  mulog2sumlem3  27519  vmalogdivsum2  27521  vmalogdivsum  27522  2vmadivsumlem  27523  selberglem1  27528  selberglem2  27529  selbergb  27532  selberg2b  27535  logdivbnd  27539  selberg3lem1  27540  selberg3  27542  selberg4lem1  27543  selberg4  27544  pntrsumo1  27548  pntrsumbnd  27549  pntrsumbnd2  27550  selbergr  27551  selberg3r  27552  selberg4r  27553  pntsf  27556  pntsval2  27559  pntrlog2bndlem2  27561  pntrlog2bndlem4  27563  pntrlog2bndlem5  27564  pntrlog2bndlem6  27566  pntpbnd1  27569  pntpbnd2  27570  pntibndlem2  27574  pntlemn  27583  pntlemj  27586  pntlemk  27589  pntlemo  27590  ostth2lem2  27617  subfacval2  35391  subfaclim  35392  cvmliftlem6  35494  cvmliftlem7  35495  cvmliftlem8  35496  cvmliftlem9  35497  cvmliftlem10  35498  faclimlem1  35947  faclimlem2  35948  faclim2  35952  poimirlem29  37992  opnmbllem0  37999  pellexlem2  43284  hashnzfz2  44774  hashnzfzclim  44775  stoweidlem11  46465  stoweidlem26  46480  stoweidlem42  46496  stoweidlem59  46513  etransclem23  46711