elznn0nn - Intuitionistic Logic Explorer

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

Theorem elznn0nn 8259

Description: Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.)

**Assertion**
Ref	Expression
elznn0nn	$\/$ $/\$

**Proof of Theorem elznn0nn**
Step	Hyp	Ref	Expression
1		elz 8247	. 2 $/\$ $\/$ $\/$
2		andi 731	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
3		df-3or 886	. . . 4 $\/$ $\/$ $\/$ $\/$
4	3	anbi2i 430	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
5		nn0re 8190	. . . . . 6
6	5	pm4.71ri 372	. . . . 5 $/\$
7		elnn0 8183	. . . . . . 7 $\/$
8		orcom 647	. . . . . . 7 $\/$ $\/$
9	7, 8	bitri 173	. . . . . 6 $\/$
10	9	anbi2i 430	. . . . 5 $/\$ $/\$ $\/$
11	6, 10	bitri 173	. . . 4 $/\$ $\/$
12	11	orbi1i 680	. . 3 $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
13	2, 4, 12	3bitr4i 201	. 2 $/\$ $\/$ $\/$ $\/$ $/\$
14	1, 13	bitri 173	1 $\/$ $/\$

Colors of variables: wff set class

Syntax hints: $/\$ wa 97

wb 98 $\/$ wo 629 $\/$ w3o 884

wceq 1243

wcel 1393

cr 6888

cc0 6889

cneg 7183

cn 7914

cn0 8181

cz 8245

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-sep 3875 ax-cnex 6975 ax-resscn 6976 ax-1cn 6977 ax-1re 6978 ax-icn 6979 ax-addcl 6980 ax-addrcl 6981 ax-mulcl 6982 ax-i2m1 6989 ax-rnegex 6993

This theorem depends on definitions: df-bi 110 df-3or 886 df-3an 887 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ral 2311 df-rex 2312 df-rab 2315 df-v 2559 df-un 2922 df-in 2924 df-ss 2931 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-int 3616 df-br 3765 df-iota 4867 df-fv 4910 df-ov 5515 df-neg 7185 df-inn 7915 df-n0 8182 df-z 8246

This theorem is referenced by: peano2z 8281 zindd 8356 expcl2lemap 9267 mulexpzap 9295 expaddzap 9299 expmulzap 9301 absexpzap 9676