Theorem nngt0 8340

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 8322	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 8338	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 7512	. . 3 ⊢ 0 < 1
4		0re 7390	. . . 4 ⊢ 0 ∈ ℝ
5		1re 7389	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 7476	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
7	4, 5, 6	mp3an12 1259	. . 3 ⊢ (𝐴 ∈ ℝ → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
8	3, 7	mpani 421	. 2 ⊢ (𝐴 ∈ ℝ → (1 ≤ 𝐴 → 0 < 𝐴))
9	1, 2, 8	sylc 61	1 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1434   class class class wbr 3811  ℝcr 7251  0cc0 7252  1c1 7253   < clt 7424   ≤ cle 7425  ℕcn 8315

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 3999  ax-un 4223  ax-setind 4315  ax-cnex 7338  ax-resscn 7339  ax-1re 7341  ax-addrcl 7344  ax-0lt1 7353  ax-0id 7355  ax-rnegex 7356  ax-pre-ltirr 7359  ax-pre-ltwlin 7360  ax-pre-lttrn 7361  ax-pre-ltadd 7363

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-rab 2362  df-v 2614  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-br 3812  df-opab 3866  df-xp 4406  df-cnv 4408  df-iota 4933  df-fv 4976  df-ov 5593  df-pnf 7426  df-mnf 7427  df-xr 7428  df-ltxr 7429  df-le 7430  df-inn 8316

This theorem is referenced by:  nnap0  8344  nngt0i  8345  nn2ge  8347  nn1gt1  8348  nnsub  8353  nngt0d  8358  nnrecl  8562  nn0ge0  8589  0mnnnnn0  8596  elnnnn0b  8608  elnnz  8655  elnn0z  8658  ztri3or0  8687  nnm1ge0  8727  gtndiv  8736  nnrp  9037  nnledivrp  9131  fzo1fzo0n0  9482  ubmelfzo  9499  adddivflid  9587  flltdivnn0lt  9599  intfracq  9615  zmodcl  9639  zmodfz  9641  zmodid2  9647  m1modnnsub1  9665  expinnval  9794  nnlesq  9893  facdiv  9980  faclbnd  9983  bc0k  9998  dvdsval3  10579  nndivdvds  10581  moddvds  10584  evennn2n  10662  nnoddm1d2  10689  divalglemnn  10697  ndvdssub  10709  ndvdsadd  10710  modgcd  10761  sqgcd  10797  lcmgcdlem  10838  qredeu  10858  divdenle  10954  hashgcdlem  10982  znnen  10990