Metamath Proof Explorer

Theorem fourierdlem106

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 fourierdlem106.f 
|- ( ph -> F : RR --> RR )
fourierdlem106.t 
|- T = ( 2 x. _pi )
fourierdlem106.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem106.g 
|- G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
fourierdlem106.dmdv 
|- ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
fourierdlem106.dvcn 
|- ( ph -> G e. ( dom G -cn-> CC ) )
fourierdlem106.rlim 
|- ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
fourierdlem106.llim 
|- ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
fourierdlem106.x 
|- ( ph -> X e. RR )
Assertion fourierdlem106 
|- ( ph -> ( ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) /\ ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem106.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem106.t 
 |-  T = ( 2 x. _pi )
3 fourierdlem106.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fourierdlem106.g 
 |-  G = ( ( RR _D F ) |` ( -u _pi (,) _pi ) )
5 fourierdlem106.dmdv 
 |-  ( ph -> ( ( -u _pi (,) _pi ) \ dom G ) e. Fin )
6 fourierdlem106.dvcn 
 |-  ( ph -> G e. ( dom G -cn-> CC ) )
7 fourierdlem106.rlim 
 |-  ( ( ph /\ x e. ( ( -u _pi [,) _pi ) \ dom G ) ) -> ( ( G |` ( x (,) +oo ) ) limCC x ) =/= (/) )
8 fourierdlem106.llim 
 |-  ( ( ph /\ x e. ( ( -u _pi (,] _pi ) \ dom G ) ) -> ( ( G |` ( -oo (,) x ) ) limCC x ) =/= (/) )
9 fourierdlem106.x 
 |-  ( ph -> X e. RR )
10 eqid 
 |-  ( k e. NN |-> { w e. ( RR ^m ( 0 ... k ) ) | ( ( ( w ` 0 ) = -u _pi /\ ( w ` k ) = _pi ) /\ A. z e. ( 0 ..^ k ) ( w ` z ) < ( w ` ( z + 1 ) ) ) } ) = ( k e. NN |-> { w e. ( RR ^m ( 0 ... k ) ) | ( ( ( w ` 0 ) = -u _pi /\ ( w ` k ) = _pi ) /\ A. z e. ( 0 ..^ k ) ( w ` z ) < ( w ` ( z + 1 ) ) ) } )
11 id 
 |-  ( y = x -> y = x )
12 oveq2 
 |-  ( y = x -> ( _pi - y ) = ( _pi - x ) )
13 12 oveq1d 
 |-  ( y = x -> ( ( _pi - y ) / T ) = ( ( _pi - x ) / T ) )
14 13 fveq2d 
 |-  ( y = x -> ( |_ ` ( ( _pi - y ) / T ) ) = ( |_ ` ( ( _pi - x ) / T ) ) )
15 14 oveq1d 
 |-  ( y = x -> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) = ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) )
16 11 15 oveq12d 
 |-  ( y = x -> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) = ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) )
17 16 cbvmptv 
 |-  ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) )
18 eqid 
 |-  ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) = ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) )
19 eqid 
 |-  ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) = ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 )
20 isoeq1 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) ) )
21 20 cbviotavw 
 |-  ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) - 1 ) ) , ( { -u _pi , _pi , ( ( y e. RR |-> ( y + ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ) ` X ) } u. ( ( -u _pi [,] _pi ) \ dom G ) ) ) )
22 1 2 3 4 5 6 7 8 9 10 17 18 19 21 fourierdlem102 
 |-  ( ph -> ( ( ( F |` ( -oo (,) X ) ) limCC X ) =/= (/) /\ ( ( F |` ( X (,) +oo ) ) limCC X ) =/= (/) ) )