Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem znnen 7445

Description: The set of integers and the set of natural numbers are equinumerous. Exercise 1 of [Gleason] p. 140.

Assertion

Ref	Expression
znnen

---

Proof of Theorem znnen

Step	Hyp	Ref	Expression
1		zex 6091	. . . 4
2		elnn0z 6094	. . . . . . . 8
3		2nn0 6062	. . . . . . . . 9
4		nn0mulclt 6070	. . . . . . . . 9
5	3, 4	mpan 693	. . . . . . . 8
6	2, 5	sylbir 201	. . . . . . 7
7		iftrue 2356	. . . . . . . . 9
8	7	eleq1d 1532	. . . . . . . 8
9	8	adantl 388	. . . . . . 7
10	6, 9	mpbird 196	. . . . . 6
11		2z 6107	. . . . . . . . . . . 12
12		znegclt 6110	. . . . . . . . . . . 12
13	11, 12	ax-mp 7	. . . . . . . . . . 11
14		zmulclt 6127	. . . . . . . . . . 11
15	13, 14	mpan 693	. . . . . . . . . 10
16	15	adantr 389	. . . . . . . . 9
17		zret 6086	. . . . . . . . . . 11
18		renegclt 5409	. . . . . . . . . . . . . 14
19		2pos 5936	. . . . . . . . . . . . . . 15
20		2re 5926	. . . . . . . . . . . . . . . 16
21		axmulgt0 5478	. . . . . . . . . . . . . . . 16
22	20, 21	mpan 693	. . . . . . . . . . . . . . 15
23	19, 22	mpani 696	. . . . . . . . . . . . . 14
24	18, 23	syl 10	. . . . . . . . . . . . 13
25		0re 5412	. . . . . . . . . . . . . . 15
26		ltnlet 5483	. . . . . . . . . . . . . . 15
27	25, 26	mpan2 694	. . . . . . . . . . . . . 14
28		lt0neg1t 5641	. . . . . . . . . . . . . 14
29	27, 28	bitr3d 528	. . . . . . . . . . . . 13
30		recnt 5285	. . . . . . . . . . . . . . 15
31		2cn 5927	. . . . . . . . . . . . . . . 16
32		mulneg12t 5425	. . . . . . . . . . . . . . . 16
33	31, 32	mpan 693	. . . . . . . . . . . . . . 15
34	30, 33	syl 10	. . . . . . . . . . . . . 14
35	34	breq2d 2620	. . . . . . . . . . . . 13
36	24, 29, 35	3imtr4d 541	. . . . . . . . . . . 12
37	20	renegcl 5388	. . . . . . . . . . . . . 14
38		axmulrcl 5246	. . . . . . . . . . . . . 14
39	37, 38	mpan 693	. . . . . . . . . . . . 13
40		ltlet 5493	. . . . . . . . . . . . . 14
41	25, 40	mpan 693	. . . . . . . . . . . . 13
42	39, 41	syl 10	. . . . . . . . . . . 12
43	36, 42	syld 27	. . . . . . . . . . 11
44	17, 43	syl 10	. . . . . . . . . 10
45	44	imp 350	. . . . . . . . 9
46	16, 45	jca 288	. . . . . . . 8
47		elnn0z 6094	. . . . . . . . 9
48	47	biimpr 152	. . . . . . . 8
49		peano2nn0 6071	. . . . . . . 8
50	46, 48, 49	3syl 20	. . . . . . 7
51		iffalse 2357	. . . . . . . . 9
52	51	eleq1d 1532	. . . . . . . 8
53	52	adantl 388	. . . . . . 7
54	50, 53	mpbird 196	. . . . . 6
55	10, 54	pm2.61dan 476	. . . . 5
56		iftrue 2356	. . . . . . . . . . 11
57	7, 56	eqeqan12d 1482	. . . . . . . . . 10
58		2ne0 5937	. . . . . . . . . . . . 13
59	58	mulcant2 5660	. . . . . . . . . . . 12
60	31, 59	mp3an1 900	. . . . . . . . . . 11
61		zcnt 6087	. . . . . . . . . . 11
62		zcnt 6087	. . . . . . . . . . 11
63	60, 61, 62	syl2an 454	. . . . . . . . . 10
64	57, 63	sylan9bb 538	. . . . . . . . 9
65	64	bicomd 519	. . . . . . . 8
66	65	ex 373	. . . . . . 7
67		znnenlem 7443	. . . . . . . . 9
68		iffalse 2357	. . . . . . . . . . 11
69	7, 68	eqeqan12d 1482	. . . . . . . . . 10
70	69	adantr 389	. . . . . . . . 9
71	67, 70	bitr4d 529	. . . . . .