Theorem znnen 4930

Description: The set of integers and the set of natural numbers are equinumerous.

Assertion

Ref	Expression
znnen	|- ZZ ~~ NN

Proof of Theorem znnen

Step	Hyp	Ref	Expression
1		zex 4571	. . . 4 |- ZZ e. V
2		elnn0z 4574	. . . . . . . 8 |- (x e. NN0 <-> (x e. ZZ /\ 0 <_ x))
3		2nn0 4548	. . . . . . . . 9 |- 2 e. NN0
4		nn0mulclt 4554	. . . . . . . . 9 |- ((2 e. NN0 /\ x e. NN0) -> (2 x. x) e. NN0)
5	3, 4	mpan 518	. . . . . . . 8 |- (x e. NN0 -> (2 x. x) e. NN0)
6	2, 5	sylbir 176	. . . . . . 7 |- ((x e. ZZ /\ 0 <_ x) -> (2 x. x) e. NN0)
7		iftrue 1780	. . . . . . . . 9 |- (0 <_ x -> if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) = (2 x. x))
8	7	eleq1d 1155	. . . . . . . 8 |- (0 <_ x -> (if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) e. NN0 <-> (2 x. x) e. NN0))
9	8	adantl 305	. . . . . . 7 |- ((x e. ZZ /\ 0 <_ x) -> (if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) e. NN0 <-> (2 x. x) e. NN0))
10	6, 9	mpbird 171	. . . . . 6 |- ((x e. ZZ /\ 0 <_ x) -> if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) e. NN0)
11		2z 4585	. . . . . . . . . . . 12 |- 2 e. ZZ
12		znegclt 4588	. . . . . . . . . . . 12 |- (2 e. ZZ -> -u2 e. ZZ)
13	11, 12	ax-mp 6	. . . . . . . . . . 11 |- -u2 e. ZZ
14		zmulclt 4596	. . . . . . . . . . 11 |- ((-u2 e. ZZ /\ x e. ZZ) -> (-u2 x. x) e. ZZ)
15	13, 14	mpan 518	. . . . . . . . . 10 |- (x e. ZZ -> (-u2 x. x) e. ZZ)
16	15	adantr 306	. . . . . . . . 9 |- ((x e. ZZ /\ -. 0 <_ x) -> (-u2 x. x) e. ZZ)
17		zret 4567	. . . . . . . . . . 11 |- (x e. ZZ -> x e. RR)
18		renegclt 4172	. . . . . . . . . . . . . 14 |- (x e. RR -> -ux e. RR)
19		2pos 4479	. . . . . . . . . . . . . . 15 |- 0 < 2
20		2re 4470	. . . . . . . . . . . . . . . 16 |- 2 e. RR
21		axmulgt0 4086	. . . . . . . . . . . . . . . 16 |- ((2 e. RR /\ -ux e. RR) -> ((0 < 2 /\ 0 < -ux) -> 0 < (2 x. -ux)))
22	20, 21	mpan 518	. . . . . . . . . . . . . . 15 |- (-ux e. RR -> ((0 < 2 /\ 0 < -ux) -> 0 < (2 x. -ux)))
23	19, 22	mpani 521	. . . . . . . . . . . . . 14 |- (-ux e. RR -> (0 < -ux -> 0 < (2 x. -ux)))
24	18, 23	syl 12	. . . . . . . . . . . . 13 |- (x e. RR -> (0 < -ux -> 0 < (2 x. -ux)))
25		ax0re 4063	. . . . . . . . . . . . . . . 16 |- 0 e. RR
26		leltt 4278	. . . . . . . . . . . . . . . 16 |- ((0 e. RR /\ x e. RR) -> (0 <_ x <-> -. x < 0))
27	25, 26	mpan 518	. . . . . . . . . . . . . . 15 |- (x e. RR -> (0 <_ x <-> -. x < 0))
28	27	bicon2d 404	. . . . . . . . . . . . . 14 |- (x e. RR -> (x < 0 <-> -. 0 <_ x))
29		lt0neg1t 4370	. . . . . . . . . . . . . 14 |- (x e. RR -> (x < 0 <-> 0 < -ux))
30	28, 29	bitr3d 408	. . . . . . . . . . . . 13 |- (x e. RR -> (-. 0 <_ x <-> 0 < -ux))
31		recnt 4097	. . . . . . . . . . . . . . 15 |- (x e. RR -> x e. CC)
32		2cn 4471	. . . . . . . . . . . . . . . 16 |- 2 e. CC
33		mulneg12t 4198	. . . . . . . . . . . . . . . 16 |- ((2 e. CC /\ x e. CC) -> (-u2 x. x) = (2 x. -ux))
34	32, 33	mpan 518	. . . . . . . . . . . . . . 15 |- (x e. CC -> (-u2 x. x) = (2 x. -ux))
35	31, 34	syl 12	. . . . . . . . . . . . . 14 |- (x e. RR -> (-u2 x. x) = (2 x. -ux))
36	35	breq2d 2072	. . . . . . . . . . . . 13 |- (x e. RR -> (0 < (-u2 x. x) <-> 0 < (2 x. -ux)))
37	24, 30, 36	3imtr4d 421	. . . . . . . . . . . 12 |- (x e. RR -> (-. 0 <_ x -> 0 < (-u2 x. x)))
38	20	renegcl 4171	. . . . . . . . . . . . . 14 |- -u2 e. RR
39		axmulrcl 4069	. . . . . . . . . . . . . 14 |- ((-u2 e. RR /\ x e. RR) -> (-u2 x. x) e. RR)
40	38, 39	mpan 518	. . . . . . . . . . . . 13 |- (x e. RR -> (-u2 x. x) e. RR)
41		ltlet 4286	. . . . . . . . . . . . . 14 |- ((0 e. RR /\ (-u2 x. x) e. RR) -> (0 < (-u2 x. x) -> 0 <_ (-u2 x. x)))
42	25, 41	mpan 518	. . . . . . . . . . . . 13 |- ((-u2 x. x) e. RR -> (0 < (-u2 x. x) -> 0 <_ (-u2 x. x)))
43	40, 42	syl 12	. . . . . . . . . . . 12 |- (x e. RR -> (0 < (-u2 x. x) -> 0 <_ (-u2 x. x)))
44	37, 43	syld 27	. . . . . . . . . . 11 |- (x e. RR -> (-. 0 <_ x -> 0 <_ (-u2 x. x)))
45	17, 44	syl 12	. . . . . . . . . 10 |- (x e. ZZ -> (-. 0 <_ x -> 0 <_ (-u2 x. x)))
46	45	imp 277	. . . . . . . . 9 |- ((x e. ZZ /\ -. 0 <_ x) -> 0 <_ (-u2 x. x))
47	16, 46	jca 236	. . . . . . . 8 |- ((x e. ZZ /\ -. 0 <_ x) -> ((-u2 x. x) e. ZZ /\ 0 <_ (-u2 x. x)))
48		elnn0z 4574	. . . . . . . . 9 |- ((-u2 x. x) e. NN0 <-> ((-u2 x. x) e. ZZ /\ 0 <_ (-u2 x. x)))
49	48	biimpr 134	. . . . . . . 8 |- (((-u2 x. x) e. ZZ /\ 0 <_ (-u2 x. x)) -> (-u2 x. x) e. NN0)
50		peano2nn0 4555	. . . . . . . 8 |- ((-u2 x. x) e. NN0 -> ((-u2 x. x) + 1) e. NN0)
51	47, 49, 50	3syl 21	. . . . . . 7 |- ((x e. ZZ /\ -. 0 <_ x) -> ((-u2 x. x) + 1) e. NN0)
52		iffalse 1781	. . . . . . . . 9 |- (-. 0 <_ x -> if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) = ((-u2 x. x) + 1))
53	52	eleq1d 1155	. . . . . . . 8 |- (-. 0 <_ x -> (if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) e. NN0 <-> ((-u2 x. x) + 1) e. NN0))
54	53	adantl 305	. . . . . . 7 |- ((x e. ZZ /\ -. 0 <_ x) -> (if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) e. NN0 <-> ((-u2 x. x) + 1) e. NN0))
55	51, 54	mpbird 171	. . . . . 6 |- ((x e. ZZ /\ -. 0 <_ x) -> if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) e. NN0)
56	10, 55	pm2.61an2 365	. . . . 5 |- (x e. ZZ -> if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) e. NN0)
57		iftrue 1780	. . . . . . . . . . 11 |- (0 <_ y -> if(0 <_ y, (2 x. y), ((-u2 x. y) + 1)) = (2 x. y))
58	7, 57	cleqan12d 1116	. . . . . . . . . 10 |- ((0 <_ x /\ 0 <_ y) -> (if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) = if(0 <_ y, (2 x. y), ((-u2 x. y) + 1)) <-> (2 x. x) = (2 x. y)))
59	20, 19	gt0ne0i 4345	. . . . . . . . . . . . 13 |- 2 =/= 0
60	59	mulcant 4208	. . . . . . . . . . . 12 |- ((2 e. CC /\ x e. CC /\ y e. CC) -> ((2 x. x) = (2 x. y) <-> x = y))
61	32, 60	mp3an1 639	. . . . . . . . . . 11 |- ((x e. CC /\ y e. CC) -> ((2 x. x) = (2 x. y) <-> x = y))
62		zcnt 4568	. . . . . . . . . . 11 |- (x e. ZZ -> x e. CC)
63		zcnt 4568	. . . . . . . . . . 11 |- (y e. ZZ -> y e. CC)
64	61, 62, 63	syl2an 349	. . . . . . . . . 10 |- ((x e. ZZ /\ y e. ZZ) -> ((2 x. x) = (2 x. y) <-> x = y))
65	58, 64	sylan9bb 418	. . . . . . . . 9 |- (((0 <_ x /\ 0 <_ y) /\ (x e. ZZ /\ y e. ZZ)) -> (if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) = if(0 <_ y, (2 x. y), ((-u2 x. y) + 1)) <-> x = y))
66	65	bicomd 399	. . . . . . . 8 |- (((0 <_ x /\ 0 <_ y) /\ (x e. ZZ /\ y e. ZZ)) -> (x = y <-> if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) = if(0 <_ y, (2 x. y), ((-u2 x. y) + 1))))
67	66	exp 291	. . . . . . 7 |- ((0 <_ x /\ 0 <_ y) -> ((x e. ZZ /\ y e. ZZ) -> (x = y <-> if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) = if(0 <_ y, (2 x. y), ((-u2 x. y) + 1)))))
68		znnenlem 4929	. . . . . . . . . 10 |- (((0 <_ x /\ -. 0 <_ y) /\ (x e. ZZ /\ y e. ZZ)) -> (y = x <-> (2 x. x) = ((-u2 x. y) + 1)))
69		eqcomb 812	. . . . . . . . . 10 |- (x = y <-> y = x)
70	68, 69	syl5bb 410	. . . . . . . . 9 |- (((0 <_ x /\ -. 0 <_ y) /\ (x e. ZZ /\ y e. ZZ)) -> (x = y <-> (2 x. x) = ((-u2 x. y) + 1)))
71		iffalse 1781	. . . . . . . . . . 11 |- (-. 0 <_ y -> if(0 <_ y, (2 x. y), ((-u2 x. y) + 1)) = ((-u2 x. y) + 1))
72	7, 71	cleqan12d 1116	. . . . . . . . . 10 |- ((0 <_ x /\ -. 0 <_ y) -> (if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) = if(0 <_ y, (2 x. y), ((-u2 x. y) + 1)) <-> (2 x. x) = ((-u2 x. y) + 1)))
73	72	adantr 306	. . . . . . . . 9 |- (((0 <_ x /\ -. 0 <_ y) /\ (x e. ZZ /\ y e. ZZ)) -> (if(0 <_ x, (2 x. x), ((-u2 x. x) + 1)) = if(0 <_ y, (2 x. y), ((-u2 x. y) + 1)) <-> (2 x. x) = ((-u2 x. y)