Step | Hyp | Ref
| Expression |
1 | | nqpi 7377 |
. 2
โข (๐ด โ Q โ
โ๐งโ๐ค((๐ง โ N โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q
)) |
2 | | 1pi 7314 |
. . . . . . 7
โข
1o โ N |
3 | | addclpi 7326 |
. . . . . . 7
โข ((๐ง โ N โง
1o โ N) โ (๐ง +N 1o)
โ N) |
4 | 2, 3 | mpan2 425 |
. . . . . 6
โข (๐ง โ N โ
(๐ง
+N 1o) โ
N) |
5 | 4 | adantr 276 |
. . . . 5
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง
+N 1o) โ
N) |
6 | 5 | adantr 276 |
. . . 4
โข (((๐ง โ N โง
๐ค โ N)
โง ๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โ
(๐ง
+N 1o) โ
N) |
7 | | pinn 7308 |
. . . . . . . . . . . . . 14
โข (๐ง โ N โ
๐ง โ
ฯ) |
8 | | 1onn 6521 |
. . . . . . . . . . . . . 14
โข
1o โ ฯ |
9 | | nnacl 6481 |
. . . . . . . . . . . . . 14
โข ((๐ง โ ฯ โง
1o โ ฯ) โ (๐ง +o 1o) โ
ฯ) |
10 | 7, 8, 9 | sylancl 413 |
. . . . . . . . . . . . 13
โข (๐ง โ N โ
(๐ง +o
1o) โ ฯ) |
11 | 10 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง +o
1o) โ ฯ) |
12 | | nnm1 6526 |
. . . . . . . . . . . 12
โข ((๐ง +o 1o)
โ ฯ โ ((๐ง
+o 1o) ยทo 1o) = (๐ง +o
1o)) |
13 | 11, 12 | syl 14 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
๐ค โ N)
โ ((๐ง +o
1o) ยทo 1o) = (๐ง +o
1o)) |
14 | | elni2 7313 |
. . . . . . . . . . . . . 14
โข (๐ค โ N โ
(๐ค โ ฯ โง
โ
โ ๐ค)) |
15 | | nnord 4612 |
. . . . . . . . . . . . . . 15
โข (๐ค โ ฯ โ Ord ๐ค) |
16 | | ordgt0ge1 6436 |
. . . . . . . . . . . . . . . 16
โข (Ord
๐ค โ (โ
โ
๐ค โ 1o
โ ๐ค)) |
17 | 16 | biimpa 296 |
. . . . . . . . . . . . . . 15
โข ((Ord
๐ค โง โ
โ
๐ค) โ 1o
โ ๐ค) |
18 | 15, 17 | sylan 283 |
. . . . . . . . . . . . . 14
โข ((๐ค โ ฯ โง โ
โ ๐ค) โ
1o โ ๐ค) |
19 | 14, 18 | sylbi 121 |
. . . . . . . . . . . . 13
โข (๐ค โ N โ
1o โ ๐ค) |
20 | 19 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ง โ N โง
๐ค โ N)
โ 1o โ ๐ค) |
21 | | pinn 7308 |
. . . . . . . . . . . . . 14
โข (๐ค โ N โ
๐ค โ
ฯ) |
22 | 21 | adantl 277 |
. . . . . . . . . . . . 13
โข ((๐ง โ N โง
๐ค โ N)
โ ๐ค โ
ฯ) |
23 | | nnaword1 6514 |
. . . . . . . . . . . . . . . 16
โข ((๐ง โ ฯ โง
1o โ ฯ) โ ๐ง โ (๐ง +o
1o)) |
24 | 7, 8, 23 | sylancl 413 |
. . . . . . . . . . . . . . 15
โข (๐ง โ N โ
๐ง โ (๐ง +o
1o)) |
25 | | elni2 7313 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ N โ
(๐ง โ ฯ โง
โ
โ ๐ง)) |
26 | 25 | simprbi 275 |
. . . . . . . . . . . . . . 15
โข (๐ง โ N โ
โ
โ ๐ง) |
27 | 24, 26 | sseldd 3157 |
. . . . . . . . . . . . . 14
โข (๐ง โ N โ
โ
โ (๐ง
+o 1o)) |
28 | 27 | adantr 276 |
. . . . . . . . . . . . 13
โข ((๐ง โ N โง
๐ค โ N)
โ โ
โ (๐ง
+o 1o)) |
29 | | nnmword 6519 |
. . . . . . . . . . . . . 14
โข
(((1o โ ฯ โง ๐ค โ ฯ โง (๐ง +o 1o) โ ฯ)
โง โ
โ (๐ง
+o 1o)) โ (1o โ ๐ค โ ((๐ง +o 1o)
ยทo 1o) โ ((๐ง +o 1o)
ยทo ๐ค))) |
30 | 8, 29 | mp3anl1 1331 |
. . . . . . . . . . . . 13
โข (((๐ค โ ฯ โง (๐ง +o 1o)
โ ฯ) โง โ
โ (๐ง +o 1o)) โ
(1o โ ๐ค
โ ((๐ง +o
1o) ยทo 1o) โ ((๐ง +o 1o)
ยทo ๐ค))) |
31 | 22, 11, 28, 30 | syl21anc 1237 |
. . . . . . . . . . . 12
โข ((๐ง โ N โง
๐ค โ N)
โ (1o โ ๐ค โ ((๐ง +o 1o)
ยทo 1o) โ ((๐ง +o 1o)
ยทo ๐ค))) |
32 | 20, 31 | mpbid 147 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
๐ค โ N)
โ ((๐ง +o
1o) ยทo 1o) โ ((๐ง +o 1o)
ยทo ๐ค)) |
33 | 13, 32 | eqsstrrd 3193 |
. . . . . . . . . 10
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง +o
1o) โ ((๐ง
+o 1o) ยทo ๐ค)) |
34 | | nna0 6475 |
. . . . . . . . . . . . 13
โข (๐ง โ ฯ โ (๐ง +o โ
) = ๐ง) |
35 | | 0lt1o 6441 |
. . . . . . . . . . . . . 14
โข โ
โ 1o |
36 | | nnaordi 6509 |
. . . . . . . . . . . . . . 15
โข
((1o โ ฯ โง ๐ง โ ฯ) โ (โ
โ
1o โ (๐ง
+o โ
) โ (๐ง +o
1o))) |
37 | 8, 36 | mpan 424 |
. . . . . . . . . . . . . 14
โข (๐ง โ ฯ โ (โ
โ 1o โ (๐ง +o โ
) โ (๐ง +o
1o))) |
38 | 35, 37 | mpi 15 |
. . . . . . . . . . . . 13
โข (๐ง โ ฯ โ (๐ง +o โ
) โ
(๐ง +o
1o)) |
39 | 34, 38 | eqeltrrd 2255 |
. . . . . . . . . . . 12
โข (๐ง โ ฯ โ ๐ง โ (๐ง +o
1o)) |
40 | 7, 39 | syl 14 |
. . . . . . . . . . 11
โข (๐ง โ N โ
๐ง โ (๐ง +o
1o)) |
41 | 40 | adantr 276 |
. . . . . . . . . 10
โข ((๐ง โ N โง
๐ค โ N)
โ ๐ง โ (๐ง +o
1o)) |
42 | 33, 41 | sseldd 3157 |
. . . . . . . . 9
โข ((๐ง โ N โง
๐ค โ N)
โ ๐ง โ ((๐ง +o 1o)
ยทo ๐ค)) |
43 | | mulclpi 7327 |
. . . . . . . . . . . 12
โข (((๐ง +N
1o) โ N โง ๐ค โ N) โ ((๐ง +N
1o) ยทN ๐ค) โ N) |
44 | 4, 43 | sylan 283 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
๐ค โ N)
โ ((๐ง
+N 1o) ยทN
๐ค) โ
N) |
45 | | ltpiord 7318 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
((๐ง
+N 1o) ยทN
๐ค) โ N)
โ (๐ง
<N ((๐ง +N 1o)
ยทN ๐ค) โ ๐ง โ ((๐ง +N 1o)
ยทN ๐ค))) |
46 | 44, 45 | syldan 282 |
. . . . . . . . . 10
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง
<N ((๐ง +N 1o)
ยทN ๐ค) โ ๐ง โ ((๐ง +N 1o)
ยทN ๐ค))) |
47 | | mulpiord 7316 |
. . . . . . . . . . . . 13
โข (((๐ง +N
1o) โ N โง ๐ค โ N) โ ((๐ง +N
1o) ยทN ๐ค) = ((๐ง +N 1o)
ยทo ๐ค)) |
48 | 4, 47 | sylan 283 |
. . . . . . . . . . . 12
โข ((๐ง โ N โง
๐ค โ N)
โ ((๐ง
+N 1o) ยทN
๐ค) = ((๐ง +N 1o)
ยทo ๐ค)) |
49 | | addpiord 7315 |
. . . . . . . . . . . . . . 15
โข ((๐ง โ N โง
1o โ N) โ (๐ง +N 1o) =
(๐ง +o
1o)) |
50 | 2, 49 | mpan2 425 |
. . . . . . . . . . . . . 14
โข (๐ง โ N โ
(๐ง
+N 1o) = (๐ง +o
1o)) |
51 | 50 | adantr 276 |
. . . . . . . . . . . . 13
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง
+N 1o) = (๐ง +o
1o)) |
52 | 51 | oveq1d 5890 |
. . . . . . . . . . . 12
โข ((๐ง โ N โง
๐ค โ N)
โ ((๐ง
+N 1o) ยทo ๐ค) = ((๐ง +o 1o)
ยทo ๐ค)) |
53 | 48, 52 | eqtrd 2210 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
๐ค โ N)
โ ((๐ง
+N 1o) ยทN
๐ค) = ((๐ง +o 1o)
ยทo ๐ค)) |
54 | 53 | eleq2d 2247 |
. . . . . . . . . 10
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง โ ((๐ง +N
1o) ยทN ๐ค) โ ๐ง โ ((๐ง +o 1o)
ยทo ๐ค))) |
55 | 46, 54 | bitrd 188 |
. . . . . . . . 9
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง
<N ((๐ง +N 1o)
ยทN ๐ค) โ ๐ง โ ((๐ง +o 1o)
ยทo ๐ค))) |
56 | 42, 55 | mpbird 167 |
. . . . . . . 8
โข ((๐ง โ N โง
๐ค โ N)
โ ๐ง
<N ((๐ง +N 1o)
ยทN ๐ค)) |
57 | | mulcompig 7330 |
. . . . . . . . . 10
โข (((๐ง +N
1o) โ N โง ๐ค โ N) โ ((๐ง +N
1o) ยทN ๐ค) = (๐ค ยทN (๐ง +N
1o))) |
58 | 4, 57 | sylan 283 |
. . . . . . . . 9
โข ((๐ง โ N โง
๐ค โ N)
โ ((๐ง
+N 1o) ยทN
๐ค) = (๐ค ยทN (๐ง +N
1o))) |
59 | 58 | breq2d 4016 |
. . . . . . . 8
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง
<N ((๐ง +N 1o)
ยทN ๐ค) โ ๐ง <N (๐ค
ยทN (๐ง +N
1o)))) |
60 | 56, 59 | mpbid 147 |
. . . . . . 7
โข ((๐ง โ N โง
๐ค โ N)
โ ๐ง
<N (๐ค ยทN (๐ง +N
1o))) |
61 | 5, 2 | jctir 313 |
. . . . . . . . 9
โข ((๐ง โ N โง
๐ค โ N)
โ ((๐ง
+N 1o) โ N โง
1o โ N)) |
62 | | ordpipqqs 7373 |
. . . . . . . . 9
โข (((๐ง โ N โง
๐ค โ N)
โง ((๐ง
+N 1o) โ N โง
1o โ N)) โ ([โจ๐ง, ๐คโฉ] ~Q
<Q [โจ(๐ง +N 1o),
1oโฉ] ~Q โ (๐ง ยทN
1o) <N (๐ค ยทN (๐ง +N
1o)))) |
63 | 61, 62 | mpdan 421 |
. . . . . . . 8
โข ((๐ง โ N โง
๐ค โ N)
โ ([โจ๐ง, ๐คโฉ]
~Q <Q [โจ(๐ง +N
1o), 1oโฉ] ~Q โ (๐ง
ยทN 1o)
<N (๐ค ยทN (๐ง +N
1o)))) |
64 | | mulidpi 7317 |
. . . . . . . . . 10
โข (๐ง โ N โ
(๐ง
ยทN 1o) = ๐ง) |
65 | 64 | adantr 276 |
. . . . . . . . 9
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง
ยทN 1o) = ๐ง) |
66 | 65 | breq1d 4014 |
. . . . . . . 8
โข ((๐ง โ N โง
๐ค โ N)
โ ((๐ง
ยทN 1o)
<N (๐ค ยทN (๐ง +N
1o)) โ ๐ง
<N (๐ค ยทN (๐ง +N
1o)))) |
67 | 63, 66 | bitrd 188 |
. . . . . . 7
โข ((๐ง โ N โง
๐ค โ N)
โ ([โจ๐ง, ๐คโฉ]
~Q <Q [โจ(๐ง +N
1o), 1oโฉ] ~Q โ ๐ง <N
(๐ค
ยทN (๐ง +N
1o)))) |
68 | 60, 67 | mpbird 167 |
. . . . . 6
โข ((๐ง โ N โง
๐ค โ N)
โ [โจ๐ง, ๐คโฉ]
~Q <Q [โจ(๐ง +N
1o), 1oโฉ] ~Q
) |
69 | 68 | adantr 276 |
. . . . 5
โข (((๐ง โ N โง
๐ค โ N)
โง ๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โ
[โจ๐ง, ๐คโฉ]
~Q <Q [โจ(๐ง +N
1o), 1oโฉ] ~Q
) |
70 | | breq1 4007 |
. . . . . 6
โข (๐ด = [โจ๐ง, ๐คโฉ] ~Q โ
(๐ด
<Q [โจ(๐ง +N 1o),
1oโฉ] ~Q โ [โจ๐ง, ๐คโฉ] ~Q
<Q [โจ(๐ง +N 1o),
1oโฉ] ~Q )) |
71 | 70 | adantl 277 |
. . . . 5
โข (((๐ง โ N โง
๐ค โ N)
โง ๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โ
(๐ด
<Q [โจ(๐ง +N 1o),
1oโฉ] ~Q โ [โจ๐ง, ๐คโฉ] ~Q
<Q [โจ(๐ง +N 1o),
1oโฉ] ~Q )) |
72 | 69, 71 | mpbird 167 |
. . . 4
โข (((๐ง โ N โง
๐ค โ N)
โง ๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โ
๐ด
<Q [โจ(๐ง +N 1o),
1oโฉ] ~Q ) |
73 | | opeq1 3779 |
. . . . . . 7
โข (๐ฅ = (๐ง +N 1o)
โ โจ๐ฅ,
1oโฉ = โจ(๐ง +N 1o),
1oโฉ) |
74 | 73 | eceq1d 6571 |
. . . . . 6
โข (๐ฅ = (๐ง +N 1o)
โ [โจ๐ฅ,
1oโฉ] ~Q = [โจ(๐ง +N 1o),
1oโฉ] ~Q ) |
75 | 74 | breq2d 4016 |
. . . . 5
โข (๐ฅ = (๐ง +N 1o)
โ (๐ด
<Q [โจ๐ฅ, 1oโฉ]
~Q โ ๐ด <Q
[โจ(๐ง
+N 1o), 1oโฉ]
~Q )) |
76 | 75 | rspcev 2842 |
. . . 4
โข (((๐ง +N
1o) โ N โง ๐ด <Q
[โจ(๐ง
+N 1o), 1oโฉ]
~Q ) โ โ๐ฅ โ N ๐ด <Q [โจ๐ฅ, 1oโฉ]
~Q ) |
77 | 6, 72, 76 | syl2anc 411 |
. . 3
โข (((๐ง โ N โง
๐ค โ N)
โง ๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โ
โ๐ฅ โ
N ๐ด
<Q [โจ๐ฅ, 1oโฉ]
~Q ) |
78 | 77 | exlimivv 1896 |
. 2
โข
(โ๐งโ๐ค((๐ง โ N โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โ
โ๐ฅ โ
N ๐ด
<Q [โจ๐ฅ, 1oโฉ]
~Q ) |
79 | 1, 78 | syl 14 |
1
โข (๐ด โ Q โ
โ๐ฅ โ
N ๐ด
<Q [โจ๐ฅ, 1oโฉ]
~Q ) |