Metamath Proof Explorer


Theorem addsuniflem

Description: Lemma for addsunif . State the whole theorem with extra distinct variable conditions. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsuniflem.1 φ L s R
addsuniflem.2 φ M s S
addsuniflem.3 φ A = L | s R
addsuniflem.4 φ B = M | s S
Assertion addsuniflem φ A + s B = y | l L y = l + s B z | m M z = A + s m | s w | r R w = r + s B t | s S t = A + s s

Proof

Step Hyp Ref Expression
1 addsuniflem.1 φ L s R
2 addsuniflem.2 φ M s S
3 addsuniflem.3 φ A = L | s R
4 addsuniflem.4 φ B = M | s S
5 1 scutcld φ L | s R No
6 3 5 eqeltrd φ A No
7 2 scutcld φ M | s S No
8 4 7 eqeltrd φ B No
9 addsval2 A No B No A + s B = a | p L A a = p + s B b | q L B b = A + s q | s c | e R A c = e + s B d | f R B d = A + s f
10 6 8 9 syl2anc φ A + s B = a | p L A a = p + s B b | q L B b = A + s q | s c | e R A c = e + s B d | f R B d = A + s f
11 6 8 addscut φ A + s B No a | p L A a = p + s B b | q L B b = A + s q s A + s B A + s B s c | e R A c = e + s B d | f R B d = A + s f
12 11 simp2d φ a | p L A a = p + s B b | q L B b = A + s q s A + s B
13 11 simp3d φ A + s B s c | e R A c = e + s B d | f R B d = A + s f
14 ovex A + s B V
15 14 snnz A + s B
16 sslttr a | p L A a = p + s B b | q L B b = A + s q s A + s B A + s B s c | e R A c = e + s B d | f R B d = A + s f A + s B a | p L A a = p + s B b | q L B b = A + s q s c | e R A c = e + s B d | f R B d = A + s f
17 15 16 mp3an3 a | p L A a = p + s B b | q L B b = A + s q s A + s B A + s B s c | e R A c = e + s B d | f R B d = A + s f a | p L A a = p + s B b | q L B b = A + s q s c | e R A c = e + s B d | f R B d = A + s f
18 12 13 17 syl2anc φ a | p L A a = p + s B b | q L B b = A + s q s c | e R A c = e + s B d | f R B d = A + s f
19 1 3 cofcutr1d φ p L A l L p s l
20 leftssno L A No
21 20 sseli p L A p No
22 21 ad2antlr φ p L A l L p No
23 ssltss1 L s R L No
24 1 23 syl φ L No
25 24 adantr φ p L A L No
26 25 sselda φ p L A l L l No
27 8 ad2antrr φ p L A l L B No
28 22 26 27 sleadd1d φ p L A l L p s l p + s B s l + s B
29 28 rexbidva φ p L A l L p s l l L p + s B s l + s B
30 29 ralbidva φ p L A l L p s l p L A l L p + s B s l + s B
31 19 30 mpbid φ p L A l L p + s B s l + s B
32 eqeq1 y = s y = l + s B s = l + s B
33 32 rexbidv y = s l L y = l + s B l L s = l + s B
34 33 rexab s y | l L y = l + s B p + s B s s s l L s = l + s B p + s B s s
35 rexcom4 l L s s = l + s B p + s B s s s l L s = l + s B p + s B s s
36 ovex l + s B V
37 breq2 s = l + s B p + s B s s p + s B s l + s B
38 36 37 ceqsexv s s = l + s B p + s B s s p + s B s l + s B
39 38 rexbii l L s s = l + s B p + s B s s l L p + s B s l + s B
40 r19.41v l L s = l + s B p + s B s s l L s = l + s B p + s B s s
41 40 exbii s l L s = l + s B p + s B s s s l L s = l + s B p + s B s s
42 35 39 41 3bitr3ri s l L s = l + s B p + s B s s l L p + s B s l + s B
43 34 42 bitri s y | l L y = l + s B p + s B s s l L p + s B s l + s B
44 ssun1 y | l L y = l + s B y | l L y = l + s B z | m M z = A + s m
45 ssrexv y | l L y = l + s B y | l L y = l + s B z | m M z = A + s m s y | l L y = l + s B p + s B s s s y | l L y = l + s B z | m M z = A + s m p + s B s s
46 44 45 ax-mp s y | l L y = l + s B p + s B s s s y | l L y = l + s B z | m M z = A + s m p + s B s s
47 43 46 sylbir l L p + s B s l + s B s y | l L y = l + s B z | m M z = A + s m p + s B s s
48 47 ralimi p L A l L p + s B s l + s B p L A s y | l L y = l + s B z | m M z = A + s m p + s B s s
49 31 48 syl φ p L A s y | l L y = l + s B z | m M z = A + s m p + s B s s
50 2 4 cofcutr1d φ q L B m M q s m
51 leftssno L B No
52 51 sseli q L B q No
53 52 ad2antlr φ q L B m M q No
54 ssltss1 M s S M No
55 2 54 syl φ M No
56 55 adantr φ q L B M No
57 56 sselda φ q L B m M m No
58 6 ad2antrr φ q L B m M A No
59 53 57 58 sleadd2d φ q L B m M q s m A + s q s A + s m
60 59 rexbidva φ q L B m M q s m m M A + s q s A + s m
61 60 ralbidva φ q L B m M q s m q L B m M A + s q s A + s m
62 50 61 mpbid φ q L B m M A + s q s A + s m
63 eqeq1 z = s z = A + s m s = A + s m
64 63 rexbidv z = s m M z = A + s m m M s = A + s m
65 64 rexab s z | m M z = A + s m A + s q s s s m M s = A + s m A + s q s s
66 rexcom4 m M s s = A + s m A + s q s s s m M s = A + s m A + s q s s
67 ovex A + s m V
68 breq2 s = A + s m A + s q s s A + s q s A + s m
69 67 68 ceqsexv s s = A + s m A + s q s s A + s q s A + s m
70 69 rexbii m M s s = A + s m A + s q s s m M A + s q s A + s m
71 r19.41v m M s = A + s m A + s q s s m M s = A + s m A + s q s s
72 71 exbii s m M s = A + s m A + s q s s s m M s = A + s m A + s q s s
73 66 70 72 3bitr3ri s m M s = A + s m A + s q s s m M A + s q s A + s m
74 65 73 bitri s z | m M z = A + s m A + s q s s m M A + s q s A + s m
75 ssun2 z | m M z = A + s m y | l L y = l + s B z | m M z = A + s m
76 ssrexv z | m M z = A + s m y | l L y = l + s B z | m M z = A + s m s z | m M z = A + s m A + s q s s s y | l L y = l + s B z | m M z = A + s m A + s q s s
77 75 76 ax-mp s z | m M z = A + s m A + s q s s s y | l L y = l + s B z | m M z = A + s m A + s q s s
78 74 77 sylbir m M A + s q s A + s m s y | l L y = l + s B z | m M z = A + s m A + s q s s
79 78 ralimi q L B m M A + s q s A + s m q L B s y | l L y = l + s B z | m M z = A + s m A + s q s s
80 62 79 syl φ q L B s y | l L y = l + s B z | m M z = A + s m A + s q s s
81 ralunb r a | p L A a = p + s B b | q L B b = A + s q s y | l L y = l + s B z | m M z = A + s m r s s r a | p L A a = p + s B s y | l L y = l + s B z | m M z = A + s m r s s r b | q L B b = A + s q s y | l L y = l + s B z | m M z = A + s m r s s
82 eqeq1 a = r a = p + s B r = p + s B
83 82 rexbidv a = r p L A a = p + s B p L A r = p + s B
84 83 ralab r a | p L A a = p + s B s y | l L y = l + s B z | m M z = A + s m r s s r p L A r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s
85 ralcom4 p L A r r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s r p L A r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s
86 ovex p + s B V
87 breq1 r = p + s B r s s p + s B s s
88 87 rexbidv r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s s y | l L y = l + s B z | m M z = A + s m p + s B s s
89 86 88 ceqsalv r r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s s y | l L y = l + s B z | m M z = A + s m p + s B s s
90 89 ralbii p L A r r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s p L A s y | l L y = l + s B z | m M z = A + s m p + s B s s
91 r19.23v p L A r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s p L A r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s
92 91 albii r p L A r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s r p L A r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s
93 85 90 92 3bitr3ri r p L A r = p + s B s y | l L y = l + s B z | m M z = A + s m r s s p L A s y | l L y = l + s B z | m M z = A + s m p + s B s s
94 84 93 bitri r a | p L A a = p + s B s y | l L y = l + s B z | m M z = A + s m r s s p L A s y | l L y = l + s B z | m M z = A + s m p + s B s s
95 eqeq1 b = r b = A + s q r = A + s q
96 95 rexbidv b = r q L B b = A + s q q L B r = A + s q
97 96 ralab r b | q L B b = A + s q s y | l L y = l + s B z | m M z = A + s m r s s r q L B r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s
98 ralcom4 q L B r r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s r q L B r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s
99 ovex A + s q V
100 breq1 r = A + s q r s s A + s q s s
101 100 rexbidv r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s s y | l L y = l + s B z | m M z = A + s m A + s q s s
102 99 101 ceqsalv r r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s s y | l L y = l + s B z | m M z = A + s m A + s q s s
103 102 ralbii q L B r r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s q L B s y | l L y = l + s B z | m M z = A + s m A + s q s s
104 r19.23v q L B r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s q L B r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s
105 104 albii r q L B r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s r q L B r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s
106 98 103 105 3bitr3ri r q L B r = A + s q s y | l L y = l + s B z | m M z = A + s m r s s q L B s y | l L y = l + s B z | m M z = A + s m A + s q s s
107 97 106 bitri r b | q L B b = A + s q s y | l L y = l + s B z | m M z = A + s m r s s q L B s y | l L y = l + s B z | m M z = A + s m A + s q s s
108 94 107 anbi12i r a | p L A a = p + s B s y | l L y = l + s B z | m M z = A + s m r s s r b | q L B b = A + s q s y | l L y = l + s B z | m M z = A + s m r s s p L A s y | l L y = l + s B z | m M z = A + s m p + s B s s q L B s y | l L y = l + s B z | m M z = A + s m A + s q s s
109 81 108 bitri r a | p L A a = p + s B b | q L B b = A + s q s y | l L y = l + s B z | m M z = A + s m r s s p L A s y | l L y = l + s B z | m M z = A + s m p + s B s s q L B s y | l L y = l + s B z | m M z = A + s m A + s q s s
110 49 80 109 sylanbrc φ r a | p L A a = p + s B b | q L B b = A + s q s y | l L y = l + s B z | m M z = A + s m r s s
111 1 3 cofcutr2d φ e R A r R r s e
112 ssltss2 L s R R No
113 1 112 syl φ R No
114 113 adantr φ e R A R No
115 114 sselda φ e R A r R r No
116 rightssno R A No
117 116 sseli e R A e No
118 117 ad2antlr φ e R A r R e No
119 8 ad2antrr φ e R A r R B No
120 115 118 119 sleadd1d φ e R A r R r s e r + s B s e + s B
121 120 rexbidva φ e R A r R r s e r R r + s B s e + s B
122 121 ralbidva φ e R A r R r s e e R A r R r + s B s e + s B
123 111 122 mpbid φ e R A r R r + s B s e + s B
124 eqeq1 w = b w = r + s B b = r + s B
125 124 rexbidv w = b r R w = r + s B r R b = r + s B
126 125 rexab b w | r R w = r + s B b s e + s B b r R b = r + s B b s e + s B
127 rexcom4 r R b b = r + s B b s e + s B b r R b = r + s B b s e + s B
128 ovex r + s B V
129 breq1 b = r + s B b s e + s B r + s B s e + s B
130 128 129 ceqsexv b b = r + s B b s e + s B r + s B s e + s B
131 130 rexbii r R b b = r + s B b s e + s B r R r + s B s e + s B
132 r19.41v r R b = r + s B b s e + s B r R b = r + s B b s e + s B
133 132 exbii b r R b = r + s B b s e + s B b r R b = r + s B b s e + s B
134 127 131 133 3bitr3ri b r R b = r + s B b s e + s B r R r + s B s e + s B
135 126 134 bitri b w | r R w = r + s B b s e + s B r R r + s B s e + s B
136 ssun1 w | r R w = r + s B w | r R w = r + s B t | s S t = A + s s
137 ssrexv w | r R w = r + s B w | r R w = r + s B t | s S t = A + s s b w | r R w = r + s B b s e + s B b w | r R w = r + s B t | s S t = A + s s b s e + s B
138 136 137 ax-mp b w | r R w = r + s B b s e + s B b w | r R w = r + s B t | s S t = A + s s b s e + s B
139 135 138 sylbir r R r + s B s e + s B b w | r R w = r + s B t | s S t = A + s s b s e + s B
140 139 ralimi e R A r R r + s B s e + s B e R A b w | r R w = r + s B t | s S t = A + s s b s e + s B
141 123 140 syl φ e R A b w | r R w = r + s B t | s S t = A + s s b s e + s B
142 2 4 cofcutr2d φ f R B s S s s f
143 ssltss2 M s S S No
144 2 143 syl φ S No
145 144 adantr φ f R B S No
146 145 sselda φ f R B s S s No
147 rightssno R B No
148 147 sseli f R B f No
149 148 ad2antlr φ f R B s S f No
150 6 ad2antrr φ f R B s S A No
151 146 149 150 sleadd2d φ f R B s S s s f A + s s s A + s f
152 151 rexbidva φ f R B s S s s f s S A + s s s A + s f
153 152 ralbidva φ f R B s S s s f f R B s S A + s s s A + s f
154 142 153 mpbid φ f R B s S A + s s s A + s f
155 eqeq1 t = b t = A + s s b = A + s s
156 155 rexbidv t = b s S t = A + s s s S b = A + s s
157 156 rexab b t | s S t = A + s s b s A + s f b s S b = A + s s b s A + s f
158 rexcom4 s S b b = A + s s b s A + s f b s S b = A + s s b s A + s f
159 ovex A + s s V
160 breq1 b = A + s s b s A + s f A + s s s A + s f
161 159 160 ceqsexv b b = A + s s b s A + s f A + s s s A + s f
162 161 rexbii s S b b = A + s s b s A + s f s S A + s s s A + s f
163 r19.41v s S b = A + s s b s A + s f s S b = A + s s b s A + s f
164 163 exbii b s S b = A + s s b s A + s f b s S b = A + s s b s A + s f
165 158 162 164 3bitr3ri b s S b = A + s s b s A + s f s S A + s s s A + s f
166 157 165 bitri b t | s S t = A + s s b s A + s f s S A + s s s A + s f
167 ssun2 t | s S t = A + s s w | r R w = r + s B t | s S t = A + s s
168 ssrexv t | s S t = A + s s w | r R w = r + s B t | s S t = A + s s b t | s S t = A + s s b s A + s f b w | r R w = r + s B t | s S t = A + s s b s A + s f
169 167 168 ax-mp b t | s S t = A + s s b s A + s f b w | r R w = r + s B t | s S t = A + s s b s A + s f
170 166 169 sylbir s S A + s s s A + s f b w | r R w = r + s B t | s S t = A + s s b s A + s f
171 170 ralimi f R B s S A + s s s A + s f f R B b w | r R w = r + s B t | s S t = A + s s b s A + s f
172 154 171 syl φ f R B b w | r R w = r + s B t | s S t = A + s s b s A + s f
173 ralunb a c | e R A c = e + s B d | f R B d = A + s f b w | r R w = r + s B t | s S t = A + s s b s a a c | e R A c = e + s B b w | r R w = r + s B t | s S t = A + s s b s a a d | f R B d = A + s f b w | r R w = r + s B t | s S t = A + s s b s a
174 eqeq1 c = a c = e + s B a = e + s B
175 174 rexbidv c = a e R A c = e + s B e R A a = e + s B
176 175 ralab a c | e R A c = e + s B b w | r R w = r + s B t | s S t = A + s s b s a a e R A a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a
177 ralcom4 e R A a a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a a e R A a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a
178 ovex e + s B V
179 breq2 a = e + s B b s a b s e + s B
180 179 rexbidv a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a b w | r R w = r + s B t | s S t = A + s s b s e + s B
181 178 180 ceqsalv a a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a b w | r R w = r + s B t | s S t = A + s s b s e + s B
182 181 ralbii e R A a a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a e R A b w | r R w = r + s B t | s S t = A + s s b s e + s B
183 r19.23v e R A a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a e R A a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a
184 183 albii a e R A a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a a e R A a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a
185 177 182 184 3bitr3ri a e R A a = e + s B b w | r R w = r + s B t | s S t = A + s s b s a e R A b w | r R w = r + s B t | s S t = A + s s b s e + s B
186 176 185 bitri a c | e R A c = e + s B b w | r R w = r + s B t | s S t = A + s s b s a e R A b w | r R w = r + s B t | s S t = A + s s b s e + s B
187 eqeq1 d = a d = A + s f a = A + s f
188 187 rexbidv d = a f R B d = A + s f f R B a = A + s f
189 188 ralab a d | f R B d = A + s f b w | r R w = r + s B t | s S t = A + s s b s a a f R B a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a
190 ralcom4 f R B a a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a a f R B a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a
191 ovex A + s f V
192 breq2 a = A + s f b s a b s A + s f
193 192 rexbidv a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a b w | r R w = r + s B t | s S t = A + s s b s A + s f
194 191 193 ceqsalv a a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a b w | r R w = r + s B t | s S t = A + s s b s A + s f
195 194 ralbii f R B a a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a f R B b w | r R w = r + s B t | s S t = A + s s b s A + s f
196 r19.23v f R B a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a f R B a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a
197 196 albii a f R B a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a a f R B a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a
198 190 195 197 3bitr3ri a f R B a = A + s f b w | r R w = r + s B t | s S t = A + s s b s a f R B b w | r R w = r + s B t | s S t = A + s s b s A + s f
199 189 198 bitri a d | f R B d = A + s f b w | r R w = r + s B t | s S t = A + s s b s a f R B b w | r R w = r + s B t | s S t = A + s s b s A + s f
200 186 199 anbi12i a c | e R A c = e + s B b w | r R w = r + s B t | s S t = A + s s b s a a d | f R B d = A + s f b w | r R w = r + s B t | s S t = A + s s b s a e R A b w | r R w = r + s B t | s S t = A + s s b s e + s B f R B b w | r R w = r + s B t | s S t = A + s s b s A + s f
201 173 200 bitri a c | e R A c = e + s B d | f R B d = A + s f b w | r R w = r + s B t | s S t = A + s s b s a e R A b w | r R w = r + s B t | s S t = A + s s b s e + s B f R B b w | r R w = r + s B t | s S t = A + s s b s A + s f
202 141 172 201 sylanbrc φ a c | e R A c = e + s B d | f R B d = A + s f b w | r R w = r + s B t | s S t = A + s s b s a
203 eqid l L l + s B = l L l + s B
204 203 rnmpt ran l L l + s B = y | l L y = l + s B
205 ssltex1 L s R L V
206 1 205 syl φ L V
207 206 mptexd φ l L l + s B V
208 rnexg l L l + s B V ran l L l + s B V
209 207 208 syl φ ran l L l + s B V
210 204 209 eqeltrrid φ y | l L y = l + s B V
211 eqid m M A + s m = m M A + s m
212 211 rnmpt ran m M A + s m = z | m M z = A + s m
213 ssltex1 M s S M V
214 2 213 syl φ M V
215 214 mptexd φ m M A + s m V
216 rnexg m M A + s m V ran m M A + s m V
217 215 216 syl φ ran m M A + s m V
218 212 217 eqeltrrid φ z | m M z = A + s m V
219 210 218 unexd φ y | l L y = l + s B z | m M z = A + s m V
220 snex A + s B V
221 220 a1i φ A + s B V
222 24 sselda φ l L l No
223 8 adantr φ l L B No
224 222 223 addscld φ l L l + s B No
225 eleq1 y = l + s B y No l + s B No
226 224 225 syl5ibrcom φ l L y = l + s B y No
227 226 rexlimdva φ l L y = l + s B y No
228 227 abssdv φ y | l L y = l + s B No
229 6 adantr φ m M A No
230 55 sselda φ m M m No
231 229 230 addscld φ m M A + s m No
232 eleq1 z = A + s m z No A + s m No
233 231 232 syl5ibrcom φ m M z = A + s m z No
234 233 rexlimdva φ m M z = A + s m z No
235 234 abssdv φ z | m M z = A + s m No
236 228 235 unssd φ y | l L y = l + s B z | m M z = A + s m No
237 6 8 addscld φ A + s B No
238 237 snssd φ A + s B No
239 velsn b A + s B b = A + s B
240 elun a y | l L y = l + s B z | m M z = A + s m a y | l L y = l + s B a z | m M z = A + s m
241 vex a V
242 eqeq1 y = a y = l + s B a = l + s B
243 242 rexbidv y = a l L y = l + s B l L a = l + s B
244 241 243 elab a y | l L y = l + s B l L a = l + s B
245 eqeq1 z = a z = A + s m a = A + s m
246 245 rexbidv z = a m M z = A + s m m M a = A + s m
247 241 246 elab a z | m M z = A + s m m M a = A + s m
248 244 247 orbi12i a y | l L y = l + s B a z | m M z = A + s m l L a = l + s B m M a = A + s m
249 240 248 bitri a y | l L y = l + s B z | m M z = A + s m l L a = l + s B m M a = A + s m
250 scutcut L s R L | s R No L s L | s R L | s R s R
251 1 250 syl φ L | s R No L s L | s R L | s R s R
252 251 simp2d φ L s L | s R
253 252 adantr φ l L L s L | s R
254 simpr φ l L l L
255 ovex L | s R V
256 255 snid L | s R L | s R
257 256 a1i φ l L L | s R L | s R
258 253 254 257 ssltsepcd φ l L l < s L | s R
259 3 adantr φ l L A = L | s R
260 258 259 breqtrrd φ l L l < s A
261 6 adantr φ l L A No
262 222 261 223 sltadd1d φ l L l < s A l + s B < s A + s B
263 260 262 mpbid φ l L l + s B < s A + s B
264 breq1 a = l + s B a < s A + s B l + s B < s A + s B
265 263 264 syl5ibrcom φ l L a = l + s B a < s A + s B
266 265 rexlimdva φ l L a = l + s B a < s A + s B
267 scutcut M s S M | s S No M s M | s S M | s S s S
268 2 267 syl φ M | s S No M s M | s S M | s S s S
269 268 simp2d φ M s M | s S
270 269 adantr φ m M M s M | s S
271 simpr φ m M m M
272 ovex M | s S V
273 272 snid M | s S M | s S
274 273 a1i φ m M M | s S M | s S
275 270 271 274 ssltsepcd φ m M m < s M | s S
276 4 adantr φ m M B = M | s S
277 275 276 breqtrrd φ m M m < s B
278 8 adantr φ m M B No
279 230 278 229 sltadd2d φ m M m < s B A + s m < s A + s B
280 277 279 mpbid φ m M A + s m < s A + s B
281 breq1 a = A + s m a < s A + s B A + s m < s A + s B
282 280 281 syl5ibrcom φ m M a = A + s m a < s A + s B
283 282 rexlimdva φ m M a = A + s m a < s A + s B
284 266 283 jaod φ l L a = l + s B m M a = A + s m a < s A + s B
285 249 284 biimtrid φ a y | l L y = l + s B z | m M z = A + s m a < s A + s B
286 285 imp φ a y | l L y = l + s B z | m M z = A + s m a < s A + s B
287 breq2 b = A + s B a < s b a < s A + s B
288 286 287 syl5ibrcom φ a y | l L y = l + s B z | m M z = A + s m b = A + s B a < s b
289 239 288 biimtrid φ a y | l L y = l + s B z | m M z = A + s m b A + s B a < s b
290 289 3impia φ a y | l L y = l + s B z | m M z = A + s m b A + s B a < s b
291 219 221 236 238 290 ssltd φ y | l L y = l + s B z | m M z = A + s m s A + s B
292 10 sneqd φ A + s B = a | p L A a = p + s B b | q L B b = A + s q | s c | e R A c = e + s B d | f R B d = A + s f
293 291 292 breqtrd φ y | l L y = l + s B z | m M z = A + s m s a | p L A a = p + s B b | q L B b = A + s q | s c | e R A c = e + s B d | f R B d = A + s f
294 eqid r R r + s B = r R r + s B
295 294 rnmpt ran r R r + s B = w | r R w = r + s B
296 ssltex2 L s R R V
297 1 296 syl φ R V
298 297 mptexd φ r R r + s B V
299 rnexg r R r + s B V ran r R r + s B V
300 298 299 syl φ ran r R r + s B V
301 295 300 eqeltrrid φ w | r R w = r + s B V
302 eqid s S A + s s = s S A + s s
303 302 rnmpt ran s S A + s s = t | s S t = A + s s
304 ssltex2 M s S S V
305 2 304 syl φ S V
306 305 mptexd φ s S A + s s V
307 rnexg s S A + s s V ran s S A + s s V
308 306 307 syl φ ran s S A + s s V
309 303 308 eqeltrrid φ t | s S t = A + s s V
310 301 309 unexd φ w | r R w = r + s B t | s S t = A + s s V
311 113 sselda φ r R r No
312 8 adantr φ r R B No
313 311 312 addscld φ r R r + s B No
314 eleq1 w = r + s B w No r + s B No
315 313 314 syl5ibrcom φ r R w = r + s B w No
316 315 rexlimdva φ r R w = r + s B w No
317 316 abssdv φ w | r R w = r + s B No
318 6 adantr φ s S A No
319 144 sselda φ s S s No
320 318 319 addscld φ s S A + s s No
321 eleq1 t = A + s s t No A + s s No
322 320 321 syl5ibrcom φ s S t = A + s s t No
323 322 rexlimdva φ s S t = A + s s t No
324 323 abssdv φ t | s S t = A + s s No
325 317 324 unssd φ w | r R w = r + s B t | s S t = A + s s No
326 velsn a A + s B a = A + s B
327 elun b w | r R w = r + s B t | s S t = A + s s b w | r R w = r + s B b t | s S t = A + s s
328 vex b V
329 328 125 elab b w | r R w = r + s B r R b = r + s B
330 328 156 elab b t | s S t = A + s s s S b = A + s s
331 329 330 orbi12i b w | r R w = r + s B b t | s S t = A + s s r R b = r + s B s S b = A + s s
332 327 331 bitri b w | r R w = r + s B t | s S t = A + s s r R b = r + s B s S b = A + s s
333 3 adantr φ r R A = L | s R
334 251 simp3d φ L | s R s R
335 334 adantr φ r R L | s R s R
336 256 a1i φ r R L | s R L | s R
337 simpr φ r R r R
338 335 336 337 ssltsepcd φ r R L | s R < s r
339 333 338 eqbrtrd φ r R A < s r
340 6 adantr φ r R A No
341 340 311 312 sltadd1d φ r R A < s r A + s B < s r + s B
342 339 341 mpbid φ r R A + s B < s r + s B
343 breq2 b = r + s B A + s B < s b A + s B < s r + s B
344 342 343 syl5ibrcom φ r R b = r + s B A + s B < s b
345 344 rexlimdva φ r R b = r + s B A + s B < s b
346 4 adantr φ s S B = M | s S
347 268 simp3d φ M | s S s S
348 347 adantr φ s S M | s S s S
349 273 a1i φ s S M | s S M | s S
350 simpr φ s S s S
351 348 349 350 ssltsepcd φ s S M | s S < s s
352 346 351 eqbrtrd φ s S B < s s
353 8 adantr φ s S B No
354 353 319 318 sltadd2d φ s S B < s s A + s B < s A + s s
355 352 354 mpbid φ s S A + s B < s A + s s
356 breq2 b = A + s s A + s B < s b A + s B < s A + s s
357 355 356 syl5ibrcom φ s S b = A + s s A + s B < s b
358 357 rexlimdva φ s S b = A + s s A + s B < s b
359 345 358 jaod φ r R b = r + s B s S b = A + s s A + s B < s b
360 332 359 biimtrid φ b w | r R w = r + s B t | s S t = A + s s A + s B < s b
361 360 imp φ b w | r R w = r + s B t | s S t = A + s s A + s B < s b
362 breq1 a = A + s B a < s b A + s B < s b
363 361 362 syl5ibrcom φ b w | r R w = r + s B t | s S t = A + s s a = A + s B a < s b
364 363 ex φ b w | r R w = r + s B t | s S t = A + s s a = A + s B a < s b
365 364 com23 φ a = A + s B b w | r R w = r + s B t | s S t = A + s s a < s b
366 326 365 biimtrid φ a A + s B b w | r R w = r + s B t | s S t = A + s s a < s b
367 366 3imp φ a A + s B b w | r R w = r + s B t | s S t = A + s s a < s b
368 221 310 238 325 367 ssltd φ A + s B s w | r R w = r + s B t | s S t = A + s s
369 292 368 eqbrtrrd φ a | p L A a = p + s B b | q L B b = A + s q | s c | e R A c = e + s B d | f R B d = A + s f s w | r R w = r + s B t | s S t = A + s s
370 18 110 202 293 369 cofcut1d φ a | p L A a = p + s B b | q L B b = A + s q | s c | e R A c = e + s B d | f R B d = A + s f = y | l L y = l + s B z | m M z = A + s m | s w | r R w = r + s B t | s S t = A + s s
371 10 370 eqtrd φ A + s B = y | l L y = l + s B z | m M z = A + s m | s w | r R w = r + s B t | s S t = A + s s