Metamath Proof Explorer

Theorem imo72b2lem0

Description: Lemma for imo72b2 . (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses imo72b2lem0.1 
|- ( ph -> F : RR --> RR )
imo72b2lem0.2 
|- ( ph -> G : RR --> RR )
imo72b2lem0.3 
|- ( ph -> A e. RR )
imo72b2lem0.4 
|- ( ph -> B e. RR )
imo72b2lem0.5 
|- ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) )
imo72b2lem0.6 
|- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )
Assertion imo72b2lem0 
|- ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )

Proof

Step Hyp Ref Expression
1 imo72b2lem0.1 
 |-  ( ph -> F : RR --> RR )
2 imo72b2lem0.2 
 |-  ( ph -> G : RR --> RR )
3 imo72b2lem0.3 
 |-  ( ph -> A e. RR )
4 imo72b2lem0.4 
 |-  ( ph -> B e. RR )
5 imo72b2lem0.5 
 |-  ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) )
6 imo72b2lem0.6 
 |-  ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )
7 1 3 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. RR )
8 7 recnd 
 |-  ( ph -> ( F ` A ) e. CC )
9 2 4 ffvelcdmd 
 |-  ( ph -> ( G ` B ) e. RR )
10 9 recnd 
 |-  ( ph -> ( G ` B ) e. CC )
11 8 10 absmuld 
 |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) = ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) )
12 8 10 mulcld 
 |-  ( ph -> ( ( F ` A ) x. ( G ` B ) ) e. CC )
13 12 abscld 
 |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) e. RR )
14 absf 
 |-  abs : CC --> RR
15 14 a1i 
 |-  ( ph -> abs : CC --> RR )
16 15 fimassd 
 |-  ( ph -> ( abs " ( F " RR ) ) C_ RR )
17 imaco 
 |-  ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) )
18 3 ne0d 
 |-  ( ph -> RR =/= (/) )
19 ax-resscn 
 |-  RR C_ CC
20 19 a1i 
 |-  ( ph -> RR C_ CC )
21 15 20 fssresd 
 |-  ( ph -> ( abs |` RR ) : RR --> RR )
22 1 21 fco2d 
 |-  ( ph -> ( abs o. F ) : RR --> RR )
23 18 22 wnefimgd 
 |-  ( ph -> ( ( abs o. F ) " RR ) =/= (/) )
24 17 23 eqnetrrid 
 |-  ( ph -> ( abs " ( F " RR ) ) =/= (/) )
25 1red 
 |-  ( ph -> 1 e. RR )
26 simpr 
 |-  ( ( ph /\ c = 1 ) -> c = 1 )
27 26 breq2d 
 |-  ( ( ph /\ c = 1 ) -> ( x <_ c <-> x <_ 1 ) )
28 27 ralbidv 
 |-  ( ( ph /\ c = 1 ) -> ( A. x e. ( abs " ( F " RR ) ) x <_ c <-> A. x e. ( abs " ( F " RR ) ) x <_ 1 ) )
29 1 6 extoimad 
 |-  ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ 1 )
30 25 28 29 rspcedvd 
 |-  ( ph -> E. c e. RR A. x e. ( abs " ( F " RR ) ) x <_ c )
31 16 24 30 suprcld 
 |-  ( ph -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. RR )
32 2re 
 |-  2 e. RR
33 32 a1i 
 |-  ( ph -> 2 e. RR )
34 0le2 
 |-  0 <_ 2
35 34 a1i 
 |-  ( ph -> 0 <_ 2 )
36 7 9 remulcld 
 |-  ( ph -> ( ( F ` A ) x. ( G ` B ) ) e. RR )
37 35 33 36 absmulrposd 
 |-  ( ph -> ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) = ( 2 x. ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) ) )
38 5 fveq2d 
 |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) = ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) )
39 2cnd 
 |-  ( ph -> 2 e. CC )
40 39 12 mulcld 
 |-  ( ph -> ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) e. CC )
41 40 abscld 
 |-  ( ph -> ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) e. RR )
42 38 41 eqeltrd 
 |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) e. RR )
43 3 4 readdcld 
 |-  ( ph -> ( A + B ) e. RR )
44 1 43 ffvelcdmd 
 |-  ( ph -> ( F ` ( A + B ) ) e. RR )
45 44 recnd 
 |-  ( ph -> ( F ` ( A + B ) ) e. CC )
46 45 abscld 
 |-  ( ph -> ( abs ` ( F ` ( A + B ) ) ) e. RR )
47 3 4 resubcld 
 |-  ( ph -> ( A - B ) e. RR )
48 1 47 ffvelcdmd 
 |-  ( ph -> ( F ` ( A - B ) ) e. RR )
49 48 recnd 
 |-  ( ph -> ( F ` ( A - B ) ) e. CC )
50 49 abscld 
 |-  ( ph -> ( abs ` ( F ` ( A - B ) ) ) e. RR )
51 46 50 readdcld 
 |-  ( ph -> ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) e. RR )
52 33 31 remulcld 
 |-  ( ph -> ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) e. RR )
53 45 49 abstrid 
 |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) <_ ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) )
54 1 43 fvco3d 
 |-  ( ph -> ( ( abs o. F ) ` ( A + B ) ) = ( abs ` ( F ` ( A + B ) ) ) )
55 43 22 wfximgfd 
 |-  ( ph -> ( ( abs o. F ) ` ( A + B ) ) e. ( ( abs o. F ) " RR ) )
56 55 17 eleqtrdi 
 |-  ( ph -> ( ( abs o. F ) ` ( A + B ) ) e. ( abs " ( F " RR ) ) )
57 54 56 eqeltrrd 
 |-  ( ph -> ( abs ` ( F ` ( A + B ) ) ) e. ( abs " ( F " RR ) ) )
58 16 24 30 57 suprubd 
 |-  ( ph -> ( abs ` ( F ` ( A + B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
59 1 47 fvco3d 
 |-  ( ph -> ( ( abs o. F ) ` ( A - B ) ) = ( abs ` ( F ` ( A - B ) ) ) )
60 47 22 wfximgfd 
 |-  ( ph -> ( ( abs o. F ) ` ( A - B ) ) e. ( ( abs o. F ) " RR ) )
61 60 17 eleqtrdi 
 |-  ( ph -> ( ( abs o. F ) ` ( A - B ) ) e. ( abs " ( F " RR ) ) )
62 59 61 eqeltrrd 
 |-  ( ph -> ( abs ` ( F ` ( A - B ) ) ) e. ( abs " ( F " RR ) ) )
63 16 24 30 62 suprubd 
 |-  ( ph -> ( abs ` ( F ` ( A - B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
64 46 50 31 31 58 63 le2addd 
 |-  ( ph -> ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) <_ ( sup ( ( abs " ( F " RR ) ) , RR , < ) + sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
65 31 recnd 
 |-  ( ph -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. CC )
66 65 2timesd 
 |-  ( ph -> ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) = ( sup ( ( abs " ( F " RR ) ) , RR , < ) + sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
67 64 66 breqtrrd 
 |-  ( ph -> ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
68 42 51 52 53 67 letrd 
 |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
69 38 68 eqbrtrrd 
 |-  ( ph -> ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
70 37 69 eqbrtrrd 
 |-  ( ph -> ( 2 x. ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
71 2pos 
 |-  0 < 2
72 71 a1i 
 |-  ( ph -> 0 < 2 )
73 13 31 33 70 72 wwlemuld 
 |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
74 11 73 eqbrtrrd 
 |-  ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )