Step | Hyp | Ref
| Expression |
1 | | elpqn 10868 |
. . . 4
โข (๐ด โ Q โ
๐ด โ (N
ร N)) |
2 | | xp1st 7958 |
. . . 4
โข (๐ด โ (N ร
N) โ (1st โ๐ด) โ N) |
3 | 1, 2 | syl 17 |
. . 3
โข (๐ด โ Q โ
(1st โ๐ด)
โ N) |
4 | | 1pi 10826 |
. . 3
โข
1o โ N |
5 | | addclpi 10835 |
. . 3
โข
(((1st โ๐ด) โ N โง 1o
โ N) โ ((1st โ๐ด) +N 1o)
โ N) |
6 | 3, 4, 5 | sylancl 587 |
. 2
โข (๐ด โ Q โ
((1st โ๐ด)
+N 1o) โ
N) |
7 | | xp2nd 7959 |
. . . . . 6
โข (๐ด โ (N ร
N) โ (2nd โ๐ด) โ N) |
8 | 1, 7 | syl 17 |
. . . . 5
โข (๐ด โ Q โ
(2nd โ๐ด)
โ N) |
9 | | mulclpi 10836 |
. . . . 5
โข
((((1st โ๐ด) +N 1o)
โ N โง (2nd โ๐ด) โ N) โ
(((1st โ๐ด)
+N 1o) ยทN
(2nd โ๐ด))
โ N) |
10 | 6, 8, 9 | syl2anc 585 |
. . . 4
โข (๐ด โ Q โ
(((1st โ๐ด)
+N 1o) ยทN
(2nd โ๐ด))
โ N) |
11 | | eqid 2737 |
. . . . . . 7
โข
((1st โ๐ด) +N 1o)
= ((1st โ๐ด) +N
1o) |
12 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ฅ = 1o โ
((1st โ๐ด)
+N ๐ฅ) = ((1st โ๐ด) +N
1o)) |
13 | 12 | eqeq1d 2739 |
. . . . . . . 8
โข (๐ฅ = 1o โ
(((1st โ๐ด)
+N ๐ฅ) = ((1st โ๐ด) +N 1o)
โ ((1st โ๐ด) +N 1o)
= ((1st โ๐ด) +N
1o))) |
14 | 13 | rspcev 3584 |
. . . . . . 7
โข
((1o โ N โง ((1st
โ๐ด)
+N 1o) = ((1st โ๐ด) +N
1o)) โ โ๐ฅ โ N ((1st
โ๐ด)
+N ๐ฅ) = ((1st โ๐ด) +N
1o)) |
15 | 4, 11, 14 | mp2an 691 |
. . . . . 6
โข
โ๐ฅ โ
N ((1st โ๐ด) +N ๐ฅ) = ((1st
โ๐ด)
+N 1o) |
16 | | ltexpi 10845 |
. . . . . 6
โข
(((1st โ๐ด) โ N โง
((1st โ๐ด)
+N 1o) โ N) โ
((1st โ๐ด)
<N ((1st โ๐ด) +N 1o)
โ โ๐ฅ โ
N ((1st โ๐ด) +N ๐ฅ) = ((1st
โ๐ด)
+N 1o))) |
17 | 15, 16 | mpbiri 258 |
. . . . 5
โข
(((1st โ๐ด) โ N โง
((1st โ๐ด)
+N 1o) โ N) โ
(1st โ๐ด)
<N ((1st โ๐ด) +N
1o)) |
18 | 3, 6, 17 | syl2anc 585 |
. . . 4
โข (๐ด โ Q โ
(1st โ๐ด)
<N ((1st โ๐ด) +N
1o)) |
19 | | nlt1pi 10849 |
. . . . 5
โข ยฌ
(2nd โ๐ด)
<N 1o |
20 | | ltmpi 10847 |
. . . . . . 7
โข
(((1st โ๐ด) +N 1o)
โ N โ ((2nd โ๐ด) <N
1o โ (((1st โ๐ด) +N 1o)
ยทN (2nd โ๐ด)) <N
(((1st โ๐ด)
+N 1o) ยทN
1o))) |
21 | 6, 20 | syl 17 |
. . . . . 6
โข (๐ด โ Q โ
((2nd โ๐ด)
<N 1o โ (((1st
โ๐ด)
+N 1o) ยทN
(2nd โ๐ด))
<N (((1st โ๐ด) +N 1o)
ยทN 1o))) |
22 | | mulidpi 10829 |
. . . . . . . 8
โข
(((1st โ๐ด) +N 1o)
โ N โ (((1st โ๐ด) +N 1o)
ยทN 1o) = ((1st
โ๐ด)
+N 1o)) |
23 | 6, 22 | syl 17 |
. . . . . . 7
โข (๐ด โ Q โ
(((1st โ๐ด)
+N 1o) ยทN
1o) = ((1st โ๐ด) +N
1o)) |
24 | 23 | breq2d 5122 |
. . . . . 6
โข (๐ด โ Q โ
((((1st โ๐ด) +N 1o)
ยทN (2nd โ๐ด)) <N
(((1st โ๐ด)
+N 1o) ยทN
1o) โ (((1st โ๐ด) +N 1o)
ยทN (2nd โ๐ด)) <N
((1st โ๐ด)
+N 1o))) |
25 | 21, 24 | bitrd 279 |
. . . . 5
โข (๐ด โ Q โ
((2nd โ๐ด)
<N 1o โ (((1st
โ๐ด)
+N 1o) ยทN
(2nd โ๐ด))
<N ((1st โ๐ด) +N
1o))) |
26 | 19, 25 | mtbii 326 |
. . . 4
โข (๐ด โ Q โ
ยฌ (((1st โ๐ด) +N 1o)
ยทN (2nd โ๐ด)) <N
((1st โ๐ด)
+N 1o)) |
27 | | ltsopi 10831 |
. . . . 5
โข
<N Or N |
28 | | ltrelpi 10832 |
. . . . 5
โข
<N โ (N ร
N) |
29 | 27, 28 | sotri3 6089 |
. . . 4
โข
(((((1st โ๐ด) +N 1o)
ยทN (2nd โ๐ด)) โ N โง
(1st โ๐ด)
<N ((1st โ๐ด) +N 1o)
โง ยฌ (((1st โ๐ด) +N 1o)
ยทN (2nd โ๐ด)) <N
((1st โ๐ด)
+N 1o)) โ (1st โ๐ด) <N
(((1st โ๐ด)
+N 1o) ยทN
(2nd โ๐ด))) |
30 | 10, 18, 26, 29 | syl3anc 1372 |
. . 3
โข (๐ด โ Q โ
(1st โ๐ด)
<N (((1st โ๐ด) +N 1o)
ยทN (2nd โ๐ด))) |
31 | | pinq 10870 |
. . . . . 6
โข
(((1st โ๐ด) +N 1o)
โ N โ โจ((1st โ๐ด) +N
1o), 1oโฉ โ Q) |
32 | 6, 31 | syl 17 |
. . . . 5
โข (๐ด โ Q โ
โจ((1st โ๐ด) +N
1o), 1oโฉ โ Q) |
33 | | ordpinq 10886 |
. . . . 5
โข ((๐ด โ Q โง
โจ((1st โ๐ด) +N
1o), 1oโฉ โ Q) โ (๐ด <Q
โจ((1st โ๐ด) +N
1o), 1oโฉ โ ((1st โ๐ด)
ยทN (2nd
โโจ((1st โ๐ด) +N
1o), 1oโฉ)) <N
((1st โโจ((1st โ๐ด) +N
1o), 1oโฉ) ยทN
(2nd โ๐ด)))) |
34 | 32, 33 | mpdan 686 |
. . . 4
โข (๐ด โ Q โ
(๐ด
<Q โจ((1st โ๐ด) +N
1o), 1oโฉ โ ((1st โ๐ด)
ยทN (2nd
โโจ((1st โ๐ด) +N
1o), 1oโฉ)) <N
((1st โโจ((1st โ๐ด) +N
1o), 1oโฉ) ยทN
(2nd โ๐ด)))) |
35 | | ovex 7395 |
. . . . . . . 8
โข
((1st โ๐ด) +N 1o)
โ V |
36 | | 1oex 8427 |
. . . . . . . 8
โข
1o โ V |
37 | 35, 36 | op2nd 7935 |
. . . . . . 7
โข
(2nd โโจ((1st โ๐ด) +N
1o), 1oโฉ) = 1o |
38 | 37 | oveq2i 7373 |
. . . . . 6
โข
((1st โ๐ด) ยทN
(2nd โโจ((1st โ๐ด) +N
1o), 1oโฉ)) = ((1st โ๐ด)
ยทN 1o) |
39 | | mulidpi 10829 |
. . . . . . 7
โข
((1st โ๐ด) โ N โ
((1st โ๐ด)
ยทN 1o) = (1st
โ๐ด)) |
40 | 3, 39 | syl 17 |
. . . . . 6
โข (๐ด โ Q โ
((1st โ๐ด)
ยทN 1o) = (1st
โ๐ด)) |
41 | 38, 40 | eqtrid 2789 |
. . . . 5
โข (๐ด โ Q โ
((1st โ๐ด)
ยทN (2nd
โโจ((1st โ๐ด) +N
1o), 1oโฉ)) = (1st โ๐ด)) |
42 | 35, 36 | op1st 7934 |
. . . . . . 7
โข
(1st โโจ((1st โ๐ด) +N
1o), 1oโฉ) = ((1st โ๐ด) +N
1o) |
43 | 42 | oveq1i 7372 |
. . . . . 6
โข
((1st โโจ((1st โ๐ด) +N
1o), 1oโฉ) ยทN
(2nd โ๐ด))
= (((1st โ๐ด) +N 1o)
ยทN (2nd โ๐ด)) |
44 | 43 | a1i 11 |
. . . . 5
โข (๐ด โ Q โ
((1st โโจ((1st โ๐ด) +N
1o), 1oโฉ) ยทN
(2nd โ๐ด))
= (((1st โ๐ด) +N 1o)
ยทN (2nd โ๐ด))) |
45 | 41, 44 | breq12d 5123 |
. . . 4
โข (๐ด โ Q โ
(((1st โ๐ด)
ยทN (2nd
โโจ((1st โ๐ด) +N
1o), 1oโฉ)) <N
((1st โโจ((1st โ๐ด) +N
1o), 1oโฉ) ยทN
(2nd โ๐ด))
โ (1st โ๐ด) <N
(((1st โ๐ด)
+N 1o) ยทN
(2nd โ๐ด)))) |
46 | 34, 45 | bitrd 279 |
. . 3
โข (๐ด โ Q โ
(๐ด
<Q โจ((1st โ๐ด) +N
1o), 1oโฉ โ (1st โ๐ด) <N
(((1st โ๐ด)
+N 1o) ยทN
(2nd โ๐ด)))) |
47 | 30, 46 | mpbird 257 |
. 2
โข (๐ด โ Q โ
๐ด
<Q โจ((1st โ๐ด) +N
1o), 1oโฉ) |
48 | | opeq1 4835 |
. . . 4
โข (๐ฅ = ((1st โ๐ด) +N
1o) โ โจ๐ฅ, 1oโฉ =
โจ((1st โ๐ด) +N
1o), 1oโฉ) |
49 | 48 | breq2d 5122 |
. . 3
โข (๐ฅ = ((1st โ๐ด) +N
1o) โ (๐ด
<Q โจ๐ฅ, 1oโฉ โ ๐ด <Q
โจ((1st โ๐ด) +N
1o), 1oโฉ)) |
50 | 49 | rspcev 3584 |
. 2
โข
((((1st โ๐ด) +N 1o)
โ N โง ๐ด <Q
โจ((1st โ๐ด) +N
1o), 1oโฉ) โ โ๐ฅ โ N ๐ด <Q โจ๐ฅ,
1oโฉ) |
51 | 6, 47, 50 | syl2anc 585 |
1
โข (๐ด โ Q โ
โ๐ฅ โ
N ๐ด
<Q โจ๐ฅ, 1oโฉ) |