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 ⊢φ∧x∈A→B∈V
o1add2.2 ⊢φ∧x∈A→C∈V
lo1add.3 ⊢φ→x∈A⟼B∈≤𝑂⁡1
lo1add.4 ⊢φ→x∈A⟼C∈≤𝑂⁡1
Assertion lo1add ⊢φ→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 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
6 1 ralrimiva ⊢φ→∀x∈AB∈V
7 dmmptg ⊢∀x∈AB∈V→dom⁡x∈A⟼B=A
8 6 7 syl ⊢φ→dom⁡x∈A⟼B=A
9 lo1dm ⊢x∈A⟼B∈≤𝑂⁡1→dom⁡x∈A⟼B⊆ℝ
10 3 9 syl ⊢φ→dom⁡x∈A⟼B⊆ℝ
11 8 10 eqsstrrd ⊢φ→A⊆ℝ
12 11 adantr ⊢φ∧m∈ℝ∧n∈ℝ→A⊆ℝ
13 rexanre ⊢A⊆ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m∧C≤n↔∃c∈ℝ∀x∈Ac≤x→B≤m∧∃c∈ℝ∀x∈Ac≤x→C≤n
14 12 13 syl ⊢φ∧m∈ℝ∧n∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m∧C≤n↔∃c∈ℝ∀x∈Ac≤x→B≤m∧∃c∈ℝ∀x∈Ac≤x→C≤n
15 readdcl ⊢m∈ℝ∧n∈ℝ→m+n∈ℝ
16 15 adantl ⊢φ∧m∈ℝ∧n∈ℝ→m+n∈ℝ
17 1 3 lo1mptrcl ⊢φ∧x∈A→B∈ℝ
18 17 adantlr ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→B∈ℝ
19 2 4 lo1mptrcl ⊢φ∧x∈A→C∈ℝ
20 19 adantlr ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→C∈ℝ
21 simplrl ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→m∈ℝ
22 simplrr ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→n∈ℝ
23 le2add ⊢B∈ℝ∧C∈ℝ∧m∈ℝ∧n∈ℝ→B≤m∧C≤n→B+C≤m+n
24 18 20 21 22 23 syl22anc ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→B≤m∧C≤n→B+C≤m+n
25 24 imim2d ⊢φ∧m∈ℝ∧n∈ℝ∧x∈A→c≤x→B≤m∧C≤n→c≤x→B+C≤m+n
26 25 ralimdva ⊢φ∧m∈ℝ∧n∈ℝ→∀x∈Ac≤x→B≤m∧C≤n→∀x∈Ac≤x→B+C≤m+n
27 breq2 ⊢p=m+n→B+C≤p↔B+C≤m+n
28 27 imbi2d ⊢p=m+n→c≤x→B+C≤p↔c≤x→B+C≤m+n
29 28 ralbidv ⊢p=m+n→∀x∈Ac≤x→B+C≤p↔∀x∈Ac≤x→B+C≤m+n
30 29 rspcev ⊢m+n∈ℝ∧∀x∈Ac≤x→B+C≤m+n→∃p∈ℝ∀x∈Ac≤x→B+C≤p
31 16 26 30 syl6an ⊢φ∧m∈ℝ∧n∈ℝ→∀x∈Ac≤x→B≤m∧C≤n→∃p∈ℝ∀x∈Ac≤x→B+C≤p
32 31 reximdv ⊢φ∧m∈ℝ∧n∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m∧C≤n→∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→B+C≤p
33 14 32 sylbird ⊢φ∧m∈ℝ∧n∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m∧∃c∈ℝ∀x∈Ac≤x→C≤n→∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→B+C≤p
34 33 rexlimdvva ⊢φ→∃m∈ℝ∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m∧∃c∈ℝ∀x∈Ac≤x→C≤n→∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→B+C≤p
35 5 34 biimtrrid ⊢φ→∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m∧∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→C≤n→∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→B+C≤p
36 11 17 ello1mpt ⊢φ→x∈A⟼B∈≤𝑂⁡1↔∃c∈ℝ∃m∈ℝ∀x∈Ac≤x→B≤m
37 rexcom ⊢∃c∈ℝ∃m∈ℝ∀x∈Ac≤x→B≤m↔∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m
38 36 37 bitrdi ⊢φ→x∈A⟼B∈≤𝑂⁡1↔∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m
39 11 19 ello1mpt ⊢φ→x∈A⟼C∈≤𝑂⁡1↔∃c∈ℝ∃n∈ℝ∀x∈Ac≤x→C≤n
40 rexcom ⊢∃c∈ℝ∃n∈ℝ∀x∈Ac≤x→C≤n↔∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→C≤n
41 39 40 bitrdi ⊢φ→x∈A⟼C∈≤𝑂⁡1↔∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→C≤n
42 38 41 anbi12d ⊢φ→x∈A⟼B∈≤𝑂⁡1∧x∈A⟼C∈≤𝑂⁡1↔∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m∧∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→C≤n
43 17 19 readdcld ⊢φ∧x∈A→B+C∈ℝ
44 11 43 ello1mpt ⊢φ→x∈A⟼B+C∈≤𝑂⁡1↔∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→B+C≤p
45 35 42 44 3imtr4d ⊢φ→x∈A⟼B∈≤𝑂⁡1∧x∈A⟼C∈≤𝑂⁡1→x∈A⟼B+C∈≤𝑂⁡1
46 3 4 45 mp2and ⊢φ→x∈A⟼B+C∈≤𝑂⁡1