Theorem nngt0 9168

Description: A positive integer is positive. (Contributed by NM, 26-Sep-1999.)

Assertion

Ref	Expression
nngt0	⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

Proof of Theorem nngt0

Step	Hyp	Ref	Expression
1		nnre 9150	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 9166	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 8306	. . 3 ⊢ 0 < 1
4		0re 8179	. . . 4 ⊢ 0 ∈ ℝ
5		1re 8178	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 8269	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
7	4, 5, 6	mp3an12 1363	. . 3 ⊢ (𝐴 ∈ ℝ → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
8	3, 7	mpani 430	. 2 ⊢ (𝐴 ∈ ℝ → (1 ≤ 𝐴 → 0 < 𝐴))
9	1, 2, 8	sylc 62	1 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202   class class class wbr 4088  ℝcr 8031  0cc0 8032  1c1 8033   < clt 8214   ≤ cle 8215  ℕcn 9143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-xp 4731  df-cnv 4733  df-iota 5286  df-fv 5334  df-ov 6021  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-inn 9144

This theorem is referenced by:  nnap0  9172  nngt0i  9173  nn2ge  9176  nn1gt1  9177  nnsub  9182  nngt0d  9187  nnrecl  9400  nn0ge0  9427  0mnnnnn0  9434  elnnnn0b  9446  elnnz  9489  elnn0z  9492  ztri3or0  9521  nnnle0  9528  nnm1ge0  9566  gtndiv  9575  elpq  9883  elpqb  9884  nnrp  9898  nnledivrp  10001  fzo1fzo0n0  10423  ubmelfzo  10446  adddivflid  10553  flltdivnn0lt  10565  intfracq  10583  zmodcl  10607  zmodfz  10609  zmodid2  10615  m1modnnsub1  10633  expnnval  10805  nnlesq  10906  facdiv  11001  faclbnd  11004  bc0k  11019  ccatval21sw  11186  ccats1pfxeqrex  11300  dvdsval3  12357  nndivdvds  12362  moddvds  12365  evennn2n  12449  nnoddm1d2  12476  divalglemnn  12484  ndvdssub  12496  ndvdsadd  12497  modgcd  12567  sqgcd  12605  lcmgcdlem  12654  qredeu  12674  divdenle  12774  hashgcdlem  12815  oddprm  12837  pythagtriplem12  12853  pythagtriplem13  12854  pythagtriplem14  12855  pythagtriplem16  12857  pythagtriplem19  12860  pc2dvds  12908  fldivp1  12926  modsubi  12997  znnen  13024  exmidunben  13052  mulgnn  13718  mulgnegnn  13724  mulgmodid  13753  znf1o  14671  znidomb  14678  lgsval4a  15757  lgsne0  15773  gausslemma2dlem1a  15793  clwwlknonccat  16290