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 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
supadd.a2 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
supadd.a3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
supaddc.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
supaddc.c ⊢ 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + 𝐵 ) }
Assertion supaddc ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + 𝐵 ) = sup ( 𝐶 , ℝ , < ) )

Proof

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