Step | Hyp | Ref
| Expression |
1 | | df-nr 7726 |
. 2
โข
R = ((P ร P) /
~R ) |
2 | | oveq1 5882 |
. . . 4
โข
([โจ๐ฅ, ๐ฆโฉ]
~R = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) =
(๐ด
ยทR [โจ๐ข, ๐ฃโฉ] ~R
)) |
3 | 2 | breq1d 4014 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~R = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R )
<R ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) โ
(๐ด
ยทR [โจ๐ข, ๐ฃโฉ] ~R )
<R ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R
))) |
4 | | breq1 4007 |
. . . 4
โข
([โจ๐ฅ, ๐ฆโฉ]
~R = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~R
<R [โจ๐ง, ๐คโฉ] ~R โ
๐ด
<R [โจ๐ง, ๐คโฉ] ~R
)) |
5 | | breq2 4008 |
. . . 4
โข
([โจ๐ฅ, ๐ฆโฉ]
~R = ๐ด โ ([โจ๐ง, ๐คโฉ] ~R
<R [โจ๐ฅ, ๐ฆโฉ] ~R โ
[โจ๐ง, ๐คโฉ]
~R <R ๐ด)) |
6 | 4, 5 | orbi12d 793 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~R = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~R
<R [โจ๐ง, ๐คโฉ] ~R โจ
[โจ๐ง, ๐คโฉ]
~R <R [โจ๐ฅ, ๐ฆโฉ] ~R ) โ
(๐ด
<R [โจ๐ง, ๐คโฉ] ~R โจ
[โจ๐ง, ๐คโฉ]
~R <R ๐ด))) |
7 | 3, 6 | imbi12d 234 |
. 2
โข
([โจ๐ฅ, ๐ฆโฉ]
~R = ๐ด โ ((([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R )
<R ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) โ
([โจ๐ฅ, ๐ฆโฉ]
~R <R [โจ๐ง, ๐คโฉ] ~R โจ
[โจ๐ง, ๐คโฉ]
~R <R [โจ๐ฅ, ๐ฆโฉ] ~R )) โ
((๐ด
ยทR [โจ๐ข, ๐ฃโฉ] ~R )
<R ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) โ
(๐ด
<R [โจ๐ง, ๐คโฉ] ~R โจ
[โจ๐ง, ๐คโฉ]
~R <R ๐ด)))) |
8 | | oveq1 5882 |
. . . 4
โข
([โจ๐ง, ๐คโฉ]
~R = ๐ต โ ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) =
(๐ต
ยทR [โจ๐ข, ๐ฃโฉ] ~R
)) |
9 | 8 | breq2d 4016 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~R = ๐ต โ ((๐ด ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) <R ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) โ
(๐ด
ยทR [โจ๐ข, ๐ฃโฉ] ~R )
<R (๐ต ยทR
[โจ๐ข, ๐ฃโฉ]
~R ))) |
10 | | breq2 4008 |
. . . 4
โข
([โจ๐ง, ๐คโฉ]
~R = ๐ต โ (๐ด <R [โจ๐ง, ๐คโฉ] ~R โ
๐ด
<R ๐ต)) |
11 | | breq1 4007 |
. . . 4
โข
([โจ๐ง, ๐คโฉ]
~R = ๐ต โ ([โจ๐ง, ๐คโฉ] ~R
<R ๐ด โ ๐ต <R ๐ด)) |
12 | 10, 11 | orbi12d 793 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~R = ๐ต โ ((๐ด <R [โจ๐ง, ๐คโฉ] ~R โจ
[โจ๐ง, ๐คโฉ]
~R <R ๐ด) โ (๐ด <R ๐ต โจ ๐ต <R ๐ด))) |
13 | 9, 12 | imbi12d 234 |
. 2
โข
([โจ๐ง, ๐คโฉ]
~R = ๐ต โ (((๐ด ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) <R ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) โ
(๐ด
<R [โจ๐ง, ๐คโฉ] ~R โจ
[โจ๐ง, ๐คโฉ]
~R <R ๐ด)) โ ((๐ด ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) <R (๐ต ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) โ (๐ด <R ๐ต โจ ๐ต <R ๐ด)))) |
14 | | oveq2 5883 |
. . . 4
โข
([โจ๐ข, ๐ฃโฉ]
~R = ๐ถ โ (๐ด ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) = (๐ด ยทR ๐ถ)) |
15 | | oveq2 5883 |
. . . 4
โข
([โจ๐ข, ๐ฃโฉ]
~R = ๐ถ โ (๐ต ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) = (๐ต ยทR ๐ถ)) |
16 | 14, 15 | breq12d 4017 |
. . 3
โข
([โจ๐ข, ๐ฃโฉ]
~R = ๐ถ โ ((๐ด ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) <R (๐ต ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) โ (๐ด ยทR ๐ถ) <R
(๐ต
ยทR ๐ถ))) |
17 | 16 | imbi1d 231 |
. 2
โข
([โจ๐ข, ๐ฃโฉ]
~R = ๐ถ โ (((๐ด ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) <R (๐ต ยทR
[โจ๐ข, ๐ฃโฉ]
~R ) โ (๐ด <R ๐ต โจ ๐ต <R ๐ด)) โ ((๐ด ยทR ๐ถ) <R
(๐ต
ยทR ๐ถ) โ (๐ด <R ๐ต โจ ๐ต <R ๐ด)))) |
18 | | mulextsr1lem 7779 |
. . 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 ๐ฅ)))) |
19 | | mulsrpr 7745 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ข โ
P โง ๐ฃ
โ P)) โ ([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) =
[โจ((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)), ((๐ฅ ยทP ๐ฃ) +P
(๐ฆ
ยทP ๐ข))โฉ] ~R
) |
20 | 19 | 3adant2 1016 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
([โจ๐ฅ, ๐ฆโฉ]
~R ยทR [โจ๐ข, ๐ฃโฉ] ~R ) =
[โจ((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)), ((๐ฅ ยทP ๐ฃ) +P
(๐ฆ
ยทP ๐ข))โฉ] ~R
) |
21 | | mulsrpr 7745 |
. . . . . 6
โข (((๐ง โ P โง
๐ค โ P)
โง (๐ข โ
P โง ๐ฃ
โ P)) โ ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) =
[โจ((๐ง
ยทP ๐ข) +P (๐ค
ยทP ๐ฃ)), ((๐ง ยทP ๐ฃ) +P
(๐ค
ยทP ๐ข))โฉ] ~R
) |
22 | 21 | 3adant1 1015 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
([โจ๐ง, ๐คโฉ]
~R ยทR [โจ๐ข, ๐ฃโฉ] ~R ) =
[โจ((๐ง
ยทP ๐ข) +P (๐ค
ยทP ๐ฃ)), ((๐ง ยทP ๐ฃ) +P
(๐ค
ยทP ๐ข))โฉ] ~R
) |
23 | 20, 22 | breq12d 4017 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(([โจ๐ฅ, ๐ฆโฉ]
~R ยทR [โจ๐ข, ๐ฃโฉ] ~R )
<R ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) โ
[โจ((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)), ((๐ฅ ยทP ๐ฃ) +P
(๐ฆ
ยทP ๐ข))โฉ] ~R
<R [โจ((๐ง ยทP ๐ข) +P
(๐ค
ยทP ๐ฃ)), ((๐ง ยทP ๐ฃ) +P
(๐ค
ยทP ๐ข))โฉ] ~R
)) |
24 | | simp1l 1021 |
. . . . . . 7
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
๐ฅ โ
P) |
25 | | simp3l 1025 |
. . . . . . 7
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
๐ข โ
P) |
26 | | mulclpr 7571 |
. . . . . . 7
โข ((๐ฅ โ P โง
๐ข โ P)
โ (๐ฅ
ยทP ๐ข) โ P) |
27 | 24, 25, 26 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(๐ฅ
ยทP ๐ข) โ P) |
28 | | simp1r 1022 |
. . . . . . 7
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
๐ฆ โ
P) |
29 | | simp3r 1026 |
. . . . . . 7
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
๐ฃ โ
P) |
30 | | mulclpr 7571 |
. . . . . . 7
โข ((๐ฆ โ P โง
๐ฃ โ P)
โ (๐ฆ
ยทP ๐ฃ) โ P) |
31 | 28, 29, 30 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(๐ฆ
ยทP ๐ฃ) โ P) |
32 | | addclpr 7536 |
. . . . . 6
โข (((๐ฅ
ยทP ๐ข) โ P โง (๐ฆ
ยทP ๐ฃ) โ P) โ ((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)) โ P) |
33 | 27, 31, 32 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)) โ P) |
34 | | mulclpr 7571 |
. . . . . . 7
โข ((๐ฅ โ P โง
๐ฃ โ P)
โ (๐ฅ
ยทP ๐ฃ) โ P) |
35 | 24, 29, 34 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(๐ฅ
ยทP ๐ฃ) โ P) |
36 | | mulclpr 7571 |
. . . . . . 7
โข ((๐ฆ โ P โง
๐ข โ P)
โ (๐ฆ
ยทP ๐ข) โ P) |
37 | 28, 25, 36 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(๐ฆ
ยทP ๐ข) โ P) |
38 | | addclpr 7536 |
. . . . . 6
โข (((๐ฅ
ยทP ๐ฃ) โ P โง (๐ฆ
ยทP ๐ข) โ P) โ ((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข)) โ P) |
39 | 35, 37, 38 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข)) โ P) |
40 | | simp2l 1023 |
. . . . . . 7
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
๐ง โ
P) |
41 | | mulclpr 7571 |
. . . . . . 7
โข ((๐ง โ P โง
๐ข โ P)
โ (๐ง
ยทP ๐ข) โ P) |
42 | 40, 25, 41 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(๐ง
ยทP ๐ข) โ P) |
43 | | simp2r 1024 |
. . . . . . 7
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
๐ค โ
P) |
44 | | mulclpr 7571 |
. . . . . . 7
โข ((๐ค โ P โง
๐ฃ โ P)
โ (๐ค
ยทP ๐ฃ) โ P) |
45 | 43, 29, 44 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(๐ค
ยทP ๐ฃ) โ P) |
46 | | addclpr 7536 |
. . . . . 6
โข (((๐ง
ยทP ๐ข) โ P โง (๐ค
ยทP ๐ฃ) โ P) โ ((๐ง
ยทP ๐ข) +P (๐ค
ยทP ๐ฃ)) โ P) |
47 | 42, 45, 46 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
((๐ง
ยทP ๐ข) +P (๐ค
ยทP ๐ฃ)) โ P) |
48 | | mulclpr 7571 |
. . . . . . 7
โข ((๐ง โ P โง
๐ฃ โ P)
โ (๐ง
ยทP ๐ฃ) โ P) |
49 | 40, 29, 48 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(๐ง
ยทP ๐ฃ) โ P) |
50 | | mulclpr 7571 |
. . . . . . 7
โข ((๐ค โ P โง
๐ข โ P)
โ (๐ค
ยทP ๐ข) โ P) |
51 | 43, 25, 50 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(๐ค
ยทP ๐ข) โ P) |
52 | | addclpr 7536 |
. . . . . 6
โข (((๐ง
ยทP ๐ฃ) โ P โง (๐ค
ยทP ๐ข) โ P) โ ((๐ง
ยทP ๐ฃ) +P (๐ค
ยทP ๐ข)) โ P) |
53 | 49, 51, 52 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
((๐ง
ยทP ๐ฃ) +P (๐ค
ยทP ๐ข)) โ P) |
54 | | ltsrprg 7746 |
. . . . 5
โข
(((((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)) โ P โง ((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข)) โ P) โง (((๐ง
ยทP ๐ข) +P (๐ค
ยทP ๐ฃ)) โ P โง ((๐ง
ยทP ๐ฃ) +P (๐ค
ยทP ๐ข)) โ P)) โ
([โจ((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)), ((๐ฅ ยทP ๐ฃ) +P
(๐ฆ
ยทP ๐ข))โฉ] ~R
<R [โจ((๐ง ยทP ๐ข) +P
(๐ค
ยทP ๐ฃ)), ((๐ง ยทP ๐ฃ) +P
(๐ค
ยทP ๐ข))โฉ] ~R โ
(((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)) +P ((๐ง
ยทP ๐ฃ) +P (๐ค
ยทP ๐ข)))<P (((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข)) +P ((๐ง
ยทP ๐ข) +P (๐ค
ยทP ๐ฃ))))) |
55 | 33, 39, 47, 53, 54 | syl22anc 1239 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
([โจ((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)), ((๐ฅ ยทP ๐ฃ) +P
(๐ฆ
ยทP ๐ข))โฉ] ~R
<R [โจ((๐ง ยทP ๐ข) +P
(๐ค
ยทP ๐ฃ)), ((๐ง ยทP ๐ฃ) +P
(๐ค
ยทP ๐ข))โฉ] ~R โ
(((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)) +P ((๐ง
ยทP ๐ฃ) +P (๐ค
ยทP ๐ข)))<P (((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข)) +P ((๐ง
ยทP ๐ข) +P (๐ค
ยทP ๐ฃ))))) |
56 | 23, 55 | bitrd 188 |
. . 3
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(([โจ๐ฅ, ๐ฆโฉ]
~R ยทR [โจ๐ข, ๐ฃโฉ] ~R )
<R ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) โ
(((๐ฅ
ยทP ๐ข) +P (๐ฆ
ยทP ๐ฃ)) +P ((๐ง
ยทP ๐ฃ) +P (๐ค
ยทP ๐ข)))<P (((๐ฅ
ยทP ๐ฃ) +P (๐ฆ
ยทP ๐ข)) +P ((๐ง
ยทP ๐ข) +P (๐ค
ยทP ๐ฃ))))) |
57 | | ltsrprg 7746 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ ([โจ๐ฅ, ๐ฆโฉ] ~R
<R [โจ๐ง, ๐คโฉ] ~R โ
(๐ฅ
+P ๐ค)<P (๐ฆ +P
๐ง))) |
58 | 57 | 3adant3 1017 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
([โจ๐ฅ, ๐ฆโฉ]
~R <R [โจ๐ง, ๐คโฉ] ~R โ
(๐ฅ
+P ๐ค)<P (๐ฆ +P
๐ง))) |
59 | | ltsrprg 7746 |
. . . . . 6
โข (((๐ง โ P โง
๐ค โ P)
โง (๐ฅ โ
P โง ๐ฆ
โ P)) โ ([โจ๐ง, ๐คโฉ] ~R
<R [โจ๐ฅ, ๐ฆโฉ] ~R โ
(๐ง
+P ๐ฆ)<P (๐ค +P
๐ฅ))) |
60 | 59 | ancoms 268 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ ([โจ๐ง, ๐คโฉ] ~R
<R [โจ๐ฅ, ๐ฆโฉ] ~R โ
(๐ง
+P ๐ฆ)<P (๐ค +P
๐ฅ))) |
61 | 60 | 3adant3 1017 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
([โจ๐ง, ๐คโฉ]
~R <R [โจ๐ฅ, ๐ฆโฉ] ~R โ
(๐ง
+P ๐ฆ)<P (๐ค +P
๐ฅ))) |
62 | 58, 61 | orbi12d 793 |
. . 3
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(([โจ๐ฅ, ๐ฆโฉ]
~R <R [โจ๐ง, ๐คโฉ] ~R โจ
[โจ๐ง, ๐คโฉ]
~R <R [โจ๐ฅ, ๐ฆโฉ] ~R ) โ
((๐ฅ
+P ๐ค)<P (๐ฆ +P
๐ง) โจ (๐ง +P ๐ฆ)<P
(๐ค
+P ๐ฅ)))) |
63 | 18, 56, 62 | 3imtr4d 203 |
. 2
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P) โง (๐ข โ P โง ๐ฃ โ P)) โ
(([โจ๐ฅ, ๐ฆโฉ]
~R ยทR [โจ๐ข, ๐ฃโฉ] ~R )
<R ([โจ๐ง, ๐คโฉ] ~R
ยทR [โจ๐ข, ๐ฃโฉ] ~R ) โ
([โจ๐ฅ, ๐ฆโฉ]
~R <R [โจ๐ง, ๐คโฉ] ~R โจ
[โจ๐ง, ๐คโฉ]
~R <R [โจ๐ฅ, ๐ฆโฉ] ~R
))) |
64 | 1, 7, 13, 17, 63 | 3ecoptocl 6624 |
1
โข ((๐ด โ R โง
๐ต โ R
โง ๐ถ โ
R) โ ((๐ด
ยทR ๐ถ) <R (๐ต
ยทR ๐ถ) โ (๐ด <R ๐ต โจ ๐ต <R ๐ด))) |