elznn0nn - Intuitionistic Logic Explorer

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

Theorem elznn0nn 8762

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 8750	. 2 $/\$ $\/$ $\/$
2		andi 767	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
3		df-3or 925	. . . 4 $\/$ $\/$ $\/$ $\/$
4	3	anbi2i 445	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
5		nn0re 8680	. . . . . 6
6	5	pm4.71ri 384	. . . . 5 $/\$
7		elnn0 8673	. . . . . . 7 $\/$
8		orcom 682	. . . . . . 7 $\/$ $\/$
9	7, 8	bitri 182	. . . . . 6 $\/$
10	9	anbi2i 445	. . . . 5 $/\$ $/\$ $\/$
11	6, 10	bitri 182	. . . 4 $/\$ $\/$
12	11	orbi1i 715	. . 3 $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
13	2, 4, 12	3bitr4i 210	. 2 $/\$ $\/$ $\/$ $\/$ $/\$
14	1, 13	bitri 182	1 $\/$ $/\$

Colors of variables: wff set class

Syntax hints: $/\$ wa 102

wb 103 $\/$ wo 664 $\/$ w3o 923

wceq 1289

wcel 1438

cr 7347

cc0 7348

cneg 7652

cn 8420

cn0 8671

cz 8748

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-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-sep 3957 ax-cnex 7434 ax-resscn 7435 ax-1cn 7436 ax-1re 7437 ax-icn 7438 ax-addcl 7439 ax-addrcl 7440 ax-mulcl 7441 ax-i2m1 7448 ax-rnegex 7452

This theorem depends on definitions: df-bi 115 df-3or 925 df-3an 926 df-tru 1292 df-nf 1395 df-sb 1693 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ral 2364 df-rex 2365 df-rab 2368 df-v 2621 df-un 3003 df-in 3005 df-ss 3012 df-sn 3452 df-pr 3453 df-op 3455 df-uni 3654 df-int 3689 df-br 3846 df-iota 4980 df-fv 5023 df-ov 5655 df-neg 7654 df-inn 8421 df-n0 8672 df-z 8749

This theorem is referenced by: peano2z 8784 zindd 8862 expcl2lemap 9963 mulexpzap 9991 expaddzap 9995 expmulzap 9997 absexpzap 10509