Metamath Proof Explorer

Theorem supadd

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

Ref Expression
Hypotheses supadd.a1 ⊢φ→A⊆ℝ
supadd.a2 ⊢φ→A≠∅
supadd.a3 ⊢φ→∃x∈ℝ∀y∈Ay≤x
supadd.b1 ⊢φ→B⊆ℝ
supadd.b2 ⊢φ→B≠∅
supadd.b3 ⊢φ→∃x∈ℝ∀y∈By≤x
supadd.c ⊢C=z|∃v∈A∃b∈Bz=v+b
Assertion supadd ⊢φ→supAℝ<+supBℝ<=supCℝ<

Proof

Step Hyp Ref Expression
1 supadd.a1 ⊢φ→A⊆ℝ
2 supadd.a2 ⊢φ→A≠∅
3 supadd.a3 ⊢φ→∃x∈ℝ∀y∈Ay≤x
4 supadd.b1 ⊢φ→B⊆ℝ
5 supadd.b2 ⊢φ→B≠∅
6 supadd.b3 ⊢φ→∃x∈ℝ∀y∈By≤x
7 supadd.c ⊢C=z|∃v∈A∃b∈Bz=v+b
8 4 5 6 suprcld ⊢φ→supBℝ<∈ℝ
9 eqid ⊢z|∃a∈Az=a+supBℝ<=z|∃a∈Az=a+supBℝ<
10 1 2 3 8 9 supaddc ⊢φ→supAℝ<+supBℝ<=supz|∃a∈Az=a+supBℝ<ℝ<
11 1 sselda ⊢φ∧a∈A→a∈ℝ
12 11 recnd ⊢φ∧a∈A→a∈ℂ
13 8 adantr ⊢φ∧a∈A→supBℝ<∈ℝ
14 13 recnd ⊢φ∧a∈A→supBℝ<∈ℂ
15 12 14 addcomd ⊢φ∧a∈A→a+supBℝ<=supBℝ<+a
16 15 eqeq2d ⊢φ∧a∈A→z=a+supBℝ<↔z=supBℝ<+a
17 16 rexbidva ⊢φ→∃a∈Az=a+supBℝ<↔∃a∈Az=supBℝ<+a
18 17 abbidv ⊢φ→z|∃a∈Az=a+supBℝ<=z|∃a∈Az=supBℝ<+a
19 18 supeq1d ⊢φ→supz|∃a∈Az=a+supBℝ<ℝ<=supz|∃a∈Az=supBℝ<+aℝ<
20 10 19 eqtrd ⊢φ→supAℝ<+supBℝ<=supz|∃a∈Az=supBℝ<+aℝ<
21 vex ⊢w∈V
22 eqeq1 ⊢z=w→z=supBℝ<+a↔w=supBℝ<+a
23 22 rexbidv ⊢z=w→∃a∈Az=supBℝ<+a↔∃a∈Aw=supBℝ<+a
24 21 23 elab ⊢w∈z|∃a∈Az=supBℝ<+a↔∃a∈Aw=supBℝ<+a
25 4 adantr ⊢φ∧a∈A→B⊆ℝ
26 5 adantr ⊢φ∧a∈A→B≠∅
27 6 adantr ⊢φ∧a∈A→∃x∈ℝ∀y∈By≤x
28 eqid ⊢z|∃b∈Bz=b+a=z|∃b∈Bz=b+a
29 25 26 27 11 28 supaddc ⊢φ∧a∈A→supBℝ<+a=supz|∃b∈Bz=b+aℝ<
30 4 sselda ⊢φ∧b∈B→b∈ℝ
31 30 adantlr ⊢φ∧a∈A∧b∈B→b∈ℝ
32 31 recnd ⊢φ∧a∈A∧b∈B→b∈ℂ
33 11 adantr ⊢φ∧a∈A∧b∈B→a∈ℝ
34 33 recnd ⊢φ∧a∈A∧b∈B→a∈ℂ
35 32 34 addcomd ⊢φ∧a∈A∧b∈B→b+a=a+b
36 35 eqeq2d ⊢φ∧a∈A∧b∈B→z=b+a↔z=a+b
37 36 rexbidva ⊢φ∧a∈A→∃b∈Bz=b+a↔∃b∈Bz=a+b
38 37 abbidv ⊢φ∧a∈A→z|∃b∈Bz=b+a=z|∃b∈Bz=a+b
39 38 supeq1d ⊢φ∧a∈A→supz|∃b∈Bz=b+aℝ<=supz|∃b∈Bz=a+bℝ<
40 29 39 eqtrd ⊢φ∧a∈A→supBℝ<+a=supz|∃b∈Bz=a+bℝ<
41 eqeq1 ⊢z=w→z=a+b↔w=a+b
42 41 rexbidv ⊢z=w→∃b∈Bz=a+b↔∃b∈Bw=a+b
43 21 42 elab ⊢w∈z|∃b∈Bz=a+b↔∃b∈Bw=a+b
44 rspe ⊢a∈A∧∃b∈Bw=a+b→∃a∈A∃b∈Bw=a+b
45 oveq1 ⊢v=a→v+b=a+b
46 45 eqeq2d ⊢v=a→z=v+b↔z=a+b
47 46 rexbidv ⊢v=a→∃b∈Bz=v+b↔∃b∈Bz=a+b
48 47 cbvrexvw ⊢∃v∈A∃b∈Bz=v+b↔∃a∈A∃b∈Bz=a+b
49 41 2rexbidv ⊢z=w→∃a∈A∃b∈Bz=a+b↔∃a∈A∃b∈Bw=a+b
50 48 49 bitrid ⊢z=w→∃v∈A∃b∈Bz=v+b↔∃a∈A∃b∈Bw=a+b
51 21 50 7 elab2 ⊢w∈C↔∃a∈A∃b∈Bw=a+b
52 44 51 sylibr ⊢a∈A∧∃b∈Bw=a+b→w∈C
53 52 ex ⊢a∈A→∃b∈Bw=a+b→w∈C
54 1 sseld ⊢φ→a∈A→a∈ℝ
55 4 sseld ⊢φ→b∈B→b∈ℝ
56 54 55 anim12d ⊢φ→a∈A∧b∈B→a∈ℝ∧b∈ℝ
57 readdcl ⊢a∈ℝ∧b∈ℝ→a+b∈ℝ
58 56 57 syl6 ⊢φ→a∈A∧b∈B→a+b∈ℝ
59 eleq1a ⊢a+b∈ℝ→w=a+b→w∈ℝ
60 58 59 syl6 ⊢φ→a∈A∧b∈B→w=a+b→w∈ℝ
61 60 rexlimdvv ⊢φ→∃a∈A∃b∈Bw=a+b→w∈ℝ
62 51 61 biimtrid ⊢φ→w∈C→w∈ℝ
63 62 ssrdv ⊢φ→C⊆ℝ
64 ovex ⊢a+b∈V
65 64 isseti ⊢∃ww=a+b
66 65 rgenw ⊢∀b∈B∃ww=a+b
67 r19.2z ⊢B≠∅∧∀b∈B∃ww=a+b→∃b∈B∃ww=a+b
68 5 66 67 sylancl ⊢φ→∃b∈B∃ww=a+b
69 rexcom4 ⊢∃b∈B∃ww=a+b↔∃w∃b∈Bw=a+b
70 68 69 sylib ⊢φ→∃w∃b∈Bw=a+b
71 70 ralrimivw ⊢φ→∀a∈A∃w∃b∈Bw=a+b
72 r19.2z ⊢A≠∅∧∀a∈A∃w∃b∈Bw=a+b→∃a∈A∃w∃b∈Bw=a+b
73 2 71 72 syl2anc ⊢φ→∃a∈A∃w∃b∈Bw=a+b
74 rexcom4 ⊢∃a∈A∃w∃b∈Bw=a+b↔∃w∃a∈A∃b∈Bw=a+b
75 73 74 sylib ⊢φ→∃w∃a∈A∃b∈Bw=a+b
76 n0 ⊢C≠∅↔∃ww∈C
77 51 exbii ⊢∃ww∈C↔∃w∃a∈A∃b∈Bw=a+b
78 76 77 bitri ⊢C≠∅↔∃w∃a∈A∃b∈Bw=a+b
79 75 78 sylibr ⊢φ→C≠∅
80 1 2 3 suprcld ⊢φ→supAℝ<∈ℝ
81 80 8 readdcld ⊢φ→supAℝ<+supBℝ<∈ℝ
82 11 adantrr ⊢φ∧a∈A∧b∈B→a∈ℝ
83 30 adantrl ⊢φ∧a∈A∧b∈B→b∈ℝ
84 80 adantr ⊢φ∧a∈A∧b∈B→supAℝ<∈ℝ
85 8 adantr ⊢φ∧a∈A∧b∈B→supBℝ<∈ℝ
86 1 2 3 3jca ⊢φ→A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x
87 suprub ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧a∈A→a≤supAℝ<
88 86 87 sylan ⊢φ∧a∈A→a≤supAℝ<
89 88 adantrr ⊢φ∧a∈A∧b∈B→a≤supAℝ<
90 4 5 6 3jca ⊢φ→B⊆ℝ∧B≠∅∧∃x∈ℝ∀y∈By≤x
91 suprub ⊢B⊆ℝ∧B≠∅∧∃x∈ℝ∀y∈By≤x∧b∈B→b≤supBℝ<
92 90 91 sylan ⊢φ∧b∈B→b≤supBℝ<
93 92 adantrl ⊢φ∧a∈A∧b∈B→b≤supBℝ<
94 82 83 84 85 89 93 le2addd ⊢φ∧a∈A∧b∈B→a+b≤supAℝ<+supBℝ<
95 94 ex ⊢φ→a∈A∧b∈B→a+b≤supAℝ<+supBℝ<
96 breq1 ⊢w=a+b→w≤supAℝ<+supBℝ<↔a+b≤supAℝ<+supBℝ<
97 96 biimprcd ⊢a+b≤supAℝ<+supBℝ<→w=a+b→w≤supAℝ<+supBℝ<
98 95 97 syl6 ⊢φ→a∈A∧b∈B→w=a+b→w≤supAℝ<+supBℝ<
99 98 rexlimdvv ⊢φ→∃a∈A∃b∈Bw=a+b→w≤supAℝ<+supBℝ<
100 51 99 biimtrid ⊢φ→w∈C→w≤supAℝ<+supBℝ<
101 100 ralrimiv ⊢φ→∀w∈Cw≤supAℝ<+supBℝ<
102 brralrspcev ⊢supAℝ<+supBℝ<∈ℝ∧∀w∈Cw≤supAℝ<+supBℝ<→∃x∈ℝ∀w∈Cw≤x
103 81 101 102 syl2anc ⊢φ→∃x∈ℝ∀w∈Cw≤x
104 suprub ⊢C⊆ℝ∧C≠∅∧∃x∈ℝ∀w∈Cw≤x∧w∈C→w≤supCℝ<
105 104 ex ⊢C⊆ℝ∧C≠∅∧∃x∈ℝ∀w∈Cw≤x→w∈C→w≤supCℝ<
106 63 79 103 105 syl3anc ⊢φ→w∈C→w≤supCℝ<
107 53 106 sylan9r ⊢φ∧a∈A→∃b∈Bw=a+b→w≤supCℝ<
108 43 107 biimtrid ⊢φ∧a∈A→w∈z|∃b∈Bz=a+b→w≤supCℝ<
109 108 ralrimiv ⊢φ∧a∈A→∀w∈z|∃b∈Bz=a+bw≤supCℝ<
110 33 31 readdcld ⊢φ∧a∈A∧b∈B→a+b∈ℝ
111 eleq1a ⊢a+b∈ℝ→z=a+b→z∈ℝ
112 110 111 syl ⊢φ∧a∈A∧b∈B→z=a+b→z∈ℝ
113 112 rexlimdva ⊢φ∧a∈A→∃b∈Bz=a+b→z∈ℝ
114 113 abssdv ⊢φ∧a∈A→z|∃b∈Bz=a+b⊆ℝ
115 64 isseti ⊢∃zz=a+b
116 115 rgenw ⊢∀b∈B∃zz=a+b
117 r19.2z ⊢B≠∅∧∀b∈B∃zz=a+b→∃b∈B∃zz=a+b
118 5 116 117 sylancl ⊢φ→∃b∈B∃zz=a+b
119 rexcom4 ⊢∃b∈B∃zz=a+b↔∃z∃b∈Bz=a+b
120 118 119 sylib ⊢φ→∃z∃b∈Bz=a+b
121 abn0 ⊢z|∃b∈Bz=a+b≠∅↔∃z∃b∈Bz=a+b
122 120 121 sylibr ⊢φ→z|∃b∈Bz=a+b≠∅
123 122 adantr ⊢φ∧a∈A→z|∃b∈Bz=a+b≠∅
124 63 79 103 suprcld ⊢φ→supCℝ<∈ℝ
125 124 adantr ⊢φ∧a∈A→supCℝ<∈ℝ
126 brralrspcev ⊢supCℝ<∈ℝ∧∀w∈z|∃b∈Bz=a+bw≤supCℝ<→∃x∈ℝ∀w∈z|∃b∈Bz=a+bw≤x
127 125 109 126 syl2anc ⊢φ∧a∈A→∃x∈ℝ∀w∈z|∃b∈Bz=a+bw≤x
128 suprleub ⊢z|∃b∈Bz=a+b⊆ℝ∧z|∃b∈Bz=a+b≠∅∧∃x∈ℝ∀w∈z|∃b∈Bz=a+bw≤x∧supCℝ<∈ℝ→supz|∃b∈Bz=a+bℝ<≤supCℝ<↔∀w∈z|∃b∈Bz=a+bw≤supCℝ<
129 114 123 127 125 128 syl31anc ⊢φ∧a∈A→supz|∃b∈Bz=a+bℝ<≤supCℝ<↔∀w∈z|∃b∈Bz=a+bw≤supCℝ<
130 109 129 mpbird ⊢φ∧a∈A→supz|∃b∈Bz=a+bℝ<≤supCℝ<
131 40 130 eqbrtrd ⊢φ∧a∈A→supBℝ<+a≤supCℝ<
132 breq1 ⊢w=supBℝ<+a→w≤supCℝ<↔supBℝ<+a≤supCℝ<
133 131 132 syl5ibrcom ⊢φ∧a∈A→w=supBℝ<+a→w≤supCℝ<
134 133 rexlimdva ⊢φ→∃a∈Aw=supBℝ<+a→w≤supCℝ<
135 24 134 biimtrid ⊢φ→w∈z|∃a∈Az=supBℝ<+a→w≤supCℝ<
136 135 ralrimiv ⊢φ→∀w∈z|∃a∈Az=supBℝ<+aw≤supCℝ<
137 13 11 readdcld ⊢φ∧a∈A→supBℝ<+a∈ℝ
138 eleq1a ⊢supBℝ<+a∈ℝ→z=supBℝ<+a→z∈ℝ
139 137 138 syl ⊢φ∧a∈A→z=supBℝ<+a→z∈ℝ
140 139 rexlimdva ⊢φ→∃a∈Az=supBℝ<+a→z∈ℝ
141 140 abssdv ⊢φ→z|∃a∈Az=supBℝ<+a⊆ℝ
142 ovex ⊢supBℝ<+a∈V
143 142 isseti ⊢∃zz=supBℝ<+a
144 143 rgenw ⊢∀a∈A∃zz=supBℝ<+a
145 r19.2z ⊢A≠∅∧∀a∈A∃zz=supBℝ<+a→∃a∈A∃zz=supBℝ<+a
146 2 144 145 sylancl ⊢φ→∃a∈A∃zz=supBℝ<+a
147 rexcom4 ⊢∃a∈A∃zz=supBℝ<+a↔∃z∃a∈Az=supBℝ<+a
148 146 147 sylib ⊢φ→∃z∃a∈Az=supBℝ<+a
149 abn0 ⊢z|∃a∈Az=supBℝ<+a≠∅↔∃z∃a∈Az=supBℝ<+a
150 148 149 sylibr ⊢φ→z|∃a∈Az=supBℝ<+a≠∅
151 brralrspcev ⊢supCℝ<∈ℝ∧∀w∈z|∃a∈Az=supBℝ<+aw≤supCℝ<→∃x∈ℝ∀w∈z|∃a∈Az=supBℝ<+aw≤x
152 124 136 151 syl2anc ⊢φ→∃x∈ℝ∀w∈z|∃a∈Az=supBℝ<+aw≤x
153 suprleub ⊢z|∃a∈Az=supBℝ<+a⊆ℝ∧z|∃a∈Az=supBℝ<+a≠∅∧∃x∈ℝ∀w∈z|∃a∈Az=supBℝ<+aw≤x∧supCℝ<∈ℝ→supz|∃a∈Az=supBℝ<+aℝ<≤supCℝ<↔∀w∈z|∃a∈Az=supBℝ<+aw≤supCℝ<
154 141 150 152 124 153 syl31anc ⊢φ→supz|∃a∈Az=supBℝ<+aℝ<≤supCℝ<↔∀w∈z|∃a∈Az=supBℝ<+aw≤supCℝ<
155 136 154 mpbird ⊢φ→supz|∃a∈Az=supBℝ<+aℝ<≤supCℝ<
156 20 155 eqbrtrd ⊢φ→supAℝ<+supBℝ<≤supCℝ<
157 suprleub ⊢C⊆ℝ∧C≠∅∧∃x∈ℝ∀w∈Cw≤x∧supAℝ<+supBℝ<∈ℝ→supCℝ<≤supAℝ<+supBℝ<↔∀w∈Cw≤supAℝ<+supBℝ<
158 63 79 103 81 157 syl31anc ⊢φ→supCℝ<≤supAℝ<+supBℝ<↔∀w∈Cw≤supAℝ<+supBℝ<
159 101 158 mpbird ⊢φ→supCℝ<≤supAℝ<+supBℝ<
160 81 124 letri3d ⊢φ→supAℝ<+supBℝ<=supCℝ<↔supAℝ<+supBℝ<≤supCℝ<∧supCℝ<≤supAℝ<+supBℝ<
161 156 159 160 mpbir2and ⊢φ→supAℝ<+supBℝ<=supCℝ<