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 bilanri 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) = ( S ` i ) )
223 221 222 breqtrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( S ` j ) < ( S ` i ) )
224 110 adantr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( ( S ` j ) + T ) < ( S ` ( j + 1 ) ) )
225 222 224 eqbrtrrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ ( S ` i ) = ( ( S ` j ) + T ) ) -> ( S ` i ) < ( S ` ( j + 1 ) ) )
226 223 225 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 ) ) ) )
227 226 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 ) ) ) )
228 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 ) ) )
229 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 ) )
230 elfzelz 
 |-  ( i e. ( 0 ... N ) -> i e. ZZ )
231 230 ad2antlr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> i e. ZZ )
232 68 ad3antlr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> j e. ZZ )
233 simpr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> ( S ` j ) < ( S ` i ) )
234 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 } ) ) )
235 53 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> j e. ( 0 ... N ) )
236 simplr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> i e. ( 0 ... N ) )
237 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 ) ) )
238 234 235 236 237 syl12anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> ( j < i <-> ( S ` j ) < ( S ` i ) ) )
239 233 238 mpbird 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` i ) ) -> j < i )
240 239 adantrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> j < i )
241 simpr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> ( S ` i ) < ( S ` ( j + 1 ) ) )
242 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 } ) ) )
243 simplr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> i e. ( 0 ... N ) )
244 65 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> ( j + 1 ) e. ( 0 ... N ) )
245 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 ) ) ) )
246 242 243 244 245 syl12anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> ( i < ( j + 1 ) <-> ( S ` i ) < ( S ` ( j + 1 ) ) ) )
247 241 246 mpbird 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) -> i < ( j + 1 ) )
248 247 adantrl 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> i < ( j + 1 ) )
249 btwnnz 
 |-  ( ( j e. ZZ /\ j < i /\ i < ( j + 1 ) ) -> -. i e. ZZ )
250 232 240 248 249 syl3anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) /\ ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) ) -> -. i e. ZZ )
251 231 250 pm2.65da 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ... N ) ) -> -. ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
252 228 229 251 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 ) ) ) )
253 227 252 pm2.65da 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) /\ i e. ( 0 ... N ) ) -> -. ( S ` i ) = ( ( S ` j ) + T ) )
254 253 nrexdv 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) ) -> -. E. i e. ( 0 ... N ) ( S ` i ) = ( ( S ` j ) + T ) )
255 254 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 ) )
256 220 255 condan 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` ( j + 1 ) ) <_ ( ( S ` j ) + T ) )
257 62 rexrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` j ) e. RR* )
258 85 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> T e. RR )
259 62 258 readdcld 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( S ` j ) + T ) e. RR )
260 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 ) ) ) )
261 257 259 260 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 ) ) ) )
262 67 77 256 261 mpbir3and 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( S ` ( j + 1 ) ) e. ( ( S ` j ) (,] ( ( S ` j ) + T ) ) )
263 57 60 61 2 10 62 63 262 fourierdlem26 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` ( j + 1 ) ) ) = ( A + ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) )
264 263 oveq1d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - A ) = ( ( A + ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) - A ) )
265 57 recnd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> A e. CC )
266 66 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. CC )
267 266 139 subcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. CC )
268 267 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) e. CC )
269 265 268 pncan2d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( A + ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) - A ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
270 59 264 269 3eqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
271 11 a1i 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) ) )
272 eqcom 
 |-  ( y = ( E ` ( S ` j ) ) <-> ( E ` ( S ` j ) ) = y )
273 272 bilani 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> ( E ` ( S ` j ) ) = y )
274 neqne 
 |-  ( -. ( E ` ( S ` j ) ) = B -> ( E ` ( S ` j ) ) =/= B )
275 274 adantr 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> ( E ` ( S ` j ) ) =/= B )
276 273 275 eqnetrrd 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> y =/= B )
277 276 neneqd 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> -. y = B )
278 277 iffalsed 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = y )
279 simpr 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> y = ( E ` ( S ` j ) ) )
280 278 279 eqtrd 
 |-  ( ( -. ( E ` ( S ` j ) ) = B /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = ( E ` ( S ` j ) ) )
281 280 adantll 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ y = ( E ` ( S ` j ) ) ) -> if ( y = B , A , y ) = ( E ` ( S ` j ) ) )
282 55 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) e. ( A (,] B ) )
283 271 281 282 282 fvmptd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( L ` ( E ` ( S ` j ) ) ) = ( E ` ( S ` j ) ) )
284 283 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 ) ) ) )
285 id 
 |-  ( x = ( S ` ( j + 1 ) ) -> x = ( S ` ( j + 1 ) ) )
286 oveq2 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( B - x ) = ( B - ( S ` ( j + 1 ) ) ) )
287 286 oveq1d 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( j + 1 ) ) ) / T ) )
288 287 fveq2d 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) )
289 288 oveq1d 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) )
290 285 289 oveq12d 
 |-  ( x = ( S ` ( j + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) )
291 290 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 ) ) )
292 129 66 resubcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( S ` ( j + 1 ) ) ) e. RR )
293 292 102 rerpdivcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) e. RR )
294 293 flcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. ZZ )
295 294 zred 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. RR )
296 295 86 remulcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) e. RR )
297 66 296 readdcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) e. RR )
298 121 291 66 297 fvmptd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` ( j + 1 ) ) ) = ( ( S ` ( j + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) ) )
299 298 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 ) ) ) )
300 299 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 ) ) ) )
301 flle 
 |-  ( ( ( B - ( S ` ( j + 1 ) ) ) / T ) e. RR -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` ( j + 1 ) ) ) / T ) )
302 293 301 syl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` ( j + 1 ) ) ) / T ) )
303 54 66 76 ltled 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) <_ ( S ` ( j + 1 ) ) )
304 54 66 129 303 lesub2dd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( S ` ( j + 1 ) ) ) <_ ( B - ( S ` j ) ) )
305 292 130 102 304 lediv1dd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) <_ ( ( B - ( S ` j ) ) / T ) )
306 295 293 131 302 305 letrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` j ) ) / T ) )
307 306 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) <_ ( ( B - ( S ` j ) ) / T ) )
308 295 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. RR )
309 1red 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> 1 e. RR )
310 308 309 readdcld 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) e. RR )
311 131 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) ) -> ( ( B - ( S ` j ) ) / T ) e. RR )
312 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 ) )
313 310 311 312 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 ) )
314 313 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 ) )
315 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 } ) )
316 89 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> C e. RR )
317 93 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> D e. RR )
318 136 135 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) e. RR )
319 129 318 resubcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( E ` ( S ` j ) ) ) e. RR )
320 54 319 readdcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) e. RR )
321 12 320 eqeltrid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> Z e. RR )
322 321 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z e. RR )
323 20 rexrd 
 |-  ( ph -> A e. RR* )
324 323 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A e. RR* )
325 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 ) ) )
326 324 129 325 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 ) ) )
327 55 326 mpbid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` j ) ) e. RR /\ A < ( E ` ( S ` j ) ) /\ ( E ` ( S ` j ) ) <_ B ) )
328 327 simp3d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) <_ B )
329 129 318 subge0d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( 0 <_ ( B - ( E ` ( S ` j ) ) ) <-> ( E ` ( S ` j ) ) <_ B ) )
330 328 329 mpbird 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> 0 <_ ( B - ( E ` ( S ` j ) ) ) )
331 54 319 addge01d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( 0 <_ ( B - ( E ` ( S ` j ) ) ) <-> ( S ` j ) <_ ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) ) )
332 330 331 mpbid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) <_ ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) )
333 89 54 320 97 332 letrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> C <_ ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) )
334 333 12 breqtrrdi 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> C <_ Z )
335 334 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> C <_ Z )
336 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 )
337 293 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 )
338 reflcl 
 |-  ( ( ( B - ( S ` ( j + 1 ) ) ) / T ) e. RR -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. RR )
339 peano2re 
 |-  ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. RR -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) e. RR )
340 337 338 339 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 )
341 129 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> B e. RR )
342 341 322 resubcld 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> ( B - Z ) e. RR )
343 102 ad2antrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> T e. RR+ )
344 342 343 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 )
345 flltp1 
 |-  ( ( ( B - ( S ` ( j + 1 ) ) ) / T ) e. RR -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) )
346 293 345 syl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( S ` ( j + 1 ) ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) )
347 346 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 ) )
348 294 peano2zd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) e. ZZ )
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 ) ) + 1 ) e. ZZ )
350 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 )
351 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 ) )
352 319 102 rerpdivcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( E ` ( S ` j ) ) ) / T ) e. RR )
353 352 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 )
354 20 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A e. RR )
355 327 simp2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> A < ( E ` ( S ` j ) ) )
356 354 318 129 355 ltsub2dd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( E ` ( S ` j ) ) ) < ( B - A ) )
357 356 2 breqtrrdi 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( E ` ( S ` j ) ) ) < T )
358 319 86 102 357 ltdiv1dd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( E ` ( S ` j ) ) ) / T ) < ( T / T ) )
359 144 145 dividd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( T / T ) = 1 )
360 358 359 breqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( E ` ( S ` j ) ) ) / T ) < 1 )
361 360 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 )
362 130 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( S ` j ) ) e. CC )
363 319 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( E ` ( S ` j ) ) ) e. CC )
364 362 363 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 ) ) )
365 364 eqcomd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) = ( ( ( B - ( S ` j ) ) - ( B - ( E ` ( S ` j ) ) ) ) / T ) )
366 129 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> B e. CC )
367 318 recnd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E ` ( S ` j ) ) e. CC )
368 366 139 367 nnncan1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( S ` j ) ) - ( B - ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
369 368 oveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) - ( B - ( E ` ( S ` j ) ) ) ) / T ) = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) )
370 365 369 eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) )
371 370 148 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) e. ZZ )
372 371 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 )
373 349 350 351 353 361 372 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 ) ) )
374 12 a1i 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> Z = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) )
375 374 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - Z ) = ( B - ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) ) )
376 139 366 367 addsub12d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( B + ( ( S ` j ) - ( E ` ( S ` j ) ) ) ) )
377 366 367 139 subsub2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) = ( B + ( ( S ` j ) - ( E ` ( S ` j ) ) ) ) )
378 376 377 eqtr4d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( B - ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) )
379 378 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) ) = ( B - ( B - ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) ) )
380 367 139 subcld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` j ) ) - ( S ` j ) ) e. CC )
381 366 380 nncand 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - ( B - ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
382 375 379 381 3eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - Z ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
383 382 oveq1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - Z ) / T ) = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) )
384 369 365 383 3eqtr4d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( S ` j ) ) / T ) - ( ( B - ( E ` ( S ` j ) ) ) / T ) ) = ( ( B - Z ) / T ) )
385 384 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 ) )
386 373 385 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 ) )
387 337 340 344 347 386 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 ) )
388 292 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 )
389 388 342 343 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 ) ) )
390 387 389 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 ) )
391 322 336 341 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 ) ) )
392 390 391 mpbird 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z < ( S ` ( j + 1 ) ) )
393 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 )
394 322 336 317 392 393 ltletrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z < D )
395 322 317 394 ltled 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z <_ D )
396 316 317 322 335 395 eliccd 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) /\ ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) <_ ( ( B - ( S ` j ) ) / T ) ) -> Z e. ( C [,] D ) )
397 33 a1i 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( B - A ) = T )
398 397 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) = ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) )
399 380 144 145 divcan1d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. T ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
400 398 399 eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) = ( ( E ` ( S ` j ) ) - ( S ` j ) ) )
401 374 400 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 ) ) ) )
402 139 363 addcomd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( ( B - ( E ` ( S ` j ) ) ) + ( S ` j ) ) )
403 402 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 ) ) ) )
404 363 139 367 ppncand 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( E ` ( S ` j ) ) ) + ( S ` j ) ) + ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) = ( ( B - ( E ` ( S ` j ) ) ) + ( E ` ( S ` j ) ) ) )
405 366 367 npcand 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( B - ( E ` ( S ` j ) ) ) + ( E ` ( S ` j ) ) ) = B )
406 404 405 eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( B - ( E ` ( S ` j ) ) ) + ( S ` j ) ) + ( ( E ` ( S ` j ) ) - ( S ` j ) ) ) = B )
407 401 403 406 3eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Z + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) ) = B )
408 200 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> B e. ran Q )
409 407 408 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( Z + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) ) e. ran Q )
410 oveq1 
 |-  ( k = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) -> ( k x. ( B - A ) ) = ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) )
411 410 oveq2d 
 |-  ( k = ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) -> ( Z + ( k x. ( B - A ) ) ) = ( Z + ( ( ( ( E ` ( S ` j ) ) - ( S ` j ) ) / T ) x. ( B - A ) ) ) )
412 411 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 ) )
413 412 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 )
414 148 409 413 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. k e. ZZ ( Z + ( k x. ( B - A ) ) ) e. ran Q )
415 414 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 )
416 oveq1 
 |-  ( y = Z -> ( y + ( k x. ( B - A ) ) ) = ( Z + ( k x. ( B - A ) ) ) )
417 416 eleq1d 
 |-  ( y = Z -> ( ( y + ( k x. ( B - A ) ) ) e. ran Q <-> ( Z + ( k x. ( B - A ) ) ) e. ran Q ) )
418 417 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 ) )
419 418 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 ) )
420 396 415 419 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 } )
421 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 } ) )
422 420 421 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 } ) )
423 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 ) )
424 315 422 423 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 ) )
425 54 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` j ) e. RR )
426 319 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( B - ( E ` ( S ` j ) ) ) e. RR )
427 318 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) e. RR )
428 21 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> B e. RR )
429 328 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) <_ B )
430 274 necomd 
 |-  ( -. ( E ` ( S ` j ) ) = B -> B =/= ( E ` ( S ` j ) ) )
431 430 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> B =/= ( E ` ( S ` j ) ) )
432 427 428 429 431 leneltd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( E ` ( S ` j ) ) < B )
433 427 428 posdifd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` j ) ) < B <-> 0 < ( B - ( E ` ( S ` j ) ) ) ) )
434 432 433 mpbid 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> 0 < ( B - ( E ` ( S ` j ) ) ) )
435 426 434 elrpd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( B - ( E ` ( S ` j ) ) ) e. RR+ )
436 425 435 ltaddrpd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` j ) < ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) )
437 436 12 breqtrrdi 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` j ) < Z )
438 437 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 )
439 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 ) )
440 438 439 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 ) )
441 392 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 ) ) )
442 439 441 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 ) ) )
443 440 442 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 ) ) ) )
444 443 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 ) ) ) ) )
445 444 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 ) ) ) ) )
446 424 445 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 ) ) ) )
447 314 446 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 ) ) ) )
448 251 nrexdv 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> -. E. i e. ( 0 ... N ) ( ( S ` j ) < ( S ` i ) /\ ( S ` i ) < ( S ` ( j + 1 ) ) ) )
449 448 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 ) ) ) )
450 447 449 condan 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( B - ( S ` j ) ) / T ) < ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) + 1 ) )
451 307 450 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 ) ) )
452 131 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( B - ( S ` j ) ) / T ) e. RR )
453 294 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) e. ZZ )
454 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 ) ) ) )
455 452 453 454 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 ) ) ) )
456 451 455 mpbird 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( |_ ` ( ( B - ( S ` j ) ) / T ) ) = ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) )
457 456 eqcomd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) = ( |_ ` ( ( B - ( S ` j ) ) / T ) ) )
458 457 oveq1d 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( |_ ` ( ( B - ( S ` ( j + 1 ) ) ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) )
459 458 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 ) ) )
460 459 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 ) ) ) )
461 266 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` ( j + 1 ) ) e. CC )
462 139 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( S ` j ) e. CC )
463 140 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( |_ ` ( ( B - ( S ` j ) ) / T ) ) x. T ) e. CC )
464 461 462 463 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 ) ) )
465 460 464 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 ) ) )
466 284 300 465 3eqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ -. ( E ` ( S ` j ) ) = B ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
467 270 466 pm2.61dan 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )