Metamath Proof Explorer

Theorem fourierdlem65

Description: The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem65.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem65.t 
|- T = ( B - A )
fourierdlem65.m 
|- ( ph -> M e. NN )
fourierdlem65.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem65.c 
|- ( ph -> C e. RR )
fourierdlem65.d 
|- ( ph -> D e. ( C (,) +oo ) )
fourierdlem65.o 
|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem65.n 
|- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
fourierdlem65.s 
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
fourierdlem65.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem65.l 
|- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
fourierdlem65.z 
|- Z = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )
Assertion fourierdlem65 
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem65.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
2 fourierdlem65.t 
 |-  T = ( B - A )
3 fourierdlem65.m 
 |-  ( ph -> M e. NN )
4 fourierdlem65.q 
 |-  ( ph -> Q e. ( P ` M ) )
5 fourierdlem65.c 
 |-  ( ph -> C e. RR )
6 fourierdlem65.d 
 |-  ( ph -> D e. ( C (,) +oo ) )
7 fourierdlem65.o 
 |-  O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
8 fourierdlem65.n 
 |-  N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
9 fourierdlem65.s 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
10 fourierdlem65.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
11 fourierdlem65.l 
 |-  L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
12 fourierdlem65.z 
 |-  Z = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )
13 11 a1i 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) )
14 simpr 
 |-  ( ( ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> y = ( E ` ( S ` j ) ) )
15 simpl 
 |-  ( ( ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> ( E ` ( S ` j ) ) = B )
16 14 15 eqtrd 
 |-  ( ( ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> y = B )
17 16 iftrued 
 |-  ( ( ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = A )
18 17 adantll 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = A )
19 1 3 4 fourierdlem11 
 |-  ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
20 19 simp1d 
 |-  ( ph -> A e. RR )
21 19 simp2d 
 |-  ( ph -> B e. RR )
22 19 simp3d 
 |-  ( ph -> A < B )
23 20 21 22 2 10 fourierdlem4 
 |-  ( ph -> E : RR --> ( A (,] B ) )
24 23 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> E : RR --> ( A (,] B ) )
25 ioossre 
 |-  ( C (,) +oo ) C_ RR
26 25 6 sselid 
 |-  ( ph -> D e. RR )
27 5 rexrd 
 |-  ( ph -> C e. RR* )
28 pnfxr 
 |-  +oo e. RR*
29 28 a1i 
 |-  ( ph -> +oo e. RR* )
30 ioogtlb 
 |-  ( ( C e. RR* /\ +oo e. RR* /\ D e. ( C (,) +oo ) ) -> C < D )
31 27 29 6 30 syl3anc 
 |-  ( ph -> C < D )
32 id 
 |-  ( y = x -> y = x )
33 2 eqcomi 
 |-  ( B - A ) = T
34 33 oveq2i 
 |-  ( k x. ( B - A ) ) = ( k x. T )
35 34 a1i 
 |-  ( y = x -> ( k x. ( B - A ) ) = ( k x. T ) )
36 32 35 oveq12d 
 |-  ( y = x -> ( y + ( k x. ( B - A ) ) ) = ( x + ( k x. T ) ) )
37 36 eleq1d 
 |-  ( y = x -> ( ( y + ( k x. ( B - A ) ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
38 37 rexbidv 
 |-  ( y = x -> ( E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q <-> E. k e. ZZ ( x + ( k x. T ) ) e. ran Q ) )
39 38 cbvrabv 
 |-  { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } = { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q }
40 39 uneq2i 
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
41 2 1 3 4 5 26 31 7 40 8 9 fourierdlem54 
 |-  ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) ) )
42 41 simpld 
 |-  ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
43 42 simprd 
 |-  ( ph -> S e. ( O ` N ) )
44 42 simpld 
 |-  ( ph -> N e. NN )
45 7 fourierdlem2 
 |-  ( N e. NN -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
46 44 45 syl 
 |-  ( ph -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
47 43 46 mpbid 
 |-  ( ph -> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
48 47 simpld 
 |-  ( ph -> S e. ( RR ^m ( 0 ... N ) ) )
49 elmapi 
 |-  ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
50 48 49 syl 
 |-  ( ph -> S : ( 0 ... N ) --> RR )
51 50 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> S : ( 0 ... N ) --> RR )
52 elfzofz 
 |-  ( j e. ( 0 ..^ N ) -> j e. ( 0 ... N ) )
53 52 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ... N ) )
54 51 53 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. RR )
55 24 54 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) e. ( A (,] B ) )
56 55 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) e. ( A (,] B ) )
57 20 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> A e. RR )
58 13 18 56 57 fvmptd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( L ` ( E ` ( S ` j ) ) ) = A )
59 58 oveq2d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( j + 1 ) ) ) - A ) )
60 21 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> B e. RR )
61 22 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> A < B )
62 54 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` j ) e. RR )
63 simpr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) = B )
64 fzofzp1 
 |-  ( j e. ( 0 ..^ N ) -> ( j + 1 ) e. ( 0 ... N ) )
65 64 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( j + 1 ) e. ( 0 ... N ) )
66 51 65 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. RR )
67 66 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` ( j + 1 ) ) e. RR )
68 elfzoelz 
 |-  ( j e. ( 0 ..^ N ) -> j e. ZZ )
69 68 zred 
 |-  ( j e. ( 0 ..^ N ) -> j e. RR )
70 69 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. RR )
71 70 ltp1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> j < ( j + 1 ) )
72 41 simprd 
 |-  ( ph -> S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
73 72 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
74 isorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) /\ ( j e. ( 0 ... N ) /\ ( j + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
75 73 53 65 74 syl12anc 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
76 71 75 mpbid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) < ( S ` ( j + 1 ) ) )
77 76 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` j ) < ( S ` ( j + 1 ) ) )
78 isof1o 
 |-  ( S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) -> S : ( 0 ... N ) -1-1-onto-> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
79 f1ofo 
 |-  ( S : ( 0 ... N ) -1-1-onto-> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) -> S : ( 0 ... N ) -onto-> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
80 72 78 79 3syl 
 |-  ( ph -> S : ( 0 ... N ) -onto-> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
81 80 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> S : ( 0 ... N ) -onto-> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
82 5 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> C e. RR )
83 26 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> D e. RR )
84 21 20 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
85 2 84 eqeltrid 
 |-  ( ph -> T e. RR )
86 85 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> T e. RR )
87 54 86 readdcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + T ) e. RR )
88 87 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) e. RR )
89 5 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> C e. RR )
90 7 44 43 fourierdlem15 
 |-  ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
91 90 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> S : ( 0 ... N ) --> ( C [,] D ) )
92 91 53 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. ( C [,] D ) )
93 26 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> D e. RR )
94 elicc2 
 |-  ( ( C e. RR /\ D e. RR ) -> ( ( S ` j ) e. ( C [,] D ) <-> ( ( S ` j ) e. RR /\ C <_ ( S ` j ) /\ ( S ` j ) <_ D ) ) )
95 89 93 94 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) e. ( C [,] D ) <-> ( ( S ` j ) e. RR /\ C <_ ( S ` j ) /\ ( S ` j ) <_ D ) ) )
96 92 95 mpbid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) e. RR /\ C <_ ( S ` j ) /\ ( S ` j ) <_ D ) )
97 96 simp2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> C <_ ( S ` j ) )
98 20 21 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
99 22 98 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
100 99 2 breqtrrdi 
 |-  ( ph -> 0 < T )
101 85 100 elrpd 
 |-  ( ph -> T e. RR+ )
102 101 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> T e. RR+ )
103 54 102 ltaddrpd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) < ( ( S ` j ) + T ) )
104 89 54 87 97 103 lelttrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> C < ( ( S ` j ) + T ) )
105 89 87 104 ltled 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> C <_ ( ( S ` j ) + T ) )
106 105 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> C <_ ( ( S ` j ) + T ) )
107 66 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( S ` ( j + 1 ) ) e. RR )
108 simpr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) )
109 88 107 ltnled 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( ( S ` j ) + T ) < ( S ` ( j + 1 ) ) <-> -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) )
110 108 109 mpbird 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) < ( S ` ( j + 1 ) ) )
111 91 65 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. ( C [,] D ) )
112 elicc2 
 |-  ( ( C e. RR /\ D e. RR ) -> ( ( S ` ( j + 1 ) ) e. ( C [,] D ) <-> ( ( S ` ( j + 1 ) ) e. RR /\ C <_ ( S ` ( j + 1 ) ) /\ ( S ` ( j + 1 ) ) <_ D ) ) )
113 89 93 112 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` ( j + 1 ) ) e. ( C [,] D ) <-> ( ( S ` ( j + 1 ) ) e. RR /\ C <_ ( S ` ( j + 1 ) ) /\ ( S ` ( j + 1 ) ) <_ D ) ) )
114 111 113 mpbid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` ( j + 1 ) ) e. RR /\ C <_ ( S ` ( j + 1 ) ) /\ ( S ` ( j + 1 ) ) <_ D ) )
115 114 simp3d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) <_ D )
116 115 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( S ` ( j + 1 ) ) <_ D )
117 88 107 83 110 116 ltletrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) < D )
118 88 83 117 ltled 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) <_ D )
119 82 83 88 106 118 eliccd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) e. ( C [,] D ) )
120 119 adantlr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) e. ( C [,] D ) )
121 10 a1i 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
122 id 
 |-  ( x = ( S ` j ) -> x = ( S ` j ) )
123 oveq2 
 |-  ( x = ( S ` j ) -> ( B - x ) = ( B - ( S ` j ) ) )
124 123 oveq1d 
 |-  ( x = ( S ` j ) -> ( ( B - x ) / T ) = ( ( B - ( S ` j ) ) / T ) )
125 124 fveq2d 
 |-  ( x = ( S ` j ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` j ) ) / T ) ) )
126 125 oveq1d 
 |-  ( x = ( S ` j ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) )
127 122 126 oveq12d 
 |-  ( x = ( S ` j ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) )
128 127 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ x = ( S ` j ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) )
129 21 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> B e. RR )
130 129 54 resubcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( S ` j ) ) e. RR )
131 130 102 rerpdivcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( S ` j ) ) / T ) e. RR )
132 131 flcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` j ) ) / T ) ) e. ZZ )
133 132 zred 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` j ) ) / T ) ) e. RR )
134 133 86 remulcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) e. RR )
135 54 134 readdcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) e. RR )
136 121 128 54 135 fvmptd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) = ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) )
137 136 oveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` j ) ) - ( S ` j ) ) = ( ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) - ( S ` j ) ) )
138 137 oveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) = ( ( ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) - ( S ` j ) ) / T ) )
139 54 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. CC )
140 134 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) e. CC )
141 139 140 pncan2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) - ( S ` j ) ) = ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) )
142 141 oveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) - ( S ` j ) ) / T ) = ( ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) / T ) )
143 133 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` j ) ) / T ) ) e. CC )
144 86 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> T e. CC )
145 102 rpne0d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> T =/= 0 )
146 143 144 145 divcan4d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - ( S ` j ) ) / T ) ) )
147 138 142 146 3eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) = ( |_ ` ( ( B - ( S ` j ) ) / T ) ) )
148 147 132 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) e. ZZ )
149 peano2zm 
 |-  ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) e. ZZ -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) e. ZZ )
150 148 149 syl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) e. ZZ )
151 150 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) e. ZZ )
152 33 oveq2i 
 |-  ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) = ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. T )
153 152 oveq2i 
 |-  ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) ) = ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. T ) )
154 153 a1i 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) ) = ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. T ) ) )
155 136 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) = ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) )
156 oveq1 
 |-  ( ( E ` ( S ` j ) ) = B -> ( ( E ` ( S ` j ) ) - ( S ` j ) ) = ( B - ( S ` j ) ) )
157 156 eqcomd 
 |-  ( ( E ` ( S ` j ) ) = B -> ( B - ( S ` j ) ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
158 157 oveq1d 
 |-  ( ( E ` ( S ` j ) ) = B -> ( ( B - ( S ` j ) ) / T ) = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) )
159 158 fveq2d 
 |-  ( ( E ` ( S ` j ) ) = B -> ( |_ ` ( ( B - ( S ` j ) ) / T ) ) = ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) )
160 159 oveq1d 
 |-  ( ( E ` ( S ` j ) ) = B -> ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) = ( ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) x. T ) )
161 160 oveq2d 
 |-  ( ( E ` ( S ` j ) ) = B -> ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) = ( ( S ` j ) + ( ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) x. T ) ) )
162 161 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) = ( ( S ` j ) + ( ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) x. T ) ) )
163 147 143 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) e. CC )
164 1cnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> 1 e. CC )
165 163 164 144 subdird 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. T ) = ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) - ( 1 x. T ) ) )
166 85 recnd 
 |-  ( ph -> T e. CC )
167 166 mullidd 
 |-  ( ph -> ( 1 x. T ) = T )
168 167 oveq2d 
 |-  ( ph -> ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) - ( 1 x. T ) ) = ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) - T ) )
169 168 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) - ( 1 x. T ) ) = ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) - T ) )
170 165 169 eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. T ) = ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) - T ) )
171 170 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. T ) ) = ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) - T ) ) )
172 163 144 mulcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) e. CC )
173 139 144 172 ppncand 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) - T ) ) = ( ( S ` j ) + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) ) )
174 flid 
 |-  ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) e. ZZ -> ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) )
175 148 174 syl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) )
176 175 eqcomd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) = ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) )
177 176 oveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) = ( ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) x. T ) )
178 177 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) ) = ( ( S ` j ) + ( ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) x. T ) ) )
179 171 173 178 3eqtrrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) x. T ) ) = ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. T ) ) )
180 179 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( S ` j ) + ( ( |_ ` ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) ) x. T ) ) = ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. T ) ) )
181 155 162 180 3eqtrrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. T ) ) = ( E ` ( S ` j ) ) )
182 154 181 63 3eqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) ) = B )
183 1 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
184 3 183 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
185 4 184 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
186 185 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
187 186 simpld 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
188 187 simprd 
 |-  ( ph -> ( Q ` M ) = B )
189 188 eqcomd 
 |-  ( ph -> B = ( Q ` M ) )
190 1 3 4 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
191 ffn 
 |-  ( Q : ( 0 ... M ) --> ( A [,] B ) -> Q Fn ( 0 ... M ) )
192 190 191 syl 
 |-  ( ph -> Q Fn ( 0 ... M ) )
193 3 nnnn0d 
 |-  ( ph -> M e. NN0 )
194 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
195 193 194 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
196 eluzfz2 
 |-  ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
197 195 196 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
198 fnfvelrn 
 |-  ( ( Q Fn ( 0 ... M ) /\ M e. ( 0 ... M ) ) -> ( Q ` M ) e. ran Q )
199 192 197 198 syl2anc 
 |-  ( ph -> ( Q ` M ) e. ran Q )
200 189 199 eqeltrd 
 |-  ( ph -> B e. ran Q )
201 200 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> B e. ran Q )
202 182 201 eqeltrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) ) e. ran Q )
203 202 adantr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) ) e. ran Q )
204 oveq1 
 |-  ( k = ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) -> ( k x. ( B - A ) ) = ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) )
205 204 oveq2d 
 |-  ( k = ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) -> ( ( ( S ` j ) + T ) + ( k x. ( B - A ) ) ) = ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) ) )
206 205 eleq1d 
 |-  ( k = ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) -> ( ( ( ( S ` j ) + T ) + ( k x. ( B - A ) ) ) e. ran Q <-> ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) ) e. ran Q ) )
207 206 rspcev 
 |-  ( ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) e. ZZ /\ ( ( ( S ` j ) + T ) + ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) - 1 ) x. ( B - A ) ) ) e. ran Q ) -> E. k e. ZZ ( ( ( S ` j ) + T ) + ( k x. ( B - A ) ) ) e. ran Q )
208 151 203 207 syl2anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> E. k e. ZZ ( ( ( S ` j ) + T ) + ( k x. ( B - A ) ) ) e. ran Q )
209 oveq1 
 |-  ( y = ( ( S ` j ) + T ) -> ( y + ( k x. ( B - A ) ) ) = ( ( ( S ` j ) + T ) + ( k x. ( B - A ) ) ) )
210 209 eleq1d 
 |-  ( y = ( ( S ` j ) + T ) -> ( ( y + ( k x. ( B - A ) ) ) e. ran Q <-> ( ( ( S ` j ) + T ) + ( k x. ( B - A ) ) ) e. ran Q ) )
211 210 rexbidv 
 |-  ( y = ( ( S ` j ) + T ) -> ( E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q <-> E. k e. ZZ ( ( ( S ` j ) + T ) + ( k x. ( B - A ) ) ) e. ran Q ) )
212 211 elrab 
 |-  ( ( ( S ` j ) + T ) e. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } <-> ( ( ( S ` j ) + T ) e. ( C [,] D ) /\ E. k e. ZZ ( ( ( S ` j ) + T ) + ( k x. ( B - A ) ) ) e. ran Q ) )
213 120 208 212 sylanbrc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) e. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } )
214 elun2 
 |-  ( ( ( S ` j ) + T ) e. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } -> ( ( S ` j ) + T ) e. ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
215 213 214 syl 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) e. ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
216 foelrn 
 |-  ( ( S : ( 0 ... N ) -onto-> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) /\ ( ( S ` j ) + T ) e. ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) -> E. i e. ( 0 ... N ) ( ( S ` j ) + T ) = ( S ` i ) )
217 81 215 216 syl2anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> E. i e. ( 0 ... N ) ( ( S ` j ) + T ) = ( S ` i ) )
218 eqcom 
 |-  ( ( ( S ` j ) + T ) = ( S ` i ) <-> ( S ` i ) = ( ( S ` j ) + T ) )
219 218 rexbii 
 |-  ( E. i e. ( 0 ... N ) ( ( S ` j ) + T ) = ( S ` i ) <-> E. i e. ( 0 ... N ) ( S ` i ) = ( ( S ` j ) + T ) )
220 217 219 sylib 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> E. i e. ( 0 ... N ) ( S ` i ) = ( ( S ` j ) + T ) )
221 103 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( S ` j ) < ( ( S ` j ) + T ) )
222 218 biimpri 
 |-  ( ( S ` i ) = ( ( S ` j ) + T ) -> ( ( S ` j ) + T ) = ( S ` i ) )
223 222 adantl 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) = ( S ` i ) )
224 221 223 breqtrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( S ` j ) < ( S ` i ) )
225 110 adantr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) < ( S ` ( j + 1 ) ) )
226 223 225 eqbrtrrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( S ` i ) < ( S ` ( j + 1 ) ) )
227 224 226 jca 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
228 227 adantlr 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
229 simplll 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( ph /\ j e. ( 0 ..^ N ) ) )
230 simplr 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> i e. ( 0 ... N ) )
231 elfzelz 
 |-  ( i e. ( 0 ... N ) -> i e. ZZ )
232 231 ad2antlr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> i e. ZZ )
233 68 ad3antlr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> j e. ZZ )
234 simpr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> ( S ` j ) < ( S ` i ) )
235 73 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
236 53 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> j e. ( 0 ... N ) )
237 simplr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> i e. ( 0 ... N ) )
238 isorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) /\ ( j e. ( 0 ... N ) /\ i e. ( 0 ... N ) ) ) -> ( j < i <-> ( S ` j ) < ( S ` i ) ) )
239 235 236 237 238 syl12anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> ( j < i <-> ( S ` j ) < ( S ` i ) ) )
240 234 239 mpbird 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> j < i )
241 240 adantrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> j < i )
242 simpr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> ( S ` i ) < ( S ` ( j + 1 ) ) )
243 73 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
244 simplr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> i e. ( 0 ... N ) )
245 65 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> ( j + 1 ) e. ( 0 ... N ) )
246 isorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) /\ ( i e. ( 0 ... N ) /\ ( j + 1 ) e. ( 0 ... N ) ) ) -> ( i < ( j + 1 ) <-> ( S ` i ) < ( S ` ( j + 1 ) ) ) )
247 243 244 245 246 syl12anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> ( i < ( j + 1 ) <-> ( S ` i ) < ( S ` ( j + 1 ) ) ) )
248 242 247 mpbird 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> i < ( j + 1 ) )
249 248 adantrl 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> i < ( j + 1 ) )
250 btwnnz 
 |-  ( ( j e. ZZ /\ j < i /\ i < ( j + 1 ) ) -> -. i e. ZZ )
251 233 241 249 250 syl3anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> -. i e. ZZ )
252 232 251 pm2.65da 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) -> -. ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
253 229 230 252 syl2anc 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> -. ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
254 228 253 pm2.65da 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ i e. ( 0 ... N ) ) -> -. ( S ` i ) = ( ( S ` j ) + T ) )
255 254 nrexdv 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> -. E. i e. ( 0 ... N ) ( S ` i ) = ( ( S ` j ) + T ) )
256 255 adantlr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> -. E. i e. ( 0 ... N ) ( S ` i ) = ( ( S ` j ) + T ) )
257 220 256 condan 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) )
258 62 rexrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` j ) e. RR* )
259 85 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> T e. RR )
260 62 259 readdcld 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( S ` j ) + T ) e. RR )
261 elioc2 
 |-  ( ( ( S ` j ) e. RR* /\ ( ( S ` j ) + T ) e. RR ) -> ( ( S ` ( j + 1 ) ) e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) <-> ( ( S ` ( j + 1 ) ) e. RR /\ ( S ` j ) < ( S ` ( j + 1 ) ) /\ ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) ) )
262 258 260 261 syl2anc 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( S ` ( j + 1 ) ) e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) <-> ( ( S ` ( j + 1 ) ) e. RR /\ ( S ` j ) < ( S ` ( j + 1 ) ) /\ ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) ) )
263 67 77 257 262 mpbir3and 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` ( j + 1 ) ) e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) )
264 57 60 61 2 10 62 63 263 fourierdlem26 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` ( j + 1 ) ) ) = ( A + ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) )
265 264 oveq1d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - A ) = ( ( A + ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) - A ) )
266 57 recnd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> A e. CC )
267 66 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. CC )
268 267 139 subcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. CC )
269 268 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. CC )
270 266 269 pncan2d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( A + ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) - A ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
271 59 265 270 3eqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
272 11 a1i 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) )
273 eqcom 
 |-  ( y = ( E ` ( S ` j ) ) <-> ( E ` ( S ` j ) ) = y )
274 273 biimpi 
 |-  ( y = ( E ` ( S ` j ) ) -> ( E ` ( S ` j ) ) = y )
275 274 adantl 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> ( E ` ( S ` j ) ) = y )
276 neqne 
 |-  ( -. ( E ` ( S ` j ) ) = B -> ( E ` ( S ` j ) ) =/= B )
277 276 adantr 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> ( E ` ( S ` j ) ) =/= B )
278 275 277 eqnetrrd 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> y =/= B )
279 278 neneqd 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> -. y = B )
280 279 iffalsed 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = y )
281 simpr 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> y = ( E ` ( S ` j ) ) )
282 280 281 eqtrd 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = ( E ` ( S ` j ) ) )
283 282 adantll 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = ( E ` ( S ` j ) ) )
284 55 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) e. ( A (,] B ) )
285 272 283 284 284 fvmptd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( L ` ( E ` ( S ` j ) ) ) = ( E ` ( S ` j ) ) )
286 285 oveq2d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( j + 1 ) ) ) - ( E ` ( S ` j ) ) ) )
287 id 
 |-  ( x = ( S ` ( j + 1 ) ) -> x = ( S ` ( j + 1 ) ) )
288 oveq2 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( B - x ) = ( B - ( S ` ( j + 1 ) ) ) )
289 288 oveq1d 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( j + 1 ) ) ) / T ) )
290 289 fveq2d 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) )
291 290 oveq1d 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) )
292 287 291 oveq12d 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) )
293 292 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ x = ( S ` ( j + 1 ) ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) )
294 129 66 resubcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( S ` ( j + 1 ) ) ) e. RR )
295 294 102 rerpdivcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) e. RR )
296 295 flcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. ZZ )
297 296 zred 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. RR )
298 297 86 remulcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) e. RR )
299 66 298 readdcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) e. RR )
300 121 293 66 299 fvmptd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` ( j + 1 ) ) ) = ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) )
301 300 136 oveq12d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( E ` ( S ` j ) ) ) = ( ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) - ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) ) )
302 301 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( E ` ( S ` j ) ) ) = ( ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) - ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) ) )
303 flle 
 |-  ( ( ( B - ( S ` ( j + 1 ) ) ) / T ) e. RR -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` ( j + 1 ) ) ) / T ) )
304 295 303 syl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` ( j + 1 ) ) ) / T ) )
305 54 66 76 ltled 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) <_ ( S ` ( j + 1 ) ) )
306 54 66 129 305 lesub2dd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( S ` ( j + 1 ) ) ) <_ ( B - ( S ` j ) ) )
307 294 130 102 306 lediv1dd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) <_ ( ( B - ( S ` j ) ) / T ) )
308 297 295 131 304 307 letrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` j ) ) / T ) )
309 308 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` j ) ) / T ) )
310 297 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. RR )
311 1red 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> 1 e. RR )
312 310 311 readdcld 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) e. RR )
313 131 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> ( ( B - ( S ` j ) ) / T ) e. RR )
314 simpr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) )
315 312 313 314 nltled 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) )
316 315 adantlr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) )
317 80 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> S : ( 0 ... N ) -onto-> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
318 89 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> C e. RR )
319 93 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> D e. RR )
320 136 135 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) e. RR )
321 129 320 resubcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( E ` ( S ` j ) ) ) e. RR )
322 54 321 readdcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) e. RR )
323 12 322 eqeltrid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> Z e. RR )
324 323 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z e. RR )
325 20 rexrd 
 |-  ( ph -> A e. RR* )
326 325 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A e. RR* )
327 elioc2 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( E ` ( S ` j ) ) e. ( A (,] B ) <-> ( ( E ` ( S ` j ) ) e. RR /\ A < ( E ` ( S ` j ) ) /\ ( E ` ( S ` j ) ) <_ B ) ) )
328 326 129 327 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` j ) ) e. ( A (,] B ) <-> ( ( E ` ( S ` j ) ) e. RR /\ A < ( E ` ( S ` j ) ) /\ ( E ` ( S ` j ) ) <_ B ) ) )
329 55 328 mpbid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` j ) ) e. RR /\ A < ( E ` ( S ` j ) ) /\ ( E ` ( S ` j ) ) <_ B ) )
330 329 simp3d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) <_ B )
331 129 320 subge0d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( 0 <_ ( B - ( E ` ( S ` j ) ) ) <-> ( E ` ( S ` j ) ) <_ B ) )
332 330 331 mpbird 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 <_ ( B - ( E ` ( S ` j ) ) ) )
333 54 321 addge01d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( 0 <_ ( B - ( E ` ( S ` j ) ) ) <-> ( S ` j ) <_ ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) ) )
334 332 333 mpbid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) <_ ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) )
335 89 54 322 97 334 letrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> C <_ ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) )
336 335 12 breqtrrdi 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> C <_ Z )
337 336 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> C <_ Z )
338 66 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( S ` ( j + 1 ) ) e. RR )
339 295 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) e. RR )
340 reflcl 
 |-  ( ( ( B - ( S ` ( j + 1 ) ) ) / T ) e. RR -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. RR )
341 peano2re 
 |-  ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. RR -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) e. RR )
342 339 340 341 3syl 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) e. RR )
343 129 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> B e. RR )
344 343 324 resubcld 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( B - Z ) e. RR )
345 102 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> T e. RR+ )
346 344 345 rerpdivcld 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( B - Z ) / T ) e. RR )
347 flltp1 
 |-  ( ( ( B - ( S ` ( j + 1 ) ) ) / T ) e. RR -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) )
348 295 347 syl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) )
349 348 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) )
350 296 peano2zd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) e. ZZ )
351 350 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) e. ZZ )
352 131 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( B - ( S ` j ) ) / T ) e. RR )
353 simpr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) )
354 321 102 rerpdivcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( E ` ( S ` j ) ) ) / T ) e. RR )
355 354 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( B - ( E ` ( S ` j ) ) ) / T ) e. RR )
356 20 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A e. RR )
357 329 simp2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A < ( E ` ( S ` j ) ) )
358 356 320 129 357 ltsub2dd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( E ` ( S ` j ) ) ) < ( B - A ) )
359 358 2 breqtrrdi 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( E ` ( S ` j ) ) ) < T )
360 321 86 102 359 ltdiv1dd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( E ` ( S ` j ) ) ) / T ) < ( T / T ) )
361 144 145 dividd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( T / T ) = 1 )
362 360 361 breqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( E ` ( S ` j ) ) ) / T ) < 1 )
363 362 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( B - ( E ` ( S ` j ) ) ) / T ) < 1 )
364 130 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( S ` j ) ) e. CC )
365 321 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( E ` ( S ` j ) ) ) e. CC )
366 364 365 144 145 divsubdird 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) - ( B - ( E ` ( S ` j ) ) ) ) / T ) = ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) )
367 366 eqcomd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) = ( ( ( B - ( S ` j ) ) - ( B - ( E ` ( S ` j ) ) ) ) / T ) )
368 129 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> B e. CC )
369 320 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) e. CC )
370 368 139 369 nnncan1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( S ` j ) ) - ( B - ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
371 370 oveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) - ( B - ( E ` ( S ` j ) ) ) ) / T ) = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) )
372 367 371 eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) )
373 372 148 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) e. ZZ )
374 373 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) e. ZZ )
375 351 352 353 355 363 374 zltlesub 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) )
376 12 a1i 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> Z = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) )
377 376 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - Z ) = ( B - ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) ) )
378 139 368 369 addsub12d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( B + ( ( S ` j ) - ( E ` ( S ` j ) ) ) ) )
379 368 369 139 subsub2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) = ( B + ( ( S ` j ) - ( E ` ( S ` j ) ) ) ) )
380 378 379 eqtr4d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( B - ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) )
381 380 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) ) = ( B - ( B - ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) ) )
382 369 139 subcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` j ) ) - ( S ` j ) ) e. CC )
383 368 382 nncand 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( B - ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
384 377 381 383 3eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - Z ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
385 384 oveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - Z ) / T ) = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) )
386 371 367 385 3eqtr4d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) = ( ( B - Z ) / T ) )
387 386 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) = ( ( B - Z ) / T ) )
388 375 387 breqtrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - Z ) / T ) )
389 339 342 346 349 388 ltletrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) < ( ( B - Z ) / T ) )
390 294 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( B - ( S ` ( j + 1 ) ) ) e. RR )
391 390 344 345 ltdiv1d 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) < ( B - Z ) <-> ( ( B - ( S ` ( j + 1 ) ) ) / T ) < ( ( B - Z ) / T ) ) )
392 389 391 mpbird 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( B - ( S ` ( j + 1 ) ) ) < ( B - Z ) )
393 324 338 343 ltsub2d 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( Z < ( S ` ( j + 1 ) ) <-> ( B - ( S ` ( j + 1 ) ) ) < ( B - Z ) ) )
394 392 393 mpbird 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z < ( S ` ( j + 1 ) ) )
395 115 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( S ` ( j + 1 ) ) <_ D )
396 324 338 319 394 395 ltletrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z < D )
397 324 319 396 ltled 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z <_ D )
398 318 319 324 337 397 eliccd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z e. ( C [,] D ) )
399 33 a1i 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - A ) = T )
400 399 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) = ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) )
401 382 144 145 divcan1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
402 400 401 eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
403 376 402 oveq12d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Z + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) ) = ( ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) + ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) )
404 139 365 addcomd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( ( B - ( E ` ( S ` j ) ) ) + ( S ` j ) ) )
405 404 oveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) + ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) = ( ( ( B - ( E ` ( S ` j ) ) ) + ( S ` j ) ) + ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) )
406 365 139 369 ppncand 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( E ` ( S ` j ) ) ) + ( S ` j ) ) + ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) = ( ( B - ( E ` ( S ` j ) ) ) + ( E ` ( S ` j ) ) ) )
407 368 369 npcand 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( E ` ( S ` j ) ) ) + ( E ` ( S ` j ) ) ) = B )
408 406 407 eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( E ` ( S ` j ) ) ) + ( S ` j ) ) + ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) = B )
409 403 405 408 3eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Z + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) ) = B )
410 200 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> B e. ran Q )
411 409 410 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Z + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) ) e. ran Q )
412 oveq1 
 |-  ( k = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) -> ( k x. ( B - A ) ) = ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) )
413 412 oveq2d 
 |-  ( k = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) -> ( Z + ( k x. ( B - A ) ) ) = ( Z + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) ) )
414 413 eleq1d 
 |-  ( k = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) -> ( ( Z + ( k x. ( B - A ) ) ) e. ran Q <-> ( Z + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) ) e. ran Q ) )
415 414 rspcev 
 |-  ( ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) e. ZZ /\ ( Z + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) ) e. ran Q ) -> E. k e. ZZ ( Z + ( k x. ( B - A ) ) ) e. ran Q )
416 148 411 415 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. k e. ZZ ( Z + ( k x. ( B - A ) ) ) e. ran Q )
417 416 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> E. k e. ZZ ( Z + ( k x. ( B - A ) ) ) e. ran Q )
418 oveq1 
 |-  ( y = Z -> ( y + ( k x. ( B - A ) ) ) = ( Z + ( k x. ( B - A ) ) ) )
419 418 eleq1d 
 |-  ( y = Z -> ( ( y + ( k x. ( B - A ) ) ) e. ran Q <-> ( Z + ( k x. ( B - A ) ) ) e. ran Q ) )
420 419 rexbidv 
 |-  ( y = Z -> ( E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q <-> E. k e. ZZ ( Z + ( k x. ( B - A ) ) ) e. ran Q ) )
421 420 elrab 
 |-  ( Z e. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } <-> ( Z e. ( C [,] D ) /\ E. k e. ZZ ( Z + ( k x. ( B - A ) ) ) e. ran Q ) )
422 398 417 421 sylanbrc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z e. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } )
423 elun2 
 |-  ( Z e. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } -> Z e. ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
424 422 423 syl 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z e. ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
425 foelrn 
 |-  ( ( S : ( 0 ... N ) -onto-> ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) /\ Z e. ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) -> E. i e. ( 0 ... N ) Z = ( S ` i ) )
426 317 424 425 syl2anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> E. i e. ( 0 ... N ) Z = ( S ` i ) )
427 54 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` j ) e. RR )
428 321 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( B - ( E ` ( S ` j ) ) ) e. RR )
429 320 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) e. RR )
430 21 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> B e. RR )
431 330 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) <_ B )
432 276 necomd 
 |-  ( -. ( E ` ( S ` j ) ) = B -> B =/= ( E ` ( S ` j ) ) )
433 432 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> B =/= ( E ` ( S ` j ) ) )
434 429 430 431 433 leneltd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) < B )
435 429 430 posdifd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` j ) ) < B <-> 0 < ( B - ( E ` ( S ` j ) ) ) ) )
436 434 435 mpbid 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> 0 < ( B - ( E ` ( S ` j ) ) ) )
437 428 436 elrpd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( B - ( E ` ( S ` j ) ) ) e. RR+ )
438 427 437 ltaddrpd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` j ) < ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) )
439 438 12 breqtrrdi 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` j ) < Z )
440 439 ad2antrr 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) /\ Z = ( S ` i ) ) -> ( S ` j ) < Z )
441 simpr 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) /\ Z = ( S ` i ) ) -> Z = ( S ` i ) )
442 440 441 breqtrd 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) /\ Z = ( S ` i ) ) -> ( S ` j ) < ( S ` i ) )
443 394 adantr 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) /\ Z = ( S ` i ) ) -> Z < ( S ` ( j + 1 ) ) )
444 441 443 eqbrtrrd 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) /\ Z = ( S ` i ) ) -> ( S ` i ) < ( S ` ( j + 1 ) ) )
445 442 444 jca 
 |-  ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) /\ Z = ( S ` i ) ) -> ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
446 445 ex 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( Z = ( S ` i ) -> ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) )
447 446 reximdv 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( E. i e. ( 0 ... N ) Z = ( S ` i ) -> E. i e. ( 0 ... N ) ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) )
448 426 447 mpd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> E. i e. ( 0 ... N ) ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
449 316 448 syldan 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> E. i e. ( 0 ... N ) ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
450 252 nrexdv 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> -. E. i e. ( 0 ... N ) ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
451 450 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> -. E. i e. ( 0 ... N ) ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
452 449 451 condan 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) )
453 309 452 jca 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` j ) ) / T ) /\ ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) )
454 131 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( B - ( S ` j ) ) / T ) e. RR )
455 296 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. ZZ )
456 flbi 
 |-  ( ( ( ( B - ( S ` j ) ) / T ) e. RR /\ ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. ZZ ) -> ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) = ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <-> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` j ) ) / T ) /\ ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) ) )
457 454 455 456 syl2anc 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) = ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <-> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` j ) ) / T ) /\ ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) ) )
458 453 457 mpbird 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( |_ ` ( ( B - ( S ` j ) ) / T ) ) = ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) )
459 458 eqcomd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) = ( |_ ` ( ( B - ( S ` j ) ) / T ) ) )
460 459 oveq1d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) )
461 460 oveq2d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) = ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) )
462 461 oveq1d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) - ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) ) = ( ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) - ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) ) )
463 267 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` ( j + 1 ) ) e. CC )
464 139 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` j ) e. CC )
465 140 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) e. CC )
466 463 464 465 pnpcan2d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) - ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
467 462 466 eqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) - ( ( S ` j ) + ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
468 286 302 467 3eqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
469 271 468 pm2.61dan 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )