Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . . . 5
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ต โ P) |
2 | | simprlr 779 |
. . . . 5
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ฆ โ ๐ต) |
3 | | elprnq 10934 |
. . . . 5
โข ((๐ต โ P โง
๐ฆ โ ๐ต) โ ๐ฆ โ Q) |
4 | 1, 2, 3 | syl2anc 585 |
. . . 4
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ฆ โ Q) |
5 | | simp1 1137 |
. . . . 5
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ ๐ด
โ P) |
6 | | simprl 770 |
. . . . 5
โข (((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ)) โ ๐ โ ๐ด) |
7 | | elprnq 10934 |
. . . . 5
โข ((๐ด โ P โง
๐ โ ๐ด) โ ๐ โ Q) |
8 | 5, 6, 7 | syl2an 597 |
. . . 4
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ โ Q) |
9 | | simpl3 1194 |
. . . . 5
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ถ โ P) |
10 | | simprrr 781 |
. . . . 5
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ง โ ๐ถ) |
11 | | elprnq 10934 |
. . . . 5
โข ((๐ถ โ P โง
๐ง โ ๐ถ) โ ๐ง โ Q) |
12 | 9, 10, 11 | syl2anc 585 |
. . . 4
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ง โ Q) |
13 | | vex 3452 |
. . . . . 6
โข ๐ฅ โ V |
14 | | vex 3452 |
. . . . . 6
โข ๐ โ V |
15 | | ltmnq 10915 |
. . . . . 6
โข (๐ข โ Q โ
(๐ค
<Q ๐ฃ โ (๐ข ยทQ ๐ค) <Q
(๐ข
ยทQ ๐ฃ))) |
16 | | vex 3452 |
. . . . . 6
โข ๐ฆ โ V |
17 | | mulcomnq 10896 |
. . . . . 6
โข (๐ค
ยทQ ๐ฃ) = (๐ฃ ยทQ ๐ค) |
18 | 13, 14, 15, 16, 17 | caovord2 7571 |
. . . . 5
โข (๐ฆ โ Q โ
(๐ฅ
<Q ๐ โ (๐ฅ ยทQ ๐ฆ) <Q
(๐
ยทQ ๐ฆ))) |
19 | | mulclnq 10890 |
. . . . . 6
โข ((๐ โ Q โง
๐ง โ Q)
โ (๐
ยทQ ๐ง) โ Q) |
20 | | ovex 7395 |
. . . . . . 7
โข (๐ฅ
ยทQ ๐ฆ) โ V |
21 | | ovex 7395 |
. . . . . . 7
โข (๐
ยทQ ๐ฆ) โ V |
22 | | ltanq 10914 |
. . . . . . 7
โข (๐ข โ Q โ
(๐ค
<Q ๐ฃ โ (๐ข +Q ๐ค) <Q
(๐ข
+Q ๐ฃ))) |
23 | | ovex 7395 |
. . . . . . 7
โข (๐
ยทQ ๐ง) โ V |
24 | | addcomnq 10894 |
. . . . . . 7
โข (๐ค +Q
๐ฃ) = (๐ฃ +Q ๐ค) |
25 | 20, 21, 22, 23, 24 | caovord2 7571 |
. . . . . 6
โข ((๐
ยทQ ๐ง) โ Q โ ((๐ฅ
ยทQ ๐ฆ) <Q (๐
ยทQ ๐ฆ) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)))) |
26 | 19, 25 | syl 17 |
. . . . 5
โข ((๐ โ Q โง
๐ง โ Q)
โ ((๐ฅ
ยทQ ๐ฆ) <Q (๐
ยทQ ๐ฆ) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)))) |
27 | 18, 26 | sylan9bb 511 |
. . . 4
โข ((๐ฆ โ Q โง
(๐ โ Q
โง ๐ง โ
Q)) โ (๐ฅ
<Q ๐ โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)))) |
28 | 4, 8, 12, 27 | syl12anc 836 |
. . 3
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ฅ <Q ๐ โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)))) |
29 | | simpl1 1192 |
. . . . 5
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ด โ P) |
30 | | addclpr 10961 |
. . . . . . 7
โข ((๐ต โ P โง
๐ถ โ P)
โ (๐ต
+P ๐ถ) โ P) |
31 | 30 | 3adant1 1131 |
. . . . . 6
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ต
+P ๐ถ) โ P) |
32 | 31 | adantr 482 |
. . . . 5
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ต +P ๐ถ) โ
P) |
33 | | mulclpr 10963 |
. . . . 5
โข ((๐ด โ P โง
(๐ต
+P ๐ถ) โ P) โ (๐ด
ยทP (๐ต +P ๐ถ)) โ
P) |
34 | 29, 32, 33 | syl2anc 585 |
. . . 4
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ด ยทP (๐ต +P
๐ถ)) โ
P) |
35 | | distrnq 10904 |
. . . . 5
โข (๐
ยทQ (๐ฆ +Q ๐ง)) = ((๐ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) |
36 | | simprrl 780 |
. . . . . 6
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ โ ๐ด) |
37 | | df-plp 10926 |
. . . . . . . . 9
โข
+P = (๐ข โ P, ๐ฃ โ P โฆ {๐ค โฃ โ๐ โ ๐ข โโ โ ๐ฃ ๐ค = (๐ +Q โ)}) |
38 | | addclnq 10888 |
. . . . . . . . 9
โข ((๐ โ Q โง
โ โ Q)
โ (๐
+Q โ) โ Q) |
39 | 37, 38 | genpprecl 10944 |
. . . . . . . 8
โข ((๐ต โ P โง
๐ถ โ P)
โ ((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โ (๐ฆ +Q ๐ง) โ (๐ต +P ๐ถ))) |
40 | 39 | imp 408 |
. . . . . . 7
โข (((๐ต โ P โง
๐ถ โ P)
โง (๐ฆ โ ๐ต โง ๐ง โ ๐ถ)) โ (๐ฆ +Q ๐ง) โ (๐ต +P ๐ถ)) |
41 | 1, 9, 2, 10, 40 | syl22anc 838 |
. . . . . 6
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ฆ +Q ๐ง) โ (๐ต +P ๐ถ)) |
42 | | df-mp 10927 |
. . . . . . . 8
โข
ยทP = (๐ข โ P, ๐ฃ โ P โฆ {๐ค โฃ โ๐ โ ๐ข โโ โ ๐ฃ ๐ค = (๐ ยทQ โ)}) |
43 | | mulclnq 10890 |
. . . . . . . 8
โข ((๐ โ Q โง
โ โ Q)
โ (๐
ยทQ โ) โ Q) |
44 | 42, 43 | genpprecl 10944 |
. . . . . . 7
โข ((๐ด โ P โง
(๐ต
+P ๐ถ) โ P) โ ((๐ โ ๐ด โง (๐ฆ +Q ๐ง) โ (๐ต +P ๐ถ)) โ (๐ ยทQ (๐ฆ +Q
๐ง)) โ (๐ด
ยทP (๐ต +P ๐ถ)))) |
45 | 44 | imp 408 |
. . . . . 6
โข (((๐ด โ P โง
(๐ต
+P ๐ถ) โ P) โง (๐ โ ๐ด โง (๐ฆ +Q ๐ง) โ (๐ต +P ๐ถ))) โ (๐ ยทQ (๐ฆ +Q
๐ง)) โ (๐ด
ยทP (๐ต +P ๐ถ))) |
46 | 29, 32, 36, 41, 45 | syl22anc 838 |
. . . . 5
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ ยทQ (๐ฆ +Q
๐ง)) โ (๐ด
ยทP (๐ต +P ๐ถ))) |
47 | 35, 46 | eqeltrrid 2843 |
. . . 4
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ((๐ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ))) |
48 | | prcdnq 10936 |
. . . 4
โข (((๐ด
ยทP (๐ต +P ๐ถ)) โ P โง
((๐
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ))) โ (((๐ฅ
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)) <Q ((๐
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
49 | 34, 47, 48 | syl2anc 585 |
. . 3
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
50 | 28, 49 | sylbid 239 |
. 2
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ฅ <Q ๐ โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
51 | | simpll 766 |
. . . . 5
โข (((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ)) โ ๐ฅ โ ๐ด) |
52 | | elprnq 10934 |
. . . . 5
โข ((๐ด โ P โง
๐ฅ โ ๐ด) โ ๐ฅ โ Q) |
53 | 5, 51, 52 | syl2an 597 |
. . . 4
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ฅ โ Q) |
54 | | vex 3452 |
. . . . . 6
โข ๐ง โ V |
55 | 14, 13, 15, 54, 17 | caovord2 7571 |
. . . . 5
โข (๐ง โ Q โ
(๐
<Q ๐ฅ โ (๐ ยทQ ๐ง) <Q
(๐ฅ
ยทQ ๐ง))) |
56 | | mulclnq 10890 |
. . . . . 6
โข ((๐ฅ โ Q โง
๐ฆ โ Q)
โ (๐ฅ
ยทQ ๐ฆ) โ Q) |
57 | | ltanq 10914 |
. . . . . 6
โข ((๐ฅ
ยทQ ๐ฆ) โ Q โ ((๐
ยทQ ๐ง) <Q (๐ฅ
ยทQ ๐ง) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐ฅ
ยทQ ๐ฆ) +Q (๐ฅ
ยทQ ๐ง)))) |
58 | 56, 57 | syl 17 |
. . . . 5
โข ((๐ฅ โ Q โง
๐ฆ โ Q)
โ ((๐
ยทQ ๐ง) <Q (๐ฅ
ยทQ ๐ง) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐ฅ
ยทQ ๐ฆ) +Q (๐ฅ
ยทQ ๐ง)))) |
59 | 55, 58 | sylan9bbr 512 |
. . . 4
โข (((๐ฅ โ Q โง
๐ฆ โ Q)
โง ๐ง โ
Q) โ (๐
<Q ๐ฅ โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐ฅ
ยทQ ๐ฆ) +Q (๐ฅ
ยทQ ๐ง)))) |
60 | 53, 4, 12, 59 | syl21anc 837 |
. . 3
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ <Q ๐ฅ โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐ฅ
ยทQ ๐ฆ) +Q (๐ฅ
ยทQ ๐ง)))) |
61 | | distrnq 10904 |
. . . . 5
โข (๐ฅ
ยทQ (๐ฆ +Q ๐ง)) = ((๐ฅ ยทQ ๐ฆ) +Q
(๐ฅ
ยทQ ๐ง)) |
62 | | simprll 778 |
. . . . . 6
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ๐ฅ โ ๐ด) |
63 | 42, 43 | genpprecl 10944 |
. . . . . . 7
โข ((๐ด โ P โง
(๐ต
+P ๐ถ) โ P) โ ((๐ฅ โ ๐ด โง (๐ฆ +Q ๐ง) โ (๐ต +P ๐ถ)) โ (๐ฅ ยทQ (๐ฆ +Q
๐ง)) โ (๐ด
ยทP (๐ต +P ๐ถ)))) |
64 | 63 | imp 408 |
. . . . . 6
โข (((๐ด โ P โง
(๐ต
+P ๐ถ) โ P) โง (๐ฅ โ ๐ด โง (๐ฆ +Q ๐ง) โ (๐ต +P ๐ถ))) โ (๐ฅ ยทQ (๐ฆ +Q
๐ง)) โ (๐ด
ยทP (๐ต +P ๐ถ))) |
65 | 29, 32, 62, 41, 64 | syl22anc 838 |
. . . . 5
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ฅ ยทQ (๐ฆ +Q
๐ง)) โ (๐ด
ยทP (๐ต +P ๐ถ))) |
66 | 61, 65 | eqeltrrid 2843 |
. . . 4
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐ฅ
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ))) |
67 | | prcdnq 10936 |
. . . 4
โข (((๐ด
ยทP (๐ต +P ๐ถ)) โ P โง
((๐ฅ
ยทQ ๐ฆ) +Q (๐ฅ
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ))) โ (((๐ฅ
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)) <Q ((๐ฅ
ยทQ ๐ฆ) +Q (๐ฅ
ยทQ ๐ง)) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
68 | 34, 66, 67 | syl2anc 585 |
. . 3
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) <Q ((๐ฅ
ยทQ ๐ฆ) +Q (๐ฅ
ยทQ ๐ง)) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
69 | 60, 68 | sylbid 239 |
. 2
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ <Q ๐ฅ โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
70 | | ltsonq 10912 |
. . . . 5
โข
<Q Or Q |
71 | | sotrieq 5579 |
. . . . 5
โข ((
<Q Or Q โง (๐ฅ โ Q โง ๐ โ Q)) โ
(๐ฅ = ๐ โ ยฌ (๐ฅ <Q ๐ โจ ๐ <Q ๐ฅ))) |
72 | 70, 71 | mpan 689 |
. . . 4
โข ((๐ฅ โ Q โง
๐ โ Q)
โ (๐ฅ = ๐ โ ยฌ (๐ฅ <Q
๐ โจ ๐ <Q ๐ฅ))) |
73 | 53, 8, 72 | syl2anc 585 |
. . 3
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ฅ = ๐ โ ยฌ (๐ฅ <Q ๐ โจ ๐ <Q ๐ฅ))) |
74 | | oveq1 7369 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ฅ ยทQ ๐ง) = (๐ ยทQ ๐ง)) |
75 | 74 | oveq2d 7378 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐ฅ
ยทQ ๐ง)) = ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง))) |
76 | 61, 75 | eqtrid 2789 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ฅ ยทQ (๐ฆ +Q
๐ง)) = ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง))) |
77 | 76 | eleq1d 2823 |
. . . 4
โข (๐ฅ = ๐ โ ((๐ฅ ยทQ (๐ฆ +Q
๐ง)) โ (๐ด
ยทP (๐ต +P ๐ถ)) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
78 | 65, 77 | syl5ibcom 244 |
. . 3
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (๐ฅ = ๐ โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
79 | 73, 78 | sylbird 260 |
. 2
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (ยฌ (๐ฅ <Q ๐ โจ ๐ <Q ๐ฅ) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
80 | 50, 69, 79 | ecase3d 1033 |
1
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ))) |