Step | Hyp | Ref
| Expression |
1 | | omopthlem1.1 |
. . . . 5
โข ๐ด โ ฯ |
2 | | peano2 7883 |
. . . . 5
โข (๐ด โ ฯ โ suc ๐ด โ
ฯ) |
3 | 1, 2 | ax-mp 5 |
. . . 4
โข suc ๐ด โ ฯ |
4 | | omopthlem1.2 |
. . . 4
โข ๐ถ โ ฯ |
5 | | nnmwordi 8637 |
. . . 4
โข ((suc
๐ด โ ฯ โง
๐ถ โ ฯ โง suc
๐ด โ ฯ) โ
(suc ๐ด โ ๐ถ โ (suc ๐ด ยทo suc ๐ด) โ (suc ๐ด ยทo ๐ถ))) |
6 | 3, 4, 3, 5 | mp3an 1459 |
. . 3
โข (suc
๐ด โ ๐ถ โ (suc ๐ด ยทo suc ๐ด) โ (suc ๐ด ยทo ๐ถ)) |
7 | | nnmwordri 8638 |
. . . 4
โข ((suc
๐ด โ ฯ โง
๐ถ โ ฯ โง
๐ถ โ ฯ) โ
(suc ๐ด โ ๐ถ โ (suc ๐ด ยทo ๐ถ) โ (๐ถ ยทo ๐ถ))) |
8 | 3, 4, 4, 7 | mp3an 1459 |
. . 3
โข (suc
๐ด โ ๐ถ โ (suc ๐ด ยทo ๐ถ) โ (๐ถ ยทo ๐ถ)) |
9 | 6, 8 | sstrd 3991 |
. 2
โข (suc
๐ด โ ๐ถ โ (suc ๐ด ยทo suc ๐ด) โ (๐ถ ยทo ๐ถ)) |
10 | 1 | nnoni 7864 |
. . 3
โข ๐ด โ On |
11 | 4 | nnoni 7864 |
. . 3
โข ๐ถ โ On |
12 | 10, 11 | onsucssi 7832 |
. 2
โข (๐ด โ ๐ถ โ suc ๐ด โ ๐ถ) |
13 | 1, 1 | nnmcli 8617 |
. . . . . 6
โข (๐ด ยทo ๐ด) โ
ฯ |
14 | | 2onn 8643 |
. . . . . . 7
โข
2o โ ฯ |
15 | 1, 14 | nnmcli 8617 |
. . . . . 6
โข (๐ด ยทo
2o) โ ฯ |
16 | 13, 15 | nnacli 8616 |
. . . . 5
โข ((๐ด ยทo ๐ด) +o (๐ด ยทo
2o)) โ ฯ |
17 | 16 | nnoni 7864 |
. . . 4
โข ((๐ด ยทo ๐ด) +o (๐ด ยทo
2o)) โ On |
18 | 4, 4 | nnmcli 8617 |
. . . . 5
โข (๐ถ ยทo ๐ถ) โ
ฯ |
19 | 18 | nnoni 7864 |
. . . 4
โข (๐ถ ยทo ๐ถ) โ On |
20 | 17, 19 | onsucssi 7832 |
. . 3
โข (((๐ด ยทo ๐ด) +o (๐ด ยทo
2o)) โ (๐ถ
ยทo ๐ถ)
โ suc ((๐ด
ยทo ๐ด)
+o (๐ด
ยทo 2o)) โ (๐ถ ยทo ๐ถ)) |
21 | 3, 1 | nnmcli 8617 |
. . . . . 6
โข (suc
๐ด ยทo
๐ด) โ
ฯ |
22 | | nnasuc 8608 |
. . . . . 6
โข (((suc
๐ด ยทo
๐ด) โ ฯ โง
๐ด โ ฯ) โ
((suc ๐ด
ยทo ๐ด)
+o suc ๐ด) = suc
((suc ๐ด
ยทo ๐ด)
+o ๐ด)) |
23 | 21, 1, 22 | mp2an 688 |
. . . . 5
โข ((suc
๐ด ยทo
๐ด) +o suc ๐ด) = suc ((suc ๐ด ยทo ๐ด) +o ๐ด) |
24 | | nnmsuc 8609 |
. . . . . 6
โข ((suc
๐ด โ ฯ โง
๐ด โ ฯ) โ
(suc ๐ด ยทo
suc ๐ด) = ((suc ๐ด ยทo ๐ด) +o suc ๐ด)) |
25 | 3, 1, 24 | mp2an 688 |
. . . . 5
โข (suc
๐ด ยทo suc
๐ด) = ((suc ๐ด ยทo ๐ด) +o suc ๐ด) |
26 | | nnaass 8624 |
. . . . . . . 8
โข (((๐ด ยทo ๐ด) โ ฯ โง ๐ด โ ฯ โง ๐ด โ ฯ) โ (((๐ด ยทo ๐ด) +o ๐ด) +o ๐ด) = ((๐ด ยทo ๐ด) +o (๐ด +o ๐ด))) |
27 | 13, 1, 1, 26 | mp3an 1459 |
. . . . . . 7
โข (((๐ด ยทo ๐ด) +o ๐ด) +o ๐ด) = ((๐ด ยทo ๐ด) +o (๐ด +o ๐ด)) |
28 | | nnmcom 8628 |
. . . . . . . . . 10
โข ((suc
๐ด โ ฯ โง
๐ด โ ฯ) โ
(suc ๐ด ยทo
๐ด) = (๐ด ยทo suc ๐ด)) |
29 | 3, 1, 28 | mp2an 688 |
. . . . . . . . 9
โข (suc
๐ด ยทo
๐ด) = (๐ด ยทo suc ๐ด) |
30 | | nnmsuc 8609 |
. . . . . . . . . 10
โข ((๐ด โ ฯ โง ๐ด โ ฯ) โ (๐ด ยทo suc ๐ด) = ((๐ด ยทo ๐ด) +o ๐ด)) |
31 | 1, 1, 30 | mp2an 688 |
. . . . . . . . 9
โข (๐ด ยทo suc ๐ด) = ((๐ด ยทo ๐ด) +o ๐ด) |
32 | 29, 31 | eqtri 2758 |
. . . . . . . 8
โข (suc
๐ด ยทo
๐ด) = ((๐ด ยทo ๐ด) +o ๐ด) |
33 | 32 | oveq1i 7421 |
. . . . . . 7
โข ((suc
๐ด ยทo
๐ด) +o ๐ด) = (((๐ด ยทo ๐ด) +o ๐ด) +o ๐ด) |
34 | | nnm2 8654 |
. . . . . . . . 9
โข (๐ด โ ฯ โ (๐ด ยทo
2o) = (๐ด
+o ๐ด)) |
35 | 1, 34 | ax-mp 5 |
. . . . . . . 8
โข (๐ด ยทo
2o) = (๐ด
+o ๐ด) |
36 | 35 | oveq2i 7422 |
. . . . . . 7
โข ((๐ด ยทo ๐ด) +o (๐ด ยทo
2o)) = ((๐ด
ยทo ๐ด)
+o (๐ด
+o ๐ด)) |
37 | 27, 33, 36 | 3eqtr4ri 2769 |
. . . . . 6
โข ((๐ด ยทo ๐ด) +o (๐ด ยทo
2o)) = ((suc ๐ด
ยทo ๐ด)
+o ๐ด) |
38 | | suceq 6429 |
. . . . . 6
โข (((๐ด ยทo ๐ด) +o (๐ด ยทo
2o)) = ((suc ๐ด
ยทo ๐ด)
+o ๐ด) โ suc
((๐ด ยทo
๐ด) +o (๐ด ยทo
2o)) = suc ((suc ๐ด ยทo ๐ด) +o ๐ด)) |
39 | 37, 38 | ax-mp 5 |
. . . . 5
โข suc
((๐ด ยทo
๐ด) +o (๐ด ยทo
2o)) = suc ((suc ๐ด ยทo ๐ด) +o ๐ด) |
40 | 23, 25, 39 | 3eqtr4ri 2769 |
. . . 4
โข suc
((๐ด ยทo
๐ด) +o (๐ด ยทo
2o)) = (suc ๐ด
ยทo suc ๐ด) |
41 | 40 | sseq1i 4009 |
. . 3
โข (suc
((๐ด ยทo
๐ด) +o (๐ด ยทo
2o)) โ (๐ถ
ยทo ๐ถ)
โ (suc ๐ด
ยทo suc ๐ด)
โ (๐ถ
ยทo ๐ถ)) |
42 | 20, 41 | bitri 274 |
. 2
โข (((๐ด ยทo ๐ด) +o (๐ด ยทo
2o)) โ (๐ถ
ยทo ๐ถ)
โ (suc ๐ด
ยทo suc ๐ด)
โ (๐ถ
ยทo ๐ถ)) |
43 | 9, 12, 42 | 3imtr4i 291 |
1
โข (๐ด โ ๐ถ โ ((๐ด ยทo ๐ด) +o (๐ด ยทo 2o)) โ
(๐ถ ยทo
๐ถ)) |