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∈Ac≤x→B≤m∧∃c∈ℝ∀x∈Ac≤x→C≤n↔∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m∧∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→C≤n
7 1 ralrimiva ⊢φ→∀x∈AB∈V
8 dmmptg ⊢∀x∈AB∈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∈Ac≤x→B≤m∧C≤n↔∃c∈ℝ∀x∈Ac≤x→B≤m∧∃c∈ℝ∀x∈Ac≤x→C≤n
15 13 14 syl ⊢φ∧m∈ℝ∧n∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m∧C≤n↔∃c∈ℝ∀x∈Ac≤x→B≤m∧∃c∈ℝ∀x∈Ac≤x→C≤n
16 simprl ⊢φ∧m∈ℝ∧n∈ℝ→m∈ℝ
17 simprr ⊢φ∧m∈ℝ∧n∈ℝ→n∈ℝ
18 0re ⊢0∈ℝ
19 ifcl ⊢n∈ℝ∧0∈ℝ→if0≤nn0∈ℝ
20 17 18 19 sylancl ⊢φ∧m∈ℝ∧n∈ℝ→if0≤nn0∈ℝ
21 16 20 remulcld ⊢φ∧m∈ℝ∧n∈ℝ→m⁢if0≤nn0∈ℝ
22 simplrr ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→n∈ℝ
23 max2 ⊢0∈ℝ∧n∈ℝ→n≤if0≤nn0
24 18 22 23 sylancr ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→n≤if0≤nn0
25 2 4 lo1mptrcl ⊢φ∧x∈A→C∈ℝ
26 25 adantlr ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→C∈ℝ
27 22 18 19 sylancl ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→if0≤nn0∈ℝ
28 letr ⊢C∈ℝ∧n∈ℝ∧if0≤nn0∈ℝ→C≤n∧n≤if0≤nn0→C≤if0≤nn0
29 26 22 27 28 syl3anc ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→C≤n∧n≤if0≤nn0→C≤if0≤nn0
30 24 29 mpan2d ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→C≤n→C≤if0≤nn0
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≤if0≤nn0
37 18 22 36 sylancr ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→0≤if0≤nn0
38 27 37 jca ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→if0≤nn0∈ℝ∧0≤if0≤nn0
39 lemul12b ⊢B∈ℝ∧0≤B∧m∈ℝ∧C∈ℝ∧if0≤nn0∈ℝ∧0≤if0≤nn0→B≤m∧C≤if0≤nn0→B⁢C≤m⁢if0≤nn0
40 34 35 26 38 39 syl22anc ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→B≤m∧C≤if0≤nn0→B⁢C≤m⁢if0≤nn0
41 30 40 sylan2d ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→B≤m∧C≤n→B⁢C≤m⁢if0≤nn0
42 41 imim2d ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→c≤x→B≤m∧C≤n→c≤x→B⁢C≤m⁢if0≤nn0
43 42 ralimdva ⊢φ∧m∈ℝ∧n∈ℝ→∀x∈Ac≤x→B≤m∧C≤n→∀x∈Ac≤x→B⁢C≤m⁢if0≤nn0
44 breq2 ⊢p=m⁢if0≤nn0→B⁢C≤p↔B⁢C≤m⁢if0≤nn0
45 44 imbi2d ⊢p=m⁢if0≤nn0→c≤x→B⁢C≤p↔c≤x→B⁢C≤m⁢if0≤nn0
46 45 ralbidv ⊢p=m⁢if0≤nn0→∀x∈Ac≤x→B⁢C≤p↔∀x∈Ac≤x→B⁢C≤m⁢if0≤nn0
47 46 rspcev ⊢m⁢if0≤nn0∈ℝ∧∀x∈Ac≤x→B⁢C≤m⁢if0≤nn0→∃p∈ℝ∀x∈Ac≤x→B⁢C≤p
48 21 43 47 syl6an ⊢φ∧m∈ℝ∧n∈ℝ→∀x∈Ac≤x→B≤m∧C≤n→∃p∈ℝ∀x∈Ac≤x→B⁢C≤p
49 48 reximdv ⊢φ∧m∈ℝ∧n∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m∧C≤n→∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→B⁢C≤p
50 15 49 sylbird ⊢φ∧m∈ℝ∧n∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m∧∃c∈ℝ∀x∈Ac≤x→C≤n→∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→B⁢C≤p
51 50 rexlimdvva ⊢φ→∃m∈ℝ∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m∧∃c∈ℝ∀x∈Ac≤x→C≤n→∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→B⁢C≤p
52 6 51 biimtrrid ⊢φ→∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m∧∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→C≤n→∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→B⁢C≤p
53 12 31 ello1mpt ⊢φ→x∈A⟼B∈≤𝑂⁡1↔∃c∈ℝ∃m∈ℝ∀x∈Ac≤x→B≤m
54 rexcom ⊢∃c∈ℝ∃m∈ℝ∀x∈Ac≤x→B≤m↔∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m
55 53 54 bitrdi ⊢φ→x∈A⟼B∈≤𝑂⁡1↔∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m
56 12 25 ello1mpt ⊢φ→x∈A⟼C∈≤𝑂⁡1↔∃c∈ℝ∃n∈ℝ∀x∈Ac≤x→C≤n
57 rexcom ⊢∃c∈ℝ∃n∈ℝ∀x∈Ac≤x→C≤n↔∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→C≤n
58 56 57 bitrdi ⊢φ→x∈A⟼C∈≤𝑂⁡1↔∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→C≤n
59 55 58 anbi12d ⊢φ→x∈A⟼B∈≤𝑂⁡1∧x∈A⟼C∈≤𝑂⁡1↔∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m∧∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→C≤n
60 31 25 remulcld ⊢φ∧x∈A→B⁢C∈ℝ
61 12 60 ello1mpt ⊢φ→x∈A⟼B⁢C∈≤𝑂⁡1↔∃c∈ℝ∃p∈ℝ∀x∈Ac≤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