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 ) )