![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nngt0 | GIF version |
Description: A positive integer is positive. (Contributed by NM, 26-Sep-1999.) |
Ref | Expression |
---|---|
nngt0 | ⊢ (𝐴 ∈ ℕ → 0 < 𝐴) |
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 < 𝐴) |
Colors of variables: wff set class |
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 |
Copyright terms: Public domain | W3C validator |