Theorem iccelpart 38618

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 5882	. . 3 |- ( x = 1 -> (RePart ` x ) = (RePart ` 1 ) )
2		fveq2 5882	. . . . . 6 |- ( x = 1 -> ( p ` x ) = ( p ` 1 ) )
3	2	oveq2d 6322	. . . . 5 |- ( x = 1 -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` 1 ) ) )
4	3	eleq2d 2492	. . . 4 |- ( x = 1 -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
5		oveq2 6314	. . . . . 6 |- ( x = 1 -> ( 0..^ x ) = ( 0..^ 1 ) )
6		fzo01 12002	. . . . . 6 |- ( 0..^ 1 ) = { 0 }
7	5, 6	syl6eq 2479	. . . . 5 |- ( x = 1 -> ( 0..^ x ) = { 0 } )
8	7	rexeqdv 3029	. . . 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 321	. . 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 3036	. 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 5882	. . 3 |- ( x = y -> (RePart ` x ) = (RePart ` y ) )
12		fveq2 5882	. . . . . 6 |- ( x = y -> ( p ` x ) = ( p ` y ) )
13	12	oveq2d 6322	. . . . 5 |- ( x = y -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` y ) ) )
14	13	eleq2d 2492	. . . 4 |- ( x = y -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) )
15		oveq2 6314	. . . . 5 |- ( x = y -> ( 0..^ x ) = ( 0..^ y ) )
16	15	rexeqdv 3029	. . . 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 321	. . 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 3036	. 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 5882	. . 3 |- ( x = ( y + 1 ) -> (RePart ` x ) = (RePart ` ( y + 1 ) ) )
20		fveq2 5882	. . . . . 6 |- ( x = ( y + 1 ) -> ( p ` x ) = ( p ` ( y + 1 ) ) )
21	20	oveq2d 6322	. . . . 5 |- ( x = ( y + 1 ) -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) )
22	21	eleq2d 2492	. . . 4 |- ( x = ( y + 1 ) -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` ( y + 1 ) ) ) ) )
23		oveq2 6314	. . . . 5 |- ( x = ( y + 1 ) -> ( 0..^ x ) = ( 0..^ ( y + 1 ) ) )
24	23	rexeqdv 3029	. . . 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 321	. . 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 3036	. 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 5882	. . 3 |- ( x = M -> (RePart ` x ) = (RePart ` M ) )
28		fveq2 5882	. . . . . 6 |- ( x = M -> ( p ` x ) = ( p ` M ) )
29	28	oveq2d 6322	. . . . 5 |- ( x = M -> ( ( p ` 0 ) [,) ( p ` x ) ) = ( ( p ` 0 ) [,) ( p ` M ) ) )
30	29	eleq2d 2492	. . . 4 |- ( x = M -> ( X e. ( ( p ` 0 ) [,) ( p ` x ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` M ) ) ) )
31		oveq2 6314	. . . . 5 |- ( x = M -> ( 0..^ x ) = ( 0..^ M ) )
32	31	rexeqdv 3029	. . . 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 321	. . 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 3036	. 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 10892	. . . . 5 |- 0 e. NN0
36		fveq2 5882	. . . . . . . 8 |- ( i = 0 -> ( p ` i ) = ( p ` 0 ) )
37		oveq1 6313	. . . . . . . . . 10 |- ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
38		0p1e1 10729	. . . . . . . . . 10 |- ( 0 + 1 ) = 1
39	37, 38	syl6eq 2479	. . . . . . . . 9 |- ( i = 0 -> ( i + 1 ) = 1 )
40	39	fveq2d 5886	. . . . . . . 8 |- ( i = 0 -> ( p ` ( i + 1 ) ) = ( p ` 1 ) )
41	36, 40	oveq12d 6324	. . . . . . 7 |- ( i = 0 -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( p ` 0 ) [,) ( p ` 1 ) ) )
42	41	eleq2d 2492	. . . . . 6 |- ( i = 0 -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) ) )
43	42	rexsng 4035	. . . . 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 209	. . 3 |- ( X e. ( ( p ` 0 ) [,) ( p ` 1 ) ) -> E. i e. { 0 } X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) )
46	45	rgenw 2783	. 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 1755	. . . . 5 |- F/ p y e. NN
48		nfra1 2803	. . . . 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 1988	. . . 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 10884	. . . . . . . . . 10 |- ( y e. NN -> y e. NN0 )
51		fzonn0p1 11997	. . . . . . . . . 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 730	. . . . . . . 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 5882	. . . . . . . . . . 11 |- ( i = y -> ( p ` i ) = ( p ` y ) )
55		oveq1 6313	. . . . . . . . . . . 12 |- ( i = y -> ( i + 1 ) = ( y + 1 ) )
56	55	fveq2d 5886	. . . . . . . . . . 11 |- ( i = y -> ( p ` ( i + 1 ) ) = ( p ` ( y + 1 ) ) )
57	54, 56	oveq12d 6324	. . . . . . . . . 10 |- ( i = y -> ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) = ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) )
58	57	eleq2d 2492	. . . . . . . . 9 |- ( i = y -> ( X e. ( ( p ` i ) [,) ( p ` ( i + 1 ) ) ) <-> X e. ( ( p ` y ) [,) ( p ` ( y + 1 ) ) ) ) )
59	58	adantl 467	. . . . . . . 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 10629	. . . . . . . . . . . . . . . 16 |- ( y e. NN -> ( y + 1 ) e. NN )
61	60	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( y + 1 ) e. NN )
62		simpr 462	. . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> p e. (RePart ` ( y + 1 ) ) )
63	60	nnnn0d 10933	. . . . . . . . . . . . . . . . 17 |- ( y e. NN -> ( y + 1 ) e. NN0 )
64		0elfz 11897	. . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> 0 e. ( 0 ... ( y + 1 ) ) )
67	61, 62, 66	iccpartxr 38604	. . . . . . . . . . . . . 14 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` 0 ) e. RR* )
68		nn0fz0 11898	. . . . . . . . . . . . . . . . 17 |- ( ( y + 1 ) e. NN0 <-> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
69	63, 68	sylib 199	. . . . . . . . . . . . . . . 16 |- ( y e. NN -> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
70	69	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( y + 1 ) e. ( 0 ... ( y + 1 ) ) )
71	61, 62, 70	iccpartxr 38604	. . . . . . . . . . . . . 14 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` ( y + 1 ) ) e. RR* )
72	67, 71	jca 534	. . . . . . . . . . . . 13 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
73	72	adantlr 719	. . . . . . . . . . . 12 |- ( ( ( y e. NN /\ ( p ` y ) <_ X ) /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
74		elico1 11687	. . . . . . . . . . . 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 1005	. . . . . . . . . . . . . . . 16 |- ( ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) -> X e. RR* )
77	76	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X e. RR* )
78		simpl 458	. . . . . . . . . . . . . . 15 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> ( p ` y ) <_ X )
79		simpr3 1013	. . . . . . . . . . . . . . 15 |- ( ( ( p ` y ) <_ X /\ ( X e. RR* /\ ( p ` 0 ) <_ X /\ X < ( p ` ( y + 1 ) ) ) ) -> X < ( p ` ( y + 1 ) ) )
80	77, 78, 79	3jca 1185	. . . . . . . . . . . . . 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 435	. . . . . . . . . . . . 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 467	. . . . . . . . . . . 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 466	. . . . . . . . . . 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 218	. . . . . . . . . 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 623	. . . . . . . . 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 11898	. . . . . . . . . . . . . . . 16 |- ( y e. NN0 <-> y e. ( 0 ... y ) )
87	50, 86	sylib 199	. . . . . . . . . . . . . . 15 |- ( y e. NN -> y e. ( 0 ... y ) )
88		fzelp1 11856	. . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . 13 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> y e. ( 0 ... ( y + 1 ) ) )
91	61, 62, 90	iccpartxr 38604	. . . . . . . . . . . 12 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` y ) e. RR* )
92	91, 71	jca 534	. . . . . . . . . . 11 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` y ) e. RR* /\ ( p ` ( y + 1 ) ) e. RR* ) )
93	92	ad2ant2r 751	. . . . . . . . . 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 11687	. . . . . . . . . 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 235	. . . . . . . 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 3187	. . . . . . 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 615	. . . . . 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 466	. . . . 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 38603	. . . . . . . . 9 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p |` ( 0 ... y ) ) e. (RePart ` y ) )
101		rspsbca 3379	. . . . . . . . . . . 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 3083	. . . . . . . . . . . . . . 15 |- p e. _V
103	102	resex 5167	. . . . . . . . . . . . . 14 |- ( p |` ( 0 ... y ) ) e. _V
104		sbcimg 3341	. . . . . . . . . . . . . . 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 3808	. . . . . . . . . . . . . . . . 17 |- ( [. ( p |` ( 0 ... y ) ) / p ]. X e. ( ( p ` 0 ) [,) ( p ` y ) ) <-> X e. [_ ( p |` ( 0 ... y ) ) / p ]_ ( ( p ` 0 ) [,) ( p ` y ) ) )
106		csbov12g 6342	. . . . . . . . . . . . . . . . . . 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 5917	. . . . . . . . . . . . . . . . . . . . 21 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ 0 )
108		csbvarg 3822	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ p = ( p |` ( 0 ... y ) ) )
109		csbconstg 3408	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ 0 = 0 )
110	108, 109	fveq12d 5888	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
111	107, 110	syl5eq 2475	. . . . . . . . . . . . . . . . . . . 20 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
112		csbfv12 5917	. . . . . . . . . . . . . . . . . . . . 21 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ y )
113		csbconstg 3408	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ y = y )
114	108, 113	fveq12d 5888	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
115	112, 114	syl5eq 2475	. . . . . . . . . . . . . . . . . . . 20 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
116	111, 115	oveq12d 6324	. . . . . . . . . . . . . . . . . . 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 2463	. . . . . . . . . . . . . . . . . 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 2492	. . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . 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 3375	. . . . . . . . . . . . . . . . 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 3808	. . . . . . . . . . . . . . . . . . 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 6342	. . . . . . . . . . . . . . . . . . . . 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 5917	. . . . . . . . . . . . . . . . . . . . . . 23 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ i )
124		csbconstg 3408	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ i = i )
125	108, 124	fveq12d 5888	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( p |` ( 0 ... y ) ) e. _V -> ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ i ) = ( ( p |` ( 0 ... y ) ) ` i ) )
126	123, 125	syl5eq 2475	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` i ) = ( ( p |` ( 0 ... y ) ) ` i ) )
127		csbfv12 5917	. . . . . . . . . . . . . . . . . . . . . . 23 |- [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) = ( [_ ( p |` ( 0 ... y ) ) / p ]_ p ` [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) )
128		csbconstg 3408	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( i + 1 ) = ( i + 1 ) )
129	108, 128	fveq12d 5888	. . . . . . . . . . . . . . . . . . . . . . 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 2475	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p |` ( 0 ... y ) ) e. _V -> [_ ( p |` ( 0 ... y ) ) / p ]_ ( p ` ( i + 1 ) ) = ( ( p |` ( 0 ... y ) ) ` ( i + 1 ) ) )
131	126, 130	oveq12d 6324	. . . . . . . . . . . . . . . . . . . . 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 2463	. . . . . . . . . . . . . . . . . . . 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 2492	. . . . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . . . 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 2936	. . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . 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 321	. . . . . . . . . . . . . . 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 256	. . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . . . 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 1012	. . . . . . . . . . . . . . . . . . . . 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 9709	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( X e. RR* /\ ( p ` y ) e. RR* ) -> ( X < ( p ` y ) <-> -. ( p ` y ) <_ X ) )
145	76, 91, 144	syl2anr 480	. . . . . . . . . . . . . . . . . . . . . . . 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 626	. . . . . . . . . . . . . . . . . . . . . . 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 433	. . . . . . . . . . . . . . . . . . . . 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 1185	. . . . . . . . . . . . . . . . . . . 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 534	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) e. RR* /\ ( p ` y ) e. RR* ) )
151	150	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . 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 11687	. . . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . 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 218	. . . . . . . . . . . . . . . . 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 11897	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y e. NN0 -> 0 e. ( 0 ... y ) )
158	50, 157	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. NN -> 0 e. ( 0 ... y ) )
159	158	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> 0 e. ( 0 ... y ) )
160		fvres 5896	. . . . . . . . . . . . . . . . . . . . . . . . 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 2430	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` 0 ) = ( ( p |` ( 0 ... y ) ) ` 0 ) )
163	87	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> y e. ( 0 ... y ) )
164		fvres 5896	. . . . . . . . . . . . . . . . . . . . . . . . 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 2430	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( p ` y ) = ( ( p |` ( 0 ... y ) ) ` y ) )
167	162, 166	oveq12d 6324	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) -> ( ( p ` 0 ) [,) ( p ` y ) ) = ( ( ( p |` ( 0 ... y ) ) ` 0 ) [,) ( ( p |` ( 0 ... y ) ) ` y ) ) )
168	167	eleq2d 2492	. . . . . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . . . 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 11943	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( i e. ( 0..^ y ) -> i e. ( 0 ... y ) )
171	170	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . 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 5896	. . . . . . . . . . . . . . . . . . . . . . . . 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 12015	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( i e. ( 0..^ y ) -> ( i + 1 ) e. ( 0 ... y ) )
175	174	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ i e. ( 0..^ y ) ) -> ( i + 1 ) e. ( 0 ... y ) )
176		fvres 5896	. . . . . . . . . . . . . . . . . . . . . . . . . 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 719	. . . . . . . . . . . . . . . . . . . . . . . 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 6324	. . . . . . . . . . . . . . . . . . . . . . 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 2492	. . . . . . . . . . . . . . . . . . . . . 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 2933	. . . . . . . . . . . . . . . . . . . . 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 10967	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. NN -> y e. ZZ )
183		uzid 11181	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ZZ -> y e. ( ZZ>= ` y ) )
184	182, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. NN -> y e. ( ZZ>= ` y ) )
185		peano2uz 11220	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ZZ>= ` y ) -> ( y + 1 ) e. ( ZZ>= ` y ) )
186		fzoss2 11954	. . . . . . . . . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y e. NN /\ p e. (RePart ` ( y + 1 ) ) ) /\ X e. ( ( p ` 0 ) [,) ( p ` y ) ) ) -> ( 0..^ y ) C_ ( 0..^ ( y + 1 ) ) )
189		ssrexv 3526	. . . . . . . . . . . . . . . . . . . . . 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 218	. . . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . 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 198	. . . . . . . . . . . 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 435	. . . . . . . . . 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 435	. . . . . . 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 430	. . . . 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 161	. . . 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 2822	. . 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 435	. 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 10635	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 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1872   A.wral 2771   E.wrex 2772   _Vcvv 3080   [.wsbc 3299   [_csb 3395   C_ wss 3436   {csn 3998   class class class wbr 4423   |` cres 4855   ` cfv 5601  (class class class)co 6306   0cc0 9547   1c1 9548   + caddc 9550   RR*cxr 9682   < clt 9683   <_ cle 9684   NNcn 10617   NN0cn0 10877   ZZcz 10945   ZZ>=cuz 11167   [,)cico 11645   ...cfz 11792  ..^cfzo 11923  RePartciccp 38598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-1st 6808  df-2nd 6809  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-er 7375  df-map 7486  df-en 7582  df-dom 7583  df-sdom 7584  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-nn 10618  df-n0 10878  df-z 10946  df-uz 11168  df-ico 11649  df-fz 11793  df-fzo 11924  df-iccp 38599

This theorem is referenced by:  iccpartiun  38619  icceuelpart  38621  bgoldbtbnd  38775