Step | Hyp | Ref
| Expression |
1 | | prop 7473 |
. . . . . 6
โข (๐ด โ P โ
โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ
P) |
2 | | addnqprllem 7525 |
. . . . . 6
โข
(((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐บ โ (1st
โ๐ด)) โง ๐ โ Q) โ
(๐
<Q (๐บ +Q ๐ป) โ ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐บ) โ (1st โ๐ด))) |
3 | 1, 2 | sylanl1 402 |
. . . . 5
โข (((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง ๐ โ Q) โ
(๐
<Q (๐บ +Q ๐ป) โ ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐บ) โ (1st โ๐ด))) |
4 | 3 | adantlr 477 |
. . . 4
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
<Q (๐บ +Q ๐ป) โ ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐บ) โ (1st โ๐ด))) |
5 | | prop 7473 |
. . . . . 6
โข (๐ต โ P โ
โจ(1st โ๐ต), (2nd โ๐ต)โฉ โ
P) |
6 | | addnqprllem 7525 |
. . . . . 6
โข
(((โจ(1st โ๐ต), (2nd โ๐ต)โฉ โ P โง ๐ป โ (1st
โ๐ต)) โง ๐ โ Q) โ
(๐
<Q (๐บ +Q ๐ป) โ ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐ป) โ (1st โ๐ต))) |
7 | 5, 6 | sylanl1 402 |
. . . . 5
โข (((๐ต โ P โง
๐ป โ (1st
โ๐ต)) โง ๐ โ Q) โ
(๐
<Q (๐บ +Q ๐ป) โ ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐ป) โ (1st โ๐ต))) |
8 | 7 | adantll 476 |
. . . 4
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
<Q (๐บ +Q ๐ป) โ ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐ป) โ (1st โ๐ต))) |
9 | 4, 8 | jcad 307 |
. . 3
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
<Q (๐บ +Q ๐ป) โ (((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐บ) โ (1st โ๐ด) โง ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐ป) โ (1st โ๐ต)))) |
10 | | simpl 109 |
. . . 4
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
((๐ด โ P
โง ๐บ โ
(1st โ๐ด))
โง (๐ต โ
P โง ๐ป
โ (1st โ๐ต)))) |
11 | | simpl 109 |
. . . . 5
โข ((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โ ๐ด โ
P) |
12 | | simpl 109 |
. . . . 5
โข ((๐ต โ P โง
๐ป โ (1st
โ๐ต)) โ ๐ต โ
P) |
13 | 11, 12 | anim12i 338 |
. . . 4
โข (((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โ (๐ด โ P โง
๐ต โ
P)) |
14 | | df-iplp 7466 |
. . . . 5
โข
+P = (๐ฅ โ P, ๐ฆ โ P โฆ โจ{๐ โ Q โฃ
โ๐ โ
Q โ๐
โ Q (๐
โ (1st โ๐ฅ) โง ๐ โ (1st โ๐ฆ) โง ๐ = (๐ +Q ๐ ))}, {๐ โ Q โฃ โ๐ โ Q
โ๐ โ
Q (๐ โ
(2nd โ๐ฅ)
โง ๐ โ
(2nd โ๐ฆ)
โง ๐ = (๐ +Q
๐ ))}โฉ) |
15 | | addclnq 7373 |
. . . . 5
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
+Q ๐ ) โ Q) |
16 | 14, 15 | genpprecll 7512 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P)
โ ((((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐บ) โ (1st โ๐ด) โง ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐ป) โ (1st โ๐ต)) โ (((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐บ) +Q ((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐ป)) โ (1st โ(๐ด +P
๐ต)))) |
17 | 10, 13, 16 | 3syl 17 |
. . 3
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
((((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐บ) โ (1st โ๐ด) โง ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐ป) โ (1st โ๐ต)) โ (((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐บ) +Q ((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐ป)) โ (1st โ(๐ด +P
๐ต)))) |
18 | 9, 17 | syld 45 |
. 2
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
<Q (๐บ +Q ๐ป) โ (((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐บ) +Q ((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐ป)) โ (1st โ(๐ด +P
๐ต)))) |
19 | | simpr 110 |
. . . . 5
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
๐ โ
Q) |
20 | | elprnql 7479 |
. . . . . . . . 9
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐บ โ (1st
โ๐ด)) โ ๐บ โ
Q) |
21 | 1, 20 | sylan 283 |
. . . . . . . 8
โข ((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โ ๐บ โ
Q) |
22 | 21 | ad2antrr 488 |
. . . . . . 7
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
๐บ โ
Q) |
23 | | elprnql 7479 |
. . . . . . . . 9
โข
((โจ(1st โ๐ต), (2nd โ๐ต)โฉ โ P โง ๐ป โ (1st
โ๐ต)) โ ๐ป โ
Q) |
24 | 5, 23 | sylan 283 |
. . . . . . . 8
โข ((๐ต โ P โง
๐ป โ (1st
โ๐ต)) โ ๐ป โ
Q) |
25 | 24 | ad2antlr 489 |
. . . . . . 7
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
๐ป โ
Q) |
26 | | addclnq 7373 |
. . . . . . 7
โข ((๐บ โ Q โง
๐ป โ Q)
โ (๐บ
+Q ๐ป) โ Q) |
27 | 22, 25, 26 | syl2anc 411 |
. . . . . 6
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐บ
+Q ๐ป) โ Q) |
28 | | recclnq 7390 |
. . . . . 6
โข ((๐บ +Q
๐ป) โ Q
โ (*Qโ(๐บ +Q ๐ป)) โ
Q) |
29 | 27, 28 | syl 14 |
. . . . 5
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(*Qโ(๐บ +Q ๐ป)) โ
Q) |
30 | | mulassnqg 7382 |
. . . . 5
โข ((๐ โ Q โง
(*Qโ(๐บ +Q ๐ป)) โ Q โง
(๐บ
+Q ๐ป) โ Q) โ ((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ (๐บ +Q ๐ป)) = (๐ ยทQ
((*Qโ(๐บ +Q ๐ป))
ยทQ (๐บ +Q ๐ป)))) |
31 | 19, 29, 27, 30 | syl3anc 1238 |
. . . 4
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ (๐บ +Q ๐ป)) = (๐ ยทQ
((*Qโ(๐บ +Q ๐ป))
ยทQ (๐บ +Q ๐ป)))) |
32 | | mulclnq 7374 |
. . . . . 6
โข ((๐ โ Q โง
(*Qโ(๐บ +Q ๐ป)) โ Q)
โ (๐
ยทQ (*Qโ(๐บ +Q
๐ป))) โ
Q) |
33 | 19, 29, 32 | syl2anc 411 |
. . . . 5
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
ยทQ (*Qโ(๐บ +Q
๐ป))) โ
Q) |
34 | | distrnqg 7385 |
. . . . 5
โข (((๐
ยทQ (*Qโ(๐บ +Q
๐ป))) โ Q
โง ๐บ โ
Q โง ๐ป
โ Q) โ ((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ (๐บ +Q ๐ป)) = (((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐บ) +Q ((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐ป))) |
35 | 33, 22, 25, 34 | syl3anc 1238 |
. . . 4
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ (๐บ +Q ๐ป)) = (((๐ ยทQ
(*Qโ(๐บ +Q ๐ป)))
ยทQ ๐บ) +Q ((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐ป))) |
36 | | mulcomnqg 7381 |
. . . . . . . 8
โข
(((*Qโ(๐บ +Q ๐ป)) โ Q โง
(๐บ
+Q ๐ป) โ Q) โ
((*Qโ(๐บ +Q ๐ป))
ยทQ (๐บ +Q ๐ป)) = ((๐บ +Q ๐ป)
ยทQ (*Qโ(๐บ +Q
๐ป)))) |
37 | 29, 27, 36 | syl2anc 411 |
. . . . . . 7
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
((*Qโ(๐บ +Q ๐ป))
ยทQ (๐บ +Q ๐ป)) = ((๐บ +Q ๐ป)
ยทQ (*Qโ(๐บ +Q
๐ป)))) |
38 | | recidnq 7391 |
. . . . . . . 8
โข ((๐บ +Q
๐ป) โ Q
โ ((๐บ
+Q ๐ป) ยทQ
(*Qโ(๐บ +Q ๐ป))) =
1Q) |
39 | 27, 38 | syl 14 |
. . . . . . 7
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
((๐บ
+Q ๐ป) ยทQ
(*Qโ(๐บ +Q ๐ป))) =
1Q) |
40 | 37, 39 | eqtrd 2210 |
. . . . . 6
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
((*Qโ(๐บ +Q ๐ป))
ยทQ (๐บ +Q ๐ป)) =
1Q) |
41 | 40 | oveq2d 5890 |
. . . . 5
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
ยทQ ((*Qโ(๐บ +Q
๐ป))
ยทQ (๐บ +Q ๐ป))) = (๐ ยทQ
1Q)) |
42 | | mulidnq 7387 |
. . . . . 6
โข (๐ โ Q โ
(๐
ยทQ 1Q) = ๐) |
43 | 42 | adantl 277 |
. . . . 5
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
ยทQ 1Q) = ๐) |
44 | 41, 43 | eqtrd 2210 |
. . . 4
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
ยทQ ((*Qโ(๐บ +Q
๐ป))
ยทQ (๐บ +Q ๐ป))) = ๐) |
45 | 31, 35, 44 | 3eqtr3d 2218 |
. . 3
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐บ) +Q ((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐ป)) = ๐) |
46 | 45 | eleq1d 2246 |
. 2
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
((((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐บ) +Q ((๐
ยทQ (*Qโ(๐บ +Q
๐ป)))
ยทQ ๐ป)) โ (1st โ(๐ด +P
๐ต)) โ ๐ โ (1st
โ(๐ด
+P ๐ต)))) |
47 | 18, 46 | sylibd 149 |
1
โข ((((๐ด โ P โง
๐บ โ (1st
โ๐ด)) โง (๐ต โ P โง
๐ป โ (1st
โ๐ต))) โง ๐ โ Q) โ
(๐
<Q (๐บ +Q ๐ป) โ ๐ โ (1st โ(๐ด +P
๐ต)))) |