Theorem nngt0 8942

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 8924	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 8940	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 8082	. . 3 ⊢ 0 < 1
4		0re 7956	. . . 4 ⊢ 0 ∈ ℝ
5		1re 7955	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 8045	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
7	4, 5, 6	mp3an12 1327	. . 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 2148   class class class wbr 4003  ℝcr 7809  0cc0 7810  1c1 7811   < clt 7990   ≤ cle 7991  ℕcn 8917

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907  ax-0lt1 7916  ax-0id 7918  ax-rnegex 7919  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-ltadd 7926

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4004  df-opab 4065  df-xp 4632  df-cnv 4634  df-iota 5178  df-fv 5224  df-ov 5877  df-pnf 7992  df-mnf 7993  df-xr 7994  df-ltxr 7995  df-le 7996  df-inn 8918

This theorem is referenced by:  nnap0  8946  nngt0i  8947  nn2ge  8950  nn1gt1  8951  nnsub  8956  nngt0d  8961  nnrecl  9172  nn0ge0  9199  0mnnnnn0  9206  elnnnn0b  9218  elnnz  9261  elnn0z  9264  ztri3or0  9293  nnm1ge0  9337  gtndiv  9346  elpq  9646  elpqb  9647  nnrp  9661  nnledivrp  9764  fzo1fzo0n0  10180  ubmelfzo  10197  adddivflid  10289  flltdivnn0lt  10301  intfracq  10317  zmodcl  10341  zmodfz  10343  zmodid2  10349  m1modnnsub1  10367  expnnval  10520  nnlesq  10620  facdiv  10713  faclbnd  10716  bc0k  10731  dvdsval3  11793  nndivdvds  11798  moddvds  11801  evennn2n  11882  nnoddm1d2  11909  divalglemnn  11917  ndvdssub  11929  ndvdsadd  11930  modgcd  11986  sqgcd  12024  lcmgcdlem  12071  qredeu  12091  divdenle  12191  hashgcdlem  12232  oddprm  12253  pythagtriplem12  12269  pythagtriplem13  12270  pythagtriplem14  12271  pythagtriplem16  12273  pythagtriplem19  12276  pc2dvds  12323  fldivp1  12340  znnen  12393  exmidunben  12421  mulgnn  12943  mulgnegnn  12947  mulgmodid  12975  lgsval4a  14316  lgsne0  14332