Step | Hyp | Ref
| Expression |
1 | | nq0nn 7440 |
. 2
โข (๐ด โ
Q0 โ โ๐คโ๐ฃ((๐ค โ ฯ โง ๐ฃ โ N) โง ๐ด = [โจ๐ค, ๐ฃโฉ] ~Q0
)) |
2 | | df-0nq0 7424 |
. . . . . 6
โข
0Q0 = [โจโ
, 1oโฉ]
~Q0 |
3 | | oveq12 5883 |
. . . . . 6
โข ((๐ด = [โจ๐ค, ๐ฃโฉ] ~Q0 โง
0Q0 = [โจโ
, 1oโฉ]
~Q0 ) โ (๐ด +Q0
0Q0) = ([โจ๐ค, ๐ฃโฉ] ~Q0
+Q0 [โจโ
, 1oโฉ]
~Q0 )) |
4 | 2, 3 | mpan2 425 |
. . . . 5
โข (๐ด = [โจ๐ค, ๐ฃโฉ] ~Q0 โ
(๐ด
+Q0 0Q0) = ([โจ๐ค, ๐ฃโฉ] ~Q0
+Q0 [โจโ
, 1oโฉ]
~Q0 )) |
5 | | peano1 4593 |
. . . . . 6
โข โ
โ ฯ |
6 | | 1pi 7313 |
. . . . . 6
โข
1o โ N |
7 | | addnnnq0 7447 |
. . . . . 6
โข (((๐ค โ ฯ โง ๐ฃ โ N) โง
(โ
โ ฯ โง 1o โ N)) โ
([โจ๐ค, ๐ฃโฉ]
~Q0 +Q0 [โจโ
,
1oโฉ] ~Q0 ) = [โจ((๐ค ยทo
1o) +o (๐ฃ ยทo โ
)), (๐ฃ ยทo
1o)โฉ] ~Q0 ) |
8 | 5, 6, 7 | mpanr12 439 |
. . . . 5
โข ((๐ค โ ฯ โง ๐ฃ โ N) โ
([โจ๐ค, ๐ฃโฉ]
~Q0 +Q0 [โจโ
,
1oโฉ] ~Q0 ) = [โจ((๐ค ยทo
1o) +o (๐ฃ ยทo โ
)), (๐ฃ ยทo
1o)โฉ] ~Q0 ) |
9 | 4, 8 | sylan9eqr 2232 |
. . . 4
โข (((๐ค โ ฯ โง ๐ฃ โ N) โง
๐ด = [โจ๐ค, ๐ฃโฉ] ~Q0 ) โ
(๐ด
+Q0 0Q0) = [โจ((๐ค ยทo
1o) +o (๐ฃ ยทo โ
)), (๐ฃ ยทo
1o)โฉ] ~Q0 ) |
10 | | pinn 7307 |
. . . . . . . . . 10
โข (๐ฃ โ N โ
๐ฃ โ
ฯ) |
11 | | nnm0 6475 |
. . . . . . . . . . 11
โข (๐ฃ โ ฯ โ (๐ฃ ยทo โ
) =
โ
) |
12 | 11 | oveq2d 5890 |
. . . . . . . . . 10
โข (๐ฃ โ ฯ โ ((๐ค ยทo
1o) +o (๐ฃ ยทo โ
)) = ((๐ค ยทo
1o) +o โ
)) |
13 | 10, 12 | syl 14 |
. . . . . . . . 9
โข (๐ฃ โ N โ
((๐ค ยทo
1o) +o (๐ฃ ยทo โ
)) = ((๐ค ยทo
1o) +o โ
)) |
14 | | nnm1 6525 |
. . . . . . . . . . 11
โข (๐ค โ ฯ โ (๐ค ยทo
1o) = ๐ค) |
15 | 14 | oveq1d 5889 |
. . . . . . . . . 10
โข (๐ค โ ฯ โ ((๐ค ยทo
1o) +o โ
) = (๐ค +o โ
)) |
16 | | nna0 6474 |
. . . . . . . . . 10
โข (๐ค โ ฯ โ (๐ค +o โ
) = ๐ค) |
17 | 15, 16 | eqtrd 2210 |
. . . . . . . . 9
โข (๐ค โ ฯ โ ((๐ค ยทo
1o) +o โ
) = ๐ค) |
18 | 13, 17 | sylan9eqr 2232 |
. . . . . . . 8
โข ((๐ค โ ฯ โง ๐ฃ โ N) โ
((๐ค ยทo
1o) +o (๐ฃ ยทo โ
)) = ๐ค) |
19 | | nnm1 6525 |
. . . . . . . . . 10
โข (๐ฃ โ ฯ โ (๐ฃ ยทo
1o) = ๐ฃ) |
20 | 10, 19 | syl 14 |
. . . . . . . . 9
โข (๐ฃ โ N โ
(๐ฃ ยทo
1o) = ๐ฃ) |
21 | 20 | adantl 277 |
. . . . . . . 8
โข ((๐ค โ ฯ โง ๐ฃ โ N) โ
(๐ฃ ยทo
1o) = ๐ฃ) |
22 | 18, 21 | opeq12d 3786 |
. . . . . . 7
โข ((๐ค โ ฯ โง ๐ฃ โ N) โ
โจ((๐ค
ยทo 1o) +o (๐ฃ ยทo โ
)), (๐ฃ ยทo
1o)โฉ = โจ๐ค, ๐ฃโฉ) |
23 | 22 | eceq1d 6570 |
. . . . . 6
โข ((๐ค โ ฯ โง ๐ฃ โ N) โ
[โจ((๐ค
ยทo 1o) +o (๐ฃ ยทo โ
)), (๐ฃ ยทo
1o)โฉ] ~Q0 = [โจ๐ค, ๐ฃโฉ] ~Q0
) |
24 | 23 | eqeq2d 2189 |
. . . . 5
โข ((๐ค โ ฯ โง ๐ฃ โ N) โ
(๐ด = [โจ((๐ค ยทo
1o) +o (๐ฃ ยทo โ
)), (๐ฃ ยทo
1o)โฉ] ~Q0 โ ๐ด = [โจ๐ค, ๐ฃโฉ] ~Q0
)) |
25 | 24 | biimpar 297 |
. . . 4
โข (((๐ค โ ฯ โง ๐ฃ โ N) โง
๐ด = [โจ๐ค, ๐ฃโฉ] ~Q0 ) โ
๐ด = [โจ((๐ค ยทo
1o) +o (๐ฃ ยทo โ
)), (๐ฃ ยทo
1o)โฉ] ~Q0 ) |
26 | 9, 25 | eqtr4d 2213 |
. . 3
โข (((๐ค โ ฯ โง ๐ฃ โ N) โง
๐ด = [โจ๐ค, ๐ฃโฉ] ~Q0 ) โ
(๐ด
+Q0 0Q0) = ๐ด) |
27 | 26 | exlimivv 1896 |
. 2
โข
(โ๐คโ๐ฃ((๐ค โ ฯ โง ๐ฃ โ N) โง ๐ด = [โจ๐ค, ๐ฃโฉ] ~Q0 ) โ
(๐ด
+Q0 0Q0) = ๐ด) |
28 | 1, 27 | syl 14 |
1
โข (๐ด โ
Q0 โ (๐ด +Q0
0Q0) = ๐ด) |