Step | Hyp | Ref
| Expression |
1 | | addnqf 10891 |
. . 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 | | ordpinq 10886 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
<Q ๐ต โ ((1st โ๐ด)
ยทN (2nd โ๐ต)) <N
((1st โ๐ต)
ยทN (2nd โ๐ด)))) |
6 | 5 | 3adant3 1133 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
<Q ๐ต โ ((1st โ๐ด)
ยทN (2nd โ๐ต)) <N
((1st โ๐ต)
ยทN (2nd โ๐ด)))) |
7 | | elpqn 10868 |
. . . . . . 7
โข (๐ถ โ Q โ
๐ถ โ (N
ร N)) |
8 | 7 | 3ad2ant3 1136 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ถ
โ (N ร N)) |
9 | | elpqn 10868 |
. . . . . . 7
โข (๐ด โ Q โ
๐ด โ (N
ร N)) |
10 | 9 | 3ad2ant1 1134 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ด
โ (N ร N)) |
11 | | addpipq2 10879 |
. . . . . 6
โข ((๐ถ โ (N ร
N) โง ๐ด
โ (N ร N)) โ (๐ถ +pQ ๐ด) = โจ(((1st
โ๐ถ)
ยทN (2nd โ๐ด)) +N
((1st โ๐ด)
ยทN (2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ) |
12 | 8, 10, 11 | syl2anc 585 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ถ
+pQ ๐ด) = โจ(((1st โ๐ถ)
ยทN (2nd โ๐ด)) +N
((1st โ๐ด)
ยทN (2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ) |
13 | | elpqn 10868 |
. . . . . . 7
โข (๐ต โ Q โ
๐ต โ (N
ร N)) |
14 | 13 | 3ad2ant2 1135 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ๐ต
โ (N ร N)) |
15 | | addpipq2 10879 |
. . . . . 6
โข ((๐ถ โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ถ +pQ ๐ต) = โจ(((1st
โ๐ถ)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ) |
16 | 8, 14, 15 | syl2anc 585 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ถ
+pQ ๐ต) = โจ(((1st โ๐ถ)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ) |
17 | 12, 16 | breq12d 5123 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ถ
+pQ ๐ด) <pQ (๐ถ +pQ
๐ต) โ
โจ(((1st โ๐ถ) ยทN
(2nd โ๐ด))
+N ((1st โ๐ด) ยทN
(2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ <pQ
โจ(((1st โ๐ถ) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ)) |
18 | | addpqnq 10881 |
. . . . . . . 8
โข ((๐ถ โ Q โง
๐ด โ Q)
โ (๐ถ
+Q ๐ด) = ([Q]โ(๐ถ +pQ
๐ด))) |
19 | 18 | ancoms 460 |
. . . . . . 7
โข ((๐ด โ Q โง
๐ถ โ Q)
โ (๐ถ
+Q ๐ด) = ([Q]โ(๐ถ +pQ
๐ด))) |
20 | 19 | 3adant2 1132 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ถ
+Q ๐ด) = ([Q]โ(๐ถ +pQ
๐ด))) |
21 | | addpqnq 10881 |
. . . . . . . 8
โข ((๐ถ โ Q โง
๐ต โ Q)
โ (๐ถ
+Q ๐ต) = ([Q]โ(๐ถ +pQ
๐ต))) |
22 | 21 | ancoms 460 |
. . . . . . 7
โข ((๐ต โ Q โง
๐ถ โ Q)
โ (๐ถ
+Q ๐ต) = ([Q]โ(๐ถ +pQ
๐ต))) |
23 | 22 | 3adant1 1131 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ถ
+Q ๐ต) = ([Q]โ(๐ถ +pQ
๐ต))) |
24 | 20, 23 | breq12d 5123 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ถ
+Q ๐ด) <Q (๐ถ +Q
๐ต) โ
([Q]โ(๐ถ
+pQ ๐ด)) <Q
([Q]โ(๐ถ
+pQ ๐ต)))) |
25 | | lterpq 10913 |
. . . . 5
โข ((๐ถ +pQ
๐ด)
<pQ (๐ถ +pQ ๐ต) โ
([Q]โ(๐ถ
+pQ ๐ด)) <Q
([Q]โ(๐ถ
+pQ ๐ต))) |
26 | 24, 25 | bitr4di 289 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ถ
+Q ๐ด) <Q (๐ถ +Q
๐ต) โ (๐ถ +pQ
๐ด)
<pQ (๐ถ +pQ ๐ต))) |
27 | | xp2nd 7959 |
. . . . . . . . . 10
โข (๐ถ โ (N ร
N) โ (2nd โ๐ถ) โ N) |
28 | 8, 27 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (2nd โ๐ถ) โ N) |
29 | | mulclpi 10836 |
. . . . . . . . 9
โข
(((2nd โ๐ถ) โ N โง
(2nd โ๐ถ)
โ N) โ ((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
โ N) |
30 | 28, 28, 29 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
โ N) |
31 | | ltmpi 10847 |
. . . . . . . 8
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
โ N โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
<N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด))))) |
32 | 30, 31 | syl 17 |
. . . . . . 7
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
<N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด))))) |
33 | | xp2nd 7959 |
. . . . . . . . . . 11
โข (๐ต โ (N ร
N) โ (2nd โ๐ต) โ N) |
34 | 14, 33 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (2nd โ๐ต) โ N) |
35 | | mulclpi 10836 |
. . . . . . . . . 10
โข
(((2nd โ๐ถ) โ N โง
(2nd โ๐ต)
โ N) โ ((2nd โ๐ถ) ยทN
(2nd โ๐ต))
โ N) |
36 | 28, 34, 35 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((2nd โ๐ถ) ยทN
(2nd โ๐ต))
โ N) |
37 | | xp1st 7958 |
. . . . . . . . . . 11
โข (๐ถ โ (N ร
N) โ (1st โ๐ถ) โ N) |
38 | 8, 37 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (1st โ๐ถ) โ N) |
39 | | xp2nd 7959 |
. . . . . . . . . . 11
โข (๐ด โ (N ร
N) โ (2nd โ๐ด) โ N) |
40 | 10, 39 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (2nd โ๐ด) โ N) |
41 | | mulclpi 10836 |
. . . . . . . . . 10
โข
(((1st โ๐ถ) โ N โง
(2nd โ๐ด)
โ N) โ ((1st โ๐ถ) ยทN
(2nd โ๐ด))
โ N) |
42 | 38, 40, 41 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((1st โ๐ถ) ยทN
(2nd โ๐ด))
โ N) |
43 | | mulclpi 10836 |
. . . . . . . . 9
โข
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
โ N โง ((1st โ๐ถ) ยทN
(2nd โ๐ด))
โ N) โ (((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
โ N) |
44 | 36, 42, 43 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
โ N) |
45 | | ltapi 10846 |
. . . . . . . 8
โข
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
โ N โ ((((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
<N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ ((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))) <N
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))))) |
46 | 44, 45 | syl 17 |
. . . . . . 7
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
<N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ ((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))) <N
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))))) |
47 | 32, 46 | bitrd 279 |
. . . . . 6
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ ((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))) <N
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))))) |
48 | | mulcompi 10839 |
. . . . . . . . . 10
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
= (((1st โ๐ด) ยทN
(2nd โ๐ต))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ถ))) |
49 | | fvex 6860 |
. . . . . . . . . . 11
โข
(1st โ๐ด) โ V |
50 | | fvex 6860 |
. . . . . . . . . . 11
โข
(2nd โ๐ต) โ V |
51 | | fvex 6860 |
. . . . . . . . . . 11
โข
(2nd โ๐ถ) โ V |
52 | | mulcompi 10839 |
. . . . . . . . . . 11
โข (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ) |
53 | | mulasspi 10840 |
. . . . . . . . . . 11
โข ((๐ฅ
ยทN ๐ฆ) ยทN ๐ง) = (๐ฅ ยทN (๐ฆ
ยทN ๐ง)) |
54 | 49, 50, 51, 52, 53, 51 | caov411 7591 |
. . . . . . . . . 10
โข
(((1st โ๐ด) ยทN
(2nd โ๐ต))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ถ)))
= (((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ถ))) |
55 | 48, 54 | eqtri 2765 |
. . . . . . . . 9
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
= (((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ถ))) |
56 | 55 | oveq2i 7373 |
. . . . . . . 8
โข
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))) = ((((2nd โ๐ถ)
ยทN (2nd โ๐ต)) ยทN
((1st โ๐ถ)
ยทN (2nd โ๐ด))) +N
(((2nd โ๐ถ)
ยทN (2nd โ๐ต)) ยทN
((1st โ๐ด)
ยทN (2nd โ๐ถ)))) |
57 | | distrpi 10841 |
. . . . . . . 8
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN (((1st โ๐ถ) ยทN
(2nd โ๐ด))
+N ((1st โ๐ด) ยทN
(2nd โ๐ถ)))) = ((((2nd โ๐ถ)
ยทN (2nd โ๐ต)) ยทN
((1st โ๐ถ)
ยทN (2nd โ๐ด))) +N
(((2nd โ๐ถ)
ยทN (2nd โ๐ต)) ยทN
((1st โ๐ด)
ยทN (2nd โ๐ถ)))) |
58 | | mulcompi 10839 |
. . . . . . . 8
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN (((1st โ๐ถ) ยทN
(2nd โ๐ด))
+N ((1st โ๐ด) ยทN
(2nd โ๐ถ)))) = ((((1st โ๐ถ)
ยทN (2nd โ๐ด)) +N
((1st โ๐ด)
ยทN (2nd โ๐ถ))) ยทN
((2nd โ๐ถ)
ยทN (2nd โ๐ต))) |
59 | 56, 57, 58 | 3eqtr2i 2771 |
. . . . . . 7
โข
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))) = ((((1st โ๐ถ)
ยทN (2nd โ๐ด)) +N
((1st โ๐ด)
ยทN (2nd โ๐ถ))) ยทN
((2nd โ๐ถ)
ยทN (2nd โ๐ต))) |
60 | | mulcompi 10839 |
. . . . . . . . . 10
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
= (((1st โ๐ถ) ยทN
(2nd โ๐ด))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ต))) |
61 | | fvex 6860 |
. . . . . . . . . . 11
โข
(1st โ๐ถ) โ V |
62 | | fvex 6860 |
. . . . . . . . . . 11
โข
(2nd โ๐ด) โ V |
63 | 61, 62, 51, 52, 53, 50 | caov411 7591 |
. . . . . . . . . 10
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ด))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ต)))
= (((2nd โ๐ถ) ยทN
(2nd โ๐ด))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ต))) |
64 | 60, 63 | eqtri 2765 |
. . . . . . . . 9
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
= (((2nd โ๐ถ) ยทN
(2nd โ๐ด))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ต))) |
65 | | mulcompi 10839 |
. . . . . . . . . 10
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
= (((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ถ))) |
66 | | fvex 6860 |
. . . . . . . . . . 11
โข
(1st โ๐ต) โ V |
67 | 66, 62, 51, 52, 53, 51 | caov411 7591 |
. . . . . . . . . 10
โข
(((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ถ)))
= (((2nd โ๐ถ) ยทN
(2nd โ๐ด))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ถ))) |
68 | 65, 67 | eqtri 2765 |
. . . . . . . . 9
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
= (((2nd โ๐ถ) ยทN
(2nd โ๐ด))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ถ))) |
69 | 64, 68 | oveq12i 7374 |
. . . . . . . 8
โข
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))) = ((((2nd โ๐ถ)
ยทN (2nd โ๐ด)) ยทN
((1st โ๐ถ)
ยทN (2nd โ๐ต))) +N
(((2nd โ๐ถ)
ยทN (2nd โ๐ด)) ยทN
((1st โ๐ต)
ยทN (2nd โ๐ถ)))) |
70 | | distrpi 10841 |
. . . . . . . 8
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ด))
ยทN (((1st โ๐ถ) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ถ)))) = ((((2nd โ๐ถ)
ยทN (2nd โ๐ด)) ยทN
((1st โ๐ถ)
ยทN (2nd โ๐ต))) +N
(((2nd โ๐ถ)
ยทN (2nd โ๐ด)) ยทN
((1st โ๐ต)
ยทN (2nd โ๐ถ)))) |
71 | | mulcompi 10839 |
. . . . . . . 8
โข
(((2nd โ๐ถ) ยทN
(2nd โ๐ด))
ยทN (((1st โ๐ถ) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ถ)))) = ((((1st โ๐ถ)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ถ))) ยทN
((2nd โ๐ถ)
ยทN (2nd โ๐ด))) |
72 | 69, 70, 71 | 3eqtr2i 2771 |
. . . . . . 7
โข
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))) = ((((1st โ๐ถ)
ยทN (2nd โ๐ต)) +N
((1st โ๐ต)
ยทN (2nd โ๐ถ))) ยทN
((2nd โ๐ถ)
ยทN (2nd โ๐ด))) |
73 | 59, 72 | breq12i 5119 |
. . . . . 6
โข
(((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))) <N
((((2nd โ๐ถ) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ด)))
+N (((2nd โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))) โ ((((1st โ๐ถ)
ยทN (2nd โ๐ด)) +N
((1st โ๐ด)
ยทN (2nd โ๐ถ))) ยทN
((2nd โ๐ถ)
ยทN (2nd โ๐ต))) <N
((((1st โ๐ถ) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ถ)))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ด)))) |
74 | 47, 73 | bitrdi 287 |
. . . . 5
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ ((((1st โ๐ถ) ยทN
(2nd โ๐ด))
+N ((1st โ๐ด) ยทN
(2nd โ๐ถ)))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ต)))
<N ((((1st โ๐ถ) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ถ)))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ด))))) |
75 | | ordpipq 10885 |
. . . . 5
โข
(โจ(((1st โ๐ถ) ยทN
(2nd โ๐ด))
+N ((1st โ๐ด) ยทN
(2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ <pQ
โจ(((1st โ๐ถ) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ โ ((((1st
โ๐ถ)
ยทN (2nd โ๐ด)) +N
((1st โ๐ด)
ยทN (2nd โ๐ถ))) ยทN
((2nd โ๐ถ)
ยทN (2nd โ๐ต))) <N
((((1st โ๐ถ) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ถ)))
ยทN ((2nd โ๐ถ) ยทN
(2nd โ๐ด)))) |
76 | 74, 75 | bitr4di 289 |
. . . 4
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ โจ(((1st โ๐ถ) ยทN
(2nd โ๐ด))
+N ((1st โ๐ด) ยทN
(2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ด))โฉ <pQ
โจ(((1st โ๐ถ) ยทN
(2nd โ๐ต))
+N ((1st โ๐ต) ยทN
(2nd โ๐ถ))), ((2nd โ๐ถ)
ยทN (2nd โ๐ต))โฉ)) |
77 | 17, 26, 76 | 3bitr4rd 312 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (((1st โ๐ด) ยทN
(2nd โ๐ต))
<N ((1st โ๐ต) ยทN
(2nd โ๐ด))
โ (๐ถ
+Q ๐ด) <Q (๐ถ +Q
๐ต))) |
78 | 6, 77 | bitrd 279 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
<Q ๐ต โ (๐ถ +Q ๐ด) <Q
(๐ถ
+Q ๐ต))) |
79 | 2, 3, 4, 78 | ndmovord 7549 |
1
โข (๐ถ โ Q โ
(๐ด
<Q ๐ต โ (๐ถ +Q ๐ด) <Q
(๐ถ
+Q ๐ต))) |