Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7346 |
. 2
โข
Q = ((N ร N) /
~Q ) |
2 | | breq1 4006 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
<Q [โจ๐ง, ๐คโฉ] ~Q โ
๐ด
<Q [โจ๐ง, ๐คโฉ] ~Q
)) |
3 | | oveq2 5882 |
. . . 4
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q = ๐ด โ ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q [โจ๐ฅ, ๐ฆโฉ] ~Q ) =
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ด)) |
4 | 3 | breq1d 4013 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q = ๐ด โ (([โจ๐ฃ, ๐ขโฉ] ~Q
+Q [โจ๐ฅ, ๐ฆโฉ] ~Q )
<Q ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q ) โ
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ด) <Q
([โจ๐ฃ, ๐ขโฉ]
~Q +Q [โจ๐ง, ๐คโฉ] ~Q
))) |
5 | 2, 4 | bibi12d 235 |
. 2
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~Q
<Q [โจ๐ง, ๐คโฉ] ~Q โ
([โจ๐ฃ, ๐ขโฉ]
~Q +Q [โจ๐ฅ, ๐ฆโฉ] ~Q )
<Q ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q )) โ
(๐ด
<Q [โจ๐ง, ๐คโฉ] ~Q โ
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ด) <Q
([โจ๐ฃ, ๐ขโฉ]
~Q +Q [โจ๐ง, ๐คโฉ] ~Q
)))) |
6 | | breq2 4007 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~Q = ๐ต โ (๐ด <Q [โจ๐ง, ๐คโฉ] ~Q โ
๐ด
<Q ๐ต)) |
7 | | oveq2 5882 |
. . . 4
โข
([โจ๐ง, ๐คโฉ]
~Q = ๐ต โ ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q ) =
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ต)) |
8 | 7 | breq2d 4015 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~Q = ๐ต โ (([โจ๐ฃ, ๐ขโฉ] ~Q
+Q ๐ด) <Q
([โจ๐ฃ, ๐ขโฉ]
~Q +Q [โจ๐ง, ๐คโฉ] ~Q ) โ
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ด) <Q
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ต))) |
9 | 6, 8 | bibi12d 235 |
. 2
โข
([โจ๐ง, ๐คโฉ]
~Q = ๐ต โ ((๐ด <Q [โจ๐ง, ๐คโฉ] ~Q โ
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ด) <Q
([โจ๐ฃ, ๐ขโฉ]
~Q +Q [โจ๐ง, ๐คโฉ] ~Q )) โ
(๐ด
<Q ๐ต โ ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q ๐ด) <Q
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ต)))) |
10 | | oveq1 5881 |
. . . 4
โข
([โจ๐ฃ, ๐ขโฉ]
~Q = ๐ถ โ ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q ๐ด) = (๐ถ +Q ๐ด)) |
11 | | oveq1 5881 |
. . . 4
โข
([โจ๐ฃ, ๐ขโฉ]
~Q = ๐ถ โ ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q ๐ต) = (๐ถ +Q ๐ต)) |
12 | 10, 11 | breq12d 4016 |
. . 3
โข
([โจ๐ฃ, ๐ขโฉ]
~Q = ๐ถ โ (([โจ๐ฃ, ๐ขโฉ] ~Q
+Q ๐ด) <Q
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ต) โ (๐ถ +Q ๐ด) <Q
(๐ถ
+Q ๐ต))) |
13 | 12 | bibi2d 232 |
. 2
โข
([โจ๐ฃ, ๐ขโฉ]
~Q = ๐ถ โ ((๐ด <Q ๐ต โ ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q ๐ด) <Q
([โจ๐ฃ, ๐ขโฉ]
~Q +Q ๐ต)) โ (๐ด <Q ๐ต โ (๐ถ +Q ๐ด) <Q
(๐ถ
+Q ๐ต)))) |
14 | | addclpi 7325 |
. . . . . 6
โข ((๐ โ N โง
๐ โ N)
โ (๐
+N ๐) โ N) |
15 | 14 | adantl 277 |
. . . . 5
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N)) โ (๐
+N ๐) โ N) |
16 | | simp3l 1025 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ฃ โ
N) |
17 | | simp1r 1022 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ฆ โ
N) |
18 | | mulclpi 7326 |
. . . . . 6
โข ((๐ฃ โ N โง
๐ฆ โ N)
โ (๐ฃ
ยทN ๐ฆ) โ N) |
19 | 16, 17, 18 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฃ
ยทN ๐ฆ) โ N) |
20 | | simp3r 1026 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ข โ
N) |
21 | | simp1l 1021 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ฅ โ
N) |
22 | | mulclpi 7326 |
. . . . . 6
โข ((๐ข โ N โง
๐ฅ โ N)
โ (๐ข
ยทN ๐ฅ) โ N) |
23 | 20, 21, 22 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ข
ยทN ๐ฅ) โ N) |
24 | 15, 19, 23 | caovcld 6027 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)) โ N) |
25 | | mulclpi 7326 |
. . . . 5
โข ((๐ข โ N โง
๐ฆ โ N)
โ (๐ข
ยทN ๐ฆ) โ N) |
26 | 20, 17, 25 | syl2anc 411 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ข
ยทN ๐ฆ) โ N) |
27 | | mulclpi 7326 |
. . . . . . 7
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) โ N) |
28 | 27 | adantl 277 |
. . . . . 6
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N)) โ (๐
ยทN ๐) โ N) |
29 | | simp2r 1024 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ค โ
N) |
30 | 28, 16, 29 | caovcld 6027 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฃ
ยทN ๐ค) โ N) |
31 | | simp2l 1023 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ง โ
N) |
32 | | mulclpi 7326 |
. . . . . 6
โข ((๐ข โ N โง
๐ง โ N)
โ (๐ข
ยทN ๐ง) โ N) |
33 | 20, 31, 32 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ข
ยทN ๐ง) โ N) |
34 | 15, 30, 33 | caovcld 6027 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง)) โ N) |
35 | | mulclpi 7326 |
. . . . 5
โข ((๐ข โ N โง
๐ค โ N)
โ (๐ข
ยทN ๐ค) โ N) |
36 | 20, 29, 35 | syl2anc 411 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ข
ยทN ๐ค) โ N) |
37 | | ordpipqqs 7372 |
. . . 4
โข
(((((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)) โ N โง (๐ข
ยทN ๐ฆ) โ N) โง (((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง)) โ N โง (๐ข
ยทN ๐ค) โ N)) โ
([โจ((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)), (๐ข ยทN ๐ฆ)โฉ]
~Q <Q [โจ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง)), (๐ข ยทN ๐ค)โฉ]
~Q โ (((๐ฃ ยทN ๐ฆ) +N
(๐ข
ยทN ๐ฅ)) ยทN (๐ข
ยทN ๐ค)) <N ((๐ข
ยทN ๐ฆ) ยทN ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง))))) |
38 | 24, 26, 34, 36, 37 | syl22anc 1239 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)), (๐ข ยทN ๐ฆ)โฉ]
~Q <Q [โจ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง)), (๐ข ยทN ๐ค)โฉ]
~Q โ (((๐ฃ ยทN ๐ฆ) +N
(๐ข
ยทN ๐ฅ)) ยทN (๐ข
ยทN ๐ค)) <N ((๐ข
ยทN ๐ฆ) ยทN ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง))))) |
39 | | simp3 999 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฃ โ N
โง ๐ข โ
N)) |
40 | | simp1 997 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฅ โ N
โง ๐ฆ โ
N)) |
41 | | addpipqqs 7368 |
. . . . 5
โข (((๐ฃ โ N โง
๐ข โ N)
โง (๐ฅ โ
N โง ๐ฆ
โ N)) โ ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q [โจ๐ฅ, ๐ฆโฉ] ~Q ) =
[โจ((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)), (๐ข ยทN ๐ฆ)โฉ]
~Q ) |
42 | 39, 40, 41 | syl2anc 411 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฃ, ๐ขโฉ]
~Q +Q [โจ๐ฅ, ๐ฆโฉ] ~Q ) =
[โจ((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)), (๐ข ยทN ๐ฆ)โฉ]
~Q ) |
43 | | simp2 998 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ง โ N
โง ๐ค โ
N)) |
44 | | addpipqqs 7368 |
. . . . 5
โข (((๐ฃ โ N โง
๐ข โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q ) =
[โจ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง)), (๐ข ยทN ๐ค)โฉ]
~Q ) |
45 | 39, 43, 44 | syl2anc 411 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฃ, ๐ขโฉ]
~Q +Q [โจ๐ง, ๐คโฉ] ~Q ) =
[โจ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง)), (๐ข ยทN ๐ค)โฉ]
~Q ) |
46 | 42, 45 | breq12d 4016 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(([โจ๐ฃ, ๐ขโฉ]
~Q +Q [โจ๐ฅ, ๐ฆโฉ] ~Q )
<Q ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q ) โ
[โจ((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)), (๐ข ยทN ๐ฆ)โฉ]
~Q <Q [โจ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง)), (๐ข ยทN ๐ค)โฉ]
~Q )) |
47 | | ordpipqqs 7372 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
<Q [โจ๐ง, ๐คโฉ] ~Q โ
(๐ฅ
ยทN ๐ค) <N (๐ฆ
ยทN ๐ง))) |
48 | 47 | 3adant3 1017 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q <Q [โจ๐ง, ๐คโฉ] ~Q โ
(๐ฅ
ยทN ๐ค) <N (๐ฆ
ยทN ๐ง))) |
49 | | mulclpi 7326 |
. . . . . 6
โข ((๐ฅ โ N โง
๐ค โ N)
โ (๐ฅ
ยทN ๐ค) โ N) |
50 | 21, 29, 49 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฅ
ยทN ๐ค) โ N) |
51 | | mulclpi 7326 |
. . . . . 6
โข ((๐ฆ โ N โง
๐ง โ N)
โ (๐ฆ
ยทN ๐ง) โ N) |
52 | 17, 31, 51 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฆ
ยทN ๐ง) โ N) |
53 | | mulclpi 7326 |
. . . . . 6
โข ((๐ข โ N โง
๐ข โ N)
โ (๐ข
ยทN ๐ข) โ N) |
54 | 20, 20, 53 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ข
ยทN ๐ข) โ N) |
55 | | ltmpig 7337 |
. . . . 5
โข (((๐ฅ
ยทN ๐ค) โ N โง (๐ฆ
ยทN ๐ง) โ N โง (๐ข
ยทN ๐ข) โ N) โ ((๐ฅ
ยทN ๐ค) <N (๐ฆ
ยทN ๐ง) โ ((๐ข ยทN ๐ข)
ยทN (๐ฅ ยทN ๐ค))
<N ((๐ข ยทN ๐ข)
ยทN (๐ฆ ยทN ๐ง)))) |
56 | 50, 52, 54, 55 | syl3anc 1238 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฅ
ยทN ๐ค) <N (๐ฆ
ยทN ๐ง) โ ((๐ข ยทN ๐ข)
ยทN (๐ฅ ยทN ๐ค))
<N ((๐ข ยทN ๐ข)
ยทN (๐ฆ ยทN ๐ง)))) |
57 | | mulclpi 7326 |
. . . . . . 7
โข (((๐ข
ยทN ๐ฅ) โ N โง (๐ข
ยทN ๐ค) โ N) โ ((๐ข
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค)) โ N) |
58 | 23, 36, 57 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค)) โ N) |
59 | | mulclpi 7326 |
. . . . . . 7
โข (((๐ข
ยทN ๐ฆ) โ N โง (๐ข
ยทN ๐ง) โ N) โ ((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง)) โ N) |
60 | 26, 33, 59 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง)) โ N) |
61 | | mulclpi 7326 |
. . . . . . 7
โข (((๐ฃ
ยทN ๐ฆ) โ N โง (๐ข
ยทN ๐ค) โ N) โ ((๐ฃ
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ค)) โ N) |
62 | 19, 36, 61 | syl2anc 411 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฃ
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ค)) โ N) |
63 | | ltapig 7336 |
. . . . . 6
โข ((((๐ข
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค)) โ N โง ((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง)) โ N โง ((๐ฃ
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ค)) โ N) โ (((๐ข
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค)) <N ((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง)) โ (((๐ฃ ยทN ๐ฆ)
ยทN (๐ข ยทN ๐ค)) +N
((๐ข
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค))) <N (((๐ฃ
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ค)) +N ((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง))))) |
64 | 58, 60, 62, 63 | syl3anc 1238 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(((๐ข
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค)) <N ((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง)) โ (((๐ฃ ยทN ๐ฆ)
ยทN (๐ข ยทN ๐ค)) +N
((๐ข
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค))) <N (((๐ฃ
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ค)) +N ((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง))))) |
65 | | mulcompig 7329 |
. . . . . . . 8
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) = (๐ ยทN ๐)) |
66 | 65 | adantl 277 |
. . . . . . 7
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N)) โ (๐
ยทN ๐) = (๐ ยทN ๐)) |
67 | | mulasspig 7330 |
. . . . . . . 8
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ ((๐
ยทN ๐) ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
68 | 67 | adantl 277 |
. . . . . . 7
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N โง โ
โ N)) โ ((๐ ยทN ๐)
ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
69 | 20, 20, 21, 66, 68, 29, 28 | caov4d 6058 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ข) ยทN (๐ฅ
ยทN ๐ค)) = ((๐ข ยทN ๐ฅ)
ยทN (๐ข ยทN ๐ค))) |
70 | 20, 20, 17, 66, 68, 31, 28 | caov4d 6058 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ข) ยทN (๐ฆ
ยทN ๐ง)) = ((๐ข ยทN ๐ฆ)
ยทN (๐ข ยทN ๐ง))) |
71 | 69, 70 | breq12d 4016 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(((๐ข
ยทN ๐ข) ยทN (๐ฅ
ยทN ๐ค)) <N ((๐ข
ยทN ๐ข) ยทN (๐ฆ
ยทN ๐ง)) โ ((๐ข ยทN ๐ฅ)
ยทN (๐ข ยทN ๐ค))
<N ((๐ข ยทN ๐ฆ)
ยทN (๐ข ยทN ๐ง)))) |
72 | | distrpig 7331 |
. . . . . . . 8
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ (๐
ยทN (๐ +N โ)) = ((๐ ยทN ๐) +N
(๐
ยทN โ))) |
73 | 72 | adantl 277 |
. . . . . . 7
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N โง โ
โ N)) โ (๐ ยทN (๐ +N
โ)) = ((๐ ยทN ๐) +N
(๐
ยทN โ))) |
74 | 73, 19, 23, 36, 15, 66 | caovdir2d 6050 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)) ยทN (๐ข
ยทN ๐ค)) = (((๐ฃ ยทN ๐ฆ)
ยทN (๐ข ยทN ๐ค)) +N
((๐ข
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค)))) |
75 | 73, 26, 30, 33 | caovdid 6049 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ฆ) ยทN ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง))) = (((๐ข ยทN ๐ฆ)
ยทN (๐ฃ ยทN ๐ค)) +N
((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง)))) |
76 | 20, 17, 16, 66, 68, 29, 28 | caov411d 6059 |
. . . . . . . 8
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ฆ) ยทN (๐ฃ
ยทN ๐ค)) = ((๐ฃ ยทN ๐ฆ)
ยทN (๐ข ยทN ๐ค))) |
77 | 76 | oveq1d 5889 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(((๐ข
ยทN ๐ฆ) ยทN (๐ฃ
ยทN ๐ค)) +N ((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง))) = (((๐ฃ ยทN ๐ฆ)
ยทN (๐ข ยทN ๐ค)) +N
((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง)))) |
78 | 75, 77 | eqtrd 2210 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ฆ) ยทN ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง))) = (((๐ฃ ยทN ๐ฆ)
ยทN (๐ข ยทN ๐ค)) +N
((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง)))) |
79 | 74, 78 | breq12d 4016 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)) ยทN (๐ข
ยทN ๐ค)) <N ((๐ข
ยทN ๐ฆ) ยทN ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง))) โ (((๐ฃ ยทN ๐ฆ)
ยทN (๐ข ยทN ๐ค)) +N
((๐ข
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค))) <N (((๐ฃ
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ค)) +N ((๐ข
ยทN ๐ฆ) ยทN (๐ข
ยทN ๐ง))))) |
80 | 64, 71, 79 | 3bitr4d 220 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(((๐ข
ยทN ๐ข) ยทN (๐ฅ
ยทN ๐ค)) <N ((๐ข
ยทN ๐ข) ยทN (๐ฆ
ยทN ๐ง)) โ (((๐ฃ ยทN ๐ฆ) +N
(๐ข
ยทN ๐ฅ)) ยทN (๐ข
ยทN ๐ค)) <N ((๐ข
ยทN ๐ฆ) ยทN ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง))))) |
81 | 48, 56, 80 | 3bitrd 214 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q <Q [โจ๐ง, ๐คโฉ] ~Q โ
(((๐ฃ
ยทN ๐ฆ) +N (๐ข
ยทN ๐ฅ)) ยทN (๐ข
ยทN ๐ค)) <N ((๐ข
ยทN ๐ฆ) ยทN ((๐ฃ
ยทN ๐ค) +N (๐ข
ยทN ๐ง))))) |
82 | 38, 46, 81 | 3bitr4rd 221 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q <Q [โจ๐ง, ๐คโฉ] ~Q โ
([โจ๐ฃ, ๐ขโฉ]
~Q +Q [โจ๐ฅ, ๐ฆโฉ] ~Q )
<Q ([โจ๐ฃ, ๐ขโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q
))) |
83 | 1, 5, 9, 13, 82 | 3ecoptocl 6623 |
1
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
<Q ๐ต โ (๐ถ +Q ๐ด) <Q
(๐ถ
+Q ๐ต))) |