nn0p1gt0 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > nn0p1gt0		Unicode version

Theorem nn0p1gt0 9527

Description: A nonnegative integer increased by 1 is greater than 0. (Contributed by Alexander van der Vekens, 3-Oct-2018.)

**Assertion**
Ref	Expression
nn0p1gt0

**Proof of Theorem nn0p1gt0**
Step	Hyp	Ref	Expression
1		nn0re 9507	. 2
2		1red 8291	. 2
3		nn0ge0 9523	. 2
4		0lt1 8402	. . 3
5	4	a1i 9	. 2
6	1, 2, 3, 5	addgegt0d 8795	1

Colors of variables: wff set class

Syntax hints:

wi 4

wcel 2205 class class class wbr 4111 (class class class)co 6052

cc0 8129

c1 8130

caddc 8132

clt 8310

cn0 9498

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-sep 4230 ax-pow 4289 ax-pr 4324 ax-un 4556 ax-setind 4661 ax-cnex 8220 ax-resscn 8221 ax-1cn 8222 ax-1re 8223 ax-icn 8224 ax-addcl 8225 ax-addrcl 8226 ax-mulcl 8227 ax-addcom 8229 ax-addass 8231 ax-i2m1 8234 ax-0lt1 8235 ax-0id 8237 ax-rnegex 8238 ax-pre-ltirr 8241 ax-pre-ltwlin 8242 ax-pre-lttrn 8243 ax-pre-ltadd 8245

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-rab 2531 df-v 2817 df-dif 3215 df-un 3217 df-in 3219 df-ss 3226 df-pw 3673 df-sn 3697 df-pr 3698 df-op 3700 df-uni 3917 df-int 3952 df-br 4112 df-opab 4174 df-xp 4757 df-cnv 4759 df-iota 5314 df-fv 5362 df-ov 6055 df-pnf 8312 df-mnf 8313 df-xr 8314 df-ltxr 8315 df-le 8316 df-inn 9240 df-n0 9499

This theorem is referenced by: ubmelm1fzo 10575 nn0ltexp2 11075 ccats1pfxeq 11410 ennnfonelemp1 13174