Step | Hyp | Ref
| Expression |
1 | | oveq2 7412 |
. . . . 5
โข (๐ฅ = ๐ต โ (suc ๐ด ยทo ๐ฅ) = (suc ๐ด ยทo ๐ต)) |
2 | | oveq2 7412 |
. . . . . 6
โข (๐ฅ = ๐ต โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐ต)) |
3 | | id 22 |
. . . . . 6
โข (๐ฅ = ๐ต โ ๐ฅ = ๐ต) |
4 | 2, 3 | oveq12d 7422 |
. . . . 5
โข (๐ฅ = ๐ต โ ((๐ด ยทo ๐ฅ) +o ๐ฅ) = ((๐ด ยทo ๐ต) +o ๐ต)) |
5 | 1, 4 | eqeq12d 2749 |
. . . 4
โข (๐ฅ = ๐ต โ ((suc ๐ด ยทo ๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ฅ) โ (suc ๐ด ยทo ๐ต) = ((๐ด ยทo ๐ต) +o ๐ต))) |
6 | 5 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ต โ ((๐ด โ ฯ โ (suc ๐ด ยทo ๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ฅ)) โ (๐ด โ ฯ โ (suc ๐ด ยทo ๐ต) = ((๐ด ยทo ๐ต) +o ๐ต)))) |
7 | | oveq2 7412 |
. . . . 5
โข (๐ฅ = โ
โ (suc ๐ด ยทo ๐ฅ) = (suc ๐ด ยทo
โ
)) |
8 | | oveq2 7412 |
. . . . . 6
โข (๐ฅ = โ
โ (๐ด ยทo ๐ฅ) = (๐ด ยทo
โ
)) |
9 | | id 22 |
. . . . . 6
โข (๐ฅ = โ
โ ๐ฅ = โ
) |
10 | 8, 9 | oveq12d 7422 |
. . . . 5
โข (๐ฅ = โ
โ ((๐ด ยทo ๐ฅ) +o ๐ฅ) = ((๐ด ยทo โ
) +o
โ
)) |
11 | 7, 10 | eqeq12d 2749 |
. . . 4
โข (๐ฅ = โ
โ ((suc ๐ด ยทo ๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ฅ) โ (suc ๐ด ยทo โ
) = ((๐ด ยทo โ
)
+o โ
))) |
12 | | oveq2 7412 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (suc ๐ด ยทo ๐ฅ) = (suc ๐ด ยทo ๐ฆ)) |
13 | | oveq2 7412 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐ฆ)) |
14 | | id 22 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ๐ฅ = ๐ฆ) |
15 | 13, 14 | oveq12d 7422 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((๐ด ยทo ๐ฅ) +o ๐ฅ) = ((๐ด ยทo ๐ฆ) +o ๐ฆ)) |
16 | 12, 15 | eqeq12d 2749 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((suc ๐ด ยทo ๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ฅ) โ (suc ๐ด ยทo ๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ฆ))) |
17 | | oveq2 7412 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ (suc ๐ด ยทo ๐ฅ) = (suc ๐ด ยทo suc ๐ฆ)) |
18 | | oveq2 7412 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo suc ๐ฆ)) |
19 | | id 22 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ ๐ฅ = suc ๐ฆ) |
20 | 18, 19 | oveq12d 7422 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ ((๐ด ยทo ๐ฅ) +o ๐ฅ) = ((๐ด ยทo suc ๐ฆ) +o suc ๐ฆ)) |
21 | 17, 20 | eqeq12d 2749 |
. . . 4
โข (๐ฅ = suc ๐ฆ โ ((suc ๐ด ยทo ๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ฅ) โ (suc ๐ด ยทo suc ๐ฆ) = ((๐ด ยทo suc ๐ฆ) +o suc ๐ฆ))) |
22 | | peano2 7876 |
. . . . . . 7
โข (๐ด โ ฯ โ suc ๐ด โ
ฯ) |
23 | | nnm0 8601 |
. . . . . . 7
โข (suc
๐ด โ ฯ โ
(suc ๐ด ยทo
โ
) = โ
) |
24 | 22, 23 | syl 17 |
. . . . . 6
โข (๐ด โ ฯ โ (suc
๐ด ยทo
โ
) = โ
) |
25 | | nnm0 8601 |
. . . . . 6
โข (๐ด โ ฯ โ (๐ด ยทo โ
) =
โ
) |
26 | 24, 25 | eqtr4d 2776 |
. . . . 5
โข (๐ด โ ฯ โ (suc
๐ด ยทo
โ
) = (๐ด
ยทo โ
)) |
27 | | peano1 7874 |
. . . . . . 7
โข โ
โ ฯ |
28 | | nnmcl 8608 |
. . . . . . 7
โข ((๐ด โ ฯ โง โ
โ ฯ) โ (๐ด
ยทo โ
) โ ฯ) |
29 | 27, 28 | mpan2 690 |
. . . . . 6
โข (๐ด โ ฯ โ (๐ด ยทo โ
)
โ ฯ) |
30 | | nna0 8600 |
. . . . . 6
โข ((๐ด ยทo โ
)
โ ฯ โ ((๐ด
ยทo โ
) +o โ
) = (๐ด ยทo
โ
)) |
31 | 29, 30 | syl 17 |
. . . . 5
โข (๐ด โ ฯ โ ((๐ด ยทo โ
)
+o โ
) = (๐ด
ยทo โ
)) |
32 | 26, 31 | eqtr4d 2776 |
. . . 4
โข (๐ด โ ฯ โ (suc
๐ด ยทo
โ
) = ((๐ด
ยทo โ
) +o โ
)) |
33 | | oveq1 7411 |
. . . . . 6
โข ((suc
๐ด ยทo
๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ฆ) โ ((suc ๐ด ยทo ๐ฆ) +o suc ๐ด) = (((๐ด ยทo ๐ฆ) +o ๐ฆ) +o suc ๐ด)) |
34 | | peano2b 7867 |
. . . . . . . 8
โข (๐ด โ ฯ โ suc ๐ด โ
ฯ) |
35 | | nnmsuc 8603 |
. . . . . . . 8
โข ((suc
๐ด โ ฯ โง
๐ฆ โ ฯ) โ
(suc ๐ด ยทo
suc ๐ฆ) = ((suc ๐ด ยทo ๐ฆ) +o suc ๐ด)) |
36 | 34, 35 | sylanb 582 |
. . . . . . 7
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (suc
๐ด ยทo suc
๐ฆ) = ((suc ๐ด ยทo ๐ฆ) +o suc ๐ด)) |
37 | | nnmcl 8608 |
. . . . . . . . . . 11
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (๐ด ยทo ๐ฆ) โ
ฯ) |
38 | | peano2b 7867 |
. . . . . . . . . . . 12
โข (๐ฆ โ ฯ โ suc ๐ฆ โ
ฯ) |
39 | | nnaass 8618 |
. . . . . . . . . . . 12
โข (((๐ด ยทo ๐ฆ) โ ฯ โง ๐ด โ ฯ โง suc ๐ฆ โ ฯ) โ (((๐ด ยทo ๐ฆ) +o ๐ด) +o suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o (๐ด +o suc ๐ฆ))) |
40 | 38, 39 | syl3an3b 1406 |
. . . . . . . . . . 11
โข (((๐ด ยทo ๐ฆ) โ ฯ โง ๐ด โ ฯ โง ๐ฆ โ ฯ) โ (((๐ด ยทo ๐ฆ) +o ๐ด) +o suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o (๐ด +o suc ๐ฆ))) |
41 | 37, 40 | syl3an1 1164 |
. . . . . . . . . 10
โข (((๐ด โ ฯ โง ๐ฆ โ ฯ) โง ๐ด โ ฯ โง ๐ฆ โ ฯ) โ (((๐ด ยทo ๐ฆ) +o ๐ด) +o suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o (๐ด +o suc ๐ฆ))) |
42 | 41 | 3expb 1121 |
. . . . . . . . 9
โข (((๐ด โ ฯ โง ๐ฆ โ ฯ) โง (๐ด โ ฯ โง ๐ฆ โ ฯ)) โ
(((๐ด ยทo
๐ฆ) +o ๐ด) +o suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o (๐ด +o suc ๐ฆ))) |
43 | 42 | anidms 568 |
. . . . . . . 8
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (((๐ด ยทo ๐ฆ) +o ๐ด) +o suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o (๐ด +o suc ๐ฆ))) |
44 | | nnmsuc 8603 |
. . . . . . . . 9
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (๐ด ยทo suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ด)) |
45 | 44 | oveq1d 7419 |
. . . . . . . 8
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ ((๐ด ยทo suc ๐ฆ) +o suc ๐ฆ) = (((๐ด ยทo ๐ฆ) +o ๐ด) +o suc ๐ฆ)) |
46 | | nnaass 8618 |
. . . . . . . . . . . . . 14
โข (((๐ด ยทo ๐ฆ) โ ฯ โง ๐ฆ โ ฯ โง suc ๐ด โ ฯ) โ (((๐ด ยทo ๐ฆ) +o ๐ฆ) +o suc ๐ด) = ((๐ด ยทo ๐ฆ) +o (๐ฆ +o suc ๐ด))) |
47 | 34, 46 | syl3an3b 1406 |
. . . . . . . . . . . . 13
โข (((๐ด ยทo ๐ฆ) โ ฯ โง ๐ฆ โ ฯ โง ๐ด โ ฯ) โ (((๐ด ยทo ๐ฆ) +o ๐ฆ) +o suc ๐ด) = ((๐ด ยทo ๐ฆ) +o (๐ฆ +o suc ๐ด))) |
48 | 37, 47 | syl3an1 1164 |
. . . . . . . . . . . 12
โข (((๐ด โ ฯ โง ๐ฆ โ ฯ) โง ๐ฆ โ ฯ โง ๐ด โ ฯ) โ (((๐ด ยทo ๐ฆ) +o ๐ฆ) +o suc ๐ด) = ((๐ด ยทo ๐ฆ) +o (๐ฆ +o suc ๐ด))) |
49 | 48 | 3expb 1121 |
. . . . . . . . . . 11
โข (((๐ด โ ฯ โง ๐ฆ โ ฯ) โง (๐ฆ โ ฯ โง ๐ด โ ฯ)) โ
(((๐ด ยทo
๐ฆ) +o ๐ฆ) +o suc ๐ด) = ((๐ด ยทo ๐ฆ) +o (๐ฆ +o suc ๐ด))) |
50 | 49 | an42s 660 |
. . . . . . . . . 10
โข (((๐ด โ ฯ โง ๐ฆ โ ฯ) โง (๐ด โ ฯ โง ๐ฆ โ ฯ)) โ
(((๐ด ยทo
๐ฆ) +o ๐ฆ) +o suc ๐ด) = ((๐ด ยทo ๐ฆ) +o (๐ฆ +o suc ๐ด))) |
51 | 50 | anidms 568 |
. . . . . . . . 9
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (((๐ด ยทo ๐ฆ) +o ๐ฆ) +o suc ๐ด) = ((๐ด ยทo ๐ฆ) +o (๐ฆ +o suc ๐ด))) |
52 | | nnacom 8613 |
. . . . . . . . . . . 12
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (๐ด +o ๐ฆ) = (๐ฆ +o ๐ด)) |
53 | | suceq 6427 |
. . . . . . . . . . . 12
โข ((๐ด +o ๐ฆ) = (๐ฆ +o ๐ด) โ suc (๐ด +o ๐ฆ) = suc (๐ฆ +o ๐ด)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ suc
(๐ด +o ๐ฆ) = suc (๐ฆ +o ๐ด)) |
55 | | nnasuc 8602 |
. . . . . . . . . . 11
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (๐ด +o suc ๐ฆ) = suc (๐ด +o ๐ฆ)) |
56 | | nnasuc 8602 |
. . . . . . . . . . . 12
โข ((๐ฆ โ ฯ โง ๐ด โ ฯ) โ (๐ฆ +o suc ๐ด) = suc (๐ฆ +o ๐ด)) |
57 | 56 | ancoms 460 |
. . . . . . . . . . 11
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (๐ฆ +o suc ๐ด) = suc (๐ฆ +o ๐ด)) |
58 | 54, 55, 57 | 3eqtr4d 2783 |
. . . . . . . . . 10
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (๐ด +o suc ๐ฆ) = (๐ฆ +o suc ๐ด)) |
59 | 58 | oveq2d 7420 |
. . . . . . . . 9
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ ((๐ด ยทo ๐ฆ) +o (๐ด +o suc ๐ฆ)) = ((๐ด ยทo ๐ฆ) +o (๐ฆ +o suc ๐ด))) |
60 | 51, 59 | eqtr4d 2776 |
. . . . . . . 8
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ (((๐ด ยทo ๐ฆ) +o ๐ฆ) +o suc ๐ด) = ((๐ด ยทo ๐ฆ) +o (๐ด +o suc ๐ฆ))) |
61 | 43, 45, 60 | 3eqtr4d 2783 |
. . . . . . 7
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ ((๐ด ยทo suc ๐ฆ) +o suc ๐ฆ) = (((๐ด ยทo ๐ฆ) +o ๐ฆ) +o suc ๐ด)) |
62 | 36, 61 | eqeq12d 2749 |
. . . . . 6
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ ((suc
๐ด ยทo suc
๐ฆ) = ((๐ด ยทo suc ๐ฆ) +o suc ๐ฆ) โ ((suc ๐ด ยทo ๐ฆ) +o suc ๐ด) = (((๐ด ยทo ๐ฆ) +o ๐ฆ) +o suc ๐ด))) |
63 | 33, 62 | imbitrrid 245 |
. . . . 5
โข ((๐ด โ ฯ โง ๐ฆ โ ฯ) โ ((suc
๐ด ยทo
๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ฆ) โ (suc ๐ด ยทo suc ๐ฆ) = ((๐ด ยทo suc ๐ฆ) +o suc ๐ฆ))) |
64 | 63 | expcom 415 |
. . . 4
โข (๐ฆ โ ฯ โ (๐ด โ ฯ โ ((suc
๐ด ยทo
๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ฆ) โ (suc ๐ด ยทo suc ๐ฆ) = ((๐ด ยทo suc ๐ฆ) +o suc ๐ฆ)))) |
65 | 11, 16, 21, 32, 64 | finds2 7886 |
. . 3
โข (๐ฅ โ ฯ โ (๐ด โ ฯ โ (suc
๐ด ยทo
๐ฅ) = ((๐ด ยทo ๐ฅ) +o ๐ฅ))) |
66 | 6, 65 | vtoclga 3565 |
. 2
โข (๐ต โ ฯ โ (๐ด โ ฯ โ (suc
๐ด ยทo
๐ต) = ((๐ด ยทo ๐ต) +o ๐ต))) |
67 | 66 | impcom 409 |
1
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (suc
๐ด ยทo
๐ต) = ((๐ด ยทo ๐ต) +o ๐ต)) |