Theorem dfuz 6158

Description: An expression for the upper integers that start at N that is analogous to df-n 5881 for natural numbers. Warning: The HTML proof page is 1/2 megabyte in size.

Hypothesis

Ref	Expression
dfuz.1	|- N e. ZZ

Assertion

Ref	Expression
dfuz	|- {z e. ZZ | N <_ z} = |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)}

Distinct variable group:   x,y,z,N

Proof of Theorem dfuz

Step	Hyp	Ref	Expression
1		breq2 2618	. . . . 5 |- (z = m -> (N <_ z <-> N <_ m))
2	1	elrab 1901	. . . 4 |- (m e. {z e. ZZ | N <_ z} <-> (m e. ZZ /\ N <_ m))
3	2	pm3.26bi 322	. . 3 |- (m e. {z e. ZZ | N <_ z} -> m e. ZZ)
4		zex 6099	. . . . 5 |- ZZ e. V
5		eleq2 1532	. . . . . . 7 |- (x = ZZ -> (N e. x <-> N e. ZZ))
6		eleq2 1532	. . . . . . . 8 |- (x = ZZ -> ((y + 1) e. x <-> (y + 1) e. ZZ))
7	6	raleqd 1788	. . . . . . 7 |- (x = ZZ -> (A.y e. x (y + 1) e. x <-> A.y e. ZZ (y + 1) e. ZZ))
8	5, 7	anbi12d 627	. . . . . 6 |- (x = ZZ -> ((N e. x /\ A.y e. x (y + 1) e. x) <-> (N e. ZZ /\ A.y e. ZZ (y + 1) e. ZZ)))
9		dfuz.1	. . . . . . 7 |- N e. ZZ
10		peano2z 6121	. . . . . . . 8 |- (y e. ZZ -> (y + 1) e. ZZ)
11	10	rgen 1695	. . . . . . 7 |- A.y e. ZZ (y + 1) e. ZZ
12	9, 11	pm3.2i 285	. . . . . 6 |- (N e. ZZ /\ A.y e. ZZ (y + 1) e. ZZ)
13	8, 12	intmin3 2553	. . . . 5 |- (ZZ e. V -> |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)} (_ ZZ)
14	4, 13	ax-mp 7	. . . 4 |- |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)} (_ ZZ
15	14	sseli 2061	. . 3 |- (m e. |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)} -> m e. ZZ)
16		ax-17 969	. . . . . 6 |- (u e. m -> A.z u e. m)
17		ax-17 969	. . . . . 6 |- (u e. (m + (1 - N)) -> A.z u e. (m + (1 - N)))
18		1z 6114	. . . . . . . 8 |- 1 e. ZZ
19		zsubclt 6123	. . . . . . . 8 |- ((1 e. ZZ /\ N e. ZZ) -> (1 - N) e. ZZ)
20	18, 9, 19	mp2an 696	. . . . . . 7 |- (1 - N) e. ZZ
21		zaddclt 6120	. . . . . . 7 |- ((z e. ZZ /\ (1 - N) e. ZZ) -> (z + (1 - N)) e. ZZ)
22	20, 21	mpan2 695	. . . . . 6 |- (z e. ZZ -> (z + (1 - N)) e. ZZ)
23		breq2 2618	. . . . . 6 |- (v = (z + (1 - N)) -> (1 <_ v <-> 1 <_ (z + (1 - N))))
24		opreq1 3959	. . . . . 6 |- (z = m -> (z + (1 - N)) = (m + (1 - N)))
25	16, 17, 22, 23, 24	rabxfr 2897	. . . . 5 |- (m e. ZZ -> ((m + (1 - N)) e. {v e. ZZ | 1 <_ v} <-> m e. {z e. ZZ | 1 <_ (z + (1 - N))}))
26		zret 6094	. . . . . . . . 9 |- (z e. ZZ -> z e. RR)
27	9	zre 6096	. . . . . . . . . 10 |- N e. RR
28		1re 5415	. . . . . . . . . . 11 |- 1 e. RR
29	28, 27	resubcl 5419	. . . . . . . . . 10 |- (1 - N) e. RR
30		leadd1t 5607	. . . . . . . . . 10 |- ((N e. RR /\ z e. RR /\ (1 - N) e. RR) -> (N <_ z <-> (N + (1 - N)) <_ (z + (1 - N))))
31	27, 29, 30	mp3an13 905	. . . . . . . . 9 |- (z e. RR -> (N <_ z <-> (N + (1 - N)) <_ (z + (1 - N))))
32	26, 31	syl 10	. . . . . . . 8 |- (z e. ZZ -> (N <_ z <-> (N + (1 - N)) <_ (z + (1 - N))))
33	27	recn 5294	. . . . . . . . . 10 |- N e. CC
34		ax1cn 5249	. . . . . . . . . 10 |- 1 e. CC
35	33, 34	pncan3 5358	. . . . . . . . 9 |- (N + (1 - N)) = 1
36	35	breq1i 2621	. . . . . . . 8 |- ((N + (1 - N)) <_ (z + (1 - N)) <-> 1 <_ (z + (1 - N)))
37	32, 36	syl6bb 535	. . . . . . 7 |- (z e. ZZ -> (N <_ z <-> 1 <_ (z + (1 - N))))
38	37	rabbii 1801	. . . . . 6 |- {z e. ZZ | N <_ z} = {z e. ZZ | 1 <_ (z + (1 - N))}
39	38	eleq2i 1535	. . . . 5 |- (m e. {z e. ZZ | N <_ z} <-> m e. {z e. ZZ | 1 <_ (z + (1 - N))})
40	25, 39	syl6bbr 537	. . . 4 |- (m e. ZZ -> ((m + (1 - N)) e. {v e. ZZ | 1 <_ v} <-> m e. {z e. ZZ | N <_ z}))
41		opreq1 3959	. . . . . . . . . . . . . . . . 17 |- (v = (y + (1 - N)) -> (v + 1) = ((y + (1 - N)) + 1))
42	41	eleq1d 1537	. . . . . . . . . . . . . . . 16 |- (v = (y + (1 - N)) -> ((v + 1) e. w <-> ((y + (1 - N)) + 1) e. w))
43	42	rcla4v 1869	. . . . . . . . . . . . . . 15 |- ((y + (1 - N)) e. w -> (A.v e. w (v + 1) e. w -> ((y + (1 - N)) + 1) e. w))
44		recnt 5293	. . . . . . . . . . . . . . . . . . 19 |- (y e. RR -> y e. CC)
45	29	recn 5294	. . . . . . . . . . . . . . . . . . . 20 |- (1 - N) e. CC
46		add23t 5317	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. CC /\ (1 - N) e. CC /\ 1 e. CC) -> ((y + (1 - N)) + 1) = ((y + 1) + (1 - N)))
47	45, 34, 46	mp3an23 906	. . . . . . . . . . . . . . . . . . 19 |- (y e. CC -> ((y + (1 - N)) + 1) = ((y + 1) + (1 - N)))
48	44, 47	syl 10	. . . . . . . . . . . . . . . . . 18 |- (y e. RR -> ((y + (1 - N)) + 1) = ((y + 1) + (1 - N)))
49	48	eleq1d 1537	. . . . . . . . . . . . . . . . 17 |- (y e. RR -> (((y + (1 - N)) + 1) e. w <-> ((y + 1) + (1 - N)) e. w))
50	49	biimpd 153	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (((y + (1 - N)) + 1) e. w -> ((y + 1) + (1 - N)) e. w))
51		peano2re 5416	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (y + 1) e. RR)
52	50, 51	jctild 600	. . . . . . . . . . . . . . 15 |- (y e. RR -> (((y + (1 - N)) + 1) e. w -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w)))
53	43, 52	sylan9r 469	. . . . . . . . . . . . . 14 |- ((y e. RR /\ (y + (1 - N)) e. w) -> (A.v e. w (v + 1) e. w -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w)))
54	53	com12 11	. . . . . . . . . . . . 13 |- (A.v e. w (v + 1) e. w -> ((y e. RR /\ (y + (1 - N)) e. w) -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w)))
55	54	19.21aiv 1284	. . . . . . . . . . . 12 |- (A.v e. w (v + 1) e. w -> A.y((y e. RR /\ (y + (1 - N)) e. w) -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w)))
56	55	anim2i 335	. . . . . . . . . . 11 |- ((1 e. w /\ A.v e. w (v + 1) e. w) -> (1 e. w /\ A.y((y e. RR /\ (y + (1 - N)) e. w) -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w))))
57		pm3.27 323	. . . . . . . . . . 11 |- ((m e. RR /\ (m + (1 - N)) e. w) -> (m + (1 - N)) e. w)
58	56, 57	imim12i 18	. . . . . . . . . 10 |- (((1 e. w /\ A.y((y e. RR /\ (y + (1 - N)) e. w) -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w))) -> (m e. RR /\ (m + (1 - N)) e. w)) -> ((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w))
59	58	a1i 8	. . . . . . . . 9 |- (m e. ZZ -> (((1 e. w /\ A.y((y e. RR /\ (y + (1 - N)) e. w) -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w))) -> (m e. RR /\ (m + (1 - N)) e. w)) -> ((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w)))
60		reex 5292	. . . . . . . . . . 11 |- RR e. V
61	60	rabex 2720	. . . . . . . . . 10 |- {u e. RR | (u + (1 - N)) e. w} e. V
62		eleq2 1532	. . . . . . . . . . . . 13 |- (x = {u e. RR | (u + (1 - N)) e. w} -> (N e. x <-> N e. {u e. RR | (u + (1 - N)) e. w}))
63		opreq1 3959	. . . . . . . . . . . . . . . . 17 |- (u = N -> (u + (1 - N)) = (N + (1 - N)))
64	63, 35	syl6eq 1520	. . . . . . . . . . . . . . . 16 |- (u = N -> (u + (1 - N)) = 1)
65	64	eleq1d 1537	. . . . . . . . . . . . . . 15 |- (u = N -> ((u + (1 - N)) e. w <-> 1 e. w))
66	65	elrab 1901	. . . . . . . . . . . . . 14 |- (N e. {u e. RR | (u + (1 - N)) e. w} <-> (N e. RR /\ 1 e. w))
67	66, 27	mpbiran 727	. . . . . . . . . . . . 13 |- (N e. {u e. RR