Metamath Proof Explorer

Theorem lo1add

Description: The sum of two eventually upper bounded functions is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1add2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
o1add2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
lo1add.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
lo1add.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) )
Assertion lo1add ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ ≤𝑂(1) )

Proof

Step Hyp Ref Expression
1 o1add2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 o1add2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
3 lo1add.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
4 lo1add.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) )
5 reeanv ⊢ ( ∃ 𝑚 ∈ ℝ ∃ 𝑛 ∈ ℝ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) ↔ ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ∧ ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) )
6 1 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
7 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
8 6 7 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
9 lo1dm ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
10 3 9 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
11 8 10 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
12 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → 𝐴 ⊆ ℝ )
13 rexanre ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛 ) ) ↔ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) ) )
14 12 13 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛 ) ) ↔ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) ) )
15 readdcl ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 𝑚 + 𝑛 ) ∈ ℝ )
16 15 adantl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( 𝑚 + 𝑛 ) ∈ ℝ )
17 1 3 lo1mptrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
18 17 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
19 2 4 lo1mptrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
20 19 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
21 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑚 ∈ ℝ )
22 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑛 ∈ ℝ )
23 le2add ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ( 𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛 ) → ( 𝐵 + 𝐶 ) ≤ ( 𝑚 + 𝑛 ) ) )
24 18 20 21 22 23 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛 ) → ( 𝐵 + 𝐶 ) ≤ ( 𝑚 + 𝑛 ) ) )
25 24 imim2d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛 ) ) → ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ ( 𝑚 + 𝑛 ) ) ) )
26 25 ralimdva ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ ( 𝑚 + 𝑛 ) ) ) )
27 breq2 ⊢ ( 𝑝 = ( 𝑚 + 𝑛 ) → ( ( 𝐵 + 𝐶 ) ≤ 𝑝 ↔ ( 𝐵 + 𝐶 ) ≤ ( 𝑚 + 𝑛 ) ) )
28 27 imbi2d ⊢ ( 𝑝 = ( 𝑚 + 𝑛 ) → ( ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ 𝑝 ) ↔ ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ ( 𝑚 + 𝑛 ) ) ) )
29 28 ralbidv ⊢ ( 𝑝 = ( 𝑚 + 𝑛 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ 𝑝 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ ( 𝑚 + 𝑛 ) ) ) )
30 29 rspcev ⊢ ( ( ( 𝑚 + 𝑛 ) ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ ( 𝑚 + 𝑛 ) ) ) → ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ 𝑝 ) )
31 16 26 30 syl6an ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛 ) ) → ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ 𝑝 ) ) )
32 31 reximdv ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛 ) ) → ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ 𝑝 ) ) )
33 14 32 sylbird ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) → ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ 𝑝 ) ) )
34 33 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℝ ∃ 𝑛 ∈ ℝ ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) → ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ 𝑝 ) ) )
35 5 34 syl5bir ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ∧ ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) → ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ 𝑝 ) ) )
36 11 17 ello1mpt ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
37 rexcom ⊢ ( ∃ 𝑐 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ↔ ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) )
38 36 37 bitrdi ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
39 11 19 ello1mpt ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) )
40 rexcom ⊢ ( ∃ 𝑐 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) )
41 39 40 bitrdi ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ↔ ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) )
42 38 41 anbi12d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) ↔ ( ∃ 𝑚 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ∧ ∃ 𝑛 ∈ ℝ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛 ) ) ) )
43 17 19 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
44 11 43 ello1mpt ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ ≤𝑂(1) ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑝 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑐 ≤ 𝑥 → ( 𝐵 + 𝐶 ) ≤ 𝑝 ) ) )
45 35 42 44 3imtr4d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ ≤𝑂(1) ) )
46 3 4 45 mp2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ ≤𝑂(1) )