Step |
Hyp |
Ref |
Expression |
1 |
|
o1add2.1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) |
2 |
|
o1add2.2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 ) |
3 |
|
lo1add.3 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ) |
4 |
|
lo1add.4 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) |
5 |
|
lo1mul.5 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 ) |
6 |
2 4
|
lo1mptrcl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ ) |
7 |
6
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ ) |
8 |
1 3
|
lo1mptrcl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ ) |
9 |
8
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) |
10 |
7 9
|
mulcomd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) = ( 𝐵 · 𝐶 ) ) |
11 |
10
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ) |
12 |
1 2 3 4 5
|
lo1mul |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∈ ≤𝑂(1) ) |
13 |
11 12
|
eqeltrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ ≤𝑂(1) ) |