Metamath Proof Explorer


Theorem imo72b2

Description: IMO 1972 B2. (14th International Mathematical 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 sselid
 |-  ( ( ph /\ 1 < ( abs ` ( G ` B ) ) ) -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. CC )
48 18 16 sselid
 |-  ( ( 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 rspcdv2
 |-  ( 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 )