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 ) =/= (/) ) )