![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nngt0d | GIF version |
Description: A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnge1d.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ) |
Ref | Expression |
---|---|
nngt0d | ⊢ (𝜑 → 0 < 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnge1d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
2 | nngt0 8930 | . 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 0 < 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 class class class wbr 4000 0cc0 7799 < clt 7979 ℕcn 8905 |
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 4118 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-cnex 7890 ax-resscn 7891 ax-1re 7893 ax-addrcl 7896 ax-0lt1 7905 ax-0id 7907 ax-rnegex 7908 ax-pre-ltirr 7911 ax-pre-ltwlin 7912 ax-pre-lttrn 7913 ax-pre-ltadd 7915 |
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 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-br 4001 df-opab 4062 df-xp 4629 df-cnv 4631 df-iota 5174 df-fv 5220 df-ov 5872 df-pnf 7981 df-mnf 7982 df-xr 7983 df-ltxr 7984 df-le 7985 df-inn 8906 |
This theorem is referenced by: flqdiv 10304 modqmulnn 10325 modifeq2int 10369 modaddmodup 10370 modaddmodlo 10371 modsumfzodifsn 10379 addmodlteq 10381 facubnd 10706 resqrexlemdecn 11002 modfsummodlemstep 11446 divcnv 11486 cvgratnnlemabsle 11516 fprodmodd 11630 efcllemp 11647 ege2le3 11660 eftlub 11679 eflegeo 11690 eirraplem 11765 dvdslelemd 11829 dvdsmod 11848 mulmoddvds 11849 divalgmod 11912 bezoutlemnewy 11977 bezoutlemstep 11978 sqgcd 12010 eucalglt 12037 qredeu 12077 prmind2 12100 nprm 12103 sqrt2irraplemnn 12159 divdenle 12177 qnumgt0 12178 hashdvds 12201 crth 12204 phimullem 12205 eulerthlema 12210 fermltl 12214 prmdiv 12215 prmdiveq 12216 odzdvds 12225 powm2modprm 12232 modprm0 12234 nnnn0modprm0 12235 pythagtriplem11 12254 pythagtriplem13 12256 pythagtriplem19 12262 pcadd 12319 pcfaclem 12327 qexpz 12330 pockthlem 12334 pockthg 12335 4sqlem5 12360 4sqlem6 12361 4sqlem10 12365 lgsvalmod 14084 lgsmod 14091 lgsdirprm 14099 2sqlem8 14123 |
Copyright terms: Public domain | W3C validator |