This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem51

Description: X is in the periodic partition, when the considered interval is centered at X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem51.a 
|- ( ph -> A e. RR )
fourierdlem51.b 
|- ( ph -> B e. RR )
fourierdlem51.alt0 
|- ( ph -> A < 0 )
fourierdlem51.bgt0 
|- ( ph -> 0 < B )
fourierdlem51.t 
|- T = ( B - A )
fourierdlem51.cfi 
|- ( ph -> C e. Fin )
fourierdlem51.css 
|- ( ph -> C C_ ( A [,] B ) )
fourierdlem51.bc 
|- ( ph -> B e. C )
fourierdlem51.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem51.x 
|- ( ph -> X e. RR )
fourierdlem51.exc 
|- ( ph -> ( E ` X ) e. C )
fourierdlem51.d 
|- D = ( { ( A + X ) , ( B + X ) } u. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } )
fourierdlem51.f 
|- F = ( iota f f Isom < , < ( ( 0 ... ( ( # ` D ) - 1 ) ) , D ) )
fourierdlem51.h 
|- H = { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C }
Assertion fourierdlem51 
|- ( ph -> X e. ran F )

Proof

Step Hyp Ref Expression
1 fourierdlem51.a 
 |-  ( ph -> A e. RR )
2 fourierdlem51.b 
 |-  ( ph -> B e. RR )
3 fourierdlem51.alt0 
 |-  ( ph -> A < 0 )
4 fourierdlem51.bgt0 
 |-  ( ph -> 0 < B )
5 fourierdlem51.t 
 |-  T = ( B - A )
6 fourierdlem51.cfi 
 |-  ( ph -> C e. Fin )
7 fourierdlem51.css 
 |-  ( ph -> C C_ ( A [,] B ) )
8 fourierdlem51.bc 
 |-  ( ph -> B e. C )
9 fourierdlem51.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
10 fourierdlem51.x 
 |-  ( ph -> X e. RR )
11 fourierdlem51.exc 
 |-  ( ph -> ( E ` X ) e. C )
12 fourierdlem51.d 
 |-  D = ( { ( A + X ) , ( B + X ) } u. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } )
13 fourierdlem51.f 
 |-  F = ( iota f f Isom < , < ( ( 0 ... ( ( # ` D ) - 1 ) ) , D ) )
14 fourierdlem51.h 
 |-  H = { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C }
15 1 10 readdcld 
 |-  ( ph -> ( A + X ) e. RR )
16 2 10 readdcld 
 |-  ( ph -> ( B + X ) e. RR )
17 0red 
 |-  ( ph -> 0 e. RR )
18 1 17 10 3 ltadd1dd 
 |-  ( ph -> ( A + X ) < ( 0 + X ) )
19 10 recnd 
 |-  ( ph -> X e. CC )
20 19 addlidd 
 |-  ( ph -> ( 0 + X ) = X )
21 18 20 breqtrd 
 |-  ( ph -> ( A + X ) < X )
22 15 10 21 ltled 
 |-  ( ph -> ( A + X ) <_ X )
23 17 2 10 4 ltadd1dd 
 |-  ( ph -> ( 0 + X ) < ( B + X ) )
24 20 23 eqbrtrrd 
 |-  ( ph -> X < ( B + X ) )
25 10 16 24 ltled 
 |-  ( ph -> X <_ ( B + X ) )
26 15 16 10 22 25 eliccd 
 |-  ( ph -> X e. ( ( A + X ) [,] ( B + X ) ) )
27 2 10 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
28 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
29 5 28 eqeltrid 
 |-  ( ph -> T e. RR )
30 1 17 2 3 4 lttrd 
 |-  ( ph -> A < B )
31 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
32 30 31 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
33 5 eqcomi 
 |-  ( B - A ) = T
34 33 a1i 
 |-  ( ph -> ( B - A ) = T )
35 32 34 breqtrd 
 |-  ( ph -> 0 < T )
36 35 gt0ne0d 
 |-  ( ph -> T =/= 0 )
37 27 29 36 redivcld 
 |-  ( ph -> ( ( B - X ) / T ) e. RR )
38 37 flcld 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
39 9 a1i 
 |-  ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
40 id 
 |-  ( x = X -> x = X )
41 oveq2 
 |-  ( x = X -> ( B - x ) = ( B - X ) )
42 41 oveq1d 
 |-  ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
43 42 fveq2d 
 |-  ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
44 43 oveq1d 
 |-  ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
45 40 44 oveq12d 
 |-  ( x = X -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
46 45 adantl 
 |-  ( ( ph /\ x = X ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
47 38 zred 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
48 47 29 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
49 10 48 readdcld 
 |-  ( ph -> ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. RR )
50 39 46 10 49 fvmptd 
 |-  ( ph -> ( E ` X ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
51 50 11 eqeltrrd 
 |-  ( ph -> ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. C )
52 oveq1 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
53 52 oveq2d 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( X + ( k x. T ) ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
54 53 eleq1d 
 |-  ( k = ( |_ ` ( ( B - X ) / T ) ) -> ( ( X + ( k x. T ) ) e. C <-> ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. C ) )
55 54 rspcev 
 |-  ( ( ( |_ ` ( ( B - X ) / T ) ) e. ZZ /\ ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. C ) -> E. k e. ZZ ( X + ( k x. T ) ) e. C )
56 38 51 55 syl2anc 
 |-  ( ph -> E. k e. ZZ ( X + ( k x. T ) ) e. C )
57 oveq1 
 |-  ( y = X -> ( y + ( k x. T ) ) = ( X + ( k x. T ) ) )
58 57 eleq1d 
 |-  ( y = X -> ( ( y + ( k x. T ) ) e. C <-> ( X + ( k x. T ) ) e. C ) )
59 58 rexbidv 
 |-  ( y = X -> ( E. k e. ZZ ( y + ( k x. T ) ) e. C <-> E. k e. ZZ ( X + ( k x. T ) ) e. C ) )
60 59 elrab 
 |-  ( X e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } <-> ( X e. ( ( A + X ) [,] ( B + X ) ) /\ E. k e. ZZ ( X + ( k x. T ) ) e. C ) )
61 26 56 60 sylanbrc 
 |-  ( ph -> X e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } )
62 elun2 
 |-  ( X e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> X e. ( { ( A + X ) , ( B + X ) } u. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
63 61 62 syl 
 |-  ( ph -> X e. ( { ( A + X ) , ( B + X ) } u. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
64 63 12 eleqtrrdi 
 |-  ( ph -> X e. D )
65 prfi 
 |-  { ( A + X ) , ( B + X ) } e. Fin
66 snfi 
 |-  { ( A + X ) } e. Fin
67 fvres 
 |-  ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` x ) = ( E ` x ) )
68 67 adantl 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` x ) = ( E ` x ) )
69 oveq1 
 |-  ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
70 69 eleq1d 
 |-  ( y = x -> ( ( y + ( k x. T ) ) e. C <-> ( x + ( k x. T ) ) e. C ) )
71 70 rexbidv 
 |-  ( y = x -> ( E. k e. ZZ ( y + ( k x. T ) ) e. C <-> E. k e. ZZ ( x + ( k x. T ) ) e. C ) )
72 71 elrab 
 |-  ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } <-> ( x e. ( ( A + X ) (,] ( B + X ) ) /\ E. k e. ZZ ( x + ( k x. T ) ) e. C ) )
73 72 simprbi 
 |-  ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> E. k e. ZZ ( x + ( k x. T ) ) e. C )
74 73 adantl 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> E. k e. ZZ ( x + ( k x. T ) ) e. C )
75 nfv 
 |-  F/ k ph
76 nfre1 
 |-  F/ k E. k e. ZZ ( y + ( k x. T ) ) e. C
77 nfcv 
 |-  F/_ k ( ( A + X ) (,] ( B + X ) )
78 76 77 nfrabw 
 |-  F/_ k { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C }
79 78 nfcri 
 |-  F/ k x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C }
80 75 79 nfan 
 |-  F/ k ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } )
81 nfv 
 |-  F/ k ( E ` x ) e. C
82 simpl 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> ph )
83 15 rexrd 
 |-  ( ph -> ( A + X ) e. RR* )
84 iocssre 
 |-  ( ( ( A + X ) e. RR* /\ ( B + X ) e. RR ) -> ( ( A + X ) (,] ( B + X ) ) C_ RR )
85 83 16 84 syl2anc 
 |-  ( ph -> ( ( A + X ) (,] ( B + X ) ) C_ RR )
86 85 adantr 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> ( ( A + X ) (,] ( B + X ) ) C_ RR )
87 elrabi 
 |-  ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> x e. ( ( A + X ) (,] ( B + X ) ) )
88 87 adantl 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> x e. ( ( A + X ) (,] ( B + X ) ) )
89 86 88 sseldd 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> x e. RR )
90 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
91 2 adantr 
 |-  ( ( ph /\ x e. RR ) -> B e. RR )
92 91 90 resubcld 
 |-  ( ( ph /\ x e. RR ) -> ( B - x ) e. RR )
93 29 adantr 
 |-  ( ( ph /\ x e. RR ) -> T e. RR )
94 36 adantr 
 |-  ( ( ph /\ x e. RR ) -> T =/= 0 )
95 92 93 94 redivcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( B - x ) / T ) e. RR )
96 95 flcld 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. ZZ )
97 96 zred 
 |-  ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. RR )
98 97 93 remulcld 
 |-  ( ( ph /\ x e. RR ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR )
99 90 98 readdcld 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. RR )
100 9 fvmpt2 
 |-  ( ( x e. RR /\ ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. RR ) -> ( E ` x ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
101 90 99 100 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> ( E ` x ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
102 101 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( E ` x ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
103 simpl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( ( ph /\ x e. RR ) /\ k e. ZZ ) )
104 96 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( |_ ` ( ( B - x ) / T ) ) e. ZZ )
105 simpr 
 |-  ( ( ph /\ ( x + ( k x. T ) ) = A ) -> ( x + ( k x. T ) ) = A )
106 1 rexrd 
 |-  ( ph -> A e. RR* )
107 2 rexrd 
 |-  ( ph -> B e. RR* )
108 1 2 30 ltled 
 |-  ( ph -> A <_ B )
109 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
110 106 107 108 109 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
111 110 adantr 
 |-  ( ( ph /\ ( x + ( k x. T ) ) = A ) -> A e. ( A [,] B ) )
112 105 111 eqeltrd 
 |-  ( ( ph /\ ( x + ( k x. T ) ) = A ) -> ( x + ( k x. T ) ) e. ( A [,] B ) )
113 112 ad4ant14 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( x + ( k x. T ) ) e. ( A [,] B ) )
114 103 104 113 jca31 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) )
115 iocssicc 
 |-  ( A (,] B ) C_ ( A [,] B )
116 1 2 30 5 9 fourierdlem4 
 |-  ( ph -> E : RR --> ( A (,] B ) )
117 116 ffvelcdmda 
 |-  ( ( ph /\ x e. RR ) -> ( E ` x ) e. ( A (,] B ) )
118 115 117 sselid 
 |-  ( ( ph /\ x e. RR ) -> ( E ` x ) e. ( A [,] B ) )
119 101 118 eqeltrrd 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A [,] B ) )
120 119 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A [,] B ) )
121 106 adantr 
 |-  ( ( ph /\ x e. RR ) -> A e. RR* )
122 91 rexrd 
 |-  ( ( ph /\ x e. RR ) -> B e. RR* )
123 iocgtlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( E ` x ) e. ( A (,] B ) ) -> A < ( E ` x ) )
124 121 122 117 123 syl3anc 
 |-  ( ( ph /\ x e. RR ) -> A < ( E ` x ) )
125 124 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> A < ( E ` x ) )
126 id 
 |-  ( ( x + ( k x. T ) ) = A -> ( x + ( k x. T ) ) = A )
127 126 eqcomd 
 |-  ( ( x + ( k x. T ) ) = A -> A = ( x + ( k x. T ) ) )
128 127 adantl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> A = ( x + ( k x. T ) ) )
129 125 128 102 3brtr3d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( x + ( k x. T ) ) < ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
130 zre 
 |-  ( k e. ZZ -> k e. RR )
131 130 adantl 
 |-  ( ( ph /\ k e. ZZ ) -> k e. RR )
132 29 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> T e. RR )
133 131 132 remulcld 
 |-  ( ( ph /\ k e. ZZ ) -> ( k x. T ) e. RR )
134 133 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> ( k x. T ) e. RR )
135 134 adantr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( k x. T ) e. RR )
136 98 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR )
137 simpllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> x e. RR )
138 135 136 137 ltadd2d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( ( k x. T ) < ( ( |_ ` ( ( B - x ) / T ) ) x. T ) <-> ( x + ( k x. T ) ) < ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
139 129 138 mpbird 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( k x. T ) < ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
140 130 ad2antlr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> k e. RR )
141 97 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( |_ ` ( ( B - x ) / T ) ) e. RR )
142 29 35 elrpd 
 |-  ( ph -> T e. RR+ )
143 142 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> T e. RR+ )
144 140 141 143 ltmul1d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( k < ( |_ ` ( ( B - x ) / T ) ) <-> ( k x. T ) < ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
145 139 144 mpbird 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> k < ( |_ ` ( ( B - x ) / T ) ) )
146 fvex 
 |-  ( |_ ` ( ( B - x ) / T ) ) e. _V
147 eleq1 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( j e. ZZ <-> ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) )
148 147 anbi2d 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) <-> ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) ) )
149 148 anbi1d 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) <-> ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) ) )
150 oveq1 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( j x. T ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
151 150 oveq2d 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( x + ( j x. T ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
152 151 eleq1d 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( ( x + ( j x. T ) ) e. ( A [,] B ) <-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A [,] B ) ) )
153 149 152 anbi12d 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) <-> ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A [,] B ) ) ) )
154 breq2 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( k < j <-> k < ( |_ ` ( ( B - x ) / T ) ) ) )
155 153 154 anbi12d 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ k < j ) <-> ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A [,] B ) ) /\ k < ( |_ ` ( ( B - x ) / T ) ) ) ) )
156 eqeq1 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( j = ( k + 1 ) <-> ( |_ ` ( ( B - x ) / T ) ) = ( k + 1 ) ) )
157 155 156 imbi12d 
 |-  ( j = ( |_ ` ( ( B - x ) / T ) ) -> ( ( ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ k < j ) -> j = ( k + 1 ) ) <-> ( ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A [,] B ) ) /\ k < ( |_ ` ( ( B - x ) / T ) ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( k + 1 ) ) ) )
158 eleq1 
 |-  ( i = k -> ( i e. ZZ <-> k e. ZZ ) )
159 158 anbi2d 
 |-  ( i = k -> ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) <-> ( ( ph /\ x e. RR ) /\ k e. ZZ ) ) )
160 159 anbi1d 
 |-  ( i = k -> ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) <-> ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) ) )
161 oveq1 
 |-  ( i = k -> ( i x. T ) = ( k x. T ) )
162 161 oveq2d 
 |-  ( i = k -> ( x + ( i x. T ) ) = ( x + ( k x. T ) ) )
163 162 eleq1d 
 |-  ( i = k -> ( ( x + ( i x. T ) ) e. ( A [,] B ) <-> ( x + ( k x. T ) ) e. ( A [,] B ) ) )
164 160 163 anbi12d 
 |-  ( i = k -> ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) <-> ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) ) )
165 164 anbi1d 
 |-  ( i = k -> ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) <-> ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) ) )
166 breq1 
 |-  ( i = k -> ( i < j <-> k < j ) )
167 165 166 anbi12d 
 |-  ( i = k -> ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) <-> ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ k < j ) ) )
168 oveq1 
 |-  ( i = k -> ( i + 1 ) = ( k + 1 ) )
169 168 eqeq2d 
 |-  ( i = k -> ( j = ( i + 1 ) <-> j = ( k + 1 ) ) )
170 167 169 imbi12d 
 |-  ( i = k -> ( ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> j = ( i + 1 ) ) <-> ( ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ k < j ) -> j = ( k + 1 ) ) ) )
171 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> ph )
172 171 1 syl 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> A e. RR )
173 171 2 syl 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> B e. RR )
174 171 30 syl 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> A < B )
175 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> x e. RR )
176 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> i e. ZZ )
177 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> j e. ZZ )
178 simpr 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> i < j )
179 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> ( x + ( i x. T ) ) e. ( A [,] B ) )
180 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> ( x + ( j x. T ) ) e. ( A [,] B ) )
181 172 173 174 5 175 176 177 178 179 180 fourierdlem6 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ i e. ZZ ) /\ j e. ZZ ) /\ ( x + ( i x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ i < j ) -> j = ( i + 1 ) )
182 170 181 chvarvv 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ j e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( j x. T ) ) e. ( A [,] B ) ) /\ k < j ) -> j = ( k + 1 ) )
183 146 157 182 vtocl 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( |_ ` ( ( B - x ) / T ) ) e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A [,] B ) ) /\ ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A [,] B ) ) /\ k < ( |_ ` ( ( B - x ) / T ) ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( k + 1 ) )
184 114 120 145 183 syl21anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( |_ ` ( ( B - x ) / T ) ) = ( k + 1 ) )
185 184 oveq1d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( k + 1 ) x. T ) )
186 185 oveq2d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( x + ( ( k + 1 ) x. T ) ) )
187 131 recnd 
 |-  ( ( ph /\ k e. ZZ ) -> k e. CC )
188 29 recnd 
 |-  ( ph -> T e. CC )
189 188 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> T e. CC )
190 187 189 adddirp1d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( k + 1 ) x. T ) = ( ( k x. T ) + T ) )
191 190 oveq2d 
 |-  ( ( ph /\ k e. ZZ ) -> ( x + ( ( k + 1 ) x. T ) ) = ( x + ( ( k x. T ) + T ) ) )
192 191 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> ( x + ( ( k + 1 ) x. T ) ) = ( x + ( ( k x. T ) + T ) ) )
193 192 adantr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( x + ( ( k + 1 ) x. T ) ) = ( x + ( ( k x. T ) + T ) ) )
194 90 recnd 
 |-  ( ( ph /\ x e. RR ) -> x e. CC )
195 194 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> x e. CC )
196 134 recnd 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> ( k x. T ) e. CC )
197 188 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> T e. CC )
198 195 196 197 addassd 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> ( ( x + ( k x. T ) ) + T ) = ( x + ( ( k x. T ) + T ) ) )
199 198 eqcomd 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> ( x + ( ( k x. T ) + T ) ) = ( ( x + ( k x. T ) ) + T ) )
200 199 adantr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( x + ( ( k x. T ) + T ) ) = ( ( x + ( k x. T ) ) + T ) )
201 oveq1 
 |-  ( ( x + ( k x. T ) ) = A -> ( ( x + ( k x. T ) ) + T ) = ( A + T ) )
202 201 adantl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( ( x + ( k x. T ) ) + T ) = ( A + T ) )
203 2 recnd 
 |-  ( ph -> B e. CC )
204 1 recnd 
 |-  ( ph -> A e. CC )
205 203 204 188 subaddd 
 |-  ( ph -> ( ( B - A ) = T <-> ( A + T ) = B ) )
206 34 205 mpbid 
 |-  ( ph -> ( A + T ) = B )
207 206 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( A + T ) = B )
208 202 207 eqtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( ( x + ( k x. T ) ) + T ) = B )
209 193 200 208 3eqtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( x + ( ( k + 1 ) x. T ) ) = B )
210 102 186 209 3eqtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( E ` x ) = B )
211 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> B e. C )
212 210 211 eqeltrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) = A ) -> ( E ` x ) e. C )
213 212 3adantl3 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ ( x + ( k x. T ) ) = A ) -> ( E ` x ) e. C )
214 simpl1 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> ( ph /\ x e. RR ) )
215 simpl2 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> k e. ZZ )
216 7 sselda 
 |-  ( ( ph /\ ( x + ( k x. T ) ) e. C ) -> ( x + ( k x. T ) ) e. ( A [,] B ) )
217 216 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + ( k x. T ) ) e. C ) -> ( x + ( k x. T ) ) e. ( A [,] B ) )
218 217 3adant2 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) -> ( x + ( k x. T ) ) e. ( A [,] B ) )
219 218 adantr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> ( x + ( k x. T ) ) e. ( A [,] B ) )
220 neqne 
 |-  ( -. ( x + ( k x. T ) ) = A -> ( x + ( k x. T ) ) =/= A )
221 220 adantl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> ( x + ( k x. T ) ) =/= A )
222 1 adantr 
 |-  ( ( ph /\ x e. RR ) -> A e. RR )
223 214 222 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> A e. RR )
224 214 91 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> B e. RR )
225 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> x e. RR )
226 225 134 readdcld 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. RR )
227 226 rexrd 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. RR* )
228 214 215 227 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> ( x + ( k x. T ) ) e. RR* )
229 223 224 228 eliccelioc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> ( ( x + ( k x. T ) ) e. ( A (,] B ) <-> ( ( x + ( k x. T ) ) e. ( A [,] B ) /\ ( x + ( k x. T ) ) =/= A ) ) )
230 219 221 229 mpbir2and 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> ( x + ( k x. T ) ) e. ( A (,] B ) )
231 101 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> ( E ` x ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
232 1 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> A e. RR )
233 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> B e. RR )
234 30 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> A < B )
235 simpllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> x e. RR )
236 96 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> ( |_ ` ( ( B - x ) / T ) ) e. ZZ )
237 simplr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> k e. ZZ )
238 101 117 eqeltrrd 
 |-  ( ( ph /\ x e. RR ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A (,] B ) )
239 238 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) e. ( A (,] B ) )
240 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> ( x + ( k x. T ) ) e. ( A (,] B ) )
241 232 233 234 5 235 236 237 239 240 fourierdlem35 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> ( |_ ` ( ( B - x ) / T ) ) = k )
242 241 oveq1d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( k x. T ) )
243 242 oveq2d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( x + ( k x. T ) ) )
244 231 243 eqtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ ) /\ ( x + ( k x. T ) ) e. ( A (,] B ) ) -> ( E ` x ) = ( x + ( k x. T ) ) )
245 214 215 230 244 syl21anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> ( E ` x ) = ( x + ( k x. T ) ) )
246 simpl3 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> ( x + ( k x. T ) ) e. C )
247 245 246 eqeltrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) /\ -. ( x + ( k x. T ) ) = A ) -> ( E ` x ) e. C )
248 213 247 pm2.61dan 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. ZZ /\ ( x + ( k x. T ) ) e. C ) -> ( E ` x ) e. C )
249 248 3exp 
 |-  ( ( ph /\ x e. RR ) -> ( k e. ZZ -> ( ( x + ( k x. T ) ) e. C -> ( E ` x ) e. C ) ) )
250 82 89 249 syl2anc 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> ( k e. ZZ -> ( ( x + ( k x. T ) ) e. C -> ( E ` x ) e. C ) ) )
251 80 81 250 rexlimd 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> ( E. k e. ZZ ( x + ( k x. T ) ) e. C -> ( E ` x ) e. C ) )
252 74 251 mpd 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> ( E ` x ) e. C )
253 68 252 eqeltrd 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` x ) e. C )
254 eqid 
 |-  ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } |-> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` x ) ) = ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } |-> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` x ) )
255 253 254 fmptd 
 |-  ( ph -> ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } |-> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` x ) ) : { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } --> C )
256 iocssre 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
257 106 2 256 syl2anc 
 |-  ( ph -> ( A (,] B ) C_ RR )
258 116 257 fssd 
 |-  ( ph -> E : RR --> RR )
259 ssrab2 
 |-  { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } C_ ( ( A + X ) (,] ( B + X ) )
260 259 85 sstrid 
 |-  ( ph -> { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } C_ RR )
261 258 260 fssresd 
 |-  ( ph -> ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) : { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } --> RR )
262 261 feqmptd 
 |-  ( ph -> ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) = ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } |-> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` x ) ) )
263 262 feq1d 
 |-  ( ph -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) : { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } --> C <-> ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } |-> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` x ) ) : { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } --> C ) )
264 255 263 mpbird 
 |-  ( ph -> ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) : { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } --> C )
265 simplll 
 |-  ( ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) ) -> ph )
266 id 
 |-  ( w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } )
267 266 14 eleqtrrdi 
 |-  ( w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> w e. H )
268 267 ad3antlr 
 |-  ( ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) ) -> w e. H )
269 265 268 jca 
 |-  ( ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) ) -> ( ph /\ w e. H ) )
270 id 
 |-  ( z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } )
271 270 14 eleqtrrdi 
 |-  ( z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> z e. H )
272 271 ad2antlr 
 |-  ( ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) ) -> z e. H )
273 fvres 
 |-  ( z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) = ( E ` z ) )
274 273 eqcomd 
 |-  ( z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> ( E ` z ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) )
275 274 ad2antlr 
 |-  ( ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) ) -> ( E ` z ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) )
276 id 
 |-  ( ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) )
277 276 eqcomd 
 |-  ( ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) )
278 277 adantl 
 |-  ( ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) ) -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) )
279 fvres 
 |-  ( w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( E ` w ) )
280 279 ad3antlr 
 |-  ( ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) ) -> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( E ` w ) )
281 275 278 280 3eqtrd 
 |-  ( ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) ) -> ( E ` z ) = ( E ` w ) )
282 1 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> A e. RR )
283 2 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> B e. RR )
284 30 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> A < B )
285 10 ad3antrrr 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> X e. RR )
286 simpllr 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> w e. H )
287 simplr 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> z e. H )
288 simpr 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> ( E ` z ) = ( E ` w ) )
289 282 283 284 285 14 5 9 286 287 288 fourierdlem19 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> -. w < z )
290 288 eqcomd 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> ( E ` w ) = ( E ` z ) )
291 282 283 284 285 14 5 9 287 286 290 fourierdlem19 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> -. z < w )
292 14 260 eqsstrid 
 |-  ( ph -> H C_ RR )
293 292 sselda 
 |-  ( ( ph /\ w e. H ) -> w e. RR )
294 293 ad2antrr 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> w e. RR )
295 292 adantr 
 |-  ( ( ph /\ w e. H ) -> H C_ RR )
296 295 sselda 
 |-  ( ( ( ph /\ w e. H ) /\ z e. H ) -> z e. RR )
297 296 adantr 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> z e. RR )
298 294 297 lttri3d 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> ( w = z <-> ( -. w < z /\ -. z < w ) ) )
299 289 291 298 mpbir2and 
 |-  ( ( ( ( ph /\ w e. H ) /\ z e. H ) /\ ( E ` z ) = ( E ` w ) ) -> w = z )
300 269 272 281 299 syl21anc 
 |-  ( ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) ) -> w = z )
301 300 ex 
 |-  ( ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) /\ z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> ( ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) -> w = z ) )
302 301 ralrimiva 
 |-  ( ( ph /\ w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> A. z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ( ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) -> w = z ) )
303 302 ralrimiva 
 |-  ( ph -> A. w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } A. z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ( ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) -> w = z ) )
304 dff13 
 |-  ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) : { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -1-1-> C <-> ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) : { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } --> C /\ A. w e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } A. z e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ( ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` w ) = ( ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ` z ) -> w = z ) ) )
305 264 303 304 sylanbrc 
 |-  ( ph -> ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) : { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -1-1-> C )
306 f1fi 
 |-  ( ( C e. Fin /\ ( E |` { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) : { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -1-1-> C ) -> { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } e. Fin )
307 6 305 306 syl2anc 
 |-  ( ph -> { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } e. Fin )
308 unfi 
 |-  ( ( { ( A + X ) } e. Fin /\ { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } e. Fin ) -> ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) e. Fin )
309 66 307 308 sylancr 
 |-  ( ph -> ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) e. Fin )
310 simpl 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> ph )
311 elrabi 
 |-  ( x e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> x e. ( ( A + X ) [,] ( B + X ) ) )
312 311 adantl 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> x e. ( ( A + X ) [,] ( B + X ) ) )
313 71 elrab 
 |-  ( x e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } <-> ( x e. ( ( A + X ) [,] ( B + X ) ) /\ E. k e. ZZ ( x + ( k x. T ) ) e. C ) )
314 313 simprbi 
 |-  ( x e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> E. k e. ZZ ( x + ( k x. T ) ) e. C )
315 314 adantl 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> E. k e. ZZ ( x + ( k x. T ) ) e. C )
316 velsn 
 |-  ( x e. { ( A + X ) } <-> x = ( A + X ) )
317 elun1 
 |-  ( x e. { ( A + X ) } -> x e. ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
318 316 317 sylbir 
 |-  ( x = ( A + X ) -> x e. ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
319 318 adantl 
 |-  ( ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ E. k e. ZZ ( x + ( k x. T ) ) e. C ) /\ x = ( A + X ) ) -> x e. ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
320 83 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> ( A + X ) e. RR* )
321 16 rexrd 
 |-  ( ph -> ( B + X ) e. RR* )
322 321 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> ( B + X ) e. RR* )
323 15 16 iccssred 
 |-  ( ph -> ( ( A + X ) [,] ( B + X ) ) C_ RR )
324 323 sselda 
 |-  ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) -> x e. RR )
325 324 rexrd 
 |-  ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) -> x e. RR* )
326 325 adantr 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> x e. RR* )
327 15 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> ( A + X ) e. RR )
328 324 adantr 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> x e. RR )
329 83 adantr 
 |-  ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) -> ( A + X ) e. RR* )
330 321 adantr 
 |-  ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) -> ( B + X ) e. RR* )
331 simpr 
 |-  ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) -> x e. ( ( A + X ) [,] ( B + X ) ) )
332 iccgelb 
 |-  ( ( ( A + X ) e. RR* /\ ( B + X ) e. RR* /\ x e. ( ( A + X ) [,] ( B + X ) ) ) -> ( A + X ) <_ x )
333 329 330 331 332 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) -> ( A + X ) <_ x )
334 333 adantr 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> ( A + X ) <_ x )
335 neqne 
 |-  ( -. x = ( A + X ) -> x =/= ( A + X ) )
336 335 adantl 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> x =/= ( A + X ) )
337 327 328 334 336 leneltd 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> ( A + X ) < x )
338 iccleub 
 |-  ( ( ( A + X ) e. RR* /\ ( B + X ) e. RR* /\ x e. ( ( A + X ) [,] ( B + X ) ) ) -> x <_ ( B + X ) )
339 329 330 331 338 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) -> x <_ ( B + X ) )
340 339 adantr 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> x <_ ( B + X ) )
341 320 322 326 337 340 eliocd 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ -. x = ( A + X ) ) -> x e. ( ( A + X ) (,] ( B + X ) ) )
342 341 adantlr 
 |-  ( ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ E. k e. ZZ ( x + ( k x. T ) ) e. C ) /\ -. x = ( A + X ) ) -> x e. ( ( A + X ) (,] ( B + X ) ) )
343 simplr 
 |-  ( ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ E. k e. ZZ ( x + ( k x. T ) ) e. C ) /\ -. x = ( A + X ) ) -> E. k e. ZZ ( x + ( k x. T ) ) e. C )
344 342 343 72 sylanbrc 
 |-  ( ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ E. k e. ZZ ( x + ( k x. T ) ) e. C ) /\ -. x = ( A + X ) ) -> x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } )
345 elun2 
 |-  ( x e. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } -> x e. ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
346 344 345 syl 
 |-  ( ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ E. k e. ZZ ( x + ( k x. T ) ) e. C ) /\ -. x = ( A + X ) ) -> x e. ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
347 319 346 pm2.61dan 
 |-  ( ( ( ph /\ x e. ( ( A + X ) [,] ( B + X ) ) ) /\ E. k e. ZZ ( x + ( k x. T ) ) e. C ) -> x e. ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
348 310 312 315 347 syl21anc 
 |-  ( ( ph /\ x e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) -> x e. ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
349 348 ralrimiva 
 |-  ( ph -> A. x e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } x e. ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
350 dfss3 
 |-  ( { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } C_ ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) <-> A. x e. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } x e. ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
351 349 350 sylibr 
 |-  ( ph -> { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } C_ ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) )
352 ssfi 
 |-  ( ( ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) e. Fin /\ { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } C_ ( { ( A + X ) } u. { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) ) -> { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } e. Fin )
353 309 351 352 syl2anc 
 |-  ( ph -> { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } e. Fin )
354 unfi 
 |-  ( ( { ( A + X ) , ( B + X ) } e. Fin /\ { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } e. Fin ) -> ( { ( A + X ) , ( B + X ) } u. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) e. Fin )
355 65 353 354 sylancr 
 |-  ( ph -> ( { ( A + X ) , ( B + X ) } u. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) e. Fin )
356 12 355 eqeltrid 
 |-  ( ph -> D e. Fin )
357 prssi 
 |-  ( ( ( A + X ) e. RR /\ ( B + X ) e. RR ) -> { ( A + X ) , ( B + X ) } C_ RR )
358 15 16 357 syl2anc 
 |-  ( ph -> { ( A + X ) , ( B + X ) } C_ RR )
359 ssrab2 
 |-  { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } C_ ( ( A + X ) [,] ( B + X ) )
360 359 323 sstrid 
 |-  ( ph -> { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } C_ RR )
361 358 360 unssd 
 |-  ( ph -> ( { ( A + X ) , ( B + X ) } u. { y e. ( ( A + X ) [,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } ) C_ RR )
362 12 361 eqsstrid 
 |-  ( ph -> D C_ RR )
363 eqid 
 |-  ( ( # ` D ) - 1 ) = ( ( # ` D ) - 1 )
364 356 362 13 363 fourierdlem36 
 |-  ( ph -> F Isom < , < ( ( 0 ... ( ( # ` D ) - 1 ) ) , D ) )
365 isof1o 
 |-  ( F Isom < , < ( ( 0 ... ( ( # ` D ) - 1 ) ) , D ) -> F : ( 0 ... ( ( # ` D ) - 1 ) ) -1-1-onto-> D )
366 f1ofo 
 |-  ( F : ( 0 ... ( ( # ` D ) - 1 ) ) -1-1-onto-> D -> F : ( 0 ... ( ( # ` D ) - 1 ) ) -onto-> D )
367 forn 
 |-  ( F : ( 0 ... ( ( # ` D ) - 1 ) ) -onto-> D -> ran F = D )
368 364 365 366 367 4syl 
 |-  ( ph -> ran F = D )
369 64 368 eleqtrrd 
 |-  ( ph -> X e. ran F )