Step | Hyp | Ref
| Expression |
1 | | mulcmpblnrlem 11011 |
. . 3
โข (((๐ด +P
๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐
)) โ ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
)))) = ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐บ) +P (๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐))))) |
2 | | mulclpr 10961 |
. . . . . 6
โข ((๐ท โ P โง
๐น โ P)
โ (๐ท
ยทP ๐น) โ P) |
3 | 2 | ad2ant2lr 747 |
. . . . 5
โข (((๐ถ โ P โง
๐ท โ P)
โง (๐น โ
P โง ๐บ
โ P)) โ (๐ท ยทP ๐น) โ
P) |
4 | 3 | ad2ant2lr 747 |
. . . 4
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (๐ท ยทP ๐น) โ
P) |
5 | | simplll 774 |
. . . . . . 7
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ๐ด
โ P) |
6 | | simprll 778 |
. . . . . . 7
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ๐น
โ P) |
7 | | mulclpr 10961 |
. . . . . . 7
โข ((๐ด โ P โง
๐น โ P)
โ (๐ด
ยทP ๐น) โ P) |
8 | 5, 6, 7 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (๐ด ยทP ๐น) โ
P) |
9 | | simpllr 775 |
. . . . . . 7
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ๐ต
โ P) |
10 | | simprlr 779 |
. . . . . . 7
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ๐บ
โ P) |
11 | | mulclpr 10961 |
. . . . . . 7
โข ((๐ต โ P โง
๐บ โ P)
โ (๐ต
ยทP ๐บ) โ P) |
12 | 9, 10, 11 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (๐ต ยทP ๐บ) โ
P) |
13 | | addclpr 10959 |
. . . . . 6
โข (((๐ด
ยทP ๐น) โ P โง (๐ต
ยทP ๐บ) โ P) โ ((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) โ P) |
14 | 8, 12, 13 | syl2anc 585 |
. . . . 5
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ((๐ด ยทP ๐น) +P
(๐ต
ยทP ๐บ)) โ P) |
15 | | simplrl 776 |
. . . . . . 7
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ๐ถ
โ P) |
16 | | simprrr 781 |
. . . . . . 7
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ๐
โ P) |
17 | | mulclpr 10961 |
. . . . . . 7
โข ((๐ถ โ P โง
๐ โ P)
โ (๐ถ
ยทP ๐) โ P) |
18 | 15, 16, 17 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (๐ถ ยทP ๐) โ
P) |
19 | | simplrr 777 |
. . . . . . 7
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ๐ท
โ P) |
20 | | simprrl 780 |
. . . . . . 7
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ๐
โ P) |
21 | | mulclpr 10961 |
. . . . . . 7
โข ((๐ท โ P โง
๐
โ P)
โ (๐ท
ยทP ๐
) โ P) |
22 | 19, 20, 21 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (๐ท ยทP ๐
) โ
P) |
23 | | addclpr 10959 |
. . . . . 6
โข (((๐ถ
ยทP ๐) โ P โง (๐ท
ยทP ๐
) โ P) โ ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
)) โ P) |
24 | 18, 22, 23 | syl2anc 585 |
. . . . 5
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ((๐ถ ยทP ๐) +P
(๐ท
ยทP ๐
)) โ P) |
25 | | addclpr 10959 |
. . . . 5
โข ((((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) โ P โง ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
)) โ P) โ (((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
))) โ P) |
26 | 14, 24, 25 | syl2anc 585 |
. . . 4
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (((๐ด ยทP ๐น) +P
(๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
))) โ P) |
27 | | addcanpr 10987 |
. . . 4
โข (((๐ท
ยทP ๐น) โ P โง (((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
))) โ P) โ (((๐ท
ยทP ๐น) +P (((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
)))) = ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐บ) +P (๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐)))) โ (((๐ด ยทP ๐น) +P
(๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
))) = (((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐))))) |
28 | 4, 26, 27 | syl2anc 585 |
. . 3
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
)))) = ((๐ท ยทP ๐น) +P
(((๐ด
ยทP ๐บ) +P (๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐)))) โ (((๐ด ยทP ๐น) +P
(๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
))) = (((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐))))) |
29 | 1, 28 | syl5 34 |
. 2
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐
)) โ (((๐ด ยทP ๐น) +P
(๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
))) = (((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐))))) |
30 | | mulclpr 10961 |
. . . . 5
โข ((๐ด โ P โง
๐บ โ P)
โ (๐ด
ยทP ๐บ) โ P) |
31 | | mulclpr 10961 |
. . . . 5
โข ((๐ต โ P โง
๐น โ P)
โ (๐ต
ยทP ๐น) โ P) |
32 | | addclpr 10959 |
. . . . 5
โข (((๐ด
ยทP ๐บ) โ P โง (๐ต
ยทP ๐น) โ P) โ ((๐ด
ยทP ๐บ) +P (๐ต
ยทP ๐น)) โ P) |
33 | 30, 31, 32 | syl2an 597 |
. . . 4
โข (((๐ด โ P โง
๐บ โ P)
โง (๐ต โ
P โง ๐น
โ P)) โ ((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น)) โ P) |
34 | 5, 10, 9, 6, 33 | syl22anc 838 |
. . 3
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น)) โ P) |
35 | | mulclpr 10961 |
. . . . 5
โข ((๐ถ โ P โง
๐
โ P)
โ (๐ถ
ยทP ๐
) โ P) |
36 | | mulclpr 10961 |
. . . . 5
โข ((๐ท โ P โง
๐ โ P)
โ (๐ท
ยทP ๐) โ P) |
37 | | addclpr 10959 |
. . . . 5
โข (((๐ถ
ยทP ๐
) โ P โง (๐ท
ยทP ๐) โ P) โ ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐)) โ P) |
38 | 35, 36, 37 | syl2an 597 |
. . . 4
โข (((๐ถ โ P โง
๐
โ P)
โง (๐ท โ
P โง ๐
โ P)) โ ((๐ถ ยทP ๐
) +P
(๐ท
ยทP ๐)) โ P) |
39 | 15, 20, 19, 16, 38 | syl22anc 838 |
. . 3
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ ((๐ถ ยทP ๐
) +P
(๐ท
ยทP ๐)) โ P) |
40 | | enrbreq 11006 |
. . 3
โข
(((((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)) โ P โง ((๐ด
ยทP ๐บ) +P (๐ต
ยทP ๐น)) โ P) โง (((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐)) โ P โง ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
)) โ P)) โ
(โจ((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)), ((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น))โฉ ~R
โจ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐)), ((๐ถ ยทP ๐) +P
(๐ท
ยทP ๐
))โฉ โ (((๐ด ยทP ๐น) +P
(๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
))) = (((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐))))) |
41 | 14, 34, 39, 24, 40 | syl22anc 838 |
. 2
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (โจ((๐ด ยทP ๐น) +P
(๐ต
ยทP ๐บ)), ((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น))โฉ ~R
โจ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐)), ((๐ถ ยทP ๐) +P
(๐ท
ยทP ๐
))โฉ โ (((๐ด ยทP ๐น) +P
(๐ต
ยทP ๐บ)) +P ((๐ถ
ยทP ๐) +P (๐ท
ยทP ๐
))) = (((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น)) +P ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐))))) |
42 | 29, 41 | sylibrd 259 |
1
โข ((((๐ด โ P โง
๐ต โ P)
โง (๐ถ โ
P โง ๐ท
โ P)) โง ((๐น โ P โง ๐บ โ P) โง
(๐
โ P
โง ๐ โ
P))) โ (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐
)) โ โจ((๐ด
ยทP ๐น) +P (๐ต
ยทP ๐บ)), ((๐ด ยทP ๐บ) +P
(๐ต
ยทP ๐น))โฉ ~R
โจ((๐ถ
ยทP ๐
) +P (๐ท
ยทP ๐)), ((๐ถ ยทP ๐) +P
(๐ท
ยทP ๐
))โฉ)) |