Mathbox for Stanislas Polu < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  imo72b2 Structured version   Visualization version   GIF version

Theorem imo72b2 40410
 Description: IMO 1972 B2. (14th International Mathemahics Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.)
Hypotheses
Ref Expression
imo72b2.1 (𝜑𝐹:ℝ⟶ℝ)
imo72b2.2 (𝜑𝐺:ℝ⟶ℝ)
imo72b2.4 (𝜑𝐵 ∈ ℝ)
imo72b2.5 (𝜑 → ∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))))
imo72b2.6 (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹𝑦)) ≤ 1)
imo72b2.7 (𝜑 → ∃𝑥 ∈ ℝ (𝐹𝑥) ≠ 0)
Assertion
Ref Expression
imo72b2 (𝜑 → (abs‘(𝐺𝐵)) ≤ 1)
Distinct variable groups:   𝑢,𝐵,𝑣   𝑥,𝐵   𝑦,𝐵   𝑢,𝐹,𝑣   𝑥,𝐹   𝑦,𝐹   𝑢,𝐺,𝑣   𝑥,𝐺   𝑦,𝐺   𝜑,𝑢,𝑣   𝜑,𝑥   𝜑,𝑦,𝑢

Proof of Theorem imo72b2
Dummy variables 𝑐 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imo72b2.2 . . . . 5 (𝜑𝐺:ℝ⟶ℝ)
2 imo72b2.4 . . . . 5 (𝜑𝐵 ∈ ℝ)
31, 2ffvelrnd 6850 . . . 4 (𝜑 → (𝐺𝐵) ∈ ℝ)
43recnd 10663 . . 3 (𝜑 → (𝐺𝐵) ∈ ℂ)
54abscld 14791 . 2 (𝜑 → (abs‘(𝐺𝐵)) ∈ ℝ)
6 1red 10636 . 2 (𝜑 → 1 ∈ ℝ)
7 simpr 485 . . 3 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 1 < (abs‘(𝐺𝐵)))
81adantr 481 . . . . . . 7 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 𝐺:ℝ⟶ℝ)
92adantr 481 . . . . . . 7 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 𝐵 ∈ ℝ)
108, 9ffvelrnd 6850 . . . . . 6 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (𝐺𝐵) ∈ ℝ)
1110recnd 10663 . . . . 5 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (𝐺𝐵) ∈ ℂ)
1211abscld 14791 . . . 4 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs‘(𝐺𝐵)) ∈ ℝ)
136adantr 481 . . . 4 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 1 ∈ ℝ)
14 ax-resscn 10588 . . . . . . . . 9 ℝ ⊆ ℂ
15 imaco 6103 . . . . . . . . . . . 12 ((abs ∘ 𝐹) “ ℝ) = (abs “ (𝐹 “ ℝ))
1615eqcomi 2835 . . . . . . . . . . 11 (abs “ (𝐹 “ ℝ)) = ((abs ∘ 𝐹) “ ℝ)
17 imassrn 5939 . . . . . . . . . . . . 13 ((abs ∘ 𝐹) “ ℝ) ⊆ ran (abs ∘ 𝐹)
1817a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ((abs ∘ 𝐹) “ ℝ) ⊆ ran (abs ∘ 𝐹))
19 imo72b2.1 . . . . . . . . . . . . . . 15 (𝜑𝐹:ℝ⟶ℝ)
2019adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 𝐹:ℝ⟶ℝ)
21 absf 14692 . . . . . . . . . . . . . . . 16 abs:ℂ⟶ℝ
2221a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → abs:ℂ⟶ℝ)
2314a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ℝ ⊆ ℂ)
2422, 23fssresd 6544 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs ↾ ℝ):ℝ⟶ℝ)
2520, 24fco2d 40397 . . . . . . . . . . . . 13 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs ∘ 𝐹):ℝ⟶ℝ)
2625frnd 6520 . . . . . . . . . . . 12 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ran (abs ∘ 𝐹) ⊆ ℝ)
2718, 26sstrd 3981 . . . . . . . . . . 11 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ((abs ∘ 𝐹) “ ℝ) ⊆ ℝ)
2816, 27eqsstrid 4019 . . . . . . . . . 10 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs “ (𝐹 “ ℝ)) ⊆ ℝ)
29 0re 10637 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
3029ne0ii 4307 . . . . . . . . . . . . . . 15 ℝ ≠ ∅
3130a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ℝ ≠ ∅)
3231, 25wnefimgd 40396 . . . . . . . . . . . . 13 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ((abs ∘ 𝐹) “ ℝ) ≠ ∅)
3332necomd 3076 . . . . . . . . . . . 12 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ∅ ≠ ((abs ∘ 𝐹) “ ℝ))
3416a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs “ (𝐹 “ ℝ)) = ((abs ∘ 𝐹) “ ℝ))
3533, 34neeqtrrd 3095 . . . . . . . . . . 11 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ∅ ≠ (abs “ (𝐹 “ ℝ)))
3635necomd 3076 . . . . . . . . . 10 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs “ (𝐹 “ ℝ)) ≠ ∅)
37 simpr 485 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑐 = 1) → 𝑐 = 1)
3837breq2d 5075 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑐 = 1) → (𝑡𝑐𝑡 ≤ 1))
3938ralbidv 3202 . . . . . . . . . . 11 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑐 = 1) → (∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡𝑐 ↔ ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 1))
40 imo72b2.6 . . . . . . . . . . . . 13 (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹𝑦)) ≤ 1)
4119, 40extoimad 40399 . . . . . . . . . . . 12 (𝜑 → ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 1)
4241adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 1)
4313, 39, 42rspcedvd 3630 . . . . . . . . . 10 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ∃𝑐 ∈ ℝ ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡𝑐)
4428, 36, 43suprcld 11598 . . . . . . . . 9 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ∈ ℝ)
4514, 44sseldi 3969 . . . . . . . 8 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ∈ ℂ)
4614, 12sseldi 3969 . . . . . . . 8 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs‘(𝐺𝐵)) ∈ ℂ)
4745, 46mulcomd 10656 . . . . . . 7 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) · (abs‘(𝐺𝐵))) = ((abs‘(𝐺𝐵)) · sup((abs “ (𝐹 “ ℝ)), ℝ, < )))
4829a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 0 ∈ ℝ)
49 0lt1 11156 . . . . . . . . . . . . 13 0 < 1
5049a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 0 < 1)
5148, 13, 12, 50, 7lttrd 10795 . . . . . . . . . . 11 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 0 < (abs‘(𝐺𝐵)))
5251gt0ne0d 11198 . . . . . . . . . 10 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs‘(𝐺𝐵)) ≠ 0)
5344, 12, 52redivcld 11462 . . . . . . . . 9 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) / (abs‘(𝐺𝐵))) ∈ ℝ)
5420adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → 𝐹:ℝ⟶ℝ)
558adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → 𝐺:ℝ⟶ℝ)
56 simpr 485 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → 𝑢 ∈ ℝ)
579adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → 𝐵 ∈ ℝ)
58 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑣 = 𝐵) → 𝑣 = 𝐵)
5958oveq2d 7166 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑣 = 𝐵) → (𝑢 + 𝑣) = (𝑢 + 𝐵))
6059fveq2d 6673 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣 = 𝐵) → (𝐹‘(𝑢 + 𝑣)) = (𝐹‘(𝑢 + 𝐵)))
6158oveq2d 7166 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑣 = 𝐵) → (𝑢𝑣) = (𝑢𝐵))
6261fveq2d 6673 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣 = 𝐵) → (𝐹‘(𝑢𝑣)) = (𝐹‘(𝑢𝐵)))
6360, 62oveq12d 7168 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣 = 𝐵) → ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = ((𝐹‘(𝑢 + 𝐵)) + (𝐹‘(𝑢𝐵))))
6458fveq2d 6673 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑣 = 𝐵) → (𝐺𝑣) = (𝐺𝐵))
6564oveq2d 7166 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑣 = 𝐵) → ((𝐹𝑢) · (𝐺𝑣)) = ((𝐹𝑢) · (𝐺𝐵)))
6665oveq2d 7166 . . . . . . . . . . . . . . . . 17 ((𝜑𝑣 = 𝐵) → (2 · ((𝐹𝑢) · (𝐺𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝐵))))
6763, 66eqeq12d 2842 . . . . . . . . . . . . . . . 16 ((𝜑𝑣 = 𝐵) → (((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))) ↔ ((𝐹‘(𝑢 + 𝐵)) + (𝐹‘(𝑢𝐵))) = (2 · ((𝐹𝑢) · (𝐺𝐵)))))
6867ralbidv 3202 . . . . . . . . . . . . . . 15 ((𝜑𝑣 = 𝐵) → (∀𝑢 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))) ↔ ∀𝑢 ∈ ℝ ((𝐹‘(𝑢 + 𝐵)) + (𝐹‘(𝑢𝐵))) = (2 · ((𝐹𝑢) · (𝐺𝐵)))))
69 imo72b2.5 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))))
70 ralcom2 3369 . . . . . . . . . . . . . . . . . 18 (∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))) → ∀𝑣 ∈ ℝ ∀𝑢 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))))
7170a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))) → ∀𝑣 ∈ ℝ ∀𝑢 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣)))))
7271imp 407 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣)))) → ∀𝑣 ∈ ℝ ∀𝑢 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))))
7369, 72mpdan 683 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑣 ∈ ℝ ∀𝑢 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢𝑣))) = (2 · ((𝐹𝑢) · (𝐺𝑣))))
7468, 2, 73rspcdvinvd 40409 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑢 ∈ ℝ ((𝐹‘(𝑢 + 𝐵)) + (𝐹‘(𝑢𝐵))) = (2 · ((𝐹𝑢) · (𝐺𝐵))))
7574r19.21bi 3213 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ ℝ) → ((𝐹‘(𝑢 + 𝐵)) + (𝐹‘(𝑢𝐵))) = (2 · ((𝐹𝑢) · (𝐺𝐵))))
7675adantlr 711 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → ((𝐹‘(𝑢 + 𝐵)) + (𝐹‘(𝑢𝐵))) = (2 · ((𝐹𝑢) · (𝐺𝐵))))
7740ad2antrr 722 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → ∀𝑦 ∈ ℝ (abs‘(𝐹𝑦)) ≤ 1)
7854, 55, 56, 57, 76, 77imo72b2lem0 40400 . . . . . . . . . . 11 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → ((abs‘(𝐹𝑢)) · (abs‘(𝐺𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
79 0xr 10682 . . . . . . . . . . . . 13 0 ∈ ℝ*
8079a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → 0 ∈ ℝ*)
81 1xr 10694 . . . . . . . . . . . . 13 1 ∈ ℝ*
8281a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → 1 ∈ ℝ*)
8312adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → (abs‘(𝐺𝐵)) ∈ ℝ)
8483rexrd 10685 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → (abs‘(𝐺𝐵)) ∈ ℝ*)
8549a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → 0 < 1)
86 simplr 765 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → 1 < (abs‘(𝐺𝐵)))
8780, 82, 84, 85, 86xrlttrd 12547 . . . . . . . . . . 11 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → 0 < (abs‘(𝐺𝐵)))
8820ffvelrnda 6849 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → (𝐹𝑢) ∈ ℝ)
8988recnd 10663 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → (𝐹𝑢) ∈ ℂ)
9089abscld 14791 . . . . . . . . . . 11 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → (abs‘(𝐹𝑢)) ∈ ℝ)
9144adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ∈ ℝ)
9278, 87, 83, 90, 91lemuldiv3d 40407 . . . . . . . . . 10 (((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) ∧ 𝑢 ∈ ℝ) → (abs‘(𝐹𝑢)) ≤ (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) / (abs‘(𝐺𝐵))))
9392ralrimiva 3187 . . . . . . . . 9 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ∀𝑢 ∈ ℝ (abs‘(𝐹𝑢)) ≤ (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) / (abs‘(𝐺𝐵))))
9420, 53, 93imo72b2lem2 40402 . . . . . . . 8 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) / (abs‘(𝐺𝐵))))
9594, 51, 12, 44, 44lemuldiv4d 40408 . . . . . . 7 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) · (abs‘(𝐺𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
9647, 95eqbrtrrd 5087 . . . . . 6 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ((abs‘(𝐺𝐵)) · sup((abs “ (𝐹 “ ℝ)), ℝ, < )) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
97 imo72b2.7 . . . . . . . 8 (𝜑 → ∃𝑥 ∈ ℝ (𝐹𝑥) ≠ 0)
9897adantr 481 . . . . . . 7 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ∃𝑥 ∈ ℝ (𝐹𝑥) ≠ 0)
9940adantr 481 . . . . . . 7 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ∀𝑦 ∈ ℝ (abs‘(𝐹𝑦)) ≤ 1)
10020, 98, 99imo72b2lem1 40406 . . . . . 6 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < ))
10196, 100, 44, 12, 44lemuldiv3d 40407 . . . . 5 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs‘(𝐺𝐵)) ≤ (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) / sup((abs “ (𝐹 “ ℝ)), ℝ, < )))
10223, 44sseldd 3972 . . . . . . 7 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ∈ ℂ)
103100gt0ne0d 11198 . . . . . . 7 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≠ 0)
104102, 103dividd 11408 . . . . . 6 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) / sup((abs “ (𝐹 “ ℝ)), ℝ, < )) = 1)
105104eqcomd 2832 . . . . 5 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → 1 = (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) / sup((abs “ (𝐹 “ ℝ)), ℝ, < )))
106101, 105breqtrrd 5091 . . . 4 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → (abs‘(𝐺𝐵)) ≤ 1)
10712, 13, 106lensymd 10785 . . 3 ((𝜑 ∧ 1 < (abs‘(𝐺𝐵))) → ¬ 1 < (abs‘(𝐺𝐵)))
1087, 107pm2.65da 813 . 2 (𝜑 → ¬ 1 < (abs‘(𝐺𝐵)))
1095, 6, 108nltled 10784 1 (𝜑 → (abs‘(𝐺𝐵)) ≤ 1)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   = wceq 1530   ∈ wcel 2107   ≠ wne 3021  ∀wral 3143  ∃wrex 3144   ⊆ wss 3940  ∅c0 4295   class class class wbr 5063  ran crn 5555   “ cima 5557   ∘ ccom 5558  ⟶wf 6350  ‘cfv 6354  (class class class)co 7150  supcsup 8898  ℂcc 10529  ℝcr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536  ℝ*cxr 10668   < clt 10669   ≤ cle 10670   − cmin 10864   / cdiv 11291  2c2 11686  abscabs 14588 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-er 8284  df-en 8504  df-dom 8505  df-sdom 8506  df-sup 8900  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-rp 12385  df-seq 13365  df-exp 13425  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator