Metamath Proof Explorer

Theorem imo72b2

Description: IMO 1972 B2. (14th International Mathemahics Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses imo72b2.1 
|- ( ph -> F : RR --> RR )
imo72b2.2 
|- ( ph -> G : RR --> RR )
imo72b2.4 
|- ( ph -> B e. RR )
imo72b2.5 
|- ( ph -> A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) )
imo72b2.6 
|- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )
imo72b2.7 
|- ( ph -> E. x e. RR ( F ` x ) =/= 0 )
Assertion imo72b2 
|- ( ph -> ( abs ` ( G ` B ) ) <_ 1 )

Proof

Step Hyp Ref Expression
1 imo72b2.1 
 |-  ( ph -> F : RR --> RR )
2 imo72b2.2 
 |-  ( ph -> G : RR --> RR )
3 imo72b2.4 
 |-  ( ph -> B e. RR )
4 imo72b2.5 
 |-  ( ph -> A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) )
5 imo72b2.6 
 |-  ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )
6 imo72b2.7 
 |-  ( ph -> E. x e. RR ( F ` x ) =/= 0 )
7 2 3 ffvelrnd 
 |-  ( ph -> ( G ` B ) e. RR )
8 7 recnd 
 |-  ( ph -> ( G ` B ) e. CC )
9 8 abscld 
 |-  ( ph -> ( abs ` ( G ` B ) ) e. RR )
10 1red 
 |-  ( ph -> 1 e. RR )
11 simpr 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> 1 < ( abs ` ( G ` B ) ) )
12 2 adantr 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> G : RR --> RR )
13 3 adantr 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> B e. RR )
14 12 13 ffvelrnd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( G ` B ) e. RR )
15 14 recnd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( G ` B ) e. CC )
16 15 abscld 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs ` ( G ` B ) ) e. RR )
17 10 adantr 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> 1 e. RR )
18 ax-resscn 
 |-  RR C_ CC
19 imaco 
 |-  ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) )
20 19 eqcomi 
 |-  ( abs " ( F " RR ) ) = ( ( abs o. F ) " RR )
21 imassrn 
 |-  ( ( abs o. F ) " RR ) C_ ran ( abs o. F )
22 21 a1i 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( ( abs o. F ) " RR ) C_ ran ( abs o. F ) )
23 1 adantr 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> F : RR --> RR )
24 absf 
 |-  abs : CC --> RR
25 24 a1i 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> abs : CC --> RR )
26 18 a1i 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> RR C_ CC )
27 25 26 fssresd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs |` RR ) : RR --> RR )
28 23 27 fco2d 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs o. F ) : RR --> RR )
29 28 frnd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ran ( abs o. F ) C_ RR )
30 22 29 sstrd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( ( abs o. F ) " RR ) C_ RR )
31 20 30 eqsstrid 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs " ( F " RR ) ) C_ RR )
32 0re 
 |-  0 e. RR
33 32 ne0ii 
 |-  RR =/= (/)
34 33 a1i 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> RR =/= (/) )
35 34 28 wnefimgd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( ( abs o. F ) " RR ) =/= (/) )
36 35 necomd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> (/) =/= ( ( abs o. F ) " RR ) )
37 20 a1i 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs " ( F " RR ) ) = ( ( abs o. F ) " RR ) )
38 36 37 neeqtrrd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> (/) =/= ( abs " ( F " RR ) ) )
39 38 necomd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs " ( F " RR ) ) =/= (/) )
40 simpr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ c = 1 ) -> c = 1 )
41 40 breq2d 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ c = 1 ) -> ( t <_ c <-> t <_ 1 ) )
42 41 ralbidv 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ c = 1 ) -> ( A. t e. ( abs " ( F " RR ) ) t <_ c <-> A. t e. ( abs " ( F " RR ) ) t <_ 1 ) )
43 1 5 extoimad 
 |-  ( ph -> A. t e. ( abs " ( F " RR ) ) t <_ 1 )
44 43 adantr 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> A. t e. ( abs " ( F " RR ) ) t <_ 1 )
45 17 42 44 rspcedvd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> E. c e. RR A. t e. ( abs " ( F " RR ) ) t <_ c )
46 31 39 45 suprcld 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. RR )
47 18 46 sseldi 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. CC )
48 18 16 sseldi 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs ` ( G ` B ) ) e. CC )
49 47 48 mulcomd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( sup ( ( abs " ( F " RR ) ) , RR , < ) x. ( abs ` ( G ` B ) ) ) = ( ( abs ` ( G ` B ) ) x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
50 32 a1i 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> 0 e. RR )
51 0lt1 
 |-  0 < 1
52 51 a1i 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> 0 < 1 )
53 50 17 16 52 11 lttrd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> 0 < ( abs ` ( G ` B ) ) )
54 53 gt0ne0d 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs ` ( G ` B ) ) =/= 0 )
55 46 16 54 redivcld 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( sup ( ( abs " ( F " RR ) ) , RR , < ) / ( abs ` ( G ` B ) ) ) e. RR )
56 23 adantr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> F : RR --> RR )
57 12 adantr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> G : RR --> RR )
58 simpr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> u e. RR )
59 13 adantr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> B e. RR )
60 simpr 
 |-  ( ( ph /\ v = B ) -> v = B )
61 60 oveq2d 
 |-  ( ( ph /\ v = B ) -> ( u + v ) = ( u + B ) )
62 61 fveq2d 
 |-  ( ( ph /\ v = B ) -> ( F ` ( u + v ) ) = ( F ` ( u + B ) ) )
63 60 oveq2d 
 |-  ( ( ph /\ v = B ) -> ( u - v ) = ( u - B ) )
64 63 fveq2d 
 |-  ( ( ph /\ v = B ) -> ( F ` ( u - v ) ) = ( F ` ( u - B ) ) )
65 62 64 oveq12d 
 |-  ( ( ph /\ v = B ) -> ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( ( F ` ( u + B ) ) + ( F ` ( u - B ) ) ) )
66 60 fveq2d 
 |-  ( ( ph /\ v = B ) -> ( G ` v ) = ( G ` B ) )
67 66 oveq2d 
 |-  ( ( ph /\ v = B ) -> ( ( F ` u ) x. ( G ` v ) ) = ( ( F ` u ) x. ( G ` B ) ) )
68 67 oveq2d 
 |-  ( ( ph /\ v = B ) -> ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` B ) ) ) )
69 65 68 eqeq12d 
 |-  ( ( ph /\ v = B ) -> ( ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) <-> ( ( F ` ( u + B ) ) + ( F ` ( u - B ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` B ) ) ) ) )
70 69 ralbidv 
 |-  ( ( ph /\ v = B ) -> ( A. u e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) <-> A. u e. RR ( ( F ` ( u + B ) ) + ( F ` ( u - B ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` B ) ) ) ) )
71 ralcom 
 |-  ( A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) <-> A. v e. RR A. u e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) )
72 71 biimpi 
 |-  ( A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) -> A. v e. RR A. u e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) )
73 72 a1i 
 |-  ( ph -> ( A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) -> A. v e. RR A. u e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) ) )
74 73 imp 
 |-  ( ( ph /\ A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) ) -> A. v e. RR A. u e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) )
75 4 74 mpdan 
 |-  ( ph -> A. v e. RR A. u e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) )
76 70 3 75 rspcdvinvd 
 |-  ( ph -> A. u e. RR ( ( F ` ( u + B ) ) + ( F ` ( u - B ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` B ) ) ) )
77 76 r19.21bi 
 |-  ( ( ph /\ u e. RR ) -> ( ( F ` ( u + B ) ) + ( F ` ( u - B ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` B ) ) ) )
78 77 adantlr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> ( ( F ` ( u + B ) ) + ( F ` ( u - B ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` B ) ) ) )
79 5 ad2antrr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )
80 56 57 58 59 78 79 imo72b2lem0 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> ( ( abs ` ( F ` u ) ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
81 0xr 
 |-  0 e. RR*
82 81 a1i 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> 0 e. RR* )
83 1xr 
 |-  1 e. RR*
84 83 a1i 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> 1 e. RR* )
85 16 adantr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> ( abs ` ( G ` B ) ) e. RR )
86 85 rexrd 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> ( abs ` ( G ` B ) ) e. RR* )
87 51 a1i 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> 0 < 1 )
88 simplr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> 1 < ( abs ` ( G ` B ) ) )
89 82 84 86 87 88 xrlttrd 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> 0 < ( abs ` ( G ` B ) ) )
90 23 ffvelrnda 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> ( F ` u ) e. RR )
91 90 recnd 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> ( F ` u ) e. CC )
92 91 abscld 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> ( abs ` ( F ` u ) ) e. RR )
93 46 adantr 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. RR )
94 80 89 85 92 93 lemuldiv3d 
 |-  ( ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) /\ u e. RR ) -> ( abs ` ( F ` u ) ) <_ ( sup ( ( abs " ( F " RR ) ) , RR , < ) / ( abs ` ( G ` B ) ) ) )
95 94 ralrimiva 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> A. u e. RR ( abs ` ( F ` u ) ) <_ ( sup ( ( abs " ( F " RR ) ) , RR , < ) / ( abs ` ( G ` B ) ) ) )
96 23 55 95 imo72b2lem2 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> sup ( ( abs " ( F " RR ) ) , RR , < ) <_ ( sup ( ( abs " ( F " RR ) ) , RR , < ) / ( abs ` ( G ` B ) ) ) )
97 96 53 16 46 46 lemuldiv4d 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( sup ( ( abs " ( F " RR ) ) , RR , < ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
98 49 97 eqbrtrrd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( ( abs ` ( G ` B ) ) x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
99 6 adantr 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> E. x e. RR ( F ` x ) =/= 0 )
100 5 adantr 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )
101 23 99 100 imo72b2lem1 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> 0 < sup ( ( abs " ( F " RR ) ) , RR , < ) )
102 98 101 46 16 46 lemuldiv3d 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs ` ( G ` B ) ) <_ ( sup ( ( abs " ( F " RR ) ) , RR , < ) / sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
103 26 46 sseldd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. CC )
104 101 gt0ne0d 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> sup ( ( abs " ( F " RR ) ) , RR , < ) =/= 0 )
105 103 104 dividd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( sup ( ( abs " ( F " RR ) ) , RR , < ) / sup ( ( abs " ( F " RR ) ) , RR , < ) ) = 1 )
106 105 eqcomd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> 1 = ( sup ( ( abs " ( F " RR ) ) , RR , < ) / sup ( ( abs " ( F " RR ) ) , RR , < ) ) )
107 102 106 breqtrrd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> ( abs ` ( G ` B ) ) <_ 1 )
108 16 17 107 lensymd 
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> -. 1 < ( abs ` ( G ` B ) ) )
109 11 108 pm2.65da 
 |-  ( ph -> -. 1 < ( abs ` ( G ` B ) ) )
110 9 10 109 nltled 
 |-  ( ph -> ( abs ` ( G ` B ) ) <_ 1 )