Step | Hyp | Ref
| Expression |
1 | | opex 5465 |
. . 3
โข
โจ๐ด, ๐ตโฉ โ V |
2 | | opex 5465 |
. . 3
โข
โจ๐ถ, ๐ทโฉ โ V |
3 | | eleq1 2822 |
. . . . . 6
โข (๐ฅ = โจ๐ด, ๐ตโฉ โ (๐ฅ โ (N ร
N) โ โจ๐ด, ๐ตโฉ โ (N ร
N))) |
4 | 3 | anbi1d 631 |
. . . . 5
โข (๐ฅ = โจ๐ด, ๐ตโฉ โ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โ (โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N)))) |
5 | 4 | anbi1d 631 |
. . . 4
โข (๐ฅ = โจ๐ด, ๐ตโฉ โ (((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ))) โ ((โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ))))) |
6 | | fveq2 6892 |
. . . . . . . 8
โข (๐ฅ = โจ๐ด, ๐ตโฉ โ (1st โ๐ฅ) = (1st
โโจ๐ด, ๐ตโฉ)) |
7 | | opelxp 5713 |
. . . . . . . . . 10
โข
(โจ๐ด, ๐ตโฉ โ (N
ร N) โ (๐ด โ N โง ๐ต โ
N)) |
8 | | op1stg 7987 |
. . . . . . . . . 10
โข ((๐ด โ N โง
๐ต โ N)
โ (1st โโจ๐ด, ๐ตโฉ) = ๐ด) |
9 | 7, 8 | sylbi 216 |
. . . . . . . . 9
โข
(โจ๐ด, ๐ตโฉ โ (N
ร N) โ (1st โโจ๐ด, ๐ตโฉ) = ๐ด) |
10 | 9 | adantr 482 |
. . . . . . . 8
โข
((โจ๐ด, ๐ตโฉ โ (N
ร N) โง ๐ฆ โ (N ร
N)) โ (1st โโจ๐ด, ๐ตโฉ) = ๐ด) |
11 | 6, 10 | sylan9eq 2793 |
. . . . . . 7
โข ((๐ฅ = โจ๐ด, ๐ตโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N))) โ (1st
โ๐ฅ) = ๐ด) |
12 | 11 | oveq1d 7424 |
. . . . . 6
โข ((๐ฅ = โจ๐ด, ๐ตโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N))) โ ((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) = (๐ด ยทN
(2nd โ๐ฆ))) |
13 | | fveq2 6892 |
. . . . . . . 8
โข (๐ฅ = โจ๐ด, ๐ตโฉ โ (2nd โ๐ฅ) = (2nd
โโจ๐ด, ๐ตโฉ)) |
14 | | op2ndg 7988 |
. . . . . . . . . 10
โข ((๐ด โ N โง
๐ต โ N)
โ (2nd โโจ๐ด, ๐ตโฉ) = ๐ต) |
15 | 7, 14 | sylbi 216 |
. . . . . . . . 9
โข
(โจ๐ด, ๐ตโฉ โ (N
ร N) โ (2nd โโจ๐ด, ๐ตโฉ) = ๐ต) |
16 | 15 | adantr 482 |
. . . . . . . 8
โข
((โจ๐ด, ๐ตโฉ โ (N
ร N) โง ๐ฆ โ (N ร
N)) โ (2nd โโจ๐ด, ๐ตโฉ) = ๐ต) |
17 | 13, 16 | sylan9eq 2793 |
. . . . . . 7
โข ((๐ฅ = โจ๐ด, ๐ตโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N))) โ (2nd
โ๐ฅ) = ๐ต) |
18 | 17 | oveq2d 7425 |
. . . . . 6
โข ((๐ฅ = โจ๐ด, ๐ตโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N))) โ ((1st
โ๐ฆ)
ยทN (2nd โ๐ฅ)) = ((1st โ๐ฆ)
ยทN ๐ต)) |
19 | 12, 18 | breq12d 5162 |
. . . . 5
โข ((๐ฅ = โจ๐ด, ๐ตโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N))) โ (((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ)) โ (๐ด ยทN
(2nd โ๐ฆ))
<N ((1st โ๐ฆ) ยทN ๐ต))) |
20 | 19 | pm5.32da 580 |
. . . 4
โข (๐ฅ = โจ๐ด, ๐ตโฉ โ (((โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ))) โ ((โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง (๐ด ยทN
(2nd โ๐ฆ))
<N ((1st โ๐ฆ) ยทN ๐ต)))) |
21 | 5, 20 | bitrd 279 |
. . 3
โข (๐ฅ = โจ๐ด, ๐ตโฉ โ (((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ))) โ ((โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง (๐ด ยทN
(2nd โ๐ฆ))
<N ((1st โ๐ฆ) ยทN ๐ต)))) |
22 | | eleq1 2822 |
. . . . . 6
โข (๐ฆ = โจ๐ถ, ๐ทโฉ โ (๐ฆ โ (N ร
N) โ โจ๐ถ, ๐ทโฉ โ (N ร
N))) |
23 | 22 | anbi2d 630 |
. . . . 5
โข (๐ฆ = โจ๐ถ, ๐ทโฉ โ ((โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โ (โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)))) |
24 | 23 | anbi1d 631 |
. . . 4
โข (๐ฆ = โจ๐ถ, ๐ทโฉ โ (((โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง (๐ด ยทN
(2nd โ๐ฆ))
<N ((1st โ๐ฆ) ยทN ๐ต)) โ ((โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โง (๐ด
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN ๐ต)))) |
25 | | fveq2 6892 |
. . . . . . . 8
โข (๐ฆ = โจ๐ถ, ๐ทโฉ โ (2nd โ๐ฆ) = (2nd
โโจ๐ถ, ๐ทโฉ)) |
26 | | opelxp 5713 |
. . . . . . . . . 10
โข
(โจ๐ถ, ๐ทโฉ โ (N
ร N) โ (๐ถ โ N โง ๐ท โ
N)) |
27 | | op2ndg 7988 |
. . . . . . . . . 10
โข ((๐ถ โ N โง
๐ท โ N)
โ (2nd โโจ๐ถ, ๐ทโฉ) = ๐ท) |
28 | 26, 27 | sylbi 216 |
. . . . . . . . 9
โข
(โจ๐ถ, ๐ทโฉ โ (N
ร N) โ (2nd โโจ๐ถ, ๐ทโฉ) = ๐ท) |
29 | 28 | adantl 483 |
. . . . . . . 8
โข
((โจ๐ด, ๐ตโฉ โ (N
ร N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โ (2nd โโจ๐ถ, ๐ทโฉ) = ๐ท) |
30 | 25, 29 | sylan9eq 2793 |
. . . . . . 7
โข ((๐ฆ = โจ๐ถ, ๐ทโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N))) โ (2nd โ๐ฆ) = ๐ท) |
31 | 30 | oveq2d 7425 |
. . . . . 6
โข ((๐ฆ = โจ๐ถ, ๐ทโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N))) โ (๐ด ยทN
(2nd โ๐ฆ))
= (๐ด
ยทN ๐ท)) |
32 | | fveq2 6892 |
. . . . . . . 8
โข (๐ฆ = โจ๐ถ, ๐ทโฉ โ (1st โ๐ฆ) = (1st
โโจ๐ถ, ๐ทโฉ)) |
33 | | op1stg 7987 |
. . . . . . . . . 10
โข ((๐ถ โ N โง
๐ท โ N)
โ (1st โโจ๐ถ, ๐ทโฉ) = ๐ถ) |
34 | 26, 33 | sylbi 216 |
. . . . . . . . 9
โข
(โจ๐ถ, ๐ทโฉ โ (N
ร N) โ (1st โโจ๐ถ, ๐ทโฉ) = ๐ถ) |
35 | 34 | adantl 483 |
. . . . . . . 8
โข
((โจ๐ด, ๐ตโฉ โ (N
ร N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โ (1st โโจ๐ถ, ๐ทโฉ) = ๐ถ) |
36 | 32, 35 | sylan9eq 2793 |
. . . . . . 7
โข ((๐ฆ = โจ๐ถ, ๐ทโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N))) โ (1st โ๐ฆ) = ๐ถ) |
37 | 36 | oveq1d 7424 |
. . . . . 6
โข ((๐ฆ = โจ๐ถ, ๐ทโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N))) โ ((1st โ๐ฆ) ยทN ๐ต) = (๐ถ ยทN ๐ต)) |
38 | 31, 37 | breq12d 5162 |
. . . . 5
โข ((๐ฆ = โจ๐ถ, ๐ทโฉ โง (โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N))) โ ((๐ด ยทN
(2nd โ๐ฆ))
<N ((1st โ๐ฆ) ยทN ๐ต) โ (๐ด ยทN ๐ท) <N
(๐ถ
ยทN ๐ต))) |
39 | 38 | pm5.32da 580 |
. . . 4
โข (๐ฆ = โจ๐ถ, ๐ทโฉ โ (((โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โง (๐ด
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN ๐ต)) โ ((โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โง (๐ด
ยทN ๐ท) <N (๐ถ
ยทN ๐ต)))) |
40 | 24, 39 | bitrd 279 |
. . 3
โข (๐ฆ = โจ๐ถ, ๐ทโฉ โ (((โจ๐ด, ๐ตโฉ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง (๐ด ยทN
(2nd โ๐ฆ))
<N ((1st โ๐ฆ) ยทN ๐ต)) โ ((โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โง (๐ด
ยทN ๐ท) <N (๐ถ
ยทN ๐ต)))) |
41 | | df-ltpq 10905 |
. . 3
โข
<pQ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง ((1st
โ๐ฅ)
ยทN (2nd โ๐ฆ)) <N
((1st โ๐ฆ)
ยทN (2nd โ๐ฅ)))} |
42 | 1, 2, 21, 40, 41 | brab 5544 |
. 2
โข
(โจ๐ด, ๐ตโฉ
<pQ โจ๐ถ, ๐ทโฉ โ ((โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โง (๐ด
ยทN ๐ท) <N (๐ถ
ยทN ๐ต))) |
43 | | simpr 486 |
. . 3
โข
(((โจ๐ด, ๐ตโฉ โ (N
ร N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โง (๐ด
ยทN ๐ท) <N (๐ถ
ยทN ๐ต)) โ (๐ด ยทN ๐ท) <N
(๐ถ
ยทN ๐ต)) |
44 | | ltrelpi 10884 |
. . . . . 6
โข
<N โ (N ร
N) |
45 | 44 | brel 5742 |
. . . . 5
โข ((๐ด
ยทN ๐ท) <N (๐ถ
ยทN ๐ต) โ ((๐ด ยทN ๐ท) โ N โง
(๐ถ
ยทN ๐ต) โ N)) |
46 | | dmmulpi 10886 |
. . . . . . 7
โข dom
ยทN = (N ร
N) |
47 | | 0npi 10877 |
. . . . . . 7
โข ยฌ
โ
โ N |
48 | 46, 47 | ndmovrcl 7593 |
. . . . . 6
โข ((๐ด
ยทN ๐ท) โ N โ (๐ด โ N โง
๐ท โ
N)) |
49 | 46, 47 | ndmovrcl 7593 |
. . . . . 6
โข ((๐ถ
ยทN ๐ต) โ N โ (๐ถ โ N โง
๐ต โ
N)) |
50 | 48, 49 | anim12i 614 |
. . . . 5
โข (((๐ด
ยทN ๐ท) โ N โง (๐ถ
ยทN ๐ต) โ N) โ ((๐ด โ N โง
๐ท โ N)
โง (๐ถ โ
N โง ๐ต
โ N))) |
51 | | opelxpi 5714 |
. . . . . . 7
โข ((๐ด โ N โง
๐ต โ N)
โ โจ๐ด, ๐ตโฉ โ (N
ร N)) |
52 | 51 | ad2ant2rl 748 |
. . . . . 6
โข (((๐ด โ N โง
๐ท โ N)
โง (๐ถ โ
N โง ๐ต
โ N)) โ โจ๐ด, ๐ตโฉ โ (N ร
N)) |
53 | | simprl 770 |
. . . . . . 7
โข (((๐ด โ N โง
๐ท โ N)
โง (๐ถ โ
N โง ๐ต
โ N)) โ ๐ถ โ N) |
54 | | simplr 768 |
. . . . . . 7
โข (((๐ด โ N โง
๐ท โ N)
โง (๐ถ โ
N โง ๐ต
โ N)) โ ๐ท โ N) |
55 | 53, 54 | opelxpd 5716 |
. . . . . 6
โข (((๐ด โ N โง
๐ท โ N)
โง (๐ถ โ
N โง ๐ต
โ N)) โ โจ๐ถ, ๐ทโฉ โ (N ร
N)) |
56 | 52, 55 | jca 513 |
. . . . 5
โข (((๐ด โ N โง
๐ท โ N)
โง (๐ถ โ
N โง ๐ต
โ N)) โ (โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N))) |
57 | 45, 50, 56 | 3syl 18 |
. . . 4
โข ((๐ด
ยทN ๐ท) <N (๐ถ
ยทN ๐ต) โ (โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N))) |
58 | 57 | ancri 551 |
. . 3
โข ((๐ด
ยทN ๐ท) <N (๐ถ
ยทN ๐ต) โ ((โจ๐ด, ๐ตโฉ โ (N ร
N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โง (๐ด
ยทN ๐ท) <N (๐ถ
ยทN ๐ต))) |
59 | 43, 58 | impbii 208 |
. 2
โข
(((โจ๐ด, ๐ตโฉ โ (N
ร N) โง โจ๐ถ, ๐ทโฉ โ (N ร
N)) โง (๐ด
ยทN ๐ท) <N (๐ถ
ยทN ๐ต)) โ (๐ด ยทN ๐ท) <N
(๐ถ
ยทN ๐ต)) |
60 | 42, 59 | bitri 275 |
1
โข
(โจ๐ด, ๐ตโฉ
<pQ โจ๐ถ, ๐ทโฉ โ (๐ด ยทN ๐ท) <N
(๐ถ
ยทN ๐ต)) |