Step | Hyp | Ref
| Expression |
1 | | enqex 7358 |
. 2
โข
~Q โ V |
2 | | enqer 7356 |
. 2
โข
~Q Er (N ร
N) |
3 | | df-nqqs 7346 |
. 2
โข
Q = ((N ร N) /
~Q ) |
4 | | df-ltnqqs 7351 |
. 2
โข
<Q = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ Q โง ๐ฆ โ Q) โง
โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง
(๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ)))} |
5 | | enqeceq 7357 |
. . . . 5
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โ ([โจ๐ง, ๐คโฉ] ~Q =
[โจ๐ด, ๐ตโฉ] ~Q โ
(๐ง
ยทN ๐ต) = (๐ค ยทN ๐ด))) |
6 | | enqeceq 7357 |
. . . . . 6
โข (((๐ฃ โ N โง
๐ข โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ ([โจ๐ฃ, ๐ขโฉ] ~Q =
[โจ๐ถ, ๐ทโฉ] ~Q โ
(๐ฃ
ยทN ๐ท) = (๐ข ยทN ๐ถ))) |
7 | | eqcom 2179 |
. . . . . 6
โข ((๐ฃ
ยทN ๐ท) = (๐ข ยทN ๐ถ) โ (๐ข ยทN ๐ถ) = (๐ฃ ยทN ๐ท)) |
8 | 6, 7 | bitrdi 196 |
. . . . 5
โข (((๐ฃ โ N โง
๐ข โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ ([โจ๐ฃ, ๐ขโฉ] ~Q =
[โจ๐ถ, ๐ทโฉ] ~Q โ
(๐ข
ยทN ๐ถ) = (๐ฃ ยทN ๐ท))) |
9 | 5, 8 | bi2anan9 606 |
. . . 4
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (([โจ๐ง, ๐คโฉ] ~Q =
[โจ๐ด, ๐ตโฉ] ~Q โง
[โจ๐ฃ, ๐ขโฉ]
~Q = [โจ๐ถ, ๐ทโฉ] ~Q ) โ
((๐ง
ยทN ๐ต) = (๐ค ยทN ๐ด) โง (๐ข ยทN ๐ถ) = (๐ฃ ยทN ๐ท)))) |
10 | | oveq12 5883 |
. . . . 5
โข (((๐ง
ยทN ๐ต) = (๐ค ยทN ๐ด) โง (๐ข ยทN ๐ถ) = (๐ฃ ยทN ๐ท)) โ ((๐ง ยทN ๐ต)
ยทN (๐ข ยทN ๐ถ)) = ((๐ค ยทN ๐ด)
ยทN (๐ฃ ยทN ๐ท))) |
11 | | simplll 533 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ๐ง
โ N) |
12 | | simprlr 538 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ๐ข
โ N) |
13 | | simplrr 536 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ๐ต
โ N) |
14 | | mulcompig 7329 |
. . . . . . . 8
โข ((๐ฅ โ N โง
๐ฆ โ N)
โ (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ)) |
15 | 14 | adantl 277 |
. . . . . . 7
โข
(((((๐ง โ
N โง ๐ค
โ N) โง (๐ด โ N โง ๐ต โ N)) โง
((๐ฃ โ N
โง ๐ข โ
N) โง (๐ถ
โ N โง ๐ท โ N))) โง (๐ฅ โ N โง
๐ฆ โ N))
โ (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ)) |
16 | | mulasspig 7330 |
. . . . . . . 8
โข ((๐ฅ โ N โง
๐ฆ โ N
โง ๐ โ
N) โ ((๐ฅ
ยทN ๐ฆ) ยทN ๐) = (๐ฅ ยทN (๐ฆ
ยทN ๐))) |
17 | 16 | adantl 277 |
. . . . . . 7
โข
(((((๐ง โ
N โง ๐ค
โ N) โง (๐ด โ N โง ๐ต โ N)) โง
((๐ฃ โ N
โง ๐ข โ
N) โง (๐ถ
โ N โง ๐ท โ N))) โง (๐ฅ โ N โง
๐ฆ โ N
โง ๐ โ
N)) โ ((๐ฅ ยทN ๐ฆ)
ยทN ๐) = (๐ฅ ยทN (๐ฆ
ยทN ๐))) |
18 | | simprrl 539 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ๐ถ
โ N) |
19 | | mulclpi 7326 |
. . . . . . . 8
โข ((๐ฅ โ N โง
๐ฆ โ N)
โ (๐ฅ
ยทN ๐ฆ) โ N) |
20 | 19 | adantl 277 |
. . . . . . 7
โข
(((((๐ง โ
N โง ๐ค
โ N) โง (๐ด โ N โง ๐ต โ N)) โง
((๐ฃ โ N
โง ๐ข โ
N) โง (๐ถ
โ N โง ๐ท โ N))) โง (๐ฅ โ N โง
๐ฆ โ N))
โ (๐ฅ
ยทN ๐ฆ) โ N) |
21 | 11, 12, 13, 15, 17, 18, 20 | caov4d 6058 |
. . . . . 6
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ((๐ง ยทN ๐ข)
ยทN (๐ต ยทN ๐ถ)) = ((๐ง ยทN ๐ต)
ยทN (๐ข ยทN ๐ถ))) |
22 | | simpllr 534 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ๐ค
โ N) |
23 | | simprll 537 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ๐ฃ
โ N) |
24 | | simplrl 535 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ๐ด
โ N) |
25 | | simprrr 540 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ๐ท
โ N) |
26 | 22, 23, 24, 15, 17, 25, 20 | caov4d 6058 |
. . . . . 6
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ ((๐ค ยทN ๐ฃ)
ยทN (๐ด ยทN ๐ท)) = ((๐ค ยทN ๐ด)
ยทN (๐ฃ ยทN ๐ท))) |
27 | 21, 26 | eqeq12d 2192 |
. . . . 5
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (((๐ง ยทN ๐ข)
ยทN (๐ต ยทN ๐ถ)) = ((๐ค ยทN ๐ฃ)
ยทN (๐ด ยทN ๐ท)) โ ((๐ง ยทN ๐ต)
ยทN (๐ข ยทN ๐ถ)) = ((๐ค ยทN ๐ด)
ยทN (๐ฃ ยทN ๐ท)))) |
28 | 10, 27 | imbitrrid 156 |
. . . 4
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (((๐ง ยทN ๐ต) = (๐ค ยทN ๐ด) โง (๐ข ยทN ๐ถ) = (๐ฃ ยทN ๐ท)) โ ((๐ง ยทN ๐ข)
ยทN (๐ต ยทN ๐ถ)) = ((๐ค ยทN ๐ฃ)
ยทN (๐ด ยทN ๐ท)))) |
29 | 9, 28 | sylbid 150 |
. . 3
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (([โจ๐ง, ๐คโฉ] ~Q =
[โจ๐ด, ๐ตโฉ] ~Q โง
[โจ๐ฃ, ๐ขโฉ]
~Q = [โจ๐ถ, ๐ทโฉ] ~Q ) โ
((๐ง
ยทN ๐ข) ยทN (๐ต
ยทN ๐ถ)) = ((๐ค ยทN ๐ฃ)
ยทN (๐ด ยทN ๐ท)))) |
30 | | ltmpig 7337 |
. . . . 5
โข ((๐ฅ โ N โง
๐ฆ โ N
โง ๐ โ
N) โ (๐ฅ
<N ๐ฆ โ (๐ ยทN ๐ฅ) <N
(๐
ยทN ๐ฆ))) |
31 | 30 | adantl 277 |
. . . 4
โข
(((((๐ง โ
N โง ๐ค
โ N) โง (๐ด โ N โง ๐ต โ N)) โง
((๐ฃ โ N
โง ๐ข โ
N) โง (๐ถ
โ N โง ๐ท โ N))) โง (๐ฅ โ N โง
๐ฆ โ N
โง ๐ โ
N)) โ (๐ฅ
<N ๐ฆ โ (๐ ยทN ๐ฅ) <N
(๐
ยทN ๐ฆ))) |
32 | 20, 11, 12 | caovcld 6027 |
. . . 4
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (๐ง ยทN ๐ข) โ
N) |
33 | 20, 13, 18 | caovcld 6027 |
. . . 4
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (๐ต ยทN ๐ถ) โ
N) |
34 | 20, 22, 23 | caovcld 6027 |
. . . 4
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (๐ค ยทN ๐ฃ) โ
N) |
35 | 20, 24, 25 | caovcld 6027 |
. . . 4
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (๐ด ยทN ๐ท) โ
N) |
36 | 31, 32, 33, 34, 15, 35 | caovord3d 6044 |
. . 3
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (((๐ง ยทN ๐ข)
ยทN (๐ต ยทN ๐ถ)) = ((๐ค ยทN ๐ฃ)
ยทN (๐ด ยทN ๐ท)) โ ((๐ง ยทN ๐ข) <N
(๐ค
ยทN ๐ฃ) โ (๐ด ยทN ๐ท) <N
(๐ต
ยทN ๐ถ)))) |
37 | 29, 36 | syld 45 |
. 2
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ด โ
N โง ๐ต
โ N)) โง ((๐ฃ โ N โง ๐ข โ N) โง
(๐ถ โ N
โง ๐ท โ
N))) โ (([โจ๐ง, ๐คโฉ] ~Q =
[โจ๐ด, ๐ตโฉ] ~Q โง
[โจ๐ฃ, ๐ขโฉ]
~Q = [โจ๐ถ, ๐ทโฉ] ~Q ) โ
((๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ) โ (๐ด ยทN ๐ท) <N
(๐ต
ยทN ๐ถ)))) |
38 | 1, 2, 3, 4, 37 | brecop 6624 |
1
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ ([โจ๐ด, ๐ตโฉ] ~Q
<Q [โจ๐ถ, ๐ทโฉ] ~Q โ
(๐ด
ยทN ๐ท) <N (๐ต
ยทN ๐ถ))) |