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 | | mulclpi 7326 |
. . . . . . . 8
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) โ N) |
15 | 14 | adantl 277 |
. . . . . . 7
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N)) โ (๐
ยทN ๐) โ N) |
16 | | simp1l 1021 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ฅ โ
N) |
17 | | simp2r 1024 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ค โ
N) |
18 | 15, 16, 17 | caovcld 6027 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฅ
ยทN ๐ค) โ N) |
19 | | simp1r 1022 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ฆ โ
N) |
20 | | simp2l 1023 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ง โ
N) |
21 | 15, 19, 20 | caovcld 6027 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฆ
ยทN ๐ง) โ N) |
22 | | mulclpi 7326 |
. . . . . . 7
โข ((๐ฃ โ N โง
๐ข โ N)
โ (๐ฃ
ยทN ๐ข) โ N) |
23 | 22 | 3ad2ant3 1020 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฃ
ยทN ๐ข) โ N) |
24 | | ltmpig 7337 |
. . . . . 6
โข (((๐ฅ
ยทN ๐ค) โ N โง (๐ฆ
ยทN ๐ง) โ N โง (๐ฃ
ยทN ๐ข) โ N) โ ((๐ฅ
ยทN ๐ค) <N (๐ฆ
ยทN ๐ง) โ ((๐ฃ ยทN ๐ข)
ยทN (๐ฅ ยทN ๐ค))
<N ((๐ฃ ยทN ๐ข)
ยทN (๐ฆ ยทN ๐ง)))) |
25 | 18, 21, 23, 24 | syl3anc 1238 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฅ
ยทN ๐ค) <N (๐ฆ
ยทN ๐ง) โ ((๐ฃ ยทN ๐ข)
ยทN (๐ฅ ยทN ๐ค))
<N ((๐ฃ ยทN ๐ข)
ยทN (๐ฆ ยทN ๐ง)))) |
26 | | simp3l 1025 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ฃ โ
N) |
27 | | simp3r 1026 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ข โ
N) |
28 | | mulcompig 7329 |
. . . . . . . 8
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) = (๐ ยทN ๐)) |
29 | 28 | adantl 277 |
. . . . . . 7
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N)) โ (๐
ยทN ๐) = (๐ ยทN ๐)) |
30 | | mulasspig 7330 |
. . . . . . . 8
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ ((๐
ยทN ๐) ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
31 | 30 | adantl 277 |
. . . . . . 7
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N โง โ
โ N)) โ ((๐ ยทN ๐)
ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
32 | 26, 16, 27, 29, 31, 17, 15 | caov4d 6058 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฃ
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค)) = ((๐ฃ ยทN ๐ข)
ยทN (๐ฅ ยทN ๐ค))) |
33 | 27, 19, 26, 29, 31, 20, 15 | caov4d 6058 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ฆ) ยทN (๐ฃ
ยทN ๐ง)) = ((๐ข ยทN ๐ฃ)
ยทN (๐ฆ ยทN ๐ง))) |
34 | | mulcompig 7329 |
. . . . . . . . . 10
โข ((๐ข โ N โง
๐ฃ โ N)
โ (๐ข
ยทN ๐ฃ) = (๐ฃ ยทN ๐ข)) |
35 | 34 | oveq1d 5889 |
. . . . . . . . 9
โข ((๐ข โ N โง
๐ฃ โ N)
โ ((๐ข
ยทN ๐ฃ) ยทN (๐ฆ
ยทN ๐ง)) = ((๐ฃ ยทN ๐ข)
ยทN (๐ฆ ยทN ๐ง))) |
36 | 35 | ancoms 268 |
. . . . . . . 8
โข ((๐ฃ โ N โง
๐ข โ N)
โ ((๐ข
ยทN ๐ฃ) ยทN (๐ฆ
ยทN ๐ง)) = ((๐ฃ ยทN ๐ข)
ยทN (๐ฆ ยทN ๐ง))) |
37 | 36 | 3ad2ant3 1020 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ฃ) ยทN (๐ฆ
ยทN ๐ง)) = ((๐ฃ ยทN ๐ข)
ยทN (๐ฆ ยทN ๐ง))) |
38 | 33, 37 | eqtrd 2210 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ข
ยทN ๐ฆ) ยทN (๐ฃ
ยทN ๐ง)) = ((๐ฃ ยทN ๐ข)
ยทN (๐ฆ ยทN ๐ง))) |
39 | 32, 38 | breq12d 4016 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(((๐ฃ
ยทN ๐ฅ) ยทN (๐ข
ยทN ๐ค)) <N ((๐ข
ยทN ๐ฆ) ยทN (๐ฃ
ยทN ๐ง)) โ ((๐ฃ ยทN ๐ข)
ยทN (๐ฅ ยทN ๐ค))
<N ((๐ฃ ยทN ๐ข)
ยทN (๐ฆ ยทN ๐ง)))) |
40 | 25, 39 | bitr4d 191 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฅ
ยทN ๐ค) <N (๐ฆ
ยทN ๐ง) โ ((๐ฃ ยทN ๐ฅ)
ยทN (๐ข ยทN ๐ค))
<N ((๐ข ยทN ๐ฆ)
ยทN (๐ฃ ยทN ๐ง)))) |
41 | | ordpipqqs 7372 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
<Q [โจ๐ง, ๐คโฉ] ~Q โ
(๐ฅ
ยทN ๐ค) <N (๐ฆ
ยทN ๐ง))) |
42 | 41 | 3adant3 1017 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q <Q [โจ๐ง, ๐คโฉ] ~Q โ
(๐ฅ
ยทN ๐ค) <N (๐ฆ
ยทN ๐ง))) |
43 | 15, 26, 16 | caovcld 6027 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฃ
ยทN ๐ฅ) โ N) |
44 | 15, 27, 19 | caovcld 6027 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ข
ยทN ๐ฆ) โ N) |
45 | 15, 26, 20 | caovcld 6027 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฃ
ยทN ๐ง) โ N) |
46 | 15, 27, 17 | caovcld 6027 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ข
ยทN ๐ค) โ N) |
47 | | ordpipqqs 7372 |
. . . . 5
โข ((((๐ฃ
ยทN ๐ฅ) โ N โง (๐ข
ยทN ๐ฆ) โ N) โง ((๐ฃ
ยทN ๐ง) โ N โง (๐ข
ยทN ๐ค) โ N)) โ
([โจ(๐ฃ
ยทN ๐ฅ), (๐ข ยทN ๐ฆ)โฉ]
~Q <Q [โจ(๐ฃ
ยทN ๐ง), (๐ข ยทN ๐ค)โฉ]
~Q โ ((๐ฃ ยทN ๐ฅ)
ยทN (๐ข ยทN ๐ค))
<N ((๐ข ยทN ๐ฆ)
ยทN (๐ฃ ยทN ๐ง)))) |
48 | 43, 44, 45, 46, 47 | syl22anc 1239 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ(๐ฃ
ยทN ๐ฅ), (๐ข ยทN ๐ฆ)โฉ]
~Q <Q [โจ(๐ฃ
ยทN ๐ง), (๐ข ยทN ๐ค)โฉ]
~Q โ ((๐ฃ ยทN ๐ฅ)
ยทN (๐ข ยทN ๐ค))
<N ((๐ข ยทN ๐ฆ)
ยทN (๐ฃ ยทN ๐ง)))) |
49 | 40, 42, 48 | 3bitr4d 220 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q <Q [โจ๐ง, ๐คโฉ] ~Q โ
[โจ(๐ฃ
ยทN ๐ฅ), (๐ข ยทN ๐ฆ)โฉ]
~Q <Q [โจ(๐ฃ
ยทN ๐ง), (๐ข ยทN ๐ค)โฉ]
~Q )) |
50 | | mulpipqqs 7371 |
. . . . . 6
โข (((๐ฃ โ N โง
๐ข โ N)
โง (๐ฅ โ
N โง ๐ฆ
โ N)) โ ([โจ๐ฃ, ๐ขโฉ] ~Q
ยทQ [โจ๐ฅ, ๐ฆโฉ] ~Q ) =
[โจ(๐ฃ
ยทN ๐ฅ), (๐ข ยทN ๐ฆ)โฉ]
~Q ) |
51 | 50 | ancoms 268 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ฃ, ๐ขโฉ] ~Q
ยทQ [โจ๐ฅ, ๐ฆโฉ] ~Q ) =
[โจ(๐ฃ
ยทN ๐ฅ), (๐ข ยทN ๐ฆ)โฉ]
~Q ) |
52 | 51 | 3adant2 1016 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฃ, ๐ขโฉ]
~Q ยทQ [โจ๐ฅ, ๐ฆโฉ] ~Q ) =
[โจ(๐ฃ
ยทN ๐ฅ), (๐ข ยทN ๐ฆ)โฉ]
~Q ) |
53 | | mulpipqqs 7371 |
. . . . . 6
โข (((๐ฃ โ N โง
๐ข โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ([โจ๐ฃ, ๐ขโฉ] ~Q
ยทQ [โจ๐ง, ๐คโฉ] ~Q ) =
[โจ(๐ฃ
ยทN ๐ง), (๐ข ยทN ๐ค)โฉ]
~Q ) |
54 | 53 | ancoms 268 |
. . . . 5
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ฃ, ๐ขโฉ] ~Q
ยทQ [โจ๐ง, ๐คโฉ] ~Q ) =
[โจ(๐ฃ
ยทN ๐ง), (๐ข ยทN ๐ค)โฉ]
~Q ) |
55 | 54 | 3adant1 1015 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฃ, ๐ขโฉ]
~Q ยทQ [โจ๐ง, ๐คโฉ] ~Q ) =
[โจ(๐ฃ
ยทN ๐ง), (๐ข ยทN ๐ค)โฉ]
~Q ) |
56 | 52, 55 | breq12d 4016 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(([โจ๐ฃ, ๐ขโฉ]
~Q ยทQ [โจ๐ฅ, ๐ฆโฉ] ~Q )
<Q ([โจ๐ฃ, ๐ขโฉ] ~Q
ยทQ [โจ๐ง, ๐คโฉ] ~Q ) โ
[โจ(๐ฃ
ยทN ๐ฅ), (๐ข ยทN ๐ฆ)โฉ]
~Q <Q [โจ(๐ฃ
ยทN ๐ง), (๐ข ยทN ๐ค)โฉ]
~Q )) |
57 | 49, 56 | bitr4d 191 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q <Q [โจ๐ง, ๐คโฉ] ~Q โ
([โจ๐ฃ, ๐ขโฉ]
~Q ยทQ [โจ๐ฅ, ๐ฆโฉ] ~Q )
<Q ([โจ๐ฃ, ๐ขโฉ] ~Q
ยทQ [โจ๐ง, ๐คโฉ] ~Q
))) |
58 | 1, 5, 9, 13, 57 | 3ecoptocl 6623 |
1
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
<Q ๐ต โ (๐ถ ยทQ ๐ด) <Q
(๐ถ
ยทQ ๐ต))) |