elznn0nn - Intuitionistic Logic Explorer

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

Theorem elznn0nn 9492

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 9480	. 2 $/\$ $\/$ $\/$
2		andi 825	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
3		df-3or 1005	. . . 4 $\/$ $\/$ $\/$ $\/$
4	3	anbi2i 457	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
5		nn0re 9410	. . . . . 6
6	5	pm4.71ri 392	. . . . 5 $/\$
7		elnn0 9403	. . . . . . 7 $\/$
8		orcom 735	. . . . . . 7 $\/$ $\/$
9	7, 8	bitri 184	. . . . . 6 $\/$
10	9	anbi2i 457	. . . . 5 $/\$ $/\$ $\/$
11	6, 10	bitri 184	. . . 4 $/\$ $\/$
12	11	orbi1i 770	. . 3 $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
13	2, 4, 12	3bitr4i 212	. 2 $/\$ $\/$ $\/$ $\/$ $/\$
14	1, 13	bitri 184	1 $\/$ $/\$

Colors of variables: wff set class

Syntax hints: $/\$ wa 104

wb 105 $\/$ wo 715 $\/$ w3o 1003

wceq 1397

wcel 2202

cr 8030

cc0 8031

cneg 8350

cn 9142

cn0 9401

cz 9478

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-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-ext 2213 ax-sep 4207 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-i2m1 8136 ax-rnegex 8140

This theorem depends on definitions: df-bi 117 df-3or 1005 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ral 2515 df-rex 2516 df-rab 2519 df-v 2804 df-un 3204 df-in 3206 df-ss 3213 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-br 4089 df-iota 5286 df-fv 5334 df-ov 6020 df-neg 8352 df-inn 9143 df-n0 9402 df-z 9479

This theorem is referenced by: peano2z 9514 zindd 9597 expcl2lemap 10812 mulexpzap 10840 expaddzap 10844 expmulzap 10846 absexpzap 11640 bitsfzo 12515 pcid 12896 mulgsubcl 13722 mulgneg 13726 ghmmulg 13842