Theorem nndivre 12252

Description: The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)

Assertion

Ref	Expression
nndivre	⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ)

Proof of Theorem nndivre

Step	Hyp	Ref	Expression
1		nnre 12218	. . 3 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		nnne0 12245	. . 3 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
3	1, 2	jca 511	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ≠ 0))
4		redivcl 11932	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ≠ 0) → (𝐴 / 𝑁) ∈ ℝ)
5	4	3expb 1117	. 2 ⊢ ((𝐴 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 𝑁 ≠ 0)) → (𝐴 / 𝑁) ∈ ℝ)
6	3, 5	sylan2 592	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098   ≠ wne 2932  (class class class)co 7402  ℝcr 11106  0cc0 11107   / cdiv 11870  ℕcn 12211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212

This theorem is referenced by:  nnrecre  12253  nndivred  12265  fldiv2  13827  zmodcl  13857  iexpcyc  14172  01sqrexlem7  15197  expcnv  15812  ef01bndlem  16130  sin01bnd  16131  cos01bnd  16132  rpnnen2lem2  16161  rpnnen2lem3  16162  rpnnen2lem4  16163  rpnnen2lem9  16168  fldivp1  16835  ovoliunlem1  25375  dyadf  25464  dyadovol  25466  mbfi1fseqlem3  25591  mbfi1fseqlem4  25592  dveflem  25855  plyeq0lem  26087  tangtx  26380  tan4thpi  26389  root1id  26629  root1eq1  26630  root1cj  26631  cxpeq  26632  1cubrlem  26713  atan1  26800  log2tlbnd  26817  log2ublem1  26818  log2ublem2  26819  log2ub  26821  birthdaylem3  26825  birthday  26826  basellem5  26957  basellem8  26960  ppiub  27077  logfac2  27090  dchrptlem1  27137  dchrptlem2  27138  bposlem3  27159  bposlem4  27160  bposlem5  27161  bposlem6  27162  bposlem9  27165  vmadivsum  27355  dchrisum0lem1a  27359  dchrmusum2  27367  dchrvmasum2if  27370  dchrvmasumlem2  27371  dchrvmasumiflem1  27374  dchrvmasumiflem2  27375  dchrisum0re  27386  dchrisum0lem1b  27388  dchrisum0lem1  27389  dchrvmasumlem  27396  rplogsum  27400  mudivsum  27403  selberg2  27424  chpdifbndlem1  27426  selberg3lem1  27430  selbergr  27441  pntlemb  27470  pntlemg  27471  pntlemf  27478  snmlff  34837  sinccvglem  35174  circum  35176  poimirlem29  37020  poimirlem30  37021  poimirlem32  37023