MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nndivred Unicode version

Theorem nndivred 9981
Description: A natural number is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
nndivred.1  |-  ( ph  ->  A  e.  RR )
nndivred.2  |-  ( ph  ->  B  e.  NN )
Assertion
Ref Expression
nndivred  |-  ( ph  ->  ( A  /  B
)  e.  RR )

Proof of Theorem nndivred
StepHypRef Expression
1 nndivred.1 . 2  |-  ( ph  ->  A  e.  RR )
2 nndivred.2 . 2  |-  ( ph  ->  B  e.  NN )
3 nndivre 9968 . 2  |-  ( ( A  e.  RR  /\  B  e.  NN )  ->  ( A  /  B
)  e.  RR )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  /  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717  (class class class)co 6021   RRcr 8923    / cdiv 9610   NNcn 9933
This theorem is referenced by:  bcp1nk  11536  reeftcl  12605  efcllem  12608  eftlub  12638  eirrlem  12731  dvdsmod  12834  bitsfzo  12875  bitsmod  12876  bitscmp  12878  bitsuz  12914  bezoutlem3  12968  hashdvds  13092  prmdiv  13102  odzdvds  13109  pcfaclem  13195  pcfac  13196  pcbc  13197  pockthlem  13201  prmreclem4  13215  odmod  15112  zlpirlem3  16694  prmirredlem  16697  lebnumii  18863  ovoliunlem1  19266  uniioombllem4  19346  dyadss  19354  dyaddisjlem  19355  dyadmaxlem  19357  opnmbllem  19361  mbfi1fseqlem1  19475  mbfi1fseqlem3  19477  mbfi1fseqlem4  19478  mbfi1fseqlem5  19479  mbfi1fseqlem6  19480  aaliou3lem9  20135  taylthlem2  20158  advlogexp  20414  leibpilem2  20649  leibpi  20650  leibpisum  20651  birthdaylem3  20660  amgmlem  20696  fsumharmonic  20718  basellem4  20734  dvdsflf1o  20840  fsumfldivdiaglem  20842  logexprlim  20877  pcbcctr  20928  bcp1ctr  20931  bposlem2  20937  bposlem6  20941  lgseisenlem4  21004  lgseisen  21005  lgsquadlem1  21006  lgsquadlem2  21007  chebbnd1lem3  21033  chtppilimlem1  21035  vmadivsum  21044  vmadivsumb  21045  rplogsumlem1  21046  rplogsumlem2  21047  rpvmasumlem  21049  dchrisumlem1  21051  dchrvmasumlem1  21057  dchrvmasum2lem  21058  dchrvmasum2if  21059  dchrvmasumlem2  21060  dchrvmasumlem3  21061  dchrvmasumiflem1  21063  dchrvmasumiflem2  21064  rpvmasum2  21074  dchrisum0lem1  21078  dchrmusumlem  21084  dirith2  21090  mudivsum  21092  mulogsumlem  21093  mulogsum  21094  mulog2sumlem1  21096  mulog2sumlem2  21097  mulog2sumlem3  21098  vmalogdivsum2  21100  vmalogdivsum  21101  2vmadivsumlem  21102  selberglem1  21107  selberglem2  21108  selbergb  21111  selberg2b  21114  logdivbnd  21118  selberg3lem1  21119  selberg3  21121  selberg4lem1  21122  selberg4  21123  pntrsumo1  21127  pntrsumbnd  21128  pntrsumbnd2  21129  selbergr  21130  selberg3r  21131  selberg4r  21132  pntsf  21135  pntsval2  21138  pntrlog2bndlem2  21140  pntrlog2bndlem4  21142  pntrlog2bndlem5  21143  pntrlog2bndlem6  21145  pntpbnd1  21148  pntpbnd2  21149  pntibndlem2  21153  pntlemn  21162  pntlemj  21165  pntlemk  21168  pntlemo  21169  ostth2lem2  21196  lgamgulmlem2  24594  lgamgulmlem3  24595  lgamgulmlem4  24596  lgamgulmlem6  24598  lgamcvg2  24619  regamcl  24625  subfacval2  24653  subfaclim  24654  cvmliftlem6  24757  cvmliftlem7  24758  cvmliftlem8  24759  cvmliftlem9  24760  cvmliftlem10  24761  faclimlem1  25121  faclimlem2  25122  faclimlem3  25123  faclim  25124  iprodfac  25125  faclim2  25126  pellexlem2  26585  stoweidlem11  27429  stoweidlem26  27444  stoweidlem42  27460  stoweidlem59  27477
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642  ax-resscn 8981  ax-1cn 8982  ax-icn 8983  ax-addcl 8984  ax-addrcl 8985  ax-mulcl 8986  ax-mulrcl 8987  ax-mulcom 8988  ax-addass 8989  ax-mulass 8990  ax-distr 8991  ax-i2m1 8992  ax-1ne0 8993  ax-1rid 8994  ax-rnegex 8995  ax-rrecex 8996  ax-cnre 8997  ax-pre-lttri 8998  ax-pre-lttrn 8999  ax-pre-ltadd 9000  ax-pre-mulgt0 9001
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-nel 2554  df-ral 2655  df-rex 2656  df-reu 2657  df-rmo 2658  df-rab 2659  df-v 2902  df-sbc 3106  df-csb 3196  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-pss 3280  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-tp 3766  df-op 3767  df-uni 3959  df-iun 4038  df-br 4155  df-opab 4209  df-mpt 4210  df-tr 4245  df-eprel 4436  df-id 4440  df-po 4445  df-so 4446  df-fr 4483  df-we 4485  df-ord 4526  df-on 4527  df-lim 4528  df-suc 4529  df-om 4787  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402  df-fv 5403  df-ov 6024  df-oprab 6025  df-mpt2 6026  df-riota 6486  df-recs 6570  df-rdg 6605  df-er 6842  df-en 7047  df-dom 7048  df-sdom 7049  df-pnf 9056  df-mnf 9057  df-xr 9058  df-ltxr 9059  df-le 9060  df-sub 9226  df-neg 9227  df-div 9611  df-nn 9934
  Copyright terms: Public domain W3C validator