Theorem iccelpart 38882

Description: An element of any partitioned half opened interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020.)

Assertion

Ref	Expression
iccelpart	|- ( M e. NN -> A. p e. (RePart ` M ) ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )

Distinct variable groups:   i, M, p   i, X, p

Proof of Theorem iccelpart

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5892	. . 3 |- ( x = 1 -> (RePart ` x ) = (RePart ` 1 ) )
2		fveq2 5892	. . . . . 6 |- ( x = 1 -> ( p ` x ) = ( p ` 1 ) )
3	2	oveq2d 6336	. . . . 5 |- ( x = 1 -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` 1 ) ) )
4	3	eleq2d 2525	. . . 4 |- ( x = 1 -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
5		oveq2 6328	. . . . . 6 |- ( x = 1 -> ( 0..^ x ) = ( 0..^ 1 ) )
6		fzo01 12032	. . . . . 6 |- ( 0..^ 1 ) = { 0 }
7	5, 6	syl6eq 2512	. . . . 5 |- ( x = 1 -> ( 0..^ x ) = { 0 } )
8	7	rexeqdv 3006	. . . 4 |- ( x = 1 -> ( E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
9	4, 8	imbi12d 326	. . 3 |- ( x = 1 -> ( ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
10	1, 9	raleqbidv 3013	. 2 |- ( x = 1 -> ( A. p e. (RePart ` x ) ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> A. p e. (RePart ` 1 ) ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
11		fveq2 5892	. . 3 |- ( x = y -> (RePart ` x ) = (RePart ` y ) )
12		fveq2 5892	. . . . . 6 |- ( x = y -> ( p ` x ) = ( p ` y ) )
13	12	oveq2d 6336	. . . . 5 |- ( x = y -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` y ) ) )
14	13	eleq2d 2525	. . . 4 |- ( x = y -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) )
15		oveq2 6328	. . . . 5 |- ( x = y -> ( 0..^ x ) = ( 0..^ y ) )
16	15	rexeqdv 3006	. . . 4 |- ( x = y -> ( E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
17	14, 16	imbi12d 326	. . 3 |- ( x = y -> ( ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
18	11, 17	raleqbidv 3013	. 2 |- ( x = y -> ( A. p e. (RePart ` x ) ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
19		fveq2 5892	. . 3 |- ( x = ( y + 1 ) -> (RePart ` x ) = (RePart ` ( y + 1 ) ) )
20		fveq2 5892	. . . . . 6 |- ( x = ( y + 1 ) -> ( p ` x ) = ( p ` ( y + 1 ) ) )
21	20	oveq2d 6336	. . . . 5 |- ( x = ( y + 1 ) -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) )
22	21	eleq2d 2525	. . . 4 |- ( x = ( y + 1 ) -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) )
23		oveq2 6328	. . . . 5 |- ( x = ( y + 1 ) -> ( 0..^ x ) = ( 0..^ ( y + 1 ) ) )
24	23	rexeqdv 3006	. . . 4 |- ( x = ( y + 1 ) -> ( E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
25	22, 24	imbi12d 326	. . 3 |- ( x = ( y + 1 ) -> ( ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
26	19, 25	raleqbidv 3013	. 2 |- ( x = ( y + 1 ) -> ( A. p e. (RePart ` x ) ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> A. p e. (RePart ` ( y + 1 ) ) ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
27		fveq2 5892	. . 3 |- ( x = M -> (RePart ` x ) = (RePart ` M ) )
28		fveq2 5892	. . . . . 6 |- ( x = M -> ( p ` x ) = ( p ` M ) )
29	28	oveq2d 6336	. . . . 5 |- ( x = M -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` M ) ) )
30	29	eleq2d 2525	. . . 4 |- ( x = M -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` M ) ) ) )
31		oveq2 6328	. . . . 5 |- ( x = M -> ( 0..^ x ) = ( 0..^ M ) )
32	31	rexeqdv 3006	. . . 4 |- ( x = M -> ( E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
33	30, 32	imbi12d 326	. . 3 |- ( x = M -> ( ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
34	27, 33	raleqbidv 3013	. 2 |- ( x = M -> ( A. p e. (RePart ` x ) ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) -> E. i e. ( 0..^ x ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> A. p e. (RePart ` M ) ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
35		0nn0 10918	. . . . 5 |- 0 e. NN0
36		fveq2 5892	. . . . . . . 8 |- ( i = 0 -> ( p ` i ) = ( p ` 0 ) )
37		oveq1 6327	. . . . . . . . . 10 |- ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
38		0p1e1 10754	. . . . . . . . . 10 |- ( 0 + 1 ) = 1
39	37, 38	syl6eq 2512	. . . . . . . . 9 |- ( i = 0 -> ( i + 1 ) = 1 )
40	39	fveq2d 5896	. . . . . . . 8 |- ( i = 0 -> ( p ` ( i + 1 ) ) = ( p ` 1 ) )
41	36, 40	oveq12d 6338	. . . . . . 7 |- ( i = 0 -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( p ` 0 ) [,) ( p ` 1 ) ) )
42	41	eleq2d 2525	. . . . . 6 |- ( i = 0 -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
43	42	rexsng 4019	. . . . 5 |- ( 0 e. NN0 -> ( E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
44	35, 43	ax-mp 5	. . . 4 |- ( E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) )
45	44	biimpri 211	. . 3 |- ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
46	45	rgenw 2761	. 2 |- A. p e. (RePart ` 1 ) ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
47		nfv 1772	. . . . 5 |- F/ p y e. NN
48		nfra1 2781	. . . . 5 |- F/ p A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
49	47, 48	nfan 2022	. . . 4 |- F/ p ( y e. NN /\ A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
50		nnnn0 10910	. . . . . . . . . 10 |- ( y e. NN -> y e. NN0 )
51		fzonn0p1 12027	. . . . . . . . . 10 |- ( y e. NN0 -> y e. ( 0..^ ( y + 1 ) ) )
52	50, 51	syl 17	. . . . . . . . 9 |- ( y e. NN -> y e. ( 0..^ ( y + 1 ) ) )
53	52	ad2antrr 737	. . . . . . . 8 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. (RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> y e. ( 0..^ ( y + 1 ) ) )
54		fveq2 5892	. . . . . . . . . . 11 |- ( i = y -> ( p ` i ) = ( p ` y ) )
55		oveq1 6327	. . . . . . . . . . . 12 |- ( i = y -> ( i + 1 ) = ( y + 1 ) )
56	55	fveq2d 5896	. . . . . . . . . . 11 |- ( i = y -> ( p ` ( i + 1 ) ) = ( p ` ( y + 1 ) ) )
57	54, 56	oveq12d 6338	. . . . . . . . . 10 |- ( i = y -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) )
58	57	eleq2d 2525	. . . . . . . . 9 |- ( i = y -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) ) )
59	58	adantl 472	. . . . . . . 8 |- ( ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. (RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) /\ i = y ) -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) ) )
60		peano2nn 10654	. . . . . . . . . . . . . . . 16 |- ( y e. NN -> ( y + 1 ) e. NN )
61	60	adantr 471	. . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( y + 1 ) e. NN )
62		simpr 467	. . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> p e. (RePart ` ( y + 1 ) ) )
63	60	nnnn0d 10959	. . . . . . . . . . . . . . . . 17 |- ( y e. NN -> ( y + 1 ) e. NN0 )
64		0elfz 11924	. . . . . . . . . . . . . . . . 17 |- ( ( y + 1 ) e. NN0 -> 0 e. ( 0 ... ( y + 1 ) ) )
65	63, 64	syl 17	. . . . . . . . . . . . . . . 16 |- ( y e. NN -> 0 e. ( 0 ... ( y + 1 ) ) )
66	65	adantr 471	. . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> 0 e. ( 0 ... ( y + 1 ) ) )
67	61, 62, 66	iccpartxr 38868	. . . . . . . . . . . . . 14 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` 0 ) e. RR* )
68		nn0fz0 11925	. . . . . . . . . . . . . . . . 17 |- ( ( y + 1 ) e. NN0 <-> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
69	63, 68	sylib 201	. . . . . . . . . . . . . . . 16 |- ( y e. NN -> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
70	69	adantr 471	. . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
71	61, 62, 70	iccpartxr 38868	. . . . . . . . . . . . . 14 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` ( y + 1 ) ) e. RR* )
72	67, 71	jca 539	. . . . . . . . . . . . 13 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
73	72	adantlr 726	. . . . . . . . . . . 12 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
74		elico1 11713	. . . . . . . . . . . 12 |- ( ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
75	73, 74	syl 17	. . . . . . . . . . 11 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
76		simp1 1014	. . . . . . . . . . . . . . . 16 |- ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> X e. RR* )
77	76	adantl 472	. . . . . . . . . . . . . . 15 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X e. RR* )
78		simpl 463	. . . . . . . . . . . . . . 15 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( p ` y ) <_ X )
79		simpr3 1022	. . . . . . . . . . . . . . 15 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X < ( p ` ( y + 1 ) ) )
80	77, 78, 79	3jca 1194	. . . . . . . . . . . . . 14 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) )
81	80	ex 440	. . . . . . . . . . . . 13 |- ( ( p ` y ) <_ X -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
82	81	adantl 472	. . . . . . . . . . . 12 |- ( ( y e. NN /\ ( p ` y ) <_ X ) -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
83	82	adantr 471	. . . . . . . . . . 11 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
84	75, 83	sylbid 223	. . . . . . . . . 10 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
85	84	impr 629	. . . . . . . . 9 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. (RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) )
86		nn0fz0 11925	. . . . . . . . . . . . . . . 16 |- ( y e. NN0 <-> y e. ( 0 ... y ) )
87	50, 86	sylib 201	. . . . . . . . . . . . . . 15 |- ( y e. NN -> y e. ( 0 ... y ) )
88		fzelp1 11883	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ... y ) -> y e. ( 0 ... ( y + 1 ) ) )
89	87, 88	syl 17	. . . . . . . . . . . . . 14 |- ( y e. NN -> y e. ( 0 ... ( y + 1 ) ) )
90	89	adantr 471	. . . . . . . . . . . . 13 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> y e. ( 0 ... ( y + 1 ) ) )
91	61, 62, 90	iccpartxr 38868	. . . . . . . . . . . 12 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` y ) e. RR* )
92	91, 71	jca 539	. . . . . . . . . . 11 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` y ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
93	92	ad2ant2r 758	. . . . . . . . . 10 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. (RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> ( ( p ` y ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
94		elico1 11713	. . . . . . . . . 10 |- ( ( ( p ` y ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) -> ( X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
95	93, 94	syl 17	. . . . . . . . 9 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. (RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> ( X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` y ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
96	85, 95	mpbird 240	. . . . . . . 8 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. (RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) )
97	53, 59, 96	rspcedvd 3167	. . . . . . 7 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ ( p e. (RePart ` ( y + 1 ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
98	97	exp43 621	. . . . . 6 |- ( y e. NN -> ( ( p ` y ) <_ X -> ( p e. (RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
99	98	adantr 471	. . . . 5 |- ( ( y e. NN /\ A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> ( ( p ` y ) <_ X -> ( p e. (RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
100		iccpartres 38867	. . . . . . . . 9 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p |` ( 0 ... y ) ) e. (RePart ` y ) )
101		rspsbca 3359	. . . . . . . . . . . 12 |- ( ( ( p |` ( 0 ... y ) ) e. (RePart ` y ) /\ A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
102		vex 3060	. . . . . . . . . . . . . . 15 |- p e. _V
103	102	resex 5170	. . . . . . . . . . . . . 14 |- ( p |` ( 0 ... y ) ) e. _V
104		sbcimg 3321	. . . . . . . . . . . . . . 15 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> [. ( p |` ( 0 ... y ) ) / p ]. E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
105		sbcel2 3790	. . . . . . . . . . . . . . . . 17 |- ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) )
106		csbov12g 6356	. . . . . . . . . . . . . . . . . . 19 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) [,) [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) ) )
107		csbfv12 5927	. . . . . . . . . . . . . . . . . . . . 21 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ 0 )
108		csbvarg 3804	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ p = ( p |` ( 0 ... y ) ) )
109		csbconstg 3388	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ 0 = 0 )
110	108, 109	fveq12d 5898	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
111	107, 110	syl5eq 2508	. . . . . . . . . . . . . . . . . . . 20 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
112		csbfv12 5927	. . . . . . . . . . . . . . . . . . . . 21 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ y )
113		csbconstg 3388	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ y = y )
114	108, 113	fveq12d 5898	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
115	112, 114	syl5eq 2508	. . . . . . . . . . . . . . . . . . . 20 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
116	111, 115	oveq12d 6338	. . . . . . . . . . . . . . . . . . 19 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) [,) [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) ) = ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
117	106, 116	eqtrd 2496	. . . . . . . . . . . . . . . . . 18 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) = ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
118	117	eleq2d 2525	. . . . . . . . . . . . . . . . 17 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) ) )
119	105, 118	syl5bb 265	. . . . . . . . . . . . . . . 16 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) ) )
120		sbcrex 3355	. . . . . . . . . . . . . . . . 17 |- ( [. ( p |` ( 0 ... y ) ) / p ]. E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0..^ y ) [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
121		sbcel2 3790	. . . . . . . . . . . . . . . . . . 19 |- ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
122		csbov12g 6356	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) [,) [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) ) )
123		csbfv12 5927	. . . . . . . . . . . . . . . . . . . . . . 23 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ i )
124		csbconstg 3388	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ i = i )
125	108, 124	fveq12d 5898	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ i ) = ( ( p |` ( 0 ... y ) ) ` i ) )
126	123, 125	syl5eq 2508	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) = ( ( p |` ( 0 ... y ) ) ` i ) )
127		csbfv12 5927	. . . . . . . . . . . . . . . . . . . . . . 23 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) )
128		csbconstg 3388	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) = ( i + 1 ) )
129	108, 128	fveq12d 5898	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) ) = ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) )
130	127, 129	syl5eq 2508	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) = ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) )
131	126, 130	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) [,) [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) ) = ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) )
132	122, 131	eqtrd 2496	. . . . . . . . . . . . . . . . . . . 20 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) )
133	132	eleq2d 2525	. . . . . . . . . . . . . . . . . . 19 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
134	121, 133	syl5bb 265	. . . . . . . . . . . . . . . . . 18 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
135	134	rexbidv 2913	. . . . . . . . . . . . . . . . 17 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( E. i e. ( 0..^ y ) [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
136	120, 135	syl5bb 265	. . . . . . . . . . . . . . . 16 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
137	119, 136	imbi12d 326	. . . . . . . . . . . . . . 15 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> [. ( p |` ( 0 ... y ) ) / p ]. E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) ) )
138	104, 137	bitrd 261	. . . . . . . . . . . . . 14 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) ) )
139	103, 138	ax-mp 5	. . . . . . . . . . . . 13 |- ( [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) <-> ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) )
140	72, 74	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
141	140	adantr 471	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) )
142	76	adantl 472	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X e. RR* )
143		simpr2 1021	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( p ` 0 ) <_ X )
144		xrltnle 9732	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( X e. RR* /\ ( p ` y ) e. RR* ) -> ( X < ( p ` y ) <-> -. ( p ` y ) <_ X ) )
145	76, 91, 144	syl2anr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X < ( p ` y ) <-> -. ( p ` y ) <_ X ) )
146	145	exbiri 632	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> X < ( p ` y ) ) ) )
147	146	com23 81	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> X < ( p ` y ) ) ) )
148	147	imp31 438	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X < ( p ` y ) )
149	142, 143, 148	3jca 1194	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` y ) ) )
150	67, 91	jca 539	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` y ) e. RR* ) )
151	150	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` y ) e. RR* ) )
152		elico1 11713	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( p ` 0 ) e. RR* /\ ( p ` y ) e. RR* ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` y ) ) ) )
153	151, 152	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` y ) ) ) )
154	149, 153	mpbird 240	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X e. ( ( p ` 0 ) [,) ( p ` y ) ) )
155	154	ex 440	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) )
156	141, 155	sylbid 223	. . . . . . . . . . . . . . . . 17 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) )
157		0elfz 11924	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y e. NN0 -> 0 e. ( 0 ... y ) )
158	50, 157	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. NN -> 0 e. ( 0 ... y ) )
159	158	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> 0 e. ( 0 ... y ) )
160		fvres 5906	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` 0 ) = ( p ` 0 ) )
161	159, 160	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p |` ( 0 ... y ) ) ` 0 ) = ( p ` 0 ) )
162	161	eqcomd 2468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
163	87	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> y e. ( 0 ... y ) )
164		fvres 5906	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` y ) = ( p ` y ) )
165	163, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p |` ( 0 ... y ) ) ` y ) = ( p ` y ) )
166	165	eqcomd 2468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
167	162, 166	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) [,) ( p ` y ) ) = ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
168	167	eleq2d 2525	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) ) )
169	168	biimpa 491	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
170		elfzofz 11972	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( i e. ( 0..^ y ) -> i e. ( 0 ... y ) )
171	170	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0..^ y ) ) -> i e. ( 0 ... y ) )
172		fvres 5906	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( i e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` i ) = ( p ` i ) )
173	171, 172	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0..^ y ) ) -> ( ( p |` ( 0 ... y ) ) ` i ) = ( p ` i ) )
174		fzofzp1 12045	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( i e. ( 0..^ y ) -> ( i + 1 ) e. ( 0 ... y ) )
175	174	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ i e. ( 0..^ y ) ) -> ( i + 1 ) e. ( 0 ... y ) )
176		fvres 5906	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( i + 1 ) e. ( 0 ... y ) -> ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) = ( p ` ( i + 1 ) ) )
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ i e. ( 0..^ y ) ) -> ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) = ( p ` ( i + 1 ) ) )
178	177	adantlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0..^ y ) ) -> ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) = ( p ` ( i + 1 ) ) )
179	173, 178	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0..^ y ) ) -> ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) = ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
180	179	eleq2d 2525	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) /\ i e. ( 0..^ y ) ) -> ( X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) <-> X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
181	180	rexbidva 2910	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) <-> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
182		nnz 10993	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. NN -> y e. ZZ )
183		uzid 11207	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ZZ -> y e. ( ZZ>= ` y ) )
184	182, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. NN -> y e. ( ZZ>= ` y ) )
185		peano2uz 11246	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ZZ>= ` y ) -> ( y + 1 ) e. ( ZZ>= ` y ) )
186		fzoss2 11983	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y + 1 ) e. ( ZZ>= ` y ) -> ( 0..^ y ) C_ ( 0..^ ( y + 1 ) ) )
187	184, 185, 186	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. NN -> ( 0..^ y ) C_ ( 0..^ ( y + 1 ) ) )
188	187	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( 0..^ y ) C_ ( 0..^ ( y + 1 ) ) )
189		ssrexv 3506	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 0..^ y ) C_ ( 0..^ ( y + 1 ) ) -> ( E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
190	188, 189	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
191	181, 190	sylbid 223	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
192	169, 191	embantd 56	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
193	192	ex 440	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
194	193	adantr 471	. . . . . . . . . . . . . . . . 17 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
195	156, 194	syld 45	. . . . . . . . . . . . . . . 16 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ -. ( p ` y ) <_ X ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
196	195	ex 440	. . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
197	196	com34 86	. . . . . . . . . . . . . 14 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
198	197	com13 83	. . . . . . . . . . . . 13 |- ( ( X e. ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( ( p |` ( 0 ... y ) ) ` i ) [,) ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
199	139, 198	sylbi 200	. . . . . . . . . . . 12 |- ( [. ( p |` ( 0 ... y ) ) / p ]. ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
200	101, 199	syl 17	. . . . . . . . . . 11 |- ( ( ( p |` ( 0 ... y ) ) e. (RePart ` y ) /\ A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
201	200	ex 440	. . . . . . . . . 10 |- ( ( p |` ( 0 ... y ) ) e. (RePart ` y ) -> ( A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) ) )
202	201	com24 90	. . . . . . . . 9 |- ( ( p |` ( 0 ... y ) ) e. (RePart ` y ) -> ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) ) )
203	100, 202	mpcom 37	. . . . . . . 8 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( -. ( p ` y ) <_ X -> ( A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
204	203	ex 440	. . . . . . 7 |- ( y e. NN -> ( p e. (RePart ` ( y + 1 ) ) -> ( -. ( p ` y ) <_ X -> ( A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) ) )
205	204	com24 90	. . . . . 6 |- ( y e. NN -> ( A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( p e. (RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) ) )
206	205	imp 435	. . . . 5 |- ( ( y e. NN /\ A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> ( -. ( p ` y ) <_ X -> ( p e. (RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) ) )
207	99, 206	pm2.61d 163	. . . 4 |- ( ( y e. NN /\ A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> ( p e. (RePart ` ( y + 1 ) ) -> ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
208	49, 207	ralrimi 2800	. . 3 |- ( ( y e. NN /\ A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) -> A. p e. (RePart ` ( y + 1 ) ) ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )
209	208	ex 440	. 2 |- ( y e. NN -> ( A. p e. (RePart ` y ) ( X e. ( ( p ` 0 ) [,) ( p ` y ) ) -> E. i e. ( 0..^ y ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) -> A. p e. (RePart ` ( y + 1 ) ) ( X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) -> E. i e. ( 0..^ ( y + 1 ) ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) ) )
210	10, 18, 26, 34, 46, 209	nnind 10660	1 |- ( M e. NN -> A. p e. (RePart ` M ) ( X e. ( ( p ` 0 ) [,) ( p ` M ) ) -> E. i e. ( 0..^ M ) X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   A.wral 2749   E.wrex 2750   _Vcvv 3057   [.wsbc 3279   [_csb 3375   C_ wss 3416   {csn 3980   class class class wbr 4418   |` cres 4858   ` cfv 5605  (class class class)co 6320   0cc0 9570   1c1 9571   + caddc 9573   RR*cxr 9705   < clt 9706   <_ cle 9707   NNcn 10642   NN0cn0 10903   ZZcz 10971   ZZ>=cuz 11193   [,)cico 11671   ...cfz 11819  ..^cfzo 11952  RePartciccp 38862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-map 7505  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-n0 10904  df-z 10972  df-uz 11194  df-ico 11675  df-fz 11820  df-fzo 11953  df-iccp 38863

This theorem is referenced by:  iccpartiun  38883  icceuelpart  38885  bgoldbtbnd  39039