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 ffvelrnd 
 |-  ( ph -> ( F ` A ) e. RR )
8 7 recnd 
 |-  ( ph -> ( F ` A ) e. CC )
9 8 idi 
 |-  ( ph -> ( F ` A ) e. CC )
10 2 4 ffvelrnd 
 |-  ( ph -> ( G ` B ) e. RR )
11 10 recnd 
 |-  ( ph -> ( G ` B ) e. CC )
12 11 idi 
 |-  ( ph -> ( G ` B ) e. CC )
13 9 12 mulcld 
 |-  ( ph -> ( ( F ` A ) x. ( G ` B ) ) e. CC )
14 13 abscld 
 |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) e. RR )
15 imaco 
 |-  ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) )
16 15 eqcomi 
 |-  ( abs " ( F " RR ) ) = ( ( abs o. F ) " RR )
17 imassrn 
 |-  ( ( abs o. F ) " RR ) C_ ran ( abs o. F )
18 17 a1i 
 |-  ( ph -> ( ( abs o. F ) " RR ) C_ ran ( abs o. F ) )
19 absf 
 |-  abs : CC --> RR
20 19 a1i 
 |-  ( ph -> abs : CC --> RR )
21 ax-resscn 
 |-  RR C_ CC
22 21 a1i 
 |-  ( ph -> RR C_ CC )
23 20 22 fssresd 
 |-  ( ph -> ( abs |` RR ) : RR --> RR )
24 1 23 fco2d 
 |-  ( ph -> ( abs o. F ) : RR --> RR )
25 24 frnd 
 |-  ( ph -> ran ( abs o. F ) C_ RR )
26 18 25 sstrd 
 |-  ( ph -> ( ( abs o. F ) " RR ) C_ RR )
27 16 26 eqsstrid 
 |-  ( ph -> ( abs " ( F " RR ) ) C_ RR )
28 0re 
 |-  0 e. RR
29 28 ne0ii 
 |-  RR =/= (/)
30 29 a1i 
 |-  ( ph -> RR =/= (/) )
31 30 24 wnefimgd 
 |-  ( ph -> ( ( abs o. F ) " RR ) =/= (/) )
32 31 necomd 
 |-  ( ph -> (/) =/= ( ( abs o. F ) " RR ) )
33 16 a1i 
 |-  ( ph -> ( abs " ( F " RR ) ) = ( ( abs o. F ) " RR ) )
34 32 33 neeqtrrd 
 |-  ( ph -> (/) =/= ( abs " ( F " RR ) ) )
35 34 necomd 
 |-  ( ph -> ( abs " ( F " RR ) ) =/= (/) )
36 1red 
 |-  ( ph -> 1 e. RR )
37 simpr 
 |-  ( ( ph /\ c = 1 ) -> c = 1 )
38 37 breq2d 
 |-  ( ( ph /\ c = 1 ) -> ( x <_ c <-> x <_ 1 ) )
39 38 ralbidv 
 |-  ( ( ph /\ c = 1 ) -> ( A. x e. ( abs " ( F " RR ) ) x <_ c <-> A. x e. ( abs " ( F " RR ) ) x <_ 1 ) )
40 1 6 extoimad 
 |-  ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ 1 )
41 36 39 40 rspcedvd 
 |-  ( ph -> E. c e. RR A. x e. ( abs " ( F " RR ) ) x <_ c )
42 27 35 41 suprcld 
 |-  ( ph -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. RR )
43 2re 
 |-  2 e. RR
44 43 a1i 
 |-  ( ph -> 2 e. RR )
45 5 idi 
 |-  ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) )
46 45 fveq2d 
 |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) = ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) )
47 2cnd 
 |-  ( ph -> 2 e. CC )
48 47 13 mulcld 
 |-  ( ph -> ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) e. CC )
49 48 abscld 
 |-  ( ph -> ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) e. RR )
50 46 49 eqeltrd 
 |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) e. RR )
51 1 idi 
 |-  ( ph -> F : RR --> RR )
52 3 idi 
 |-  ( ph -> A e. RR )
53 4 idi 
 |-  ( ph -> B e. RR )
54 52 53 readdcld 
 |-  ( ph -> ( A + B ) e. RR )
55 51 54 ffvelrnd 
 |-  ( ph -> ( F ` ( A + B ) ) e. RR )
56 55 recnd 
 |-  ( ph -> ( F ` ( A + B ) ) e. CC )
57 56 abscld 
 |-  ( ph -> ( abs ` ( F ` ( A + B ) ) ) e. RR )
58 52 53 resubcld 
 |-  ( ph -> ( A - B ) e. RR )
59 51 58 ffvelrnd 
 |-  ( ph -> ( F ` ( A - B ) ) e. RR )
60 59 recnd 
 |-  ( ph -> ( F ` ( A - B ) ) e. CC )
61 60 abscld 
 |-  ( ph -> ( abs ` ( F ` ( A - B ) ) ) e. RR )
62 57 61 readdcld 
 |-  ( ph -> ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) e. RR )
63 44 42 remulcld 
 |-  ( ph -> ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) e. RR )
64 56 60 abstrid 
 |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) <_ ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) )
65 1 54 fvco3d 
 |-  ( ph -> ( ( abs o. F ) ` ( A + B ) ) = ( abs ` ( F ` ( A + B ) ) ) )
66 54 24 wfximgfd 
 |-  ( ph -> ( ( abs o. F ) ` ( A + B ) ) e. ( ( abs o. F ) " RR ) )
67 33 idi 
 |-  ( ph -> ( abs " ( F " RR ) ) = ( ( abs o. F ) " RR ) )
68 66 67 eleqtrrd 
 |-  ( ph -> ( ( abs o. F ) ` ( A + B ) ) e. ( abs " ( F " RR ) ) )
69 65 68 eqeltrrd 
 |-  ( ph -> ( abs ` ( F ` ( A + B ) ) ) e. ( abs " ( F " RR ) ) )
70 27 35 41 69 suprubd 
 |-  ( ph -> ( abs ` ( F ` ( A + B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
71 1 58 fvco3d 
 |-  ( ph -> ( ( abs o. F ) ` ( A - B ) ) = ( abs ` ( F ` ( A - B ) ) ) )
72 58 24 wfximgfd 
 |-  ( ph -> ( ( abs o. F ) ` ( A - B ) ) e. ( ( abs o. F ) " RR ) )
73 72 33 eleqtrrd 
 |-  ( ph -> ( ( abs o. F ) ` ( A - B ) ) e. ( abs " ( F " RR ) ) )
74 71 73 eqeltrrd 
 |-  ( ph -> ( abs ` ( F ` ( A - B ) ) ) e. ( abs " ( F " RR ) ) )
75 27 35 41 74 suprubd 
 |-  ( ph -> ( abs ` ( F ` ( A - B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
76 57 61 42 42 70 75 le2addd 
 |-  ( ph -> ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) <_ ( sup ( ( abs " ( F " RR ) ) , RR , < ) + sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
77 42 recnd 
 |-  ( ph -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. CC )
78 77 2timesd 
 |-  ( ph -> ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) = ( sup ( ( abs " ( F " RR ) ) , RR , < ) + sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
79 78 eqcomd 
 |-  ( ph -> ( sup ( ( abs " ( F " RR ) ) , RR , < ) + sup ( ( abs " ( F " RR ) ) , RR , < ) ) = ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
80 79 63 eqeltrd 
 |-  ( ph -> ( sup ( ( abs " ( F " RR ) ) , RR , < ) + sup ( ( abs " ( F " RR ) ) , RR , < ) ) e. RR )
81 76 79 62 80 leeq2d 
 |-  ( ph -> ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
82 50 62 63 64 81 letrd 
 |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
83 82 46 50 63 leeq1d 
 |-  ( ph -> ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
84 0le2 
 |-  0 <_ 2
85 84 a1i 
 |-  ( ph -> 0 <_ 2 )
86 7 idi 
 |-  ( ph -> ( F ` A ) e. RR )
87 10 idi 
 |-  ( ph -> ( G ` B ) e. RR )
88 86 87 remulcld 
 |-  ( ph -> ( ( F ` A ) x. ( G ` B ) ) e. RR )
89 85 44 88 absmulrposd 
 |-  ( ph -> ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) = ( 2 x. ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) ) )
90 83 89 49 63 leeq1d 
 |-  ( ph -> ( 2 x. ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
91 2pos 
 |-  0 < 2
92 91 a1i 
 |-  ( ph -> 0 < 2 )
93 14 42 44 90 92 wwlemuld 
 |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
94 8 11 absmuld 
 |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) = ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) )
95 94 idi 
 |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) = ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) )
96 93 95 14 42 leeq1d 
 |-  ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )