Metamath Proof Explorer

Theorem iccpartnel

Description: A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 8-Jul-2020)

Ref Expression
Hypotheses iccpartnel.m 
|- ( ph -> M e. NN )
iccpartnel.p 
|- ( ph -> P e. ( RePart ` M ) )
iccpartnel.x 
|- ( ph -> X e. ran P )
Assertion iccpartnel 
|- ( ( ph /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 iccpartnel.m 
 |-  ( ph -> M e. NN )
2 iccpartnel.p 
 |-  ( ph -> P e. ( RePart ` M ) )
3 iccpartnel.x 
 |-  ( ph -> X e. ran P )
4 elioo3g 
 |-  ( X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) <-> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) )
5 iccpart 
 |-  ( M e. NN -> ( P e. ( RePart ` M ) <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )
6 1 5 syl 
 |-  ( ph -> ( P e. ( RePart ` M ) <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )
7 elmapfn 
 |-  ( P e. ( RR* ^m ( 0 ... M ) ) -> P Fn ( 0 ... M ) )
8 7 adantr 
 |-  ( ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) -> P Fn ( 0 ... M ) )
9 6 8 biimtrdi 
 |-  ( ph -> ( P e. ( RePart ` M ) -> P Fn ( 0 ... M ) ) )
10 2 9 mpd 
 |-  ( ph -> P Fn ( 0 ... M ) )
11 fvelrnb 
 |-  ( P Fn ( 0 ... M ) -> ( X e. ran P <-> E. x e. ( 0 ... M ) ( P ` x ) = X ) )
12 10 11 syl 
 |-  ( ph -> ( X e. ran P <-> E. x e. ( 0 ... M ) ( P ` x ) = X ) )
13 3 12 mpbid 
 |-  ( ph -> E. x e. ( 0 ... M ) ( P ` x ) = X )
14 elfzelz 
 |-  ( x e. ( 0 ... M ) -> x e. ZZ )
15 14 zred 
 |-  ( x e. ( 0 ... M ) -> x e. RR )
16 15 adantl 
 |-  ( ( ph /\ x e. ( 0 ... M ) ) -> x e. RR )
17 elfzoelz 
 |-  ( I e. ( 0 ..^ M ) -> I e. ZZ )
18 17 zred 
 |-  ( I e. ( 0 ..^ M ) -> I e. RR )
19 lelttric 
 |-  ( ( x e. RR /\ I e. RR ) -> ( x <_ I \/ I < x ) )
20 16 18 19 syl2an 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( x <_ I \/ I < x ) )
21 breq2 
 |-  ( ( P ` x ) = X -> ( ( P ` I ) < ( P ` x ) <-> ( P ` I ) < X ) )
22 breq1 
 |-  ( ( P ` x ) = X -> ( ( P ` x ) < ( P ` ( I + 1 ) ) <-> X < ( P ` ( I + 1 ) ) ) )
23 21 22 anbi12d 
 |-  ( ( P ` x ) = X -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) <-> ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) )
24 leloe 
 |-  ( ( x e. RR /\ I e. RR ) -> ( x <_ I <-> ( x < I \/ x = I ) ) )
25 16 18 24 syl2an 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( x <_ I <-> ( x < I \/ x = I ) ) )
26 1 2 iccpartgt 
 |-  ( ph -> A. i e. ( 0 ... M ) A. k e. ( 0 ... M ) ( i < k -> ( P ` i ) < ( P ` k ) ) )
27 26 adantr 
 |-  ( ( ph /\ x e. ( 0 ... M ) ) -> A. i e. ( 0 ... M ) A. k e. ( 0 ... M ) ( i < k -> ( P ` i ) < ( P ` k ) ) )
28 27 adantr 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> A. i e. ( 0 ... M ) A. k e. ( 0 ... M ) ( i < k -> ( P ` i ) < ( P ` k ) ) )
29 simpr 
 |-  ( ( ph /\ x e. ( 0 ... M ) ) -> x e. ( 0 ... M ) )
30 elfzofz 
 |-  ( I e. ( 0 ..^ M ) -> I e. ( 0 ... M ) )
31 breq1 
 |-  ( i = x -> ( i < k <-> x < k ) )
32 fveq2 
 |-  ( i = x -> ( P ` i ) = ( P ` x ) )
33 32 breq1d 
 |-  ( i = x -> ( ( P ` i ) < ( P ` k ) <-> ( P ` x ) < ( P ` k ) ) )
34 31 33 imbi12d 
 |-  ( i = x -> ( ( i < k -> ( P ` i ) < ( P ` k ) ) <-> ( x < k -> ( P ` x ) < ( P ` k ) ) ) )
35 breq2 
 |-  ( k = I -> ( x < k <-> x < I ) )
36 fveq2 
 |-  ( k = I -> ( P ` k ) = ( P ` I ) )
37 36 breq2d 
 |-  ( k = I -> ( ( P ` x ) < ( P ` k ) <-> ( P ` x ) < ( P ` I ) ) )
38 35 37 imbi12d 
 |-  ( k = I -> ( ( x < k -> ( P ` x ) < ( P ` k ) ) <-> ( x < I -> ( P ` x ) < ( P ` I ) ) ) )
39 34 38 rspc2v 
 |-  ( ( x e. ( 0 ... M ) /\ I e. ( 0 ... M ) ) -> ( A. i e. ( 0 ... M ) A. k e. ( 0 ... M ) ( i < k -> ( P ` i ) < ( P ` k ) ) -> ( x < I -> ( P ` x ) < ( P ` I ) ) ) )
40 29 30 39 syl2an 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( A. i e. ( 0 ... M ) A. k e. ( 0 ... M ) ( i < k -> ( P ` i ) < ( P ` k ) ) -> ( x < I -> ( P ` x ) < ( P ` I ) ) ) )
41 28 40 mpd 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( x < I -> ( P ` x ) < ( P ` I ) ) )
42 pm3.35 
 |-  ( ( x < I /\ ( x < I -> ( P ` x ) < ( P ` I ) ) ) -> ( P ` x ) < ( P ` I ) )
43 1 adantr 
 |-  ( ( ph /\ x e. ( 0 ... M ) ) -> M e. NN )
44 2 adantr 
 |-  ( ( ph /\ x e. ( 0 ... M ) ) -> P e. ( RePart ` M ) )
45 43 44 29 iccpartxr 
 |-  ( ( ph /\ x e. ( 0 ... M ) ) -> ( P ` x ) e. RR* )
46 45 adantr 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( P ` x ) e. RR* )
47 simp1 
 |-  ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( P ` I ) e. RR* )
48 xrltle 
 |-  ( ( ( P ` x ) e. RR* /\ ( P ` I ) e. RR* ) -> ( ( P ` x ) < ( P ` I ) -> ( P ` x ) <_ ( P ` I ) ) )
49 46 47 48 syl2anr 
 |-  ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) ) -> ( ( P ` x ) < ( P ` I ) -> ( P ` x ) <_ ( P ` I ) ) )
50 xrlenlt 
 |-  ( ( ( P ` x ) e. RR* /\ ( P ` I ) e. RR* ) -> ( ( P ` x ) <_ ( P ` I ) <-> -. ( P ` I ) < ( P ` x ) ) )
51 46 47 50 syl2anr 
 |-  ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) ) -> ( ( P ` x ) <_ ( P ` I ) <-> -. ( P ` I ) < ( P ` x ) ) )
52 49 51 sylibd 
 |-  ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) ) -> ( ( P ` x ) < ( P ` I ) -> -. ( P ` I ) < ( P ` x ) ) )
53 52 ex 
 |-  ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( P ` x ) < ( P ` I ) -> -. ( P ` I ) < ( P ` x ) ) ) )
54 53 com13 
 |-  ( ( P ` x ) < ( P ` I ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> -. ( P ` I ) < ( P ` x ) ) ) )
55 54 imp 
 |-  ( ( ( P ` x ) < ( P ` I ) /\ ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> -. ( P ` I ) < ( P ` x ) ) )
56 55 imp 
 |-  ( ( ( ( P ` x ) < ( P ` I ) /\ ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) ) /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) -> -. ( P ` I ) < ( P ` x ) )
57 56 pm2.21d 
 |-  ( ( ( ( P ` x ) < ( P ` I ) /\ ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) ) /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
58 57 ex 
 |-  ( ( ( P ` x ) < ( P ` I ) /\ ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) )
59 58 ex 
 |-  ( ( P ` x ) < ( P ` I ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
60 42 59 syl 
 |-  ( ( x < I /\ ( x < I -> ( P ` x ) < ( P ` I ) ) ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
61 60 ex 
 |-  ( x < I -> ( ( x < I -> ( P ` x ) < ( P ` I ) ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
62 61 com13 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( x < I -> ( P ` x ) < ( P ` I ) ) -> ( x < I -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
63 41 62 mpd 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( x < I -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
64 63 com12 
 |-  ( x < I -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
65 fveq2 
 |-  ( x = I -> ( P ` x ) = ( P ` I ) )
66 65 breq2d 
 |-  ( x = I -> ( ( P ` I ) < ( P ` x ) <-> ( P ` I ) < ( P ` I ) ) )
67 66 adantr 
 |-  ( ( x = I /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) -> ( ( P ` I ) < ( P ` x ) <-> ( P ` I ) < ( P ` I ) ) )
68 xrltnr 
 |-  ( ( P ` I ) e. RR* -> -. ( P ` I ) < ( P ` I ) )
69 68 3ad2ant1 
 |-  ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> -. ( P ` I ) < ( P ` I ) )
70 69 adantl 
 |-  ( ( x = I /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) -> -. ( P ` I ) < ( P ` I ) )
71 70 pm2.21d 
 |-  ( ( x = I /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) -> ( ( P ` I ) < ( P ` I ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
72 67 71 sylbid 
 |-  ( ( x = I /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
73 72 ex 
 |-  ( x = I -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) )
74 73 a1d 
 |-  ( x = I -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
75 64 74 jaoi 
 |-  ( ( x < I \/ x = I ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
76 75 com12 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( x < I \/ x = I ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
77 25 76 sylbid 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( x <_ I -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
78 77 com23 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( x <_ I -> ( ( P ` I ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
79 78 com14 
 |-  ( ( P ` I ) < ( P ` x ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( x <_ I -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
80 79 adantr 
 |-  ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( x <_ I -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
81 23 80 biimtrrdi 
 |-  ( ( P ` x ) = X -> ( ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( x <_ I -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
82 81 com14 
 |-  ( x <_ I -> ( ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` x ) = X -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
83 82 com23 
 |-  ( x <_ I -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) -> ( ( P ` x ) = X -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
84 83 impd 
 |-  ( x <_ I -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> ( ( P ` x ) = X -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
85 84 com24 
 |-  ( x <_ I -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( P ` x ) = X -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
86 14 adantl 
 |-  ( ( ph /\ x e. ( 0 ... M ) ) -> x e. ZZ )
87 zltp1le 
 |-  ( ( I e. ZZ /\ x e. ZZ ) -> ( I < x <-> ( I + 1 ) <_ x ) )
88 17 86 87 syl2anr 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( I < x <-> ( I + 1 ) <_ x ) )
89 17 peano2zd 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ZZ )
90 89 zred 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. RR )
91 leloe 
 |-  ( ( ( I + 1 ) e. RR /\ x e. RR ) -> ( ( I + 1 ) <_ x <-> ( ( I + 1 ) < x \/ ( I + 1 ) = x ) ) )
92 90 16 91 syl2anr 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( I + 1 ) <_ x <-> ( ( I + 1 ) < x \/ ( I + 1 ) = x ) ) )
93 88 92 bitrd 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( I < x <-> ( ( I + 1 ) < x \/ ( I + 1 ) = x ) ) )
94 fzofzp1 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
95 breq1 
 |-  ( i = ( I + 1 ) -> ( i < k <-> ( I + 1 ) < k ) )
96 fveq2 
 |-  ( i = ( I + 1 ) -> ( P ` i ) = ( P ` ( I + 1 ) ) )
97 96 breq1d 
 |-  ( i = ( I + 1 ) -> ( ( P ` i ) < ( P ` k ) <-> ( P ` ( I + 1 ) ) < ( P ` k ) ) )
98 95 97 imbi12d 
 |-  ( i = ( I + 1 ) -> ( ( i < k -> ( P ` i ) < ( P ` k ) ) <-> ( ( I + 1 ) < k -> ( P ` ( I + 1 ) ) < ( P ` k ) ) ) )
99 breq2 
 |-  ( k = x -> ( ( I + 1 ) < k <-> ( I + 1 ) < x ) )
100 fveq2 
 |-  ( k = x -> ( P ` k ) = ( P ` x ) )
101 100 breq2d 
 |-  ( k = x -> ( ( P ` ( I + 1 ) ) < ( P ` k ) <-> ( P ` ( I + 1 ) ) < ( P ` x ) ) )
102 99 101 imbi12d 
 |-  ( k = x -> ( ( ( I + 1 ) < k -> ( P ` ( I + 1 ) ) < ( P ` k ) ) <-> ( ( I + 1 ) < x -> ( P ` ( I + 1 ) ) < ( P ` x ) ) ) )
103 98 102 rspc2v 
 |-  ( ( ( I + 1 ) e. ( 0 ... M ) /\ x e. ( 0 ... M ) ) -> ( A. i e. ( 0 ... M ) A. k e. ( 0 ... M ) ( i < k -> ( P ` i ) < ( P ` k ) ) -> ( ( I + 1 ) < x -> ( P ` ( I + 1 ) ) < ( P ` x ) ) ) )
104 94 29 103 syl2anr 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( A. i e. ( 0 ... M ) A. k e. ( 0 ... M ) ( i < k -> ( P ` i ) < ( P ` k ) ) -> ( ( I + 1 ) < x -> ( P ` ( I + 1 ) ) < ( P ` x ) ) ) )
105 28 104 mpd 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( I + 1 ) < x -> ( P ` ( I + 1 ) ) < ( P ` x ) ) )
106 pm3.35 
 |-  ( ( ( I + 1 ) < x /\ ( ( I + 1 ) < x -> ( P ` ( I + 1 ) ) < ( P ` x ) ) ) -> ( P ` ( I + 1 ) ) < ( P ` x ) )
107 simp2 
 |-  ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( P ` ( I + 1 ) ) e. RR* )
108 xrltnsym 
 |-  ( ( ( P ` x ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* ) -> ( ( P ` x ) < ( P ` ( I + 1 ) ) -> -. ( P ` ( I + 1 ) ) < ( P ` x ) ) )
109 46 107 108 syl2an 
 |-  ( ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) -> ( ( P ` x ) < ( P ` ( I + 1 ) ) -> -. ( P ` ( I + 1 ) ) < ( P ` x ) ) )
110 109 imp 
 |-  ( ( ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. ( P ` ( I + 1 ) ) < ( P ` x ) )
111 110 pm2.21d 
 |-  ( ( ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> ( ( P ` ( I + 1 ) ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
112 111 expcom 
 |-  ( ( P ` x ) < ( P ` ( I + 1 ) ) -> ( ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) /\ ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) ) -> ( ( P ` ( I + 1 ) ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) )
113 112 expd 
 |-  ( ( P ` x ) < ( P ` ( I + 1 ) ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` ( I + 1 ) ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
114 113 adantl 
 |-  ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` ( I + 1 ) ) < ( P ` x ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
115 114 com14 
 |-  ( ( P ` ( I + 1 ) ) < ( P ` x ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
116 106 115 syl 
 |-  ( ( ( I + 1 ) < x /\ ( ( I + 1 ) < x -> ( P ` ( I + 1 ) ) < ( P ` x ) ) ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
117 116 ex 
 |-  ( ( I + 1 ) < x -> ( ( ( I + 1 ) < x -> ( P ` ( I + 1 ) ) < ( P ` x ) ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
118 117 com13 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( I + 1 ) < x -> ( P ` ( I + 1 ) ) < ( P ` x ) ) -> ( ( I + 1 ) < x -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
119 105 118 mpd 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( I + 1 ) < x -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
120 119 com12 
 |-  ( ( I + 1 ) < x -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
121 fveq2 
 |-  ( ( I + 1 ) = x -> ( P ` ( I + 1 ) ) = ( P ` x ) )
122 121 breq2d 
 |-  ( ( I + 1 ) = x -> ( ( P ` I ) < ( P ` ( I + 1 ) ) <-> ( P ` I ) < ( P ` x ) ) )
123 121 breq1d 
 |-  ( ( I + 1 ) = x -> ( ( P ` ( I + 1 ) ) < ( P ` ( I + 1 ) ) <-> ( P ` x ) < ( P ` ( I + 1 ) ) ) )
124 122 123 anbi12d 
 |-  ( ( I + 1 ) = x -> ( ( ( P ` I ) < ( P ` ( I + 1 ) ) /\ ( P ` ( I + 1 ) ) < ( P ` ( I + 1 ) ) ) <-> ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) ) )
125 xrltnr 
 |-  ( ( P ` ( I + 1 ) ) e. RR* -> -. ( P ` ( I + 1 ) ) < ( P ` ( I + 1 ) ) )
126 125 3ad2ant2 
 |-  ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> -. ( P ` ( I + 1 ) ) < ( P ` ( I + 1 ) ) )
127 126 pm2.21d 
 |-  ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` ( I + 1 ) ) < ( P ` ( I + 1 ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
128 127 com12 
 |-  ( ( P ` ( I + 1 ) ) < ( P ` ( I + 1 ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
129 128 adantl 
 |-  ( ( ( P ` I ) < ( P ` ( I + 1 ) ) /\ ( P ` ( I + 1 ) ) < ( P ` ( I + 1 ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
130 124 129 biimtrrdi 
 |-  ( ( I + 1 ) = x -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) )
131 130 com23 
 |-  ( ( I + 1 ) = x -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) )
132 131 a1d 
 |-  ( ( I + 1 ) = x -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
133 120 132 jaoi 
 |-  ( ( ( I + 1 ) < x \/ ( I + 1 ) = x ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
134 133 com12 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( I + 1 ) < x \/ ( I + 1 ) = x ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
135 93 134 sylbid 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( I < x -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
136 135 com23 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( I < x -> ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
137 136 com14 
 |-  ( ( ( P ` I ) < ( P ` x ) /\ ( P ` x ) < ( P ` ( I + 1 ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( I < x -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
138 23 137 biimtrrdi 
 |-  ( ( P ` x ) = X -> ( ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( I < x -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
139 138 com14 
 |-  ( I < x -> ( ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( P ` x ) = X -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
140 139 com23 
 |-  ( I < x -> ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) -> ( ( P ` x ) = X -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) ) )
141 140 impd 
 |-  ( I < x -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> ( ( P ` x ) = X -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
142 141 com24 
 |-  ( I < x -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( P ` x ) = X -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
143 85 142 jaoi 
 |-  ( ( x <_ I \/ I < x ) -> ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( P ` x ) = X -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
144 143 com12 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( x <_ I \/ I < x ) -> ( ( P ` x ) = X -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
145 20 144 mpd 
 |-  ( ( ( ph /\ x e. ( 0 ... M ) ) /\ I e. ( 0 ..^ M ) ) -> ( ( P ` x ) = X -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) )
146 145 ex 
 |-  ( ( ph /\ x e. ( 0 ... M ) ) -> ( I e. ( 0 ..^ M ) -> ( ( P ` x ) = X -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
147 146 com23 
 |-  ( ( ph /\ x e. ( 0 ... M ) ) -> ( ( P ` x ) = X -> ( I e. ( 0 ..^ M ) -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
148 147 rexlimdva 
 |-  ( ph -> ( E. x e. ( 0 ... M ) ( P ` x ) = X -> ( I e. ( 0 ..^ M ) -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) ) )
149 13 148 mpd 
 |-  ( ph -> ( I e. ( 0 ..^ M ) -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) ) )
150 149 imp 
 |-  ( ( ph /\ I e. ( 0 ..^ M ) ) -> ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
151 150 com12 
 |-  ( ( ( ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( P ` I ) < X /\ X < ( P ` ( I + 1 ) ) ) ) -> ( ( ph /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
152 4 151 sylbi 
 |-  ( X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) -> ( ( ph /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
153 ax-1 
 |-  ( -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) -> ( ( ph /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) ) )
154 152 153 pm2.61i 
 |-  ( ( ph /\ I e. ( 0 ..^ M ) ) -> -. X e. ( ( P ` I ) (,) ( P ` ( I + 1 ) ) ) )