Metamath Proof Explorer

Theorem lo1mul

Description: The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1add2.1 ⊢ φ ∧ x ∈ A → B ∈ V
o1add2.2 ⊢ φ ∧ x ∈ A → C ∈ V
lo1add.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
lo1add.4 ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1
lo1mul.5 ⊢ φ ∧ x ∈ A → 0 ≤ B
Assertion lo1mul ⊢ φ → x ∈ A ⟼ B ⁢ C ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1add2.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 o1add2.2 ⊢ φ ∧ x ∈ A → C ∈ V
3 lo1add.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
4 lo1add.4 ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1
5 lo1mul.5 ⊢ φ ∧ x ∈ A → 0 ≤ B
6 reeanv ⊢ ∃ m ∈ ℝ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n ↔ ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
7 1 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ V
8 dmmptg ⊢ ∀ x ∈ A B ∈ V → dom ⁡ x ∈ A ⟼ B = A
9 7 8 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
10 lo1dm ⊢ x ∈ A ⟼ B ∈ ≤𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
11 3 10 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
12 9 11 eqsstrrd ⊢ φ → A ⊆ ℝ
13 12 adantr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → A ⊆ ℝ
14 rexanre ⊢ A ⊆ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
15 13 14 syl ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
16 simprl ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → m ∈ ℝ
17 simprr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → n ∈ ℝ
18 0re ⊢ 0 ∈ ℝ
19 ifcl ⊢ n ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ n n 0 ∈ ℝ
20 17 18 19 sylancl ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → if 0 ≤ n n 0 ∈ ℝ
21 16 20 remulcld ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → m ⁢ if 0 ≤ n n 0 ∈ ℝ
22 simplrr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → n ∈ ℝ
23 max2 ⊢ 0 ∈ ℝ ∧ n ∈ ℝ → n ≤ if 0 ≤ n n 0
24 18 22 23 sylancr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → n ≤ if 0 ≤ n n 0
25 2 4 lo1mptrcl ⊢ φ ∧ x ∈ A → C ∈ ℝ
26 25 adantlr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → C ∈ ℝ
27 22 18 19 sylancl ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → if 0 ≤ n n 0 ∈ ℝ
28 letr ⊢ C ∈ ℝ ∧ n ∈ ℝ ∧ if 0 ≤ n n 0 ∈ ℝ → C ≤ n ∧ n ≤ if 0 ≤ n n 0 → C ≤ if 0 ≤ n n 0
29 26 22 27 28 syl3anc ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → C ≤ n ∧ n ≤ if 0 ≤ n n 0 → C ≤ if 0 ≤ n n 0
30 24 29 mpan2d ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → C ≤ n → C ≤ if 0 ≤ n n 0
31 1 3 lo1mptrcl ⊢ φ ∧ x ∈ A → B ∈ ℝ
32 31 adantlr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → B ∈ ℝ
33 5 adantlr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → 0 ≤ B
34 32 33 jca ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → B ∈ ℝ ∧ 0 ≤ B
35 simplrl ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → m ∈ ℝ
36 max1 ⊢ 0 ∈ ℝ ∧ n ∈ ℝ → 0 ≤ if 0 ≤ n n 0
37 18 22 36 sylancr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → 0 ≤ if 0 ≤ n n 0
38 27 37 jca ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → if 0 ≤ n n 0 ∈ ℝ ∧ 0 ≤ if 0 ≤ n n 0
39 lemul12b ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ m ∈ ℝ ∧ C ∈ ℝ ∧ if 0 ≤ n n 0 ∈ ℝ ∧ 0 ≤ if 0 ≤ n n 0 → B ≤ m ∧ C ≤ if 0 ≤ n n 0 → B ⁢ C ≤ m ⁢ if 0 ≤ n n 0
40 34 35 26 38 39 syl22anc ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → B ≤ m ∧ C ≤ if 0 ≤ n n 0 → B ⁢ C ≤ m ⁢ if 0 ≤ n n 0
41 30 40 sylan2d ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → B ≤ m ∧ C ≤ n → B ⁢ C ≤ m ⁢ if 0 ≤ n n 0
42 41 imim2d ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → c ≤ x → B ≤ m ∧ C ≤ n → c ≤ x → B ⁢ C ≤ m ⁢ if 0 ≤ n n 0
43 42 ralimdva ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n → ∀ x ∈ A c ≤ x → B ⁢ C ≤ m ⁢ if 0 ≤ n n 0
44 breq2 ⊢ p = m ⁢ if 0 ≤ n n 0 → B ⁢ C ≤ p ↔ B ⁢ C ≤ m ⁢ if 0 ≤ n n 0
45 44 imbi2d ⊢ p = m ⁢ if 0 ≤ n n 0 → c ≤ x → B ⁢ C ≤ p ↔ c ≤ x → B ⁢ C ≤ m ⁢ if 0 ≤ n n 0
46 45 ralbidv ⊢ p = m ⁢ if 0 ≤ n n 0 → ∀ x ∈ A c ≤ x → B ⁢ C ≤ p ↔ ∀ x ∈ A c ≤ x → B ⁢ C ≤ m ⁢ if 0 ≤ n n 0
47 46 rspcev ⊢ m ⁢ if 0 ≤ n n 0 ∈ ℝ ∧ ∀ x ∈ A c ≤ x → B ⁢ C ≤ m ⁢ if 0 ≤ n n 0 → ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B ⁢ C ≤ p
48 21 43 47 syl6an ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n → ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B ⁢ C ≤ p
49 48 reximdv ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n → ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B ⁢ C ≤ p
50 15 49 sylbird ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n → ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B ⁢ C ≤ p
51 50 rexlimdvva ⊢ φ → ∃ m ∈ ℝ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n → ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B ⁢ C ≤ p
52 6 51 syl5bir ⊢ φ → ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n → ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B ⁢ C ≤ p
53 12 31 ello1mpt ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
54 rexcom ⊢ ∃ c ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ↔ ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
55 53 54 bitrdi ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
56 12 25 ello1mpt ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ n ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
57 rexcom ⊢ ∃ c ∈ ℝ ∃ n ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n ↔ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
58 56 57 bitrdi ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1 ↔ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
59 55 58 anbi12d ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ C ∈ ≤𝑂⁡1 ↔ ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
60 31 25 remulcld ⊢ φ ∧ x ∈ A → B ⁢ C ∈ ℝ
61 12 60 ello1mpt ⊢ φ → x ∈ A ⟼ B ⁢ C ∈ ≤𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B ⁢ C ≤ p
62 52 59 61 3imtr4d ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ C ∈ ≤𝑂⁡1 → x ∈ A ⟼ B ⁢ C ∈ ≤𝑂⁡1
63 3 4 62 mp2and ⊢ φ → x ∈ A ⟼ B ⁢ C ∈ ≤𝑂⁡1