Theorem nngt0 9143

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 9125	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nnge1 9141	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3		0lt1 8281	. . 3 ⊢ 0 < 1
4		0re 8154	. . . 4 ⊢ 0 ∈ ℝ
5		1re 8153	. . . 4 ⊢ 1 ∈ ℝ
6		ltletr 8244	. . . 4 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 < 1 ∧ 1 ≤ 𝐴) → 0 < 𝐴))
7	4, 5, 6	mp3an12 1361	. . 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 2200   class class class wbr 4083  ℝcr 8006  0cc0 8007  1c1 8008   < clt 8189   ≤ cle 8190  ℕcn 9118

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8098  ax-resscn 8099  ax-1re 8101  ax-addrcl 8104  ax-0lt1 8113  ax-0id 8115  ax-rnegex 8116  ax-pre-ltirr 8119  ax-pre-ltwlin 8120  ax-pre-lttrn 8121  ax-pre-ltadd 8123

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-xp 4725  df-cnv 4727  df-iota 5278  df-fv 5326  df-ov 6010  df-pnf 8191  df-mnf 8192  df-xr 8193  df-ltxr 8194  df-le 8195  df-inn 9119

This theorem is referenced by:  nnap0  9147  nngt0i  9148  nn2ge  9151  nn1gt1  9152  nnsub  9157  nngt0d  9162  nnrecl  9375  nn0ge0  9402  0mnnnnn0  9409  elnnnn0b  9421  elnnz  9464  elnn0z  9467  ztri3or0  9496  nnnle0  9503  nnm1ge0  9541  gtndiv  9550  elpq  9852  elpqb  9853  nnrp  9867  nnledivrp  9970  fzo1fzo0n0  10391  ubmelfzo  10414  adddivflid  10520  flltdivnn0lt  10532  intfracq  10550  zmodcl  10574  zmodfz  10576  zmodid2  10582  m1modnnsub1  10600  expnnval  10772  nnlesq  10873  facdiv  10968  faclbnd  10971  bc0k  10986  ccatval21sw  11148  ccats1pfxeqrex  11255  dvdsval3  12310  nndivdvds  12315  moddvds  12318  evennn2n  12402  nnoddm1d2  12429  divalglemnn  12437  ndvdssub  12449  ndvdsadd  12450  modgcd  12520  sqgcd  12558  lcmgcdlem  12607  qredeu  12627  divdenle  12727  hashgcdlem  12768  oddprm  12790  pythagtriplem12  12806  pythagtriplem13  12807  pythagtriplem14  12808  pythagtriplem16  12810  pythagtriplem19  12813  pc2dvds  12861  fldivp1  12879  modsubi  12950  znnen  12977  exmidunben  13005  mulgnn  13671  mulgnegnn  13677  mulgmodid  13706  znf1o  14623  znidomb  14630  lgsval4a  15709  lgsne0  15725  gausslemma2dlem1a  15745