Metamath Proof Explorer

Theorem supaddc

Description: The supremum function distributes over addition in a sense similar to that in supmul1 . (Contributed by Brendan Leahy, 25-Sep-2017)

Ref Expression
Hypotheses supadd.a1 ⊢ φ → A ⊆ ℝ
supadd.a2 ⊢ φ → A ≠ ∅
supadd.a3 ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
supaddc.b ⊢ φ → B ∈ ℝ
supaddc.c ⊢ C = z | ∃ v ∈ A z = v + B
Assertion supaddc ⊢ φ → sup A ℝ < + B = sup C ℝ <

Proof

Step Hyp Ref Expression
1 supadd.a1 ⊢ φ → A ⊆ ℝ
2 supadd.a2 ⊢ φ → A ≠ ∅
3 supadd.a3 ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
4 supaddc.b ⊢ φ → B ∈ ℝ
5 supaddc.c ⊢ C = z | ∃ v ∈ A z = v + B
6 vex ⊢ w ∈ V
7 oveq1 ⊢ v = a → v + B = a + B
8 7 eqeq2d ⊢ v = a → z = v + B ↔ z = a + B
9 8 cbvrexvw ⊢ ∃ v ∈ A z = v + B ↔ ∃ a ∈ A z = a + B
10 eqeq1 ⊢ z = w → z = a + B ↔ w = a + B
11 10 rexbidv ⊢ z = w → ∃ a ∈ A z = a + B ↔ ∃ a ∈ A w = a + B
12 9 11 bitrid ⊢ z = w → ∃ v ∈ A z = v + B ↔ ∃ a ∈ A w = a + B
13 6 12 5 elab2 ⊢ w ∈ C ↔ ∃ a ∈ A w = a + B
14 1 sselda ⊢ φ ∧ a ∈ A → a ∈ ℝ
15 1 2 3 suprcld ⊢ φ → sup A ℝ < ∈ ℝ
16 15 adantr ⊢ φ ∧ a ∈ A → sup A ℝ < ∈ ℝ
17 4 adantr ⊢ φ ∧ a ∈ A → B ∈ ℝ
18 1 2 3 3jca ⊢ φ → A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
19 suprub ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ a ∈ A → a ≤ sup A ℝ <
20 18 19 sylan ⊢ φ ∧ a ∈ A → a ≤ sup A ℝ <
21 14 16 17 20 leadd1dd ⊢ φ ∧ a ∈ A → a + B ≤ sup A ℝ < + B
22 breq1 ⊢ w = a + B → w ≤ sup A ℝ < + B ↔ a + B ≤ sup A ℝ < + B
23 21 22 syl5ibrcom ⊢ φ ∧ a ∈ A → w = a + B → w ≤ sup A ℝ < + B
24 23 rexlimdva ⊢ φ → ∃ a ∈ A w = a + B → w ≤ sup A ℝ < + B
25 13 24 biimtrid ⊢ φ → w ∈ C → w ≤ sup A ℝ < + B
26 25 ralrimiv ⊢ φ → ∀ w ∈ C w ≤ sup A ℝ < + B
27 14 17 readdcld ⊢ φ ∧ a ∈ A → a + B ∈ ℝ
28 eleq1a ⊢ a + B ∈ ℝ → w = a + B → w ∈ ℝ
29 27 28 syl ⊢ φ ∧ a ∈ A → w = a + B → w ∈ ℝ
30 29 rexlimdva ⊢ φ → ∃ a ∈ A w = a + B → w ∈ ℝ
31 13 30 biimtrid ⊢ φ → w ∈ C → w ∈ ℝ
32 31 ssrdv ⊢ φ → C ⊆ ℝ
33 ovex ⊢ a + B ∈ V
34 33 isseti ⊢ ∃ w w = a + B
35 34 rgenw ⊢ ∀ a ∈ A ∃ w w = a + B
36 r19.2z ⊢ A ≠ ∅ ∧ ∀ a ∈ A ∃ w w = a + B → ∃ a ∈ A ∃ w w = a + B
37 2 35 36 sylancl ⊢ φ → ∃ a ∈ A ∃ w w = a + B
38 13 exbii ⊢ ∃ w w ∈ C ↔ ∃ w ∃ a ∈ A w = a + B
39 n0 ⊢ C ≠ ∅ ↔ ∃ w w ∈ C
40 rexcom4 ⊢ ∃ a ∈ A ∃ w w = a + B ↔ ∃ w ∃ a ∈ A w = a + B
41 38 39 40 3bitr4i ⊢ C ≠ ∅ ↔ ∃ a ∈ A ∃ w w = a + B
42 37 41 sylibr ⊢ φ → C ≠ ∅
43 15 4 readdcld ⊢ φ → sup A ℝ < + B ∈ ℝ
44 brralrspcev ⊢ sup A ℝ < + B ∈ ℝ ∧ ∀ w ∈ C w ≤ sup A ℝ < + B → ∃ x ∈ ℝ ∀ w ∈ C w ≤ x
45 43 26 44 syl2anc ⊢ φ → ∃ x ∈ ℝ ∀ w ∈ C w ≤ x
46 suprleub ⊢ C ⊆ ℝ ∧ C ≠ ∅ ∧ ∃ x ∈ ℝ ∀ w ∈ C w ≤ x ∧ sup A ℝ < + B ∈ ℝ → sup C ℝ < ≤ sup A ℝ < + B ↔ ∀ w ∈ C w ≤ sup A ℝ < + B
47 32 42 45 43 46 syl31anc ⊢ φ → sup C ℝ < ≤ sup A ℝ < + B ↔ ∀ w ∈ C w ≤ sup A ℝ < + B
48 26 47 mpbird ⊢ φ → sup C ℝ < ≤ sup A ℝ < + B
49 32 42 45 suprcld ⊢ φ → sup C ℝ < ∈ ℝ
50 49 4 15 ltsubaddd ⊢ φ → sup C ℝ < − B < sup A ℝ < ↔ sup C ℝ < < sup A ℝ < + B
51 50 biimpar ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B → sup C ℝ < − B < sup A ℝ <
52 49 4 resubcld ⊢ φ → sup C ℝ < − B ∈ ℝ
53 suprlub ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ sup C ℝ < − B ∈ ℝ → sup C ℝ < − B < sup A ℝ < ↔ ∃ a ∈ A sup C ℝ < − B < a
54 1 2 3 52 53 syl31anc ⊢ φ → sup C ℝ < − B < sup A ℝ < ↔ ∃ a ∈ A sup C ℝ < − B < a
55 54 adantr ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B → sup C ℝ < − B < sup A ℝ < ↔ ∃ a ∈ A sup C ℝ < − B < a
56 51 55 mpbid ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B → ∃ a ∈ A sup C ℝ < − B < a
57 27 adantlr ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B ∧ a ∈ A → a + B ∈ ℝ
58 49 ad2antrr ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B ∧ a ∈ A → sup C ℝ < ∈ ℝ
59 rspe ⊢ a ∈ A ∧ w = a + B → ∃ a ∈ A w = a + B
60 59 13 sylibr ⊢ a ∈ A ∧ w = a + B → w ∈ C
61 60 adantl ⊢ φ ∧ a ∈ A ∧ w = a + B → w ∈ C
62 simplrr ⊢ φ ∧ a ∈ A ∧ w = a + B ∧ w ∈ C → w = a + B
63 32 42 45 3jca ⊢ φ → C ⊆ ℝ ∧ C ≠ ∅ ∧ ∃ x ∈ ℝ ∀ w ∈ C w ≤ x
64 suprub ⊢ C ⊆ ℝ ∧ C ≠ ∅ ∧ ∃ x ∈ ℝ ∀ w ∈ C w ≤ x ∧ w ∈ C → w ≤ sup C ℝ <
65 63 64 sylan ⊢ φ ∧ w ∈ C → w ≤ sup C ℝ <
66 65 adantlr ⊢ φ ∧ a ∈ A ∧ w = a + B ∧ w ∈ C → w ≤ sup C ℝ <
67 62 66 eqbrtrrd ⊢ φ ∧ a ∈ A ∧ w = a + B ∧ w ∈ C → a + B ≤ sup C ℝ <
68 61 67 mpdan ⊢ φ ∧ a ∈ A ∧ w = a + B → a + B ≤ sup C ℝ <
69 68 expr ⊢ φ ∧ a ∈ A → w = a + B → a + B ≤ sup C ℝ <
70 69 exlimdv ⊢ φ ∧ a ∈ A → ∃ w w = a + B → a + B ≤ sup C ℝ <
71 34 70 mpi ⊢ φ ∧ a ∈ A → a + B ≤ sup C ℝ <
72 71 adantlr ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B ∧ a ∈ A → a + B ≤ sup C ℝ <
73 57 58 72 lensymd ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B ∧ a ∈ A → ¬ sup C ℝ < < a + B
74 4 ad2antrr ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B ∧ a ∈ A → B ∈ ℝ
75 14 adantlr ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B ∧ a ∈ A → a ∈ ℝ
76 58 74 75 ltsubaddd ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B ∧ a ∈ A → sup C ℝ < − B < a ↔ sup C ℝ < < a + B
77 73 76 mtbird ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B ∧ a ∈ A → ¬ sup C ℝ < − B < a
78 77 nrexdv ⊢ φ ∧ sup C ℝ < < sup A ℝ < + B → ¬ ∃ a ∈ A sup C ℝ < − B < a
79 56 78 pm2.65da ⊢ φ → ¬ sup C ℝ < < sup A ℝ < + B
80 49 43 eqleltd ⊢ φ → sup C ℝ < = sup A ℝ < + B ↔ sup C ℝ < ≤ sup A ℝ < + B ∧ ¬ sup C ℝ < < sup A ℝ < + B
81 48 79 80 mpbir2and ⊢ φ → sup C ℝ < = sup A ℝ < + B
82 81 eqcomd ⊢ φ → sup A ℝ < + B = sup C ℝ <