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 ( 𝐶 , ℝ , < ) )