Metamath Proof Explorer

Theorem fourierdlem94

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem94.f 
|- ( ph -> F : RR --> RR )
fourierdlem94.t 
|- T = ( 2 x. _pi )
fourierdlem94.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem94.x 
|- ( ph -> X e. RR )
fourierdlem94.p 
|- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem94.m 
|- ( ph -> M e. NN )
fourierdlem94.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem94.dvcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem94.dvlb 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) =/= (/) )
fourierdlem94.dvub 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) =/= (/) )
Assertion fourierdlem94 
|- ( ph -> ( ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) /\ ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem94.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem94.t 
 |-  T = ( 2 x. _pi )
3 fourierdlem94.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fourierdlem94.x 
 |-  ( ph -> X e. RR )
5 fourierdlem94.p 
 |-  P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
6 fourierdlem94.m 
 |-  ( ph -> M e. NN )
7 fourierdlem94.q 
 |-  ( ph -> Q e. ( P ` M ) )
8 fourierdlem94.dvcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
9 fourierdlem94.dvlb 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) =/= (/) )
10 fourierdlem94.dvub 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) =/= (/) )
11 pire 
 |-  _pi e. RR
12 11 renegcli 
 |-  -u _pi e. RR
13 12 a1i 
 |-  ( ph -> -u _pi e. RR )
14 11 a1i 
 |-  ( ph -> _pi e. RR )
15 negpilt0 
 |-  -u _pi < 0
16 pipos 
 |-  0 < _pi
17 0re 
 |-  0 e. RR
18 12 17 11 lttri 
 |-  ( ( -u _pi < 0 /\ 0 < _pi ) -> -u _pi < _pi )
19 15 16 18 mp2an 
 |-  -u _pi < _pi
20 19 a1i 
 |-  ( ph -> -u _pi < _pi )
21 picn 
 |-  _pi e. CC
22 21 2timesi 
 |-  ( 2 x. _pi ) = ( _pi + _pi )
23 21 21 subnegi 
 |-  ( _pi - -u _pi ) = ( _pi + _pi )
24 22 2 23 3eqtr4i 
 |-  T = ( _pi - -u _pi )
25 ssid 
 |-  RR C_ RR
26 25 a1i 
 |-  ( ph -> RR C_ RR )
27 simp2 
 |-  ( ( ph /\ x e. RR /\ k e. ZZ ) -> x e. RR )
28 zre 
 |-  ( k e. ZZ -> k e. RR )
29 28 3ad2ant3 
 |-  ( ( ph /\ x e. RR /\ k e. ZZ ) -> k e. RR )
30 2re 
 |-  2 e. RR
31 30 11 remulcli 
 |-  ( 2 x. _pi ) e. RR
32 31 a1i 
 |-  ( ph -> ( 2 x. _pi ) e. RR )
33 2 32 eqeltrid 
 |-  ( ph -> T e. RR )
34 33 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> T e. RR )
35 34 3adant2 
 |-  ( ( ph /\ x e. RR /\ k e. ZZ ) -> T e. RR )
36 29 35 remulcld 
 |-  ( ( ph /\ x e. RR /\ k e. ZZ ) -> ( k x. T ) e. RR )
37 27 36 readdcld 
 |-  ( ( ph /\ x e. RR /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. RR )
38 simp1 
 |-  ( ( ph /\ x e. RR /\ k e. ZZ ) -> ph )
39 simp3 
 |-  ( ( ph /\ x e. RR /\ k e. ZZ ) -> k e. ZZ )
40 ax-resscn 
 |-  RR C_ CC
41 40 a1i 
 |-  ( ph -> RR C_ CC )
42 1 41 fssd 
 |-  ( ph -> F : RR --> CC )
43 42 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> F : RR --> CC )
44 43 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> F : RR --> CC )
45 34 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> T e. RR )
46 simplr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> k e. ZZ )
47 simpr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> x e. RR )
48 eleq1w 
 |-  ( x = y -> ( x e. RR <-> y e. RR ) )
49 48 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. RR ) <-> ( ph /\ y e. RR ) ) )
50 oveq1 
 |-  ( x = y -> ( x + T ) = ( y + T ) )
51 50 fveq2d 
 |-  ( x = y -> ( F ` ( x + T ) ) = ( F ` ( y + T ) ) )
52 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
53 51 52 eqeq12d 
 |-  ( x = y -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( y + T ) ) = ( F ` y ) ) )
54 49 53 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ y e. RR ) -> ( F ` ( y + T ) ) = ( F ` y ) ) ) )
55 54 3 chvarvv 
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + T ) ) = ( F ` y ) )
56 55 ad4ant14 
 |-  ( ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) /\ y e. RR ) -> ( F ` ( y + T ) ) = ( F ` y ) )
57 44 45 46 47 56 fperiodmul 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
58 38 39 27 57 syl21anc 
 |-  ( ( ph /\ x e. RR /\ k e. ZZ ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
59 40 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> RR C_ CC )
60 ioossre 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
61 60 a1i 
 |-  ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
62 1 61 fssresd 
 |-  ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
63 62 41 fssd 
 |-  ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
64 63 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
65 60 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
66 42 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : RR --> CC )
67 25 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> RR C_ RR )
68 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
69 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
70 68 69 dvres 
 |-  ( ( ( RR C_ CC /\ F : RR --> CC ) /\ ( RR C_ RR /\ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
71 59 66 67 65 70 syl22anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
72 71 dmeqd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = dom ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
73 ioontr 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) )
74 73 reseq2i 
 |-  ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
75 74 dmeqi 
 |-  dom ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
76 75 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
77 cncff 
 |-  ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
78 fdm 
 |-  ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC -> dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
79 8 77 78 3syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
80 72 76 79 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
81 dvcn 
 |-  ( ( ( RR C_ CC /\ ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC /\ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR ) /\ dom ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
82 59 64 65 80 81 syl31anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
83 65 40 sstrdi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
84 5 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
85 6 84 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
86 7 85 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
87 86 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
88 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
89 87 88 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
90 89 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
91 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
92 91 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
93 90 92 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
94 93 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
95 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
96 95 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
97 90 96 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
98 86 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
99 98 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
100 68 94 97 99 lptioo2cn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
101 62 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
102 41 42 26 dvbss 
 |-  ( ph -> dom ( RR _D F ) C_ RR )
103 dvfre 
 |-  ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
104 1 26 103 syl2anc 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
105 86 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
106 105 simplld 
 |-  ( ph -> ( Q ` 0 ) = -u _pi )
107 105 simplrd 
 |-  ( ph -> ( Q ` M ) = _pi )
108 8 77 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
109 97 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
110 68 109 93 99 lptioo1cn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
111 108 83 110 9 68 ellimciota 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( iota x x e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
112 108 83 100 10 68 ellimciota 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( iota x x e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) ) e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
113 28 adantl 
 |-  ( ( ph /\ k e. ZZ ) -> k e. RR )
114 113 34 remulcld 
 |-  ( ( ph /\ k e. ZZ ) -> ( k x. T ) e. RR )
115 43 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> F : RR --> CC )
116 34 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> T e. RR )
117 simplr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> k e. ZZ )
118 simpr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> t e. RR )
119 3 ad4ant14 
 |-  ( ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
120 115 116 117 118 119 fperiodmul 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> ( F ` ( t + ( k x. T ) ) ) = ( F ` t ) )
121 eqid 
 |-  ( RR _D F ) = ( RR _D F )
122 43 114 120 121 fperdvper 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. dom ( RR _D F ) ) -> ( ( t + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( t + ( k x. T ) ) ) = ( ( RR _D F ) ` t ) ) )
123 122 an32s 
 |-  ( ( ( ph /\ t e. dom ( RR _D F ) ) /\ k e. ZZ ) -> ( ( t + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( t + ( k x. T ) ) ) = ( ( RR _D F ) ` t ) ) )
124 123 simpld 
 |-  ( ( ( ph /\ t e. dom ( RR _D F ) ) /\ k e. ZZ ) -> ( t + ( k x. T ) ) e. dom ( RR _D F ) )
125 123 simprd 
 |-  ( ( ( ph /\ t e. dom ( RR _D F ) ) /\ k e. ZZ ) -> ( ( RR _D F ) ` ( t + ( k x. T ) ) ) = ( ( RR _D F ) ` t ) )
126 fveq2 
 |-  ( j = i -> ( Q ` j ) = ( Q ` i ) )
127 oveq1 
 |-  ( j = i -> ( j + 1 ) = ( i + 1 ) )
128 127 fveq2d 
 |-  ( j = i -> ( Q ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) )
129 126 128 oveq12d 
 |-  ( j = i -> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
130 129 cbvmptv 
 |-  ( j e. ( 0 ..^ M ) |-> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) = ( i e. ( 0 ..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
131 eqid 
 |-  ( t e. RR |-> ( t + ( ( |_ ` ( ( _pi - t ) / T ) ) x. T ) ) ) = ( t e. RR |-> ( t + ( ( |_ ` ( ( _pi - t ) / T ) ) x. T ) ) )
132 102 104 13 14 20 24 6 89 106 107 8 111 112 124 125 130 131 fourierdlem71 
 |-  ( ph -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
133 132 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
134 nfv 
 |-  F/ t ( ph /\ i e. ( 0 ..^ M ) )
135 nfra1 
 |-  F/ t A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z
136 134 135 nfan 
 |-  F/ t ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
137 71 74 eqtrdi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
138 137 fveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) = ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) )
139 fvres 
 |-  ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
140 138 139 sylan9eq 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
141 140 fveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
142 141 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
143 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
144 ssdmres 
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
145 79 144 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
146 145 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
147 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
148 146 147 sseldd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. dom ( RR _D F ) )
149 rspa 
 |-  ( ( A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z /\ t e. dom ( RR _D F ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
150 143 148 149 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
151 142 150 eqbrtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z )
152 151 ex 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z ) )
153 136 152 ralrimi 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) -> A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z )
154 153 ex 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z ) )
155 154 reximdv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> E. z e. RR A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z ) )
156 133 155 mpd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. z e. RR A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z )
157 93 97 101 80 156 ioodvbdlimc2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) =/= (/) )
158 64 83 100 157 68 ellimciota 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( iota y y e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
159 oveq2 
 |-  ( y = x -> ( _pi - y ) = ( _pi - x ) )
160 159 oveq1d 
 |-  ( y = x -> ( ( _pi - y ) / T ) = ( ( _pi - x ) / T ) )
161 160 fveq2d 
 |-  ( y = x -> ( |_ ` ( ( _pi - y ) / T ) ) = ( |_ ` ( ( _pi - x ) / T ) ) )
162 161 oveq1d 
 |-  ( y = x -> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) = ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) )
163 162 cbvmptv 
 |-  ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) = ( x e. RR |-> ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) )
164 id 
 |-  ( z = x -> z = x )
165 fveq2 
 |-  ( z = x -> ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` z ) = ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` x ) )
166 164 165 oveq12d 
 |-  ( z = x -> ( z + ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` z ) ) = ( x + ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` x ) ) )
167 166 cbvmptv 
 |-  ( z e. RR |-> ( z + ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` z ) ) ) = ( x e. RR |-> ( x + ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` x ) ) )
168 13 14 20 5 24 6 7 26 1 37 58 82 158 4 163 167 fourierdlem49 
 |-  ( ph -> ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) )
169 93 97 101 80 156 ioodvbdlimc1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) =/= (/) )
170 64 83 110 169 68 ellimciota 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( iota y y e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
171 biid 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ZZ ) /\ w = ( X + ( k x. T ) ) ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ZZ ) /\ w = ( X + ( k x. T ) ) ) )
172 13 14 20 5 24 6 7 1 37 58 82 170 4 163 167 171 fourierdlem48 
 |-  ( ph -> ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) )
173 168 172 jca 
 |-  ( ph -> ( ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) /\ ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) )