Step | Hyp | Ref
| Expression |
1 | | omopthlem2.3 |
. . . . . . 7
โข ๐ถ โ ฯ |
2 | 1, 1 | nnmcli 8615 |
. . . . . 6
โข (๐ถ ยทo ๐ถ) โ
ฯ |
3 | | omopthlem2.4 |
. . . . . 6
โข ๐ท โ ฯ |
4 | 2, 3 | nnacli 8614 |
. . . . 5
โข ((๐ถ ยทo ๐ถ) +o ๐ท) โ
ฯ |
5 | 4 | nnoni 7862 |
. . . 4
โข ((๐ถ ยทo ๐ถ) +o ๐ท) โ On |
6 | 5 | onirri 6478 |
. . 3
โข ยฌ
((๐ถ ยทo
๐ถ) +o ๐ท) โ ((๐ถ ยทo ๐ถ) +o ๐ท) |
7 | | eleq1 2822 |
. . 3
โข (((๐ถ ยทo ๐ถ) +o ๐ท) = (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ (((๐ถ ยทo ๐ถ) +o ๐ท) โ ((๐ถ ยทo ๐ถ) +o ๐ท) โ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ ((๐ถ ยทo ๐ถ) +o ๐ท))) |
8 | 6, 7 | mtbii 326 |
. 2
โข (((๐ถ ยทo ๐ถ) +o ๐ท) = (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ ยฌ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ ((๐ถ ยทo ๐ถ) +o ๐ท)) |
9 | | nnaword1 8629 |
. . . 4
โข (((๐ถ ยทo ๐ถ) โ ฯ โง ๐ท โ ฯ) โ (๐ถ ยทo ๐ถ) โ ((๐ถ ยทo ๐ถ) +o ๐ท)) |
10 | 2, 3, 9 | mp2an 691 |
. . 3
โข (๐ถ ยทo ๐ถ) โ ((๐ถ ยทo ๐ถ) +o ๐ท) |
11 | | omopthlem2.2 |
. . . . . . . . 9
โข ๐ต โ ฯ |
12 | | omopthlem2.1 |
. . . . . . . . . . 11
โข ๐ด โ ฯ |
13 | 12, 11 | nnacli 8614 |
. . . . . . . . . 10
โข (๐ด +o ๐ต) โ ฯ |
14 | 13, 12 | nnacli 8614 |
. . . . . . . . 9
โข ((๐ด +o ๐ต) +o ๐ด) โ ฯ |
15 | | nnaword1 8629 |
. . . . . . . . 9
โข ((๐ต โ ฯ โง ((๐ด +o ๐ต) +o ๐ด) โ ฯ) โ ๐ต โ (๐ต +o ((๐ด +o ๐ต) +o ๐ด))) |
16 | 11, 14, 15 | mp2an 691 |
. . . . . . . 8
โข ๐ต โ (๐ต +o ((๐ด +o ๐ต) +o ๐ด)) |
17 | | nnacom 8617 |
. . . . . . . . 9
โข ((๐ต โ ฯ โง ((๐ด +o ๐ต) +o ๐ด) โ ฯ) โ (๐ต +o ((๐ด +o ๐ต) +o ๐ด)) = (((๐ด +o ๐ต) +o ๐ด) +o ๐ต)) |
18 | 11, 14, 17 | mp2an 691 |
. . . . . . . 8
โข (๐ต +o ((๐ด +o ๐ต) +o ๐ด)) = (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) |
19 | 16, 18 | sseqtri 4019 |
. . . . . . 7
โข ๐ต โ (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) |
20 | | nnaass 8622 |
. . . . . . . . 9
โข (((๐ด +o ๐ต) โ ฯ โง ๐ด โ ฯ โง ๐ต โ ฯ) โ (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต))) |
21 | 13, 12, 11, 20 | mp3an 1462 |
. . . . . . . 8
โข (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) = ((๐ด +o ๐ต) +o (๐ด +o ๐ต)) |
22 | | nnm2 8652 |
. . . . . . . . 9
โข ((๐ด +o ๐ต) โ ฯ โ ((๐ด +o ๐ต) ยทo 2o) =
((๐ด +o ๐ต) +o (๐ด +o ๐ต))) |
23 | 13, 22 | ax-mp 5 |
. . . . . . . 8
โข ((๐ด +o ๐ต) ยทo 2o) =
((๐ด +o ๐ต) +o (๐ด +o ๐ต)) |
24 | 21, 23 | eqtr4i 2764 |
. . . . . . 7
โข (((๐ด +o ๐ต) +o ๐ด) +o ๐ต) = ((๐ด +o ๐ต) ยทo
2o) |
25 | 19, 24 | sseqtri 4019 |
. . . . . 6
โข ๐ต โ ((๐ด +o ๐ต) ยทo
2o) |
26 | | 2onn 8641 |
. . . . . . . 8
โข
2o โ ฯ |
27 | 13, 26 | nnmcli 8615 |
. . . . . . 7
โข ((๐ด +o ๐ต) ยทo 2o) โ
ฯ |
28 | 13, 13 | nnmcli 8615 |
. . . . . . 7
โข ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โ ฯ |
29 | | nnawordi 8621 |
. . . . . . 7
โข ((๐ต โ ฯ โง ((๐ด +o ๐ต) ยทo 2o) โ
ฯ โง ((๐ด
+o ๐ต)
ยทo (๐ด
+o ๐ต)) โ
ฯ) โ (๐ต โ
((๐ด +o ๐ต) ยทo
2o) โ (๐ต
+o ((๐ด
+o ๐ต)
ยทo (๐ด
+o ๐ต))) โ
(((๐ด +o ๐ต) ยทo
2o) +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))))) |
30 | 11, 27, 28, 29 | mp3an 1462 |
. . . . . 6
โข (๐ต โ ((๐ด +o ๐ต) ยทo 2o) โ
(๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))) โ (((๐ด +o ๐ต) ยทo 2o)
+o ((๐ด
+o ๐ต)
ยทo (๐ด
+o ๐ต)))) |
31 | 25, 30 | ax-mp 5 |
. . . . 5
โข (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))) โ (((๐ด +o ๐ต) ยทo 2o)
+o ((๐ด
+o ๐ต)
ยทo (๐ด
+o ๐ต))) |
32 | | nnacom 8617 |
. . . . . 6
โข ((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โ ฯ โง ๐ต โ ฯ) โ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)))) |
33 | 28, 11, 32 | mp2an 691 |
. . . . 5
โข (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (๐ต +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))) |
34 | | nnacom 8617 |
. . . . . 6
โข ((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) โ ฯ โง ((๐ด +o ๐ต) ยทo 2o) โ
ฯ) โ (((๐ด
+o ๐ต)
ยทo (๐ด
+o ๐ต))
+o ((๐ด
+o ๐ต)
ยทo 2o)) = (((๐ด +o ๐ต) ยทo 2o)
+o ((๐ด
+o ๐ต)
ยทo (๐ด
+o ๐ต)))) |
35 | 28, 27, 34 | mp2an 691 |
. . . . 5
โข (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) =
(((๐ด +o ๐ต) ยทo
2o) +o ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต))) |
36 | 31, 33, 35 | 3sstr4i 4026 |
. . . 4
โข (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo
2o)) |
37 | 13, 1 | omopthlem1 8658 |
. . . 4
โข ((๐ด +o ๐ต) โ ๐ถ โ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o))
โ (๐ถ
ยทo ๐ถ)) |
38 | 28, 11 | nnacli 8614 |
. . . . . 6
โข (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ ฯ |
39 | 38 | nnoni 7862 |
. . . . 5
โข (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ On |
40 | 2 | nnoni 7862 |
. . . . 5
โข (๐ถ ยทo ๐ถ) โ On |
41 | | ontr2 6412 |
. . . . 5
โข
(((((๐ด +o
๐ต) ยทo
(๐ด +o ๐ต)) +o ๐ต) โ On โง (๐ถ ยทo ๐ถ) โ On) โ (((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) โง
(((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o))
โ (๐ถ
ยทo ๐ถ))
โ (((๐ด +o
๐ต) ยทo
(๐ด +o ๐ต)) +o ๐ต) โ (๐ถ ยทo ๐ถ))) |
42 | 39, 40, 41 | mp2an 691 |
. . . 4
โข
(((((๐ด +o
๐ต) ยทo
(๐ด +o ๐ต)) +o ๐ต) โ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o)) โง
(((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ((๐ด +o ๐ต) ยทo 2o))
โ (๐ถ
ยทo ๐ถ))
โ (((๐ด +o
๐ต) ยทo
(๐ด +o ๐ต)) +o ๐ต) โ (๐ถ ยทo ๐ถ)) |
43 | 36, 37, 42 | sylancr 588 |
. . 3
โข ((๐ด +o ๐ต) โ ๐ถ โ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ (๐ถ ยทo ๐ถ)) |
44 | 10, 43 | sselid 3981 |
. 2
โข ((๐ด +o ๐ต) โ ๐ถ โ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) โ ((๐ถ ยทo ๐ถ) +o ๐ท)) |
45 | 8, 44 | nsyl3 138 |
1
โข ((๐ด +o ๐ต) โ ๐ถ โ ยฌ ((๐ถ ยทo ๐ถ) +o ๐ท) = (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต)) |