Metamath Proof Explorer

Theorem fourierdlem77

Description: If H is bounded, then U is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem77.f 
|- ( ph -> F : RR --> RR )
fourierdlem77.x 
|- ( ph -> X e. RR )
fourierdlem77.y 
|- ( ph -> Y e. RR )
fourierdlem77.w 
|- ( ph -> W e. RR )
fourierdlem77.h 
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem77.k 
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem77.u 
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
fourierdlem77.bd 
|- ( ph -> E. a e. RR A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a )
Assertion fourierdlem77 
|- ( ph -> E. b e. RR+ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ b )

Proof

Step Hyp Ref Expression
1 fourierdlem77.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem77.x 
 |-  ( ph -> X e. RR )
3 fourierdlem77.y 
 |-  ( ph -> Y e. RR )
4 fourierdlem77.w 
 |-  ( ph -> W e. RR )
5 fourierdlem77.h 
 |-  H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
6 fourierdlem77.k 
 |-  K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
7 fourierdlem77.u 
 |-  U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
8 fourierdlem77.bd 
 |-  ( ph -> E. a e. RR A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a )
9 pire 
 |-  _pi e. RR
10 9 renegcli 
 |-  -u _pi e. RR
11 10 a1i 
 |-  ( T. -> -u _pi e. RR )
12 9 a1i 
 |-  ( T. -> _pi e. RR )
13 pirp 
 |-  _pi e. RR+
14 neglt 
 |-  ( _pi e. RR+ -> -u _pi < _pi )
15 13 14 ax-mp 
 |-  -u _pi < _pi
16 10 9 15 ltleii 
 |-  -u _pi <_ _pi
17 16 a1i 
 |-  ( T. -> -u _pi <_ _pi )
18 6 fourierdlem62 
 |-  K e. ( ( -u _pi [,] _pi ) -cn-> RR )
19 18 a1i 
 |-  ( T. -> K e. ( ( -u _pi [,] _pi ) -cn-> RR ) )
20 11 12 17 19 evthiccabs 
 |-  ( T. -> ( E. c e. ( -u _pi [,] _pi ) A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) /\ E. x e. ( -u _pi [,] _pi ) A. y e. ( -u _pi [,] _pi ) ( abs ` ( K ` x ) ) <_ ( abs ` ( K ` y ) ) ) )
21 20 mptru 
 |-  ( E. c e. ( -u _pi [,] _pi ) A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) /\ E. x e. ( -u _pi [,] _pi ) A. y e. ( -u _pi [,] _pi ) ( abs ` ( K ` x ) ) <_ ( abs ` ( K ` y ) ) )
22 21 simpli 
 |-  E. c e. ( -u _pi [,] _pi ) A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) )
23 22 a1i 
 |-  ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) -> E. c e. ( -u _pi [,] _pi ) A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) )
24 simpl 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> a e. RR )
25 6 fourierdlem43 
 |-  K : ( -u _pi [,] _pi ) --> RR
26 25 ffvelrni 
 |-  ( c e. ( -u _pi [,] _pi ) -> ( K ` c ) e. RR )
27 26 adantl 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> ( K ` c ) e. RR )
28 24 27 remulcld 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> ( a x. ( K ` c ) ) e. RR )
29 28 recnd 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> ( a x. ( K ` c ) ) e. CC )
30 29 abscld 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> ( abs ` ( a x. ( K ` c ) ) ) e. RR )
31 29 absge0d 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> 0 <_ ( abs ` ( a x. ( K ` c ) ) ) )
32 30 31 ge0p1rpd 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) e. RR+ )
33 32 3ad2antl2 
 |-  ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) e. RR+ )
34 33 3adant3 
 |-  ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) -> ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) e. RR+ )
35 nfv 
 |-  F/ s ph
36 nfv 
 |-  F/ s a e. RR
37 nfra1 
 |-  F/ s A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a
38 35 36 37 nf3an 
 |-  F/ s ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a )
39 nfv 
 |-  F/ s c e. ( -u _pi [,] _pi )
40 nfra1 
 |-  F/ s A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) )
41 38 39 40 nf3an 
 |-  F/ s ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) )
42 simpl11 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ph )
43 simpl12 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> a e. RR )
44 42 43 jca 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ph /\ a e. RR ) )
45 simpl13 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a )
46 rspa 
 |-  ( ( A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( H ` s ) ) <_ a )
47 45 46 sylancom 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( H ` s ) ) <_ a )
48 simpl2 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> c e. ( -u _pi [,] _pi ) )
49 44 47 48 jca31 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) )
50 rspa 
 |-  ( ( A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) )
51 50 3ad2antl3 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) )
52 simpr 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( -u _pi [,] _pi ) )
53 simp-5l 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ph )
54 simpr 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( -u _pi [,] _pi ) )
55 1 2 3 4 5 fourierdlem9 
 |-  ( ph -> H : ( -u _pi [,] _pi ) --> RR )
56 55 ffvelrnda 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( H ` s ) e. RR )
57 25 ffvelrni 
 |-  ( s e. ( -u _pi [,] _pi ) -> ( K ` s ) e. RR )
58 57 adantl 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( K ` s ) e. RR )
59 56 58 remulcld 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( ( H ` s ) x. ( K ` s ) ) e. RR )
60 7 fvmpt2 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ ( ( H ` s ) x. ( K ` s ) ) e. RR ) -> ( U ` s ) = ( ( H ` s ) x. ( K ` s ) ) )
61 54 59 60 syl2anc 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( U ` s ) = ( ( H ` s ) x. ( K ` s ) ) )
62 61 59 eqeltrd 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( U ` s ) e. RR )
63 62 recnd 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( U ` s ) e. CC )
64 63 abscld 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) e. RR )
65 53 64 sylancom 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) e. RR )
66 simp-5r 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> a e. RR )
67 simpllr 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> c e. ( -u _pi [,] _pi ) )
68 66 67 30 syl2anc 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( a x. ( K ` c ) ) ) e. RR )
69 peano2re 
 |-  ( ( abs ` ( a x. ( K ` c ) ) ) e. RR -> ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) e. RR )
70 68 69 syl 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) e. RR )
71 61 fveq2d 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) = ( abs ` ( ( H ` s ) x. ( K ` s ) ) ) )
72 53 71 sylancom 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) = ( abs ` ( ( H ` s ) x. ( K ` s ) ) ) )
73 56 recnd 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( H ` s ) e. CC )
74 73 abscld 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( H ` s ) ) e. RR )
75 53 74 sylancom 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( H ` s ) ) e. RR )
76 recn 
 |-  ( a e. RR -> a e. CC )
77 76 abscld 
 |-  ( a e. RR -> ( abs ` a ) e. RR )
78 66 77 syl 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` a ) e. RR )
79 57 recnd 
 |-  ( s e. ( -u _pi [,] _pi ) -> ( K ` s ) e. CC )
80 79 abscld 
 |-  ( s e. ( -u _pi [,] _pi ) -> ( abs ` ( K ` s ) ) e. RR )
81 80 adantl 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( K ` s ) ) e. RR )
82 26 recnd 
 |-  ( c e. ( -u _pi [,] _pi ) -> ( K ` c ) e. CC )
83 82 abscld 
 |-  ( c e. ( -u _pi [,] _pi ) -> ( abs ` ( K ` c ) ) e. RR )
84 67 83 syl 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( K ` c ) ) e. RR )
85 73 absge0d 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> 0 <_ ( abs ` ( H ` s ) ) )
86 53 85 sylancom 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> 0 <_ ( abs ` ( H ` s ) ) )
87 82 absge0d 
 |-  ( c e. ( -u _pi [,] _pi ) -> 0 <_ ( abs ` ( K ` c ) ) )
88 67 87 syl 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> 0 <_ ( abs ` ( K ` c ) ) )
89 74 ad4ant14 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( H ` s ) ) e. RR )
90 simpllr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ s e. ( -u _pi [,] _pi ) ) -> a e. RR )
91 77 ad3antlr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` a ) e. RR )
92 simplr 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( H ` s ) ) <_ a )
93 90 leabsd 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ s e. ( -u _pi [,] _pi ) ) -> a <_ ( abs ` a ) )
94 89 90 91 92 93 letrd 
 |-  ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( H ` s ) ) <_ ( abs ` a ) )
95 94 ad4ant14 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( H ` s ) ) <_ ( abs ` a ) )
96 simplr 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) )
97 75 78 81 84 86 88 95 96 lemul12bd 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( abs ` ( H ` s ) ) x. ( abs ` ( K ` s ) ) ) <_ ( ( abs ` a ) x. ( abs ` ( K ` c ) ) ) )
98 58 recnd 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( K ` s ) e. CC )
99 73 98 absmuld 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( H ` s ) x. ( K ` s ) ) ) = ( ( abs ` ( H ` s ) ) x. ( abs ` ( K ` s ) ) ) )
100 53 99 sylancom 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( H ` s ) x. ( K ` s ) ) ) = ( ( abs ` ( H ` s ) ) x. ( abs ` ( K ` s ) ) ) )
101 76 adantr 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> a e. CC )
102 27 recnd 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> ( K ` c ) e. CC )
103 101 102 absmuld 
 |-  ( ( a e. RR /\ c e. ( -u _pi [,] _pi ) ) -> ( abs ` ( a x. ( K ` c ) ) ) = ( ( abs ` a ) x. ( abs ` ( K ` c ) ) ) )
104 66 67 103 syl2anc 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( a x. ( K ` c ) ) ) = ( ( abs ` a ) x. ( abs ` ( K ` c ) ) ) )
105 97 100 104 3brtr4d 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( ( H ` s ) x. ( K ` s ) ) ) <_ ( abs ` ( a x. ( K ` c ) ) ) )
106 72 105 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) <_ ( abs ` ( a x. ( K ` c ) ) ) )
107 68 ltp1d 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( a x. ( K ` c ) ) ) < ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) )
108 65 68 70 106 107 lelttrd 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) < ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) )
109 65 70 108 ltled 
 |-  ( ( ( ( ( ( ph /\ a e. RR ) /\ ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) ) /\ ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) <_ ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) )
110 49 51 52 109 syl21anc 
 |-  ( ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) /\ s e. ( -u _pi [,] _pi ) ) -> ( abs ` ( U ` s ) ) <_ ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) )
111 110 ex 
 |-  ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) -> ( s e. ( -u _pi [,] _pi ) -> ( abs ` ( U ` s ) ) <_ ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) ) )
112 41 111 ralrimi 
 |-  ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) -> A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) )
113 breq2 
 |-  ( b = ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) -> ( ( abs ` ( U ` s ) ) <_ b <-> ( abs ` ( U ` s ) ) <_ ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) ) )
114 113 ralbidv 
 |-  ( b = ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) -> ( A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ b <-> A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) ) )
115 114 rspcev 
 |-  ( ( ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) e. RR+ /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ ( ( abs ` ( a x. ( K ` c ) ) ) + 1 ) ) -> E. b e. RR+ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ b )
116 34 112 115 syl2anc 
 |-  ( ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) /\ c e. ( -u _pi [,] _pi ) /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) ) -> E. b e. RR+ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ b )
117 116 rexlimdv3a 
 |-  ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) -> ( E. c e. ( -u _pi [,] _pi ) A. s e. ( -u _pi [,] _pi ) ( abs ` ( K ` s ) ) <_ ( abs ` ( K ` c ) ) -> E. b e. RR+ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ b ) )
118 23 117 mpd 
 |-  ( ( ph /\ a e. RR /\ A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a ) -> E. b e. RR+ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ b )
119 118 rexlimdv3a 
 |-  ( ph -> ( E. a e. RR A. s e. ( -u _pi [,] _pi ) ( abs ` ( H ` s ) ) <_ a -> E. b e. RR+ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ b ) )
120 8 119 mpd 
 |-  ( ph -> E. b e. RR+ A. s e. ( -u _pi [,] _pi ) ( abs ` ( U ` s ) ) <_ b )