elznn0 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem elznn0 6149

Description: Integer property expressed in terms of nonnegative integers.

**Assertion**
Ref	Expression
elznn0	$/\$ $\/$

**Proof of Theorem elznn0**
Step	Hyp	Ref	Expression
1		elz 6137	. 2 $/\$ $\/$ $\/$
2		elnn0 6101	. . . . . 6 $\/$
3	2	a1i 8	. . . . 5 $\/$
4		recnt 5313	. . . . . . . . 9
5		0cn 5328	. . . . . . . . . 10
6		negcon1t 5410	. . . . . . . . . 10 $/\$
7	5, 6	mpan2 696	. . . . . . . . 9
8	4, 7	syl 10	. . . . . . . 8
9		neg0 5415	. . . . . . . . . 10
10	9	eqeq1i 1482	. . . . . . . . 9
11		eqcom 1477	. . . . . . . . 9
12	10, 11	bitr 173	. . . . . . . 8
13	8, 12	syl6bb 536	. . . . . . 7
14	13	orbi2d 614	. . . . . 6 $\/$ $\/$
15		elnn0 6101	. . . . . 6 $\/$
16	14, 15	syl5bb 532	. . . . 5 $\/$
17	3, 16	orbi12d 627	. . . 4 $\/$ $\/$ $\/$ $\/$
18		3orass 778	. . . . 5 $\/$ $\/$ $\/$ $\/$
19		orcom 246	. . . . 5 $\/$ $\/$ $\/$ $\/$
20		orordir 267	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
21	18, 19, 20	3bitrr 178	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
22	17, 21	syl6rbb 537	. . 3 $\/$ $\/$ $\/$
23	22	pm5.32i 645	. 2 $/\$ $\/$ $\/$ $/\$ $\/$
24	1, 23	bitr 173	1 $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

wb 146 $\/$ wo 222 $/\$ wa 223 $\/$ w3o 774

wceq 956

wcel 958

cc 5232

cr 5233

cc0 5234

cneg 5293

cn 5296

cn0 5297

cz 5298

This theorem is referenced by: zaddclt 6165 zmulclt 6180 zltp1let 6181 sinperlem2 8687

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-9 965 ax-10 966 ax-11 967 ax-12 968 ax-13 969 ax-14 970 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-rep 2693 ax-sep 2703 ax-nul 2710 ax-pow 2742 ax-pr 2779 ax-un 2866 ax-inf2 4625

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 776 df-3an 777 df-ex 981 df-sb 1172 df-eu 1382 df-mo 1383 df-clab 1464 df-cleq 1469 df-clel 1472 df-ne 1587 df-ral 1649 df-rex 1650 df-reu 1651 df-rab 1652 df-v 1812 df-sbc 1942 df-csb 2002 df-dif 2049 df-un 2050 df-in 2051 df-ss 2053 df-pss 2055 df-nul 2281 df-if 2362 df-pw 2402 df-sn 2412 df-pr 2413 df-tp 2415 df-op 2416 df-uni 2504 df-int 2534 df-iun 2568 df-br 2620 df-opab 2667 df-tr 2681 df-eprel 2832 df-id 2835 df-po 2840 df-so 2850 df-fr 2917 df-we 2934 df-ord 2951 df-on 2952 df-lim 2953 df-suc 2954 df-om 3132 df-xp 3184 df-rel 3185 df-cnv 3186 df-co 3187 df-dm 3188 df-rn 3189 df-res 3190 df-ima 3191 df-fun 3192 df-fn 3193 df-f 3194 df-fv 3198 df-rdg 3932 df-opr 3965 df-oprab 3966 df-1st 4079 df-2nd 4080 df-1o 4133 df-oadd 4135 df-omul 4136 df-er 4261 df-ec 4263 df-qs 4266 df-ni 5000 df-pli 5001 df-mi 5002 df-lti 5003 df-plpq 5035 df-mpq 5036 df-enq 5037 df-nq 5038 df-plq 5039 df-mq 5040 df-rq 5041 df-ltq 5042 df-1q 5043 df-np 5086 df-1p 5087 df-plp 5088 df-mp 5089 df-ltp 5090 df-plpr 5164 df-mpr 5165 df-enr 5166 df-nr 5167 df-plr 5168 df-mr 5169 df-0r 5171 df-1r 5172 df-m1r 5173 df-c 5240 df-0 5241 df-1 5242 df-i 5243 df-r 5244 df-plus 5245 df-mul 5246 df-sub 5356 df-neg 5358 df-n0 6100 df-z 6136