Step | Hyp | Ref
| Expression |
1 | | mulnqf 10892 |
. . 3
โข
ยทQ :(Q ร
Q)โถQ |
2 | 1 | fdmi 6685 |
. 2
โข dom
ยทQ = (Q ร
Q) |
3 | | ltrelnq 10869 |
. 2
โข
<Q โ (Q ร
Q) |
4 | | 0nnq 10867 |
. 2
โข ยฌ
โ
โ Q |
5 | | elpqn 10868 |
. . . . . . . . . 10
โข (๐ถ โ Q โ
๐ถ โ (N
ร N)) |
6 | 5 | 3ad2ant3 1136 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ถ
โ (N ร N)) |
7 | | xp1st 7958 |
. . . . . . . . 9
โข (๐ถ โ (N ร
N) โ (1st โ๐ถ) โ N) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (1st โ๐ถ) โ N) |
9 | | xp2nd 7959 |
. . . . . . . . 9
โข (๐ถ โ (N ร
N) โ (2nd โ๐ถ) โ N) |
10 | 6, 9 | syl 17 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (2nd โ๐ถ) โ N) |
11 | | mulclpi 10836 |
. . . . . . . 8
โข
(((1st โ๐ถ) โ N โง
(2nd โ๐ถ)
โ N) โ ((1st โ๐ถ) ยทN
(2nd โ๐ถ))
โ N) |
12 | 8, 10, 11 | syl2anc 585 |
. . . . . . 7
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((1st โ๐ถ) ยทN
(2nd โ๐ถ))
โ N) |
13 | | ltmpi 10847 |
. . . . . . 7
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ถ))
โ N โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ (((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
<N (((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด))))) |
14 | 12, 13 | syl 17 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ (((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
<N (((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด))))) |
15 | | fvex 6860 |
. . . . . . . 8
โข
(1st โ๐ถ) โ V |
16 | | fvex 6860 |
. . . . . . . 8
โข
(2nd โ๐ถ) โ V |
17 | | fvex 6860 |
. . . . . . . 8
โข
(1st โ๐ด) โ V |
18 | | mulcompi 10839 |
. . . . . . . 8
โข (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ) |
19 | | mulasspi 10840 |
. . . . . . . 8
โข ((๐ฅ
ยทN ๐ฆ) ยทN ๐ง) = (๐ฅ ยทN (๐ฆ
ยทN ๐ง)) |
20 | | fvex 6860 |
. . . . . . . 8
โข
(2nd โ๐ต) โ V |
21 | 15, 16, 17, 18, 19, 20 | caov4 7590 |
. . . . . . 7
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
= (((1st โ๐ถ) ยทN
(1st โ๐ด))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ต))) |
22 | | fvex 6860 |
. . . . . . . 8
โข
(1st โ๐ต) โ V |
23 | | fvex 6860 |
. . . . . . . 8
โข
(2nd โ๐ด) โ V |
24 | 15, 16, 22, 18, 19, 23 | caov4 7590 |
. . . . . . 7
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
= (((1st โ๐ถ) ยทN
(1st โ๐ต))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ด))) |
25 | 21, 24 | breq12i 5119 |
. . . . . 6
โข
((((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
<N (((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ (((1st โ๐ถ) ยทN
(1st โ๐ด))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ต)))
<N (((1st โ๐ถ) ยทN
(1st โ๐ต))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ด)))) |
26 | 14, 25 | bitrdi 287 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ (((1st โ๐ถ) ยทN
(1st โ๐ด))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ต)))
<N (((1st โ๐ถ) ยทN
(1st โ๐ต))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ด))))) |
27 | | ordpipq 10885 |
. . . . 5
โข
(โจ((1st โ๐ถ) ยทN
(1st โ๐ด)),
((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ <pQ
โจ((1st โ๐ถ) ยทN
(1st โ๐ต)),
((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ โ (((1st
โ๐ถ)
ยทN (1st โ๐ด)) ยทN
((2nd โ๐ถ)
ยทN (2nd โ๐ต))) <N
(((1st โ๐ถ)
ยทN (1st โ๐ต)) ยทN
((2nd โ๐ถ)
ยทN (2nd โ๐ด)))) |
28 | 26, 27 | bitr4di 289 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ โจ((1st โ๐ถ) ยทN
(1st โ๐ด)),
((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ <pQ
โจ((1st โ๐ถ) ยทN
(1st โ๐ต)),
((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ)) |
29 | | elpqn 10868 |
. . . . . . 7
โข (๐ด โ Q โ
๐ด โ (N
ร N)) |
30 | 29 | 3ad2ant1 1134 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ด
โ (N ร N)) |
31 | | mulpipq2 10882 |
. . . . . 6
โข ((๐ถ โ (N ร
N) โง ๐ด
โ (N ร N)) โ (๐ถ ยทpQ ๐ด) = โจ((1st
โ๐ถ)
ยทN (1st โ๐ด)), ((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ) |
32 | 6, 30, 31 | syl2anc 585 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ถ
ยทpQ ๐ด) = โจ((1st โ๐ถ)
ยทN (1st โ๐ด)), ((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ) |
33 | | elpqn 10868 |
. . . . . . 7
โข (๐ต โ Q โ
๐ต โ (N
ร N)) |
34 | 33 | 3ad2ant2 1135 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ต
โ (N ร N)) |
35 | | mulpipq2 10882 |
. . . . . 6
โข ((๐ถ โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ถ ยทpQ ๐ต) = โจ((1st
โ๐ถ)
ยทN (1st โ๐ต)), ((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ) |
36 | 6, 34, 35 | syl2anc 585 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ถ
ยทpQ ๐ต) = โจ((1st โ๐ถ)
ยทN (1st โ๐ต)), ((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ) |
37 | 32, 36 | breq12d 5123 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ถ
ยทpQ ๐ด) <pQ (๐ถ
ยทpQ ๐ต) โ โจ((1st โ๐ถ)
ยทN (1st โ๐ด)), ((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ <pQ
โจ((1st โ๐ถ) ยทN
(1st โ๐ต)),
((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ)) |
38 | 28, 37 | bitr4d 282 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ (๐ถ
ยทpQ ๐ด) <pQ (๐ถ
ยทpQ ๐ต))) |
39 | | ordpinq 10886 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
<Q ๐ต โ ((1st โ๐ด)
ยทN (2nd โ๐ต)) <N
((1st โ๐ต)
ยทN (2nd โ๐ด)))) |
40 | 39 | 3adant3 1133 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
<Q ๐ต โ ((1st โ๐ด)
ยทN (2nd โ๐ต)) <N
((1st โ๐ต)
ยทN (2nd โ๐ด)))) |
41 | | mulpqnq 10884 |
. . . . . . 7
โข ((๐ถ โ Q โง
๐ด โ Q)
โ (๐ถ
ยทQ ๐ด) = ([Q]โ(๐ถ
ยทpQ ๐ด))) |
42 | 41 | ancoms 460 |
. . . . . 6
โข ((๐ด โ Q โง
๐ถ โ Q)
โ (๐ถ
ยทQ ๐ด) = ([Q]โ(๐ถ
ยทpQ ๐ด))) |
43 | 42 | 3adant2 1132 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ถ
ยทQ ๐ด) = ([Q]โ(๐ถ
ยทpQ ๐ด))) |
44 | | mulpqnq 10884 |
. . . . . . 7
โข ((๐ถ โ Q โง
๐ต โ Q)
โ (๐ถ
ยทQ ๐ต) = ([Q]โ(๐ถ
ยทpQ ๐ต))) |
45 | 44 | ancoms 460 |
. . . . . 6
โข ((๐ต โ Q โง
๐ถ โ Q)
โ (๐ถ
ยทQ ๐ต) = ([Q]โ(๐ถ
ยทpQ ๐ต))) |
46 | 45 | 3adant1 1131 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ถ
ยทQ ๐ต) = ([Q]โ(๐ถ
ยทpQ ๐ต))) |
47 | 43, 46 | breq12d 5123 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ถ
ยทQ ๐ด) <Q (๐ถ
ยทQ ๐ต) โ ([Q]โ(๐ถ
ยทpQ ๐ด)) <Q
([Q]โ(๐ถ
ยทpQ ๐ต)))) |
48 | | lterpq 10913 |
. . . 4
โข ((๐ถ
ยทpQ ๐ด) <pQ (๐ถ
ยทpQ ๐ต) โ ([Q]โ(๐ถ
ยทpQ ๐ด)) <Q
([Q]โ(๐ถ
ยทpQ ๐ต))) |
49 | 47, 48 | bitr4di 289 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ถ
ยทQ ๐ด) <Q (๐ถ
ยทQ ๐ต) โ (๐ถ ยทpQ ๐ด)
<pQ (๐ถ ยทpQ ๐ต))) |
50 | 38, 40, 49 | 3bitr4d 311 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
<Q ๐ต โ (๐ถ ยทQ ๐ด) <Q
(๐ถ
ยทQ ๐ต))) |
51 | 2, 3, 4, 50 | ndmovord 7549 |
1
โข (๐ถ โ Q โ
(๐ด
<Q ๐ต โ (๐ถ ยทQ ๐ด) <Q
(๐ถ
ยทQ ๐ต))) |