Metamath Proof Explorer


Theorem supmul1

Description: The supremum function distributes over multiplication, in the sense that A x. ( sup B ) = sup ( A x. B ) , where A x. B is shorthand for { A x. b | b e. B } and is defined as C below. This is the simple version, with only one set argument; see supmul for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013)

Ref Expression
Hypotheses supmul1.1 𝐶 = { 𝑧 ∣ ∃ 𝑣𝐵 𝑧 = ( 𝐴 · 𝑣 ) }
supmul1.2 ( 𝜑 ↔ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥𝐵 0 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) ) )
Assertion supmul1 ( 𝜑 → ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) = sup ( 𝐶 , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 supmul1.1 𝐶 = { 𝑧 ∣ ∃ 𝑣𝐵 𝑧 = ( 𝐴 · 𝑣 ) }
2 supmul1.2 ( 𝜑 ↔ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥𝐵 0 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) ) )
3 vex 𝑤 ∈ V
4 oveq2 ( 𝑣 = 𝑏 → ( 𝐴 · 𝑣 ) = ( 𝐴 · 𝑏 ) )
5 4 eqeq2d ( 𝑣 = 𝑏 → ( 𝑧 = ( 𝐴 · 𝑣 ) ↔ 𝑧 = ( 𝐴 · 𝑏 ) ) )
6 5 cbvrexvw ( ∃ 𝑣𝐵 𝑧 = ( 𝐴 · 𝑣 ) ↔ ∃ 𝑏𝐵 𝑧 = ( 𝐴 · 𝑏 ) )
7 eqeq1 ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝐴 · 𝑏 ) ↔ 𝑤 = ( 𝐴 · 𝑏 ) ) )
8 7 rexbidv ( 𝑧 = 𝑤 → ( ∃ 𝑏𝐵 𝑧 = ( 𝐴 · 𝑏 ) ↔ ∃ 𝑏𝐵 𝑤 = ( 𝐴 · 𝑏 ) ) )
9 6 8 syl5bb ( 𝑧 = 𝑤 → ( ∃ 𝑣𝐵 𝑧 = ( 𝐴 · 𝑣 ) ↔ ∃ 𝑏𝐵 𝑤 = ( 𝐴 · 𝑏 ) ) )
10 3 9 1 elab2 ( 𝑤𝐶 ↔ ∃ 𝑏𝐵 𝑤 = ( 𝐴 · 𝑏 ) )
11 simpr ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥𝐵 0 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) ) → ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) )
12 2 11 sylbi ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) )
13 12 simp1d ( 𝜑𝐵 ⊆ ℝ )
14 13 sselda ( ( 𝜑𝑏𝐵 ) → 𝑏 ∈ ℝ )
15 suprcl ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
16 12 15 syl ( 𝜑 → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
17 16 adantr ( ( 𝜑𝑏𝐵 ) → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
18 simpl1 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥𝐵 0 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) ) → 𝐴 ∈ ℝ )
19 2 18 sylbi ( 𝜑𝐴 ∈ ℝ )
20 simpl2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥𝐵 0 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) ) → 0 ≤ 𝐴 )
21 2 20 sylbi ( 𝜑 → 0 ≤ 𝐴 )
22 19 21 jca ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
23 22 adantr ( ( 𝜑𝑏𝐵 ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
24 suprub ( ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) ∧ 𝑏𝐵 ) → 𝑏 ≤ sup ( 𝐵 , ℝ , < ) )
25 12 24 sylan ( ( 𝜑𝑏𝐵 ) → 𝑏 ≤ sup ( 𝐵 , ℝ , < ) )
26 lemul2a ( ( ( 𝑏 ∈ ℝ ∧ sup ( 𝐵 , ℝ , < ) ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ 𝑏 ≤ sup ( 𝐵 , ℝ , < ) ) → ( 𝐴 · 𝑏 ) ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) )
27 14 17 23 25 26 syl31anc ( ( 𝜑𝑏𝐵 ) → ( 𝐴 · 𝑏 ) ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) )
28 breq1 ( 𝑤 = ( 𝐴 · 𝑏 ) → ( 𝑤 ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ↔ ( 𝐴 · 𝑏 ) ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
29 27 28 syl5ibrcom ( ( 𝜑𝑏𝐵 ) → ( 𝑤 = ( 𝐴 · 𝑏 ) → 𝑤 ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
30 29 rexlimdva ( 𝜑 → ( ∃ 𝑏𝐵 𝑤 = ( 𝐴 · 𝑏 ) → 𝑤 ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
31 10 30 syl5bi ( 𝜑 → ( 𝑤𝐶𝑤 ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
32 31 ralrimiv ( 𝜑 → ∀ 𝑤𝐶 𝑤 ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) )
33 19 adantr ( ( 𝜑𝑏𝐵 ) → 𝐴 ∈ ℝ )
34 33 14 remulcld ( ( 𝜑𝑏𝐵 ) → ( 𝐴 · 𝑏 ) ∈ ℝ )
35 eleq1a ( ( 𝐴 · 𝑏 ) ∈ ℝ → ( 𝑤 = ( 𝐴 · 𝑏 ) → 𝑤 ∈ ℝ ) )
36 34 35 syl ( ( 𝜑𝑏𝐵 ) → ( 𝑤 = ( 𝐴 · 𝑏 ) → 𝑤 ∈ ℝ ) )
37 36 rexlimdva ( 𝜑 → ( ∃ 𝑏𝐵 𝑤 = ( 𝐴 · 𝑏 ) → 𝑤 ∈ ℝ ) )
38 10 37 syl5bi ( 𝜑 → ( 𝑤𝐶𝑤 ∈ ℝ ) )
39 38 ssrdv ( 𝜑𝐶 ⊆ ℝ )
40 simpr2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥𝐵 0 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) ) → 𝐵 ≠ ∅ )
41 2 40 sylbi ( 𝜑𝐵 ≠ ∅ )
42 ovex ( 𝐴 · 𝑏 ) ∈ V
43 42 isseti 𝑤 𝑤 = ( 𝐴 · 𝑏 )
44 43 rgenw 𝑏𝐵𝑤 𝑤 = ( 𝐴 · 𝑏 )
45 r19.2z ( ( 𝐵 ≠ ∅ ∧ ∀ 𝑏𝐵𝑤 𝑤 = ( 𝐴 · 𝑏 ) ) → ∃ 𝑏𝐵𝑤 𝑤 = ( 𝐴 · 𝑏 ) )
46 41 44 45 sylancl ( 𝜑 → ∃ 𝑏𝐵𝑤 𝑤 = ( 𝐴 · 𝑏 ) )
47 10 exbii ( ∃ 𝑤 𝑤𝐶 ↔ ∃ 𝑤𝑏𝐵 𝑤 = ( 𝐴 · 𝑏 ) )
48 n0 ( 𝐶 ≠ ∅ ↔ ∃ 𝑤 𝑤𝐶 )
49 rexcom4 ( ∃ 𝑏𝐵𝑤 𝑤 = ( 𝐴 · 𝑏 ) ↔ ∃ 𝑤𝑏𝐵 𝑤 = ( 𝐴 · 𝑏 ) )
50 47 48 49 3bitr4i ( 𝐶 ≠ ∅ ↔ ∃ 𝑏𝐵𝑤 𝑤 = ( 𝐴 · 𝑏 ) )
51 46 50 sylibr ( 𝜑𝐶 ≠ ∅ )
52 19 16 remulcld ( 𝜑 → ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ∈ ℝ )
53 brralrspcev ( ( ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ∈ ℝ ∧ ∀ 𝑤𝐶 𝑤 ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤𝐶 𝑤𝑥 )
54 52 32 53 syl2anc ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤𝐶 𝑤𝑥 )
55 39 51 54 3jca ( 𝜑 → ( 𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤𝐶 𝑤𝑥 ) )
56 suprleub ( ( ( 𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤𝐶 𝑤𝑥 ) ∧ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ∈ ℝ ) → ( sup ( 𝐶 , ℝ , < ) ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ↔ ∀ 𝑤𝐶 𝑤 ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
57 55 52 56 syl2anc ( 𝜑 → ( sup ( 𝐶 , ℝ , < ) ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ↔ ∀ 𝑤𝐶 𝑤 ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
58 32 57 mpbird ( 𝜑 → sup ( 𝐶 , ℝ , < ) ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) )
59 simpr ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) )
60 suprcl ( ( 𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤𝐶 𝑤𝑥 ) → sup ( 𝐶 , ℝ , < ) ∈ ℝ )
61 55 60 syl ( 𝜑 → sup ( 𝐶 , ℝ , < ) ∈ ℝ )
62 61 adantr ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → sup ( 𝐶 , ℝ , < ) ∈ ℝ )
63 16 adantr ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → sup ( 𝐵 , ℝ , < ) ∈ ℝ )
64 19 adantr ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → 𝐴 ∈ ℝ )
65 n0 ( 𝐵 ≠ ∅ ↔ ∃ 𝑏 𝑏𝐵 )
66 0red ( ( 𝜑𝑏𝐵 ) → 0 ∈ ℝ )
67 simpl3 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥𝐵 0 ≤ 𝑥 ) ∧ ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) ) → ∀ 𝑥𝐵 0 ≤ 𝑥 )
68 2 67 sylbi ( 𝜑 → ∀ 𝑥𝐵 0 ≤ 𝑥 )
69 breq2 ( 𝑥 = 𝑏 → ( 0 ≤ 𝑥 ↔ 0 ≤ 𝑏 ) )
70 69 rspccva ( ( ∀ 𝑥𝐵 0 ≤ 𝑥𝑏𝐵 ) → 0 ≤ 𝑏 )
71 68 70 sylan ( ( 𝜑𝑏𝐵 ) → 0 ≤ 𝑏 )
72 66 14 17 71 25 letrd ( ( 𝜑𝑏𝐵 ) → 0 ≤ sup ( 𝐵 , ℝ , < ) )
73 72 ex ( 𝜑 → ( 𝑏𝐵 → 0 ≤ sup ( 𝐵 , ℝ , < ) ) )
74 73 exlimdv ( 𝜑 → ( ∃ 𝑏 𝑏𝐵 → 0 ≤ sup ( 𝐵 , ℝ , < ) ) )
75 65 74 syl5bi ( 𝜑 → ( 𝐵 ≠ ∅ → 0 ≤ sup ( 𝐵 , ℝ , < ) ) )
76 41 75 mpd ( 𝜑 → 0 ≤ sup ( 𝐵 , ℝ , < ) )
77 76 adantr ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → 0 ≤ sup ( 𝐵 , ℝ , < ) )
78 0red ( ( 𝜑𝑤𝐶 ) → 0 ∈ ℝ )
79 38 imp ( ( 𝜑𝑤𝐶 ) → 𝑤 ∈ ℝ )
80 61 adantr ( ( 𝜑𝑤𝐶 ) → sup ( 𝐶 , ℝ , < ) ∈ ℝ )
81 21 adantr ( ( 𝜑𝑏𝐵 ) → 0 ≤ 𝐴 )
82 33 14 81 71 mulge0d ( ( 𝜑𝑏𝐵 ) → 0 ≤ ( 𝐴 · 𝑏 ) )
83 breq2 ( 𝑤 = ( 𝐴 · 𝑏 ) → ( 0 ≤ 𝑤 ↔ 0 ≤ ( 𝐴 · 𝑏 ) ) )
84 82 83 syl5ibrcom ( ( 𝜑𝑏𝐵 ) → ( 𝑤 = ( 𝐴 · 𝑏 ) → 0 ≤ 𝑤 ) )
85 84 rexlimdva ( 𝜑 → ( ∃ 𝑏𝐵 𝑤 = ( 𝐴 · 𝑏 ) → 0 ≤ 𝑤 ) )
86 10 85 syl5bi ( 𝜑 → ( 𝑤𝐶 → 0 ≤ 𝑤 ) )
87 86 imp ( ( 𝜑𝑤𝐶 ) → 0 ≤ 𝑤 )
88 suprub ( ( ( 𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤𝐶 𝑤𝑥 ) ∧ 𝑤𝐶 ) → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) )
89 55 88 sylan ( ( 𝜑𝑤𝐶 ) → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) )
90 78 79 80 87 89 letrd ( ( 𝜑𝑤𝐶 ) → 0 ≤ sup ( 𝐶 , ℝ , < ) )
91 90 ex ( 𝜑 → ( 𝑤𝐶 → 0 ≤ sup ( 𝐶 , ℝ , < ) ) )
92 91 exlimdv ( 𝜑 → ( ∃ 𝑤 𝑤𝐶 → 0 ≤ sup ( 𝐶 , ℝ , < ) ) )
93 48 92 syl5bi ( 𝜑 → ( 𝐶 ≠ ∅ → 0 ≤ sup ( 𝐶 , ℝ , < ) ) )
94 51 93 mpd ( 𝜑 → 0 ≤ sup ( 𝐶 , ℝ , < ) )
95 94 anim1i ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ( 0 ≤ sup ( 𝐶 , ℝ , < ) ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
96 0red ( 𝜑 → 0 ∈ ℝ )
97 lelttr ( ( 0 ∈ ℝ ∧ sup ( 𝐶 , ℝ , < ) ∈ ℝ ∧ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ∈ ℝ ) → ( ( 0 ≤ sup ( 𝐶 , ℝ , < ) ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → 0 < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
98 96 61 52 97 syl3anc ( 𝜑 → ( ( 0 ≤ sup ( 𝐶 , ℝ , < ) ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → 0 < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
99 98 adantr ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ( ( 0 ≤ sup ( 𝐶 , ℝ , < ) ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → 0 < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
100 95 99 mpd ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → 0 < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) )
101 prodgt02 ( ( ( 𝐴 ∈ ℝ ∧ sup ( 𝐵 , ℝ , < ) ∈ ℝ ) ∧ ( 0 ≤ sup ( 𝐵 , ℝ , < ) ∧ 0 < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ) → 0 < 𝐴 )
102 64 63 77 100 101 syl22anc ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → 0 < 𝐴 )
103 ltdivmul ( ( sup ( 𝐶 , ℝ , < ) ∈ ℝ ∧ sup ( 𝐵 , ℝ , < ) ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < sup ( 𝐵 , ℝ , < ) ↔ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
104 62 63 64 102 103 syl112anc ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ( ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < sup ( 𝐵 , ℝ , < ) ↔ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
105 59 104 mpbird ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < sup ( 𝐵 , ℝ , < ) )
106 12 adantr ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) )
107 102 gt0ne0d ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → 𝐴 ≠ 0 )
108 62 64 107 redivcld ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) ∈ ℝ )
109 suprlub ( ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑦𝑥 ) ∧ ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) ∈ ℝ ) → ( ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < sup ( 𝐵 , ℝ , < ) ↔ ∃ 𝑏𝐵 ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < 𝑏 ) )
110 106 108 109 syl2anc ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ( ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < sup ( 𝐵 , ℝ , < ) ↔ ∃ 𝑏𝐵 ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < 𝑏 ) )
111 105 110 mpbid ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ∃ 𝑏𝐵 ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < 𝑏 )
112 34 adantlr ( ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ∧ 𝑏𝐵 ) → ( 𝐴 · 𝑏 ) ∈ ℝ )
113 61 ad2antrr ( ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ∧ 𝑏𝐵 ) → sup ( 𝐶 , ℝ , < ) ∈ ℝ )
114 rspe ( ( 𝑏𝐵𝑤 = ( 𝐴 · 𝑏 ) ) → ∃ 𝑏𝐵 𝑤 = ( 𝐴 · 𝑏 ) )
115 114 10 sylibr ( ( 𝑏𝐵𝑤 = ( 𝐴 · 𝑏 ) ) → 𝑤𝐶 )
116 115 adantl ( ( 𝜑 ∧ ( 𝑏𝐵𝑤 = ( 𝐴 · 𝑏 ) ) ) → 𝑤𝐶 )
117 simplrr ( ( ( 𝜑 ∧ ( 𝑏𝐵𝑤 = ( 𝐴 · 𝑏 ) ) ) ∧ 𝑤𝐶 ) → 𝑤 = ( 𝐴 · 𝑏 ) )
118 89 adantlr ( ( ( 𝜑 ∧ ( 𝑏𝐵𝑤 = ( 𝐴 · 𝑏 ) ) ) ∧ 𝑤𝐶 ) → 𝑤 ≤ sup ( 𝐶 , ℝ , < ) )
119 117 118 eqbrtrrd ( ( ( 𝜑 ∧ ( 𝑏𝐵𝑤 = ( 𝐴 · 𝑏 ) ) ) ∧ 𝑤𝐶 ) → ( 𝐴 · 𝑏 ) ≤ sup ( 𝐶 , ℝ , < ) )
120 116 119 mpdan ( ( 𝜑 ∧ ( 𝑏𝐵𝑤 = ( 𝐴 · 𝑏 ) ) ) → ( 𝐴 · 𝑏 ) ≤ sup ( 𝐶 , ℝ , < ) )
121 120 expr ( ( 𝜑𝑏𝐵 ) → ( 𝑤 = ( 𝐴 · 𝑏 ) → ( 𝐴 · 𝑏 ) ≤ sup ( 𝐶 , ℝ , < ) ) )
122 121 exlimdv ( ( 𝜑𝑏𝐵 ) → ( ∃ 𝑤 𝑤 = ( 𝐴 · 𝑏 ) → ( 𝐴 · 𝑏 ) ≤ sup ( 𝐶 , ℝ , < ) ) )
123 43 122 mpi ( ( 𝜑𝑏𝐵 ) → ( 𝐴 · 𝑏 ) ≤ sup ( 𝐶 , ℝ , < ) )
124 123 adantlr ( ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ∧ 𝑏𝐵 ) → ( 𝐴 · 𝑏 ) ≤ sup ( 𝐶 , ℝ , < ) )
125 112 113 124 lensymd ( ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ∧ 𝑏𝐵 ) → ¬ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · 𝑏 ) )
126 14 adantlr ( ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ∧ 𝑏𝐵 ) → 𝑏 ∈ ℝ )
127 19 ad2antrr ( ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ∧ 𝑏𝐵 ) → 𝐴 ∈ ℝ )
128 102 adantr ( ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ∧ 𝑏𝐵 ) → 0 < 𝐴 )
129 ltdivmul ( ( sup ( 𝐶 , ℝ , < ) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < 𝑏 ↔ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · 𝑏 ) ) )
130 113 126 127 128 129 syl112anc ( ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ∧ 𝑏𝐵 ) → ( ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < 𝑏 ↔ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · 𝑏 ) ) )
131 125 130 mtbird ( ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ∧ 𝑏𝐵 ) → ¬ ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < 𝑏 )
132 131 nrexdv ( ( 𝜑 ∧ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) → ¬ ∃ 𝑏𝐵 ( sup ( 𝐶 , ℝ , < ) / 𝐴 ) < 𝑏 )
133 111 132 pm2.65da ( 𝜑 → ¬ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) )
134 58 133 jca ( 𝜑 → ( sup ( 𝐶 , ℝ , < ) ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ∧ ¬ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) )
135 61 52 eqleltd ( 𝜑 → ( sup ( 𝐶 , ℝ , < ) = ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ↔ ( sup ( 𝐶 , ℝ , < ) ≤ ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ∧ ¬ sup ( 𝐶 , ℝ , < ) < ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) ) ) )
136 134 135 mpbird ( 𝜑 → sup ( 𝐶 , ℝ , < ) = ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) )
137 136 eqcomd ( 𝜑 → ( 𝐴 · sup ( 𝐵 , ℝ , < ) ) = sup ( 𝐶 , ℝ , < ) )