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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
o1add2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
lo1add.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
lo1add.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) )
lo1mul.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
Assertion lo1mul ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∈ ≤𝑂(1) )

Proof

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