Theorem nnge1d 12426

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

Hypothesis

Ref	Expression
nnge1d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnge1d	⊢ (𝜑 → 1 ≤ 𝐴)

Proof of Theorem nnge1d

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnge1 12406	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → 1 ≤ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5108  1c1 11240   ≤ cle 11383  ℕcn 12375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-nn 12376

This theorem is used by:  bernneq3  14416  facwordi  14474  faclbnd  14475  faclbnd3  14477  faclbnd4lem3  14480  facavg  14486  hashge1  14574  seqcoll  14650  wrdind  14913  wrd2ind  14914  eftlub  16321  eflegeo  16333  eirrlem  16416  divdenle  16969  eulerthlem2  17003  infpnlem2  17133  4sqlem11  17177  4sqlem12  17178  prmolefac  17268  2expltfac  17314  cshwshash  17326  fislw  19890  gzrngunitlem  21792  psdmul  22542  ovoliunlem1  25878  plyn0mulidp  26657  aalioulem2  26717  aalioulem4  26719  aalioulem5  26720  aaliou2b  26725  aaliou3lem2  26727  aaliou3lem8  26729  lgamgulmlem5  27417  vmage0  27505  chpge0  27510  vma1  27550  sqff1o  27566  fsumfldivdiaglem  27573  vmalelog  27589  chtublem  27595  fsumvma2  27598  chpchtsum  27603  logfacubnd  27605  perfectlem2  27614  dchrelbas4  27627  bposlem1  27668  bposlem2  27669  bposlem5  27672  lgsdir  27716  lgsdilem2  27717  lgseisenlem1  27759  2sqlem8  27810  chebbnd1lem1  27853  chebbnd1lem2  27854  chebbnd1lem3  27855  dchrisumlem3  27875  dchrisum0flblem1  27892  dchrisum0lem1b  27899  dirith2  27912  selbergb  27933  selberg3lem2  27942  pntrlog2bndlem1  27961  pntrlog2bndlem3  27963  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  pntrlog2bnd  27968  pntpbnd1a  27969  pntlemj  27987  pntlemk  27990  flt4lem7  28046  nexple  33520  mplmulmvr  34282  esplyind  34318  submateqlem2  34551  hgt750lemb  35396  poimirlem7  38813  poimirlem19  38825  poimirlem28  38834  lcmineqlem10  43354  lcmineqlem11  43355  lcmineqlem13  43357  lcmineqlem19  43363  lcmineqlem20  43364  aks4d1p1p2  43386  aks4d1p3  43394  aks4d1p5  43396  aks4d1p6  43397  aks4d1p8  43403  aks4d1p9  43404  posbezout  43416  primrootspoweq0  43422  hashscontpow1  43437  aks6d1c2lem4  43443  sticksstones6  43467  sticksstones7  43468  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  aks6d1c6lem4  43489  aks6d1c7lem2  43497  grpods  43510  unitscyglem2  43512  unitscyglem4  43514  unitscyglem5  43515  fimgmcyc  43864  diophin  44049  irrapxlem4  44098  irrapxlem5  44099  pellexlem2  44103  pell14qrgapw  44149  pellfundgt1  44156  ltrmynn0  44221  jm2.27c  44280  jm3.1lem2  44291  fzisoeu  46589  fmuldfeq  46868  stoweidlem3  47286  stoweidlem20  47303  stoweidlem42  47325  stoweidlem51  47334  stoweidlem59  47342  stirlinglem8  47364  fourierdlem11  47401  fourierdlem41  47431  fourierdlem48  47437  fourierdlem79  47468  etransclem23  47540  etransclem28  47545  etransclem35  47552  etransclem38  47555  etransclem44  47561  etransc  47566  hoicvrrex  47839  iccpartlt  48779  lighneallem4a  48966  perfectALTVlem2  49093