Step | Hyp | Ref
| Expression |
1 | | oveq1 7364 |
. . . . . 6
โข (๐ด = if(๐ด โ ฯ, ๐ด, โ
) โ (๐ด +o ๐ต) = (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต)) |
2 | 1, 1 | oveq12d 7375 |
. . . . 5
โข (๐ด = if(๐ด โ ฯ, ๐ด, โ
) โ ((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) = ((if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต) ยทo (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต))) |
3 | 2 | oveq1d 7372 |
. . . 4
โข (๐ด = if(๐ด โ ฯ, ๐ด, โ
) โ (((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (((if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต) ยทo (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต)) +o ๐ต)) |
4 | 3 | eqeq1d 2738 |
. . 3
โข (๐ด = if(๐ด โ ฯ, ๐ด, โ
) โ ((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) โ (((if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต) ยทo (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต)) +o ๐ต) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท))) |
5 | | eqeq1 2740 |
. . . 4
โข (๐ด = if(๐ด โ ฯ, ๐ด, โ
) โ (๐ด = ๐ถ โ if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ)) |
6 | 5 | anbi1d 630 |
. . 3
โข (๐ด = if(๐ด โ ฯ, ๐ด, โ
) โ ((๐ด = ๐ถ โง ๐ต = ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ โง ๐ต = ๐ท))) |
7 | 4, 6 | bibi12d 345 |
. 2
โข (๐ด = if(๐ด โ ฯ, ๐ด, โ
) โ (((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) โ (๐ด = ๐ถ โง ๐ต = ๐ท)) โ ((((if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต) ยทo (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต)) +o ๐ต) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ โง ๐ต = ๐ท)))) |
8 | | oveq2 7365 |
. . . . . 6
โข (๐ต = if(๐ต โ ฯ, ๐ต, โ
) โ (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต) = (if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
))) |
9 | 8, 8 | oveq12d 7375 |
. . . . 5
โข (๐ต = if(๐ต โ ฯ, ๐ต, โ
) โ ((if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต) ยทo (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต)) = ((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
)))) |
10 | | id 22 |
. . . . 5
โข (๐ต = if(๐ต โ ฯ, ๐ต, โ
) โ ๐ต = if(๐ต โ ฯ, ๐ต, โ
)) |
11 | 9, 10 | oveq12d 7375 |
. . . 4
โข (๐ต = if(๐ต โ ฯ, ๐ต, โ
) โ (((if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต) ยทo (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต)) +o ๐ต) = (((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
))) |
12 | 11 | eqeq1d 2738 |
. . 3
โข (๐ต = if(๐ต โ ฯ, ๐ต, โ
) โ ((((if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต) ยทo (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต)) +o ๐ต) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) โ (((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท))) |
13 | | eqeq1 2740 |
. . . 4
โข (๐ต = if(๐ต โ ฯ, ๐ต, โ
) โ (๐ต = ๐ท โ if(๐ต โ ฯ, ๐ต, โ
) = ๐ท)) |
14 | 13 | anbi2d 629 |
. . 3
โข (๐ต = if(๐ต โ ฯ, ๐ต, โ
) โ ((if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ โง ๐ต = ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ โง if(๐ต โ ฯ, ๐ต, โ
) = ๐ท))) |
15 | 12, 14 | bibi12d 345 |
. 2
โข (๐ต = if(๐ต โ ฯ, ๐ต, โ
) โ (((((if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต) ยทo (if(๐ด โ ฯ, ๐ด, โ
) +o ๐ต)) +o ๐ต) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ โง ๐ต = ๐ท)) โ ((((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ โง if(๐ต โ ฯ, ๐ต, โ
) = ๐ท)))) |
16 | | oveq1 7364 |
. . . . . 6
โข (๐ถ = if(๐ถ โ ฯ, ๐ถ, โ
) โ (๐ถ +o ๐ท) = (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท)) |
17 | 16, 16 | oveq12d 7375 |
. . . . 5
โข (๐ถ = if(๐ถ โ ฯ, ๐ถ, โ
) โ ((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) = ((if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท) ยทo (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท))) |
18 | 17 | oveq1d 7372 |
. . . 4
โข (๐ถ = if(๐ถ โ ฯ, ๐ถ, โ
) โ (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) = (((if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท) ยทo (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท)) +o ๐ท)) |
19 | 18 | eqeq2d 2747 |
. . 3
โข (๐ถ = if(๐ถ โ ฯ, ๐ถ, โ
) โ ((((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) โ (((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท) ยทo (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท)) +o ๐ท))) |
20 | | eqeq2 2748 |
. . . 4
โข (๐ถ = if(๐ถ โ ฯ, ๐ถ, โ
) โ (if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ โ if(๐ด โ ฯ, ๐ด, โ
) = if(๐ถ โ ฯ, ๐ถ, โ
))) |
21 | 20 | anbi1d 630 |
. . 3
โข (๐ถ = if(๐ถ โ ฯ, ๐ถ, โ
) โ ((if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ โง if(๐ต โ ฯ, ๐ต, โ
) = ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = if(๐ถ โ ฯ, ๐ถ, โ
) โง if(๐ต โ ฯ, ๐ต, โ
) = ๐ท))) |
22 | 19, 21 | bibi12d 345 |
. 2
โข (๐ถ = if(๐ถ โ ฯ, ๐ถ, โ
) โ (((((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = ๐ถ โง if(๐ต โ ฯ, ๐ต, โ
) = ๐ท)) โ ((((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท) ยทo (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท)) +o ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = if(๐ถ โ ฯ, ๐ถ, โ
) โง if(๐ต โ ฯ, ๐ต, โ
) = ๐ท)))) |
23 | | oveq2 7365 |
. . . . . 6
โข (๐ท = if(๐ท โ ฯ, ๐ท, โ
) โ (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท) = (if(๐ถ โ ฯ, ๐ถ, โ
) +o if(๐ท โ ฯ, ๐ท, โ
))) |
24 | 23, 23 | oveq12d 7375 |
. . . . 5
โข (๐ท = if(๐ท โ ฯ, ๐ท, โ
) โ ((if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท) ยทo (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท)) = ((if(๐ถ โ ฯ, ๐ถ, โ
) +o if(๐ท โ ฯ, ๐ท, โ
)) ยทo
(if(๐ถ โ ฯ, ๐ถ, โ
) +o
if(๐ท โ ฯ, ๐ท, โ
)))) |
25 | | id 22 |
. . . . 5
โข (๐ท = if(๐ท โ ฯ, ๐ท, โ
) โ ๐ท = if(๐ท โ ฯ, ๐ท, โ
)) |
26 | 24, 25 | oveq12d 7375 |
. . . 4
โข (๐ท = if(๐ท โ ฯ, ๐ท, โ
) โ (((if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท) ยทo (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท)) +o ๐ท) = (((if(๐ถ โ ฯ, ๐ถ, โ
) +o if(๐ท โ ฯ, ๐ท, โ
)) ยทo
(if(๐ถ โ ฯ, ๐ถ, โ
) +o
if(๐ท โ ฯ, ๐ท, โ
))) +o
if(๐ท โ ฯ, ๐ท, โ
))) |
27 | 26 | eqeq2d 2747 |
. . 3
โข (๐ท = if(๐ท โ ฯ, ๐ท, โ
) โ ((((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท) ยทo (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท)) +o ๐ท) โ (((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((if(๐ถ โ ฯ, ๐ถ, โ
) +o
if(๐ท โ ฯ, ๐ท, โ
)) ยทo
(if(๐ถ โ ฯ, ๐ถ, โ
) +o
if(๐ท โ ฯ, ๐ท, โ
))) +o
if(๐ท โ ฯ, ๐ท, โ
)))) |
28 | | eqeq2 2748 |
. . . 4
โข (๐ท = if(๐ท โ ฯ, ๐ท, โ
) โ (if(๐ต โ ฯ, ๐ต, โ
) = ๐ท โ if(๐ต โ ฯ, ๐ต, โ
) = if(๐ท โ ฯ, ๐ท, โ
))) |
29 | 28 | anbi2d 629 |
. . 3
โข (๐ท = if(๐ท โ ฯ, ๐ท, โ
) โ ((if(๐ด โ ฯ, ๐ด, โ
) = if(๐ถ โ ฯ, ๐ถ, โ
) โง if(๐ต โ ฯ, ๐ต, โ
) = ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = if(๐ถ โ ฯ, ๐ถ, โ
) โง if(๐ต โ ฯ, ๐ต, โ
) = if(๐ท โ ฯ, ๐ท, โ
)))) |
30 | 27, 29 | bibi12d 345 |
. 2
โข (๐ท = if(๐ท โ ฯ, ๐ท, โ
) โ (((((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท) ยทo (if(๐ถ โ ฯ, ๐ถ, โ
) +o ๐ท)) +o ๐ท) โ (if(๐ด โ ฯ, ๐ด, โ
) = if(๐ถ โ ฯ, ๐ถ, โ
) โง if(๐ต โ ฯ, ๐ต, โ
) = ๐ท)) โ ((((if(๐ด โ ฯ, ๐ด, โ
) +o if(๐ต โ ฯ, ๐ต, โ
)) ยทo
(if(๐ด โ ฯ, ๐ด, โ
) +o
if(๐ต โ ฯ, ๐ต, โ
))) +o
if(๐ต โ ฯ, ๐ต, โ
)) = (((if(๐ถ โ ฯ, ๐ถ, โ
) +o
if(๐ท โ ฯ, ๐ท, โ
)) ยทo
(if(๐ถ โ ฯ, ๐ถ, โ
) +o
if(๐ท โ ฯ, ๐ท, โ
))) +o
if(๐ท โ ฯ, ๐ท, โ
)) โ (if(๐ด โ ฯ, ๐ด, โ
) = if(๐ถ โ ฯ, ๐ถ, โ
) โง if(๐ต โ ฯ, ๐ต, โ
) = if(๐ท โ ฯ, ๐ท, โ
))))) |
31 | | peano1 7825 |
. . . 4
โข โ
โ ฯ |
32 | 31 | elimel 4555 |
. . 3
โข if(๐ด โ ฯ, ๐ด, โ
) โ
ฯ |
33 | 31 | elimel 4555 |
. . 3
โข if(๐ต โ ฯ, ๐ต, โ
) โ
ฯ |
34 | 31 | elimel 4555 |
. . 3
โข if(๐ถ โ ฯ, ๐ถ, โ
) โ
ฯ |
35 | 31 | elimel 4555 |
. . 3
โข if(๐ท โ ฯ, ๐ท, โ
) โ
ฯ |
36 | 32, 33, 34, 35 | omopthi 8607 |
. 2
โข
((((if(๐ด โ
ฯ, ๐ด, โ
)
+o if(๐ต โ
ฯ, ๐ต, โ
))
ยทo (if(๐ด
โ ฯ, ๐ด, โ
)
+o if(๐ต โ
ฯ, ๐ต, โ
)))
+o if(๐ต โ
ฯ, ๐ต, โ
)) =
(((if(๐ถ โ ฯ,
๐ถ, โ
) +o
if(๐ท โ ฯ, ๐ท, โ
)) ยทo
(if(๐ถ โ ฯ, ๐ถ, โ
) +o
if(๐ท โ ฯ, ๐ท, โ
))) +o
if(๐ท โ ฯ, ๐ท, โ
)) โ (if(๐ด โ ฯ, ๐ด, โ
) = if(๐ถ โ ฯ, ๐ถ, โ
) โง if(๐ต โ ฯ, ๐ต, โ
) = if(๐ท โ ฯ, ๐ท, โ
))) |
37 | 7, 15, 22, 30, 36 | dedth4h 4547 |
1
โข (((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ถ โ ฯ โง ๐ท โ ฯ)) โ
((((๐ด +o ๐ต) ยทo (๐ด +o ๐ต)) +o ๐ต) = (((๐ถ +o ๐ท) ยทo (๐ถ +o ๐ท)) +o ๐ท) โ (๐ด = ๐ถ โง ๐ต = ๐ท))) |