Metamath Proof Explorer


Theorem fourierdlem40

Description: H is a continuous function on any partition interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem40.f
|- ( ph -> F : RR --> RR )
fourierdlem40.a
|- ( ph -> A e. ( -u _pi [,] _pi ) )
fourierdlem40.b
|- ( ph -> B e. ( -u _pi [,] _pi ) )
fourierdlem40.x
|- ( ph -> X e. RR )
fourierdlem40.nxelab
|- ( ph -> -. 0 e. ( A (,) B ) )
fourierdlem40.fcn
|- ( ph -> ( F |` ( ( A + X ) (,) ( B + X ) ) ) e. ( ( ( A + X ) (,) ( B + X ) ) -cn-> CC ) )
fourierdlem40.y
|- ( ph -> Y e. RR )
fourierdlem40.w
|- ( ph -> W e. RR )
fourierdlem40.h
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
Assertion fourierdlem40
|- ( ph -> ( H |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 fourierdlem40.f
 |-  ( ph -> F : RR --> RR )
2 fourierdlem40.a
 |-  ( ph -> A e. ( -u _pi [,] _pi ) )
3 fourierdlem40.b
 |-  ( ph -> B e. ( -u _pi [,] _pi ) )
4 fourierdlem40.x
 |-  ( ph -> X e. RR )
5 fourierdlem40.nxelab
 |-  ( ph -> -. 0 e. ( A (,) B ) )
6 fourierdlem40.fcn
 |-  ( ph -> ( F |` ( ( A + X ) (,) ( B + X ) ) ) e. ( ( ( A + X ) (,) ( B + X ) ) -cn-> CC ) )
7 fourierdlem40.y
 |-  ( ph -> Y e. RR )
8 fourierdlem40.w
 |-  ( ph -> W e. RR )
9 fourierdlem40.h
 |-  H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
10 9 reseq1i
 |-  ( H |` ( A (,) B ) ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |` ( A (,) B ) )
11 10 a1i
 |-  ( ph -> ( H |` ( A (,) B ) ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |` ( A (,) B ) ) )
12 pire
 |-  _pi e. RR
13 12 renegcli
 |-  -u _pi e. RR
14 13 a1i
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -u _pi e. RR )
15 12 a1i
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> _pi e. RR )
16 elioore
 |-  ( s e. ( A (,) B ) -> s e. RR )
17 16 adantl
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
18 13 a1i
 |-  ( ph -> -u _pi e. RR )
19 12 a1i
 |-  ( ph -> _pi e. RR )
20 18 19 iccssred
 |-  ( ph -> ( -u _pi [,] _pi ) C_ RR )
21 20 2 sseldd
 |-  ( ph -> A e. RR )
22 21 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR )
23 13 12 elicc2i
 |-  ( A e. ( -u _pi [,] _pi ) <-> ( A e. RR /\ -u _pi <_ A /\ A <_ _pi ) )
24 23 simp2bi
 |-  ( A e. ( -u _pi [,] _pi ) -> -u _pi <_ A )
25 2 24 syl
 |-  ( ph -> -u _pi <_ A )
26 25 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -u _pi <_ A )
27 22 rexrd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR* )
28 20 3 sseldd
 |-  ( ph -> B e. RR )
29 28 rexrd
 |-  ( ph -> B e. RR* )
30 29 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR* )
31 simpr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A (,) B ) )
32 ioogtlb
 |-  ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> A < s )
33 27 30 31 32 syl3anc
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A < s )
34 14 22 17 26 33 lelttrd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -u _pi < s )
35 14 17 34 ltled
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -u _pi <_ s )
36 28 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR )
37 iooltub
 |-  ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> s < B )
38 27 30 31 37 syl3anc
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s < B )
39 13 12 elicc2i
 |-  ( B e. ( -u _pi [,] _pi ) <-> ( B e. RR /\ -u _pi <_ B /\ B <_ _pi ) )
40 39 simp3bi
 |-  ( B e. ( -u _pi [,] _pi ) -> B <_ _pi )
41 3 40 syl
 |-  ( ph -> B <_ _pi )
42 41 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> B <_ _pi )
43 17 36 15 38 42 ltletrd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s < _pi )
44 17 15 43 ltled
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s <_ _pi )
45 14 15 17 35 44 eliccd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( -u _pi [,] _pi ) )
46 45 ex
 |-  ( ph -> ( s e. ( A (,) B ) -> s e. ( -u _pi [,] _pi ) ) )
47 46 ssrdv
 |-  ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) )
48 47 resmptd
 |-  ( ph -> ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) )
49 eleq1
 |-  ( s = 0 -> ( s e. ( A (,) B ) <-> 0 e. ( A (,) B ) ) )
50 49 biimpac
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
51 50 adantll
 |-  ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
52 5 ad2antrr
 |-  ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> -. 0 e. ( A (,) B ) )
53 51 52 pm2.65da
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -. s = 0 )
54 53 iffalsed
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
55 1 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> F : RR --> RR )
56 4 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> X e. RR )
57 56 17 readdcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. RR )
58 55 57 ffvelrnd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. RR )
59 7 8 ifcld
 |-  ( ph -> if ( 0 < s , Y , W ) e. RR )
60 59 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> if ( 0 < s , Y , W ) e. RR )
61 58 60 resubcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. RR )
62 61 recnd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. CC )
63 17 recnd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. CC )
64 53 neqned
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 )
65 62 63 64 divrecd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( 1 / s ) ) )
66 54 65 eqtrd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( 1 / s ) ) )
67 66 mpteq2dva
 |-  ( ph -> ( s e. ( A (,) B ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( 1 / s ) ) ) )
68 11 48 67 3eqtrd
 |-  ( ph -> ( H |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( 1 / s ) ) ) )
69 58 recnd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. CC )
70 60 recnd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> if ( 0 < s , Y , W ) e. CC )
71 69 70 negsubd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) + -u if ( 0 < s , Y , W ) ) = ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) )
72 71 eqcomd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) = ( ( F ` ( X + s ) ) + -u if ( 0 < s , Y , W ) ) )
73 72 mpteq2dva
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) = ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) + -u if ( 0 < s , Y , W ) ) ) )
74 21 4 readdcld
 |-  ( ph -> ( A + X ) e. RR )
75 74 rexrd
 |-  ( ph -> ( A + X ) e. RR* )
76 75 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( A + X ) e. RR* )
77 28 4 readdcld
 |-  ( ph -> ( B + X ) e. RR )
78 77 rexrd
 |-  ( ph -> ( B + X ) e. RR* )
79 78 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( B + X ) e. RR* )
80 21 recnd
 |-  ( ph -> A e. CC )
81 4 recnd
 |-  ( ph -> X e. CC )
82 80 81 addcomd
 |-  ( ph -> ( A + X ) = ( X + A ) )
83 82 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( A + X ) = ( X + A ) )
84 22 17 56 33 ltadd2dd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) < ( X + s ) )
85 83 84 eqbrtrd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( A + X ) < ( X + s ) )
86 17 36 56 38 ltadd2dd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( X + B ) )
87 28 recnd
 |-  ( ph -> B e. CC )
88 81 87 addcomd
 |-  ( ph -> ( X + B ) = ( B + X ) )
89 88 adantr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + B ) = ( B + X ) )
90 86 89 breqtrd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( B + X ) )
91 76 79 57 85 90 eliood
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. ( ( A + X ) (,) ( B + X ) ) )
92 fvres
 |-  ( ( X + s ) e. ( ( A + X ) (,) ( B + X ) ) -> ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) )
93 91 92 syl
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) )
94 93 eqcomd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) = ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) )
95 94 mpteq2dva
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) = ( s e. ( A (,) B ) |-> ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) ) )
96 ioosscn
 |-  ( ( A + X ) (,) ( B + X ) ) C_ CC
97 96 a1i
 |-  ( ph -> ( ( A + X ) (,) ( B + X ) ) C_ CC )
98 ioosscn
 |-  ( A (,) B ) C_ CC
99 98 a1i
 |-  ( ph -> ( A (,) B ) C_ CC )
100 97 6 99 81 91 fourierdlem23
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( F |` ( ( A + X ) (,) ( B + X ) ) ) ` ( X + s ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
101 95 100 eqeltrd
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
102 0red
 |-  ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> 0 e. RR )
103 21 ad2antrr
 |-  ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> A e. RR )
104 16 adantl
 |-  ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> s e. RR )
105 simplr
 |-  ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> 0 <_ A )
106 33 adantlr
 |-  ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> A < s )
107 102 103 104 105 106 lelttrd
 |-  ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> 0 < s )
108 107 iftrued
 |-  ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> if ( 0 < s , Y , W ) = Y )
109 108 negeqd
 |-  ( ( ( ph /\ 0 <_ A ) /\ s e. ( A (,) B ) ) -> -u if ( 0 < s , Y , W ) = -u Y )
110 109 mpteq2dva
 |-  ( ( ph /\ 0 <_ A ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) = ( s e. ( A (,) B ) |-> -u Y ) )
111 7 renegcld
 |-  ( ph -> -u Y e. RR )
112 111 recnd
 |-  ( ph -> -u Y e. CC )
113 ssid
 |-  CC C_ CC
114 113 a1i
 |-  ( ph -> CC C_ CC )
115 99 112 114 constcncfg
 |-  ( ph -> ( s e. ( A (,) B ) |-> -u Y ) e. ( ( A (,) B ) -cn-> CC ) )
116 115 adantr
 |-  ( ( ph /\ 0 <_ A ) -> ( s e. ( A (,) B ) |-> -u Y ) e. ( ( A (,) B ) -cn-> CC ) )
117 110 116 eqeltrd
 |-  ( ( ph /\ 0 <_ A ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) e. ( ( A (,) B ) -cn-> CC ) )
118 21 rexrd
 |-  ( ph -> A e. RR* )
119 118 ad2antrr
 |-  ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> A e. RR* )
120 29 ad2antrr
 |-  ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> B e. RR* )
121 0red
 |-  ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> 0 e. RR )
122 simpr
 |-  ( ( ph /\ -. 0 <_ A ) -> -. 0 <_ A )
123 21 adantr
 |-  ( ( ph /\ -. 0 <_ A ) -> A e. RR )
124 0red
 |-  ( ( ph /\ -. 0 <_ A ) -> 0 e. RR )
125 123 124 ltnled
 |-  ( ( ph /\ -. 0 <_ A ) -> ( A < 0 <-> -. 0 <_ A ) )
126 122 125 mpbird
 |-  ( ( ph /\ -. 0 <_ A ) -> A < 0 )
127 126 adantr
 |-  ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> A < 0 )
128 simpr
 |-  ( ( ph /\ -. B <_ 0 ) -> -. B <_ 0 )
129 0red
 |-  ( ( ph /\ -. B <_ 0 ) -> 0 e. RR )
130 28 adantr
 |-  ( ( ph /\ -. B <_ 0 ) -> B e. RR )
131 129 130 ltnled
 |-  ( ( ph /\ -. B <_ 0 ) -> ( 0 < B <-> -. B <_ 0 ) )
132 128 131 mpbird
 |-  ( ( ph /\ -. B <_ 0 ) -> 0 < B )
133 132 adantlr
 |-  ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> 0 < B )
134 119 120 121 127 133 eliood
 |-  ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> 0 e. ( A (,) B ) )
135 5 ad2antrr
 |-  ( ( ( ph /\ -. 0 <_ A ) /\ -. B <_ 0 ) -> -. 0 e. ( A (,) B ) )
136 134 135 condan
 |-  ( ( ph /\ -. 0 <_ A ) -> B <_ 0 )
137 16 adantl
 |-  ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> s e. RR )
138 0red
 |-  ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> 0 e. RR )
139 28 ad2antrr
 |-  ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> B e. RR )
140 38 adantlr
 |-  ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> s < B )
141 simplr
 |-  ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> B <_ 0 )
142 137 139 138 140 141 ltletrd
 |-  ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> s < 0 )
143 137 138 142 ltnsymd
 |-  ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> -. 0 < s )
144 143 iffalsed
 |-  ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> if ( 0 < s , Y , W ) = W )
145 144 negeqd
 |-  ( ( ( ph /\ B <_ 0 ) /\ s e. ( A (,) B ) ) -> -u if ( 0 < s , Y , W ) = -u W )
146 145 mpteq2dva
 |-  ( ( ph /\ B <_ 0 ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) = ( s e. ( A (,) B ) |-> -u W ) )
147 8 recnd
 |-  ( ph -> W e. CC )
148 147 negcld
 |-  ( ph -> -u W e. CC )
149 99 148 114 constcncfg
 |-  ( ph -> ( s e. ( A (,) B ) |-> -u W ) e. ( ( A (,) B ) -cn-> CC ) )
150 149 adantr
 |-  ( ( ph /\ B <_ 0 ) -> ( s e. ( A (,) B ) |-> -u W ) e. ( ( A (,) B ) -cn-> CC ) )
151 146 150 eqeltrd
 |-  ( ( ph /\ B <_ 0 ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) e. ( ( A (,) B ) -cn-> CC ) )
152 136 151 syldan
 |-  ( ( ph /\ -. 0 <_ A ) -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) e. ( ( A (,) B ) -cn-> CC ) )
153 117 152 pm2.61dan
 |-  ( ph -> ( s e. ( A (,) B ) |-> -u if ( 0 < s , Y , W ) ) e. ( ( A (,) B ) -cn-> CC ) )
154 101 153 addcncf
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) + -u if ( 0 < s , Y , W ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
155 73 154 eqeltrd
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
156 eqid
 |-  ( s e. ( CC \ { 0 } ) |-> ( 1 / s ) ) = ( s e. ( CC \ { 0 } ) |-> ( 1 / s ) )
157 1cnd
 |-  ( ph -> 1 e. CC )
158 156 cdivcncf
 |-  ( 1 e. CC -> ( s e. ( CC \ { 0 } ) |-> ( 1 / s ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) )
159 157 158 syl
 |-  ( ph -> ( s e. ( CC \ { 0 } ) |-> ( 1 / s ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) )
160 velsn
 |-  ( s e. { 0 } <-> s = 0 )
161 53 160 sylnibr
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -. s e. { 0 } )
162 63 161 eldifd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( CC \ { 0 } ) )
163 162 ralrimiva
 |-  ( ph -> A. s e. ( A (,) B ) s e. ( CC \ { 0 } ) )
164 dfss3
 |-  ( ( A (,) B ) C_ ( CC \ { 0 } ) <-> A. s e. ( A (,) B ) s e. ( CC \ { 0 } ) )
165 163 164 sylibr
 |-  ( ph -> ( A (,) B ) C_ ( CC \ { 0 } ) )
166 17 64 rereccld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 / s ) e. RR )
167 166 recnd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 / s ) e. CC )
168 156 159 165 114 167 cncfmptssg
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( 1 / s ) ) e. ( ( A (,) B ) -cn-> CC ) )
169 155 168 mulcncf
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) x. ( 1 / s ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
170 68 169 eqeltrd
 |-  ( ph -> ( H |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )