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 φF:
imo72b2.2 φG:
imo72b2.4 φB
imo72b2.5 φuvFu+v+Fuv=2FuGv
imo72b2.6 φyFy1
imo72b2.7 φxFx0
Assertion imo72b2 φGB1

Proof

Step Hyp Ref Expression
1 imo72b2.1 φF:
2 imo72b2.2 φG:
3 imo72b2.4 φB
4 imo72b2.5 φuvFu+v+Fuv=2FuGv
5 imo72b2.6 φyFy1
6 imo72b2.7 φxFx0
7 2 3 ffvelrnd φGB
8 7 recnd φGB
9 8 abscld φGB
10 1red φ1
11 simpr φ1<GB1<GB
12 2 adantr φ1<GBG:
13 3 adantr φ1<GBB
14 12 13 ffvelrnd φ1<GBGB
15 14 recnd φ1<GBGB
16 15 abscld φ1<GBGB
17 10 adantr φ1<GB1
18 ax-resscn
19 imaco absF=absF
20 19 eqcomi absF=absF
21 imassrn absFranabsF
22 21 a1i φ1<GBabsFranabsF
23 1 adantr φ1<GBF:
24 absf abs:
25 24 a1i φ1<GBabs:
26 18 a1i φ1<GB
27 25 26 fssresd φ1<GBabs:
28 23 27 fco2d φ1<GBabsF:
29 28 frnd φ1<GBranabsF
30 22 29 sstrd φ1<GBabsF
31 20 30 eqsstrid φ1<GBabsF
32 0re 0
33 32 ne0ii
34 33 a1i φ1<GB
35 34 28 wnefimgd φ1<GBabsF
36 35 necomd φ1<GBabsF
37 20 a1i φ1<GBabsF=absF
38 36 37 neeqtrrd φ1<GBabsF
39 38 necomd φ1<GBabsF
40 simpr φ1<GBc=1c=1
41 40 breq2d φ1<GBc=1tct1
42 41 ralbidv φ1<GBc=1tabsFtctabsFt1
43 1 5 extoimad φtabsFt1
44 43 adantr φ1<GBtabsFt1
45 17 42 44 rspcedvd φ1<GBctabsFtc
46 31 39 45 suprcld φ1<GBsupabsF<
47 18 46 sselid φ1<GBsupabsF<
48 18 16 sselid φ1<GBGB
49 47 48 mulcomd φ1<GBsupabsF<GB=GBsupabsF<
50 32 a1i φ1<GB0
51 0lt1 0<1
52 51 a1i φ1<GB0<1
53 50 17 16 52 11 lttrd φ1<GB0<GB
54 53 gt0ne0d φ1<GBGB0
55 46 16 54 redivcld φ1<GBsupabsF<GB
56 23 adantr φ1<GBuF:
57 12 adantr φ1<GBuG:
58 simpr φ1<GBuu
59 13 adantr φ1<GBuB
60 simpr φv=Bv=B
61 60 oveq2d φv=Bu+v=u+B
62 61 fveq2d φv=BFu+v=Fu+B
63 60 oveq2d φv=Buv=uB
64 63 fveq2d φv=BFuv=FuB
65 62 64 oveq12d φv=BFu+v+Fuv=Fu+B+FuB
66 60 fveq2d φv=BGv=GB
67 66 oveq2d φv=BFuGv=FuGB
68 67 oveq2d φv=B2FuGv=2FuGB
69 65 68 eqeq12d φv=BFu+v+Fuv=2FuGvFu+B+FuB=2FuGB
70 69 ralbidv φv=BuFu+v+Fuv=2FuGvuFu+B+FuB=2FuGB
71 ralcom uvFu+v+Fuv=2FuGvvuFu+v+Fuv=2FuGv
72 71 biimpi uvFu+v+Fuv=2FuGvvuFu+v+Fuv=2FuGv
73 72 a1i φuvFu+v+Fuv=2FuGvvuFu+v+Fuv=2FuGv
74 73 imp φuvFu+v+Fuv=2FuGvvuFu+v+Fuv=2FuGv
75 4 74 mpdan φvuFu+v+Fuv=2FuGv
76 70 3 75 rspcdv2 φuFu+B+FuB=2FuGB
77 76 r19.21bi φuFu+B+FuB=2FuGB
78 77 adantlr φ1<GBuFu+B+FuB=2FuGB
79 5 ad2antrr φ1<GBuyFy1
80 56 57 58 59 78 79 imo72b2lem0 φ1<GBuFuGBsupabsF<
81 0xr 0*
82 81 a1i φ1<GBu0*
83 1xr 1*
84 83 a1i φ1<GBu1*
85 16 adantr φ1<GBuGB
86 85 rexrd φ1<GBuGB*
87 51 a1i φ1<GBu0<1
88 simplr φ1<GBu1<GB
89 82 84 86 87 88 xrlttrd φ1<GBu0<GB
90 23 ffvelrnda φ1<GBuFu
91 90 recnd φ1<GBuFu
92 91 abscld φ1<GBuFu
93 46 adantr φ1<GBusupabsF<
94 80 89 85 92 93 lemuldiv3d φ1<GBuFusupabsF<GB
95 94 ralrimiva φ1<GBuFusupabsF<GB
96 23 55 95 imo72b2lem2 φ1<GBsupabsF<supabsF<GB
97 96 53 16 46 46 lemuldiv4d φ1<GBsupabsF<GBsupabsF<
98 49 97 eqbrtrrd φ1<GBGBsupabsF<supabsF<
99 6 adantr φ1<GBxFx0
100 5 adantr φ1<GByFy1
101 23 99 100 imo72b2lem1 φ1<GB0<supabsF<
102 98 101 46 16 46 lemuldiv3d φ1<GBGBsupabsF<supabsF<
103 26 46 sseldd φ1<GBsupabsF<
104 101 gt0ne0d φ1<GBsupabsF<0
105 103 104 dividd φ1<GBsupabsF<supabsF<=1
106 105 eqcomd φ1<GB1=supabsF<supabsF<
107 102 106 breqtrrd φ1<GBGB1
108 16 17 107 lensymd φ1<GB¬1<GB
109 11 108 pm2.65da φ¬1<GB
110 9 10 109 nltled φGB1