Theorem dfuzi 7414

Description: An expression for the upper integers that start at N that is analogous to df-n 7108 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
dfuzi	|- {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 dfuzi

Step	Hyp	Ref	Expression
1		breq2 3342	. . . . 5 |- (z = m -> (N <_ z <-> N <_ m))
2	1	elrab 2414	. . . 4 |- (m e. {z e. ZZ | N <_ z} <-> (m e. ZZ /\ N <_ m))
3	2	simplbi 349	. . 3 |- (m e. {z e. ZZ | N <_ z} -> m e. ZZ)
4		zex 7353	. . . . 5 |- ZZ e. _V
5		eleq2 1958	. . . . . . 7 |- (x = ZZ -> (N e. x <-> N e. ZZ))
6		eleq2 1958	. . . . . . . 8 |- (x = ZZ -> ((y + 1) e. x <-> (y + 1) e. ZZ))
7	6	raleqbi1dv 2271	. . . . . . 7 |- (x = ZZ -> (A.y e. x (y + 1) e. x <-> A.y e. ZZ (y + 1) e. ZZ))
8	5, 7	anbi12d 690	. . . . . 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 7375	. . . . . . . 8 |- (y e. ZZ -> (y + 1) e. ZZ)
11	10	rgen 2159	. . . . . . 7 |- A.y e. ZZ (y + 1) e. ZZ
12	9, 11	pm3.2i 307	. . . . . 6 |- (N e. ZZ /\ A.y e. ZZ (y + 1) e. ZZ)
13	8, 12	intmin3 3245	. . . . 5 |- (ZZ e. _V -> |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)} C_ ZZ)
14	4, 13	ax-mp 7	. . . 4 |- |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)} C_ ZZ
15	14	sseli 2617	. . 3 |- (m e. |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)} -> m e. ZZ)
16		ax-17 1317	. . . . . 6 |- (u e. m -> A.z u e. m)
17		ax-17 1317	. . . . . 6 |- (u e. (m + (1 - N)) -> A.z u e. (m + (1 - N)))
18		1z 7368	. . . . . . . 8 |- 1 e. ZZ
19		zsubcl 7377	. . . . . . . 8 |- ((1 e. ZZ /\ N e. ZZ) -> (1 - N) e. ZZ)
20	18, 9, 19	mp2an 761	. . . . . . 7 |- (1 - N) e. ZZ
21		zaddcl 7374	. . . . . . 7 |- ((z e. ZZ /\ (1 - N) e. ZZ) -> (z + (1 - N)) e. ZZ)
22	20, 21	mpan2 760	. . . . . 6 |- (z e. ZZ -> (z + (1 - N)) e. ZZ)
23		breq2 3342	. . . . . 6 |- (v = (z + (1 - N)) -> (1 <_ v <-> 1 <_ (z + (1 - N))))
24		opreq1 4889	. . . . . 6 |- (z = m -> (z + (1 - N)) = (m + (1 - N)))
25	16, 17, 22, 23, 24	rabxfr 3843	. . . . 5 |- (m e. ZZ -> ((m + (1 - N)) e. {v e. ZZ | 1 <_ v} <-> m e. {z e. ZZ | 1 <_ (z + (1 - N))}))
26		zre 7348	. . . . . . . . 9 |- (z e. ZZ -> z e. RR)
27	9	zrei 7350	. . . . . . . . . 10 |- N e. RR
28		1re 6598	. . . . . . . . . . 11 |- 1 e. RR
29	28, 27	resubcli 6602	. . . . . . . . . 10 |- (1 - N) e. RR
30		leadd1 6808	. . . . . . . . . 10 |- ((N e. RR /\ z e. RR /\ (1 - N) e. RR) -> (N <_ z <-> (N + (1 - N)) <_ (z + (1 - N))))
31	27, 29, 30	mp3an13 1182	. . . . . . . . 9 |- (z e. RR -> (N <_ z <-> (N + (1 - N)) <_ (z + (1 - N))))
32	26, 31	syl 12	. . . . . . . 8 |- (z e. ZZ -> (N <_ z <-> (N + (1 - N)) <_ (z + (1 - N))))
33	27	recni 6467	. . . . . . . . . 10 |- N e. CC
34		ax1cn 6422	. . . . . . . . . 10 |- 1 e. CC
35	33, 34	pncan3i 6535	. . . . . . . . 9 |- (N + (1 - N)) = 1
36	35	breq1i 3345	. . . . . . . 8 |- ((N + (1 - N)) <_ (z + (1 - N)) <-> 1 <_ (z + (1 - N)))
37	32, 36	syl6bb 595	. . . . . . 7 |- (z e. ZZ -> (N <_ z <-> 1 <_ (z + (1 - N))))
38	37	rabbiia 2285	. . . . . 6 |- {z e. ZZ | N <_ z} = {z e. ZZ | 1 <_ (z + (1 - N))}
39	38	eleq2i 1961	. . . . 5 |- (m e. {z e. ZZ | N <_ z} <-> m e. {z e. ZZ | 1 <_ (z + (1 - N))})
40	25, 39	syl6bbr 597	. . . 4 |- (m e. ZZ -> ((m + (1 - N)) e. {v e. ZZ | 1 <_ v} <-> m e. {z e. ZZ | N <_ z}))
41		opreq1 4889	. . . . . . . . . . . . . . . . 17 |- (v = (y + (1 - N)) -> (v + 1) = ((y + (1 - N)) + 1))
42	41	eleq1d 1963	. . . . . . . . . . . . . . . 16 |- (v = (y + (1 - N)) -> ((v + 1) e. w <-> ((y + (1 - N)) + 1) e. w))
43	42	rcla4v 2376	. . . . . . . . . . . . . . 15 |- ((y + (1 - N)) e. w -> (A.v e. w (v + 1) e. w -> ((y + (1 - N)) + 1) e. w))
44		recn 6466	. . . . . . . . . . . . . . . . . . 19 |- (y e. RR -> y e. CC)
45	29	recni 6467	. . . . . . . . . . . . . . . . . . . 20 |- (1 - N) e. CC
46		add23 6490	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. CC /\ (1 - N) e. CC /\ 1 e. CC) -> ((y + (1 - N)) + 1) = ((y + 1) + (1 - N)))
47	45, 34, 46	mp3an23 1183	. . . . . . . . . . . . . . . . . . 19 |- (y e. CC -> ((y + (1 - N)) + 1) = ((y + 1) + (1 - N)))
48	44, 47	syl 12	. . . . . . . . . . . . . . . . . 18 |- (y e. RR -> ((y + (1 - N)) + 1) = ((y + 1) + (1 - N)))
49	48	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (y e. RR -> (((y + (1 - N)) + 1) e. w <-> ((y + 1) + (1 - N)) e. w))
50	49	biimpd 170	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (((y + (1 - N)) + 1) e. w -> ((y + 1) + (1 - N)) e. w))
51		peano2re 6599	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (y + 1) e. RR)
52	50, 51	jctild 662	. . . . . . . . . . . . . . 15 |- (y e. RR -> (((y + (1 - N)) + 1) e. w -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w)))
53	43, 52	sylan9r 519	. . . . . . . . . . . . . 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 14	. . . . . . . . . . . . 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 1664	. . . . . . . . . . . 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 362	. . . . . . . . . . 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		simpr 350	. . . . . . . . . . 11 |- ((m e. RR /\ (m + (1 - N)) e. w) -> (m + (1 - N)) e. w)
58	56, 57	imim12i 21	. . . . . . . . . 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 6465	. . . . . . . . . . 11 |- RR e. _V
61	60	rabex 3461	. . . . . . . . . 10 |- {u e. RR | (u + (1 - N)) e. w} e. _V
62		eleq2 1958	. . . . . . . . . . . . 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 4889	. . . . . . . . . . . . . . . . 17 |- (u = N -> (u + (1 - N)) = (N + (1 - N)))
64	63, 35	syl6eq 1944	. . . . . . . . . . . . . . . 16 |- (u = N -> (u + (1 - N)) = 1)
65	64	eleq1d 1963	. . . . . . . . . . . . . . 15 |- (u = N -> ((u + (1 - N)) e. w <-> 1 e. w))
66	65	elrab 2414	. . . . . . . . . . . . . 14 |- (N e. {u e. RR | (u + (1 - N)) e. w} <-> (N e. RR /\ 1 e. w))
67	66, 27	mpbiran 798	. . . . . . . . . . . . 13 |- (N e. {u e. RR | (u + (1 - N)) e. w} <-> 1 e. w)
68	62, 67	syl6bb 595	. . . . . . . . . . . 12 |- (x = {u e. RR | (u + (1 - N)) e. w} -> (N e. x <-> 1 e. w))
69		eleq2 1958	. . . . . . . . . . . . . . . 16 |- (x = {u e. RR | (u + (1 - N)) e. w} -> (y e. x <-> y e. {u e. RR | (u + (1 - N)) e. w}))
70		opreq1 4889	. . . . . . . . . . . . . . . . . 18 |- (u = y -> (u + (1 - N)) = (y + (1 - N)))
71	70	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (u = y -> ((u + (1 - N)) e. w <-> (y + (1 - N)) e. w))
72	71	elrab 2414	. . . . . . . . . . . . . . . 16 |- (y e. {u e. RR | (u + (1 - N)) e. w} <-> (y e. RR /\ (y + (1 - N)) e. w))
73	69, 72	syl6bb 595	. . . . . . . . . . . . . . 15 |- (x = {u e. RR | (u + (1 - N)) e. w} -> (y e. x <-> (y e. RR /\ (y + (1 - N)) e. w)))
74		eleq2 1958	. . . . . . . . . . . . . . . 16 |- (x = {u e. RR | (u + (1 - N)) e. w} -> ((y + 1) e. x <-> (y + 1) e. {u e. RR | (u + (1 - N)) e. w}))
75		opreq1 4889	. . . . . . . . . . . . . . . . . 18 |- (u = (y + 1) -> (u + (1 - N)) = ((y + 1) + (1 - N)))
76	75	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (u = (y + 1) -> ((u + (1 - N)) e. w <-> ((y + 1) + (1 - N)) e. w))
77	76	elrab 2414	. . . . . . . . . . . . . . . 16 |- ((y + 1) e. {u e. RR | (u + (1 - N)) e. w} <-> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w))
78	74, 77	syl6bb 595	. . . . . . . . . . . . . . 15 |- (x = {u e. RR | (u + (1 - N)) e. w} -> ((y + 1) e. x <-> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w)))
79	73, 78	imbi12d 688	. . . . . . . . . . . . . 14 |- (x = {u e. RR | (u + (1 - N)) e. w} -> ((y e. x -> (y + 1) e. x) <-> ((y e. RR /\ (y + (1 - N)) e. w) -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w))))
80	79	albidv 1656	. . . . . . . . . . . . 13 |- (x = {u e. RR | (u + (1 - N)) e. w} -> (A.y(y e. x -> (y + 1) e. x) <-> A.y((y e. RR /\ (y + (1 - N)) e. w) -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w))))
81		df-ral 2109	. . . . . . . . . . . . 13 |- (A.y e. x (y + 1) e. x <-> A.y(y e. x -> (y + 1) e. x))
82	80, 81	syl5bb 591	. . . . . . . . . . . 12 |- (x = {u e. RR | (u + (1 - N)) e. w} -> (A.y e. x (y + 1) e. x <-> A.y((y e. RR /\ (y + (1 - N)) e. w) -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w))))
83	68, 82	anbi12d 690	. . . . . . . . . . 11 |- (x = {u e. RR | (u + (1 - N)) e. w} -> ((N e. x /\ A.y e. x (y + 1) e. x) <-> (1 e. w /\ A.y((y e. RR /\ (y + (1 - N)) e. w) -> ((y + 1) e. RR /\ ((y + 1) + (1 - N)) e. w)))))
84		eleq2 1958	. . . . . . . . . . . 12 |- (x = {u e. RR | (u + (1 - N)) e. w} -> (m e. x <-> m e. {u e. RR | (u + (1 - N)) e. w}))
85		opreq1 4889	. . . . . . . . . . . . . 14 |- (u = m -> (u + (1 - N)) = (m + (1 - N)))
86	85	eleq1d 1963	. . . . . . . . . . . . 13 |- (u = m -> ((u + (1 - N)) e. w <-> (m + (1 - N)) e. w))
87	86	elrab 2414	. . . . . . . . . . . 12 |- (m e. {u e. RR | (u + (1 - N)) e. w} <-> (m e. RR /\ (m + (1 - N)) e. w))
88	84, 87	syl6bb 595	. . . . . . . . . . 11 |- (x = {u e. RR | (u + (1 - N)) e. w} -> (m e. x <-> (m e. RR /\ (m + (1 - N)) e. w)))
89	83, 88	imbi12d 688	. . . . . . . . . 10 |- (x = {u e. RR | (u + (1 - N)) e. w} -> (((N e. x /\ A.y e. x (y + 1) e. x) -> m e. x) <-> ((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))))
90	61, 89	cla4v 2370	. . . . . . . . 9 |- (A.x((N e. x /\ A.y e. x (y + 1) e. x) -> m e. x) -> ((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)))
91	59, 90	syl5 20	. . . . . . . 8 |- (m e. ZZ -> (A.x((N e. x /\ A.y e. x (y + 1) e. x) -> m e. x) -> ((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w)))
92	91	19.21adv 1666	. . . . . . 7 |- (m e. ZZ -> (A.x((N e. x /\ A.y e. x (y + 1) e. x) -> m e. x) -> A.w((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w)))
93		opreq1 4889	. . . . . . . . . . . . . . . . 17 |- (y = (v - (1 - N)) -> (y + 1) = ((v - (1 - N)) + 1))
94	93	eleq1d 1963	. . . . . . . . . . . . . . . 16 |- (y = (v - (1 - N)) -> ((y + 1) e. x <-> ((v - (1 - N)) + 1) e. x))
95	94	rcla4v 2376	. . . . . . . . . . . . . . 15 |- ((v - (1 - N)) e. x -> (A.y e. x (y + 1) e. x -> ((v - (1 - N)) + 1) e. x))
96		recn 6466	. . . . . . . . . . . . . . . . . . 19 |- (v e. RR -> v e. CC)
97		addsub 6542	. . . . . . . . . . . . . . . . . . . 20 |- ((v e. CC /\ 1 e. CC /\ (1 - N) e. CC) -> ((v + 1) - (1 - N)) = ((v - (1 - N)) + 1))
98	34, 45, 97	mp3an23 1183	. . . . . . . . . . . . . . . . . . 19 |- (v e. CC -> ((v + 1) - (1 - N)) = ((v - (1 - N)) + 1))
99	96, 98	syl 12	. . . . . . . . . . . . . . . . . 18 |- (v e. RR -> ((v + 1) - (1 - N)) = ((v - (1 - N)) + 1))
100	99	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (v e. RR -> (((v + 1) - (1 - N)) e. x <-> ((v - (1 - N)) + 1) e. x))
101	100	biimprd 171	. . . . . . . . . . . . . . . 16 |- (v e. RR -> (((v - (1 - N)) + 1) e. x -> ((v + 1) - (1 - N)) e. x))
102		peano2re 6599	. . . . . . . . . . . . . . . 16 |- (v e. RR -> (v + 1) e. RR)
103	101, 102	jctild 662	. . . . . . . . . . . . . . 15 |- (v e. RR -> (((v - (1 - N)) + 1) e. x -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x)))
104	95, 103	sylan9r 519	. . . . . . . . . . . . . 14 |- ((v e. RR /\ (v - (1 - N)) e. x) -> (A.y e. x (y + 1) e. x -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x)))
105	104	com12 14	. . . . . . . . . . . . 13 |- (A.y e. x (y + 1) e. x -> ((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x)))
106	105	19.21aiv 1664	. . . . . . . . . . . 12 |- (A.y e. x (y + 1) e. x -> A.v((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x)))
107	106	anim2i 362	. . . . . . . . . . 11 |- ((N e. x /\ A.y e. x (y + 1) e. x) -> (N e. x /\ A.v((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x))))
108	107	a1i 8	. . . . . . . . . 10 |- (m e. ZZ -> ((N e. x /\ A.y e. x (y + 1) e. x) -> (N e. x /\ A.v((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x)))))
109		pncan 6557	. . . . . . . . . . . . . 14 |- ((m e. CC /\ (1 - N) e. CC) -> ((m + (1 - N)) - (1 - N)) = m)
110		zcn 7349	. . . . . . . . . . . . . 14 |- (m e. ZZ -> m e. CC)
111	109, 110, 45	sylancl 525	. . . . . . . . . . . . 13 |- (m e. ZZ -> ((m + (1 - N)) - (1 - N)) = m)
112	111	eleq1d 1963	. . . . . . . . . . . 12 |- (m e. ZZ -> (((m + (1 - N)) - (1 - N)) e. x <-> m e. x))
113	112	biimpd 170	. . . . . . . . . . 11 |- (m e. ZZ -> (((m + (1 - N)) - (1 - N)) e. x -> m e. x))
114	113	adantld 426	. . . . . . . . . 10 |- (m e. ZZ -> (((m + (1 - N)) e. RR /\ ((m + (1 - N)) - (1 - N)) e. x) -> m e. x))
115	108, 114	imim12d 69	. . . . . . . . 9 |- (m e. ZZ -> (((N e. x /\ A.v((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x))) -> ((m + (1 - N)) e. RR /\ ((m + (1 - N)) - (1 - N)) e. x)) -> ((N e. x /\ A.y e. x (y + 1) e. x) -> m e. x)))
116	60	rabex 3461	. . . . . . . . . 10 |- {u e. RR | (u - (1 - N)) e. x} e. _V
117		eleq2 1958	. . . . . . . . . . . . 13 |- (w = {u e. RR | (u - (1 - N)) e. x} -> (1 e. w <-> 1 e. {u e. RR | (u - (1 - N)) e. x}))
118		opreq1 4889	. . . . . . . . . . . . . . . . 17 |- (u = 1 -> (u - (1 - N)) = (1 - (1 - N)))
119		nncan 6635	. . . . . . . . . . . . . . . . . 18 |- ((1 e. CC /\ N e. CC) -> (1 - (1 - N)) = N)
120	34, 33, 119	mp2an 761	. . . . . . . . . . . . . . . . 17 |- (1 - (1 - N)) = N
121	118, 120	syl6eq 1944	. . . . . . . . . . . . . . . 16 |- (u = 1 -> (u - (1 - N)) = N)
122	121	eleq1d 1963	. . . . . . . . . . . . . . 15 |- (u = 1 -> ((u - (1 - N)) e. x <-> N e. x))
123	122	elrab 2414	. . . . . . . . . . . . . 14 |- (1 e. {u e. RR | (u - (1 - N)) e. x} <-> (1 e. RR /\ N e. x))
124	123, 28	mpbiran 798	. . . . . . . . . . . . 13 |- (1 e. {u e. RR | (u - (1 - N)) e. x} <-> N e. x)
125	117, 124	syl6bb 595	. . . . . . . . . . . 12 |- (w = {u e. RR | (u - (1 - N)) e. x} -> (1 e. w <-> N e. x))
126		eleq2 1958	. . . . . . . . . . . . . . . 16 |- (w = {u e. RR | (u - (1 - N)) e. x} -> (v e. w <-> v e. {u e. RR | (u - (1 - N)) e. x}))
127		opreq1 4889	. . . . . . . . . . . . . . . . . 18 |- (u = v -> (u - (1 - N)) = (v - (1 - N)))
128	127	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (u = v -> ((u - (1 - N)) e. x <-> (v - (1 - N)) e. x))
129	128	elrab 2414	. . . . . . . . . . . . . . . 16 |- (v e. {u e. RR | (u - (1 - N)) e. x} <-> (v e. RR /\ (v - (1 - N)) e. x))
130	126, 129	syl6bb 595	. . . . . . . . . . . . . . 15 |- (w = {u e. RR | (u - (1 - N)) e. x} -> (v e. w <-> (v e. RR /\ (v - (1 - N)) e. x)))
131		eleq2 1958	. . . . . . . . . . . . . . . 16 |- (w = {u e. RR | (u - (1 - N)) e. x} -> ((v + 1) e. w <-> (v + 1) e. {u e. RR | (u - (1 - N)) e. x}))
132		opreq1 4889	. . . . . . . . . . . . . . . . . 18 |- (u = (v + 1) -> (u - (1 - N)) = ((v + 1) - (1 - N)))
133	132	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- (u = (v + 1) -> ((u - (1 - N)) e. x <-> ((v + 1) - (1 - N)) e. x))
134	133	elrab 2414	. . . . . . . . . . . . . . . 16 |- ((v + 1) e. {u e. RR | (u - (1 - N)) e. x} <-> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x))
135	131, 134	syl6bb 595	. . . . . . . . . . . . . . 15 |- (w = {u e. RR | (u - (1 - N)) e. x} -> ((v + 1) e. w <-> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x)))
136	130, 135	imbi12d 688	. . . . . . . . . . . . . 14 |- (w = {u e. RR | (u - (1 - N)) e. x} -> ((v e. w -> (v + 1) e. w) <-> ((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x))))
137	136	albidv 1656	. . . . . . . . . . . . 13 |- (w = {u e. RR | (u - (1 - N)) e. x} -> (A.v(v e. w -> (v + 1) e. w) <-> A.v((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x))))
138		df-ral 2109	. . . . . . . . . . . . 13 |- (A.v e. w (v + 1) e. w <-> A.v(v e. w -> (v + 1) e. w))
139	137, 138	syl5bb 591	. . . . . . . . . . . 12 |- (w = {u e. RR | (u - (1 - N)) e. x} -> (A.v e. w (v + 1) e. w <-> A.v((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x))))
140	125, 139	anbi12d 690	. . . . . . . . . . 11 |- (w = {u e. RR | (u - (1 - N)) e. x} -> ((1 e. w /\ A.v e. w (v + 1) e. w) <-> (N e. x /\ A.v((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x)))))
141		eleq2 1958	. . . . . . . . . . . 12 |- (w = {u e. RR | (u - (1 - N)) e. x} -> ((m + (1 - N)) e. w <-> (m + (1 - N)) e. {u e. RR | (u - (1 - N)) e. x}))
142		opreq1 4889	. . . . . . . . . . . . . 14 |- (u = (m + (1 - N)) -> (u - (1 - N)) = ((m + (1 - N)) - (1 - N)))
143	142	eleq1d 1963	. . . . . . . . . . . . 13 |- (u = (m + (1 - N)) -> ((u - (1 - N)) e. x <-> ((m + (1 - N)) - (1 - N)) e. x))
144	143	elrab 2414	. . . . . . . . . . . 12 |- ((m + (1 - N)) e. {u e. RR | (u - (1 - N)) e. x} <-> ((m + (1 - N)) e. RR /\ ((m + (1 - N)) - (1 - N)) e. x))
145	141, 144	syl6bb 595	. . . . . . . . . . 11 |- (w = {u e. RR | (u - (1 - N)) e. x} -> ((m + (1 - N)) e. w <-> ((m + (1 - N)) e. RR /\ ((m + (1 - N)) - (1 - N)) e. x)))
146	140, 145	imbi12d 688	. . . . . . . . . 10 |- (w = {u e. RR | (u - (1 - N)) e. x} -> (((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w) <-> ((N e. x /\ A.v((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x))) -> ((m + (1 - N)) e. RR /\ ((m + (1 - N)) - (1 - N)) e. x))))
147	116, 146	cla4v 2370	. . . . . . . . 9 |- (A.w((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w) -> ((N e. x /\ A.v((v e. RR /\ (v - (1 - N)) e. x) -> ((v + 1) e. RR /\ ((v + 1) - (1 - N)) e. x))) -> ((m + (1 - N)) e. RR /\ ((m + (1 - N)) - (1 - N)) e. x)))
148	115, 147	syl5 20	. . . . . . . 8 |- (m e. ZZ -> (A.w((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w) -> ((N e. x /\ A.y e. x (y + 1) e. x) -> m e. x)))
149	148	19.21adv 1666	. . . . . . 7 |- (m e. ZZ -> (A.w((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w) -> A.x((N e. x /\ A.y e. x (y + 1) e. x) -> m e. x)))
150	92, 149	impbid 574	. . . . . 6 |- (m e. ZZ -> (A.x((N e. x /\ A.y e. x (y + 1) e. x) -> m e. x) <-> A.w((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w)))
151		visset 2295	. . . . . . 7 |- m e. _V
152	151	elintab 3227	. . . . . 6 |- (m e. |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)} <-> A.x((N e. x /\ A.y e. x (y + 1) e. x) -> m e. x))
153		oprex 4907	. . . . . . 7 |- (m + (1 - N)) e. _V
154	153	elintab 3227	. . . . . 6 |- ((m + (1 - N)) e. |^|{w | (1 e. w /\ A.v e. w (v + 1) e. w)} <-> A.w((1 e. w /\ A.v e. w (v + 1) e. w) -> (m + (1 - N)) e. w))
155	150, 152, 154	3bitr4g 614	. . . . 5 |- (m e. ZZ -> (m e. |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)} <-> (m + (1 - N)) e. |^|{w | (1 e. w /\ A.v e. w (v + 1) e. w)}))
156		df-n 7108	. . . . . . 7 |- NN = |^|{w | (1 e. w /\ A.v e. w (v + 1) e. w)}
157		nnzrab 7366	. . . . . . 7 |- NN = {v e. ZZ | 1 <_ v}
158	156, 157	eqtr3i 1910	. . . . . 6 |- |^|{w | (1 e. w /\ A.v e. w (v + 1) e. w)} = {v e. ZZ | 1 <_ v}
159	158	eleq2i 1961	. . . . 5 |- ((m + (1 - N)) e. |^|{w | (1 e. w /\ A.v e. w (v + 1) e. w)} <-> (m + (1 - N)) e. {v e. ZZ | 1 <_ v})
160	155, 159	syl6rbb 596	. . . 4 |- (m e. ZZ -> ((m + (1 - N)) e. {v e. ZZ | 1 <_ v} <-> m e. |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)}))
161	40, 160	bitr3d 589	. . 3 |- (m e. ZZ -> (m e. {z e. ZZ | N <_ z} <-> m e. |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)}))
162	3, 15, 161	pm5.21nii 743	. 2 |- (m e. {z e. ZZ | N <_ z} <-> m e. |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)})
163	162	eqriv 1881	1 |- {z e. ZZ | N <_ z} = |^|{x | (N e. x /\ A.y e. x (y + 1) e. x)}

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  {cab 1871  A.wral 2105  {crab 2108  _Vcvv 2292   C_ wss 2593  |^|cint 3214   class class class wbr 3338  (class class class)co 4884  CCcc 6384  RRcr 6385  1c1 6387   + caddc 6389   - cmin 6445   <_ cle 6448  NNcn 6449  ZZcz 6451

This theorem is referenced by:  peano5uzi 7415

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-n0 7309  df-z 7345

Copyright terms: Public domain