Step | Hyp | Ref
| Expression |
1 | | oveq2 5883 |
. . . . . 6
โข (๐ฅ = ๐ถ โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = ((๐ด ยทo ๐ต) ยทo ๐ถ)) |
2 | | oveq2 5883 |
. . . . . . 7
โข (๐ฅ = ๐ถ โ (๐ต ยทo ๐ฅ) = (๐ต ยทo ๐ถ)) |
3 | 2 | oveq2d 5891 |
. . . . . 6
โข (๐ฅ = ๐ถ โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = (๐ด ยทo (๐ต ยทo ๐ถ))) |
4 | 1, 3 | eqeq12d 2192 |
. . . . 5
โข (๐ฅ = ๐ถ โ (((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)) โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ)))) |
5 | 4 | imbi2d 230 |
. . . 4
โข (๐ฅ = ๐ถ โ (((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ))) โ ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ))))) |
6 | | oveq2 5883 |
. . . . . 6
โข (๐ฅ = โ
โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = ((๐ด ยทo ๐ต) ยทo
โ
)) |
7 | | oveq2 5883 |
. . . . . . 7
โข (๐ฅ = โ
โ (๐ต ยทo ๐ฅ) = (๐ต ยทo
โ
)) |
8 | 7 | oveq2d 5891 |
. . . . . 6
โข (๐ฅ = โ
โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = (๐ด ยทo (๐ต ยทo
โ
))) |
9 | 6, 8 | eqeq12d 2192 |
. . . . 5
โข (๐ฅ = โ
โ (((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)) โ ((๐ด ยทo ๐ต) ยทo โ
) = (๐ด ยทo (๐ต ยทo
โ
)))) |
10 | | oveq2 5883 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = ((๐ด ยทo ๐ต) ยทo ๐ฆ)) |
11 | | oveq2 5883 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐ต ยทo ๐ฅ) = (๐ต ยทo ๐ฆ)) |
12 | 11 | oveq2d 5891 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = (๐ด ยทo (๐ต ยทo ๐ฆ))) |
13 | 10, 12 | eqeq12d 2192 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)) โ ((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)))) |
14 | | oveq2 5883 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = ((๐ด ยทo ๐ต) ยทo suc ๐ฆ)) |
15 | | oveq2 5883 |
. . . . . . 7
โข (๐ฅ = suc ๐ฆ โ (๐ต ยทo ๐ฅ) = (๐ต ยทo suc ๐ฆ)) |
16 | 15 | oveq2d 5891 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ (๐ด ยทo (๐ต ยทo ๐ฅ)) = (๐ด ยทo (๐ต ยทo suc ๐ฆ))) |
17 | 14, 16 | eqeq12d 2192 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ (((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)))) |
18 | | nnmcl 6482 |
. . . . . . 7
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (๐ด ยทo ๐ต) โ
ฯ) |
19 | | nnm0 6476 |
. . . . . . 7
โข ((๐ด ยทo ๐ต) โ ฯ โ ((๐ด ยทo ๐ต) ยทo โ
)
= โ
) |
20 | 18, 19 | syl 14 |
. . . . . 6
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) ยทo โ
)
= โ
) |
21 | | nnm0 6476 |
. . . . . . . 8
โข (๐ต โ ฯ โ (๐ต ยทo โ
) =
โ
) |
22 | 21 | oveq2d 5891 |
. . . . . . 7
โข (๐ต โ ฯ โ (๐ด ยทo (๐ต ยทo โ
))
= (๐ด ยทo
โ
)) |
23 | | nnm0 6476 |
. . . . . . 7
โข (๐ด โ ฯ โ (๐ด ยทo โ
) =
โ
) |
24 | 22, 23 | sylan9eqr 2232 |
. . . . . 6
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (๐ด ยทo (๐ต ยทo โ
))
= โ
) |
25 | 20, 24 | eqtr4d 2213 |
. . . . 5
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) ยทo โ
)
= (๐ด ยทo
(๐ต ยทo
โ
))) |
26 | | oveq1 5882 |
. . . . . . . . 9
โข (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) +o (๐ด ยทo ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
27 | | nnmsuc 6478 |
. . . . . . . . . . . 12
โข (((๐ด ยทo ๐ต) โ ฯ โง ๐ฆ โ ฯ) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (((๐ด ยทo ๐ต) ยทo ๐ฆ) +o (๐ด ยทo ๐ต))) |
28 | 18, 27 | sylan 283 |
. . . . . . . . . . 11
โข (((๐ด โ ฯ โง ๐ต โ ฯ) โง ๐ฆ โ ฯ) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (((๐ด ยทo ๐ต) ยทo ๐ฆ) +o (๐ด ยทo ๐ต))) |
29 | 28 | 3impa 1194 |
. . . . . . . . . 10
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ฆ โ ฯ) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (((๐ด ยทo ๐ต) ยทo ๐ฆ) +o (๐ด ยทo ๐ต))) |
30 | | nnmsuc 6478 |
. . . . . . . . . . . . 13
โข ((๐ต โ ฯ โง ๐ฆ โ ฯ) โ (๐ต ยทo suc ๐ฆ) = ((๐ต ยทo ๐ฆ) +o ๐ต)) |
31 | 30 | 3adant1 1015 |
. . . . . . . . . . . 12
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ฆ โ ฯ) โ (๐ต ยทo suc ๐ฆ) = ((๐ต ยทo ๐ฆ) +o ๐ต)) |
32 | 31 | oveq2d 5891 |
. . . . . . . . . . 11
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ฆ โ ฯ) โ (๐ด ยทo (๐ต ยทo suc ๐ฆ)) = (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต))) |
33 | | nnmcl 6482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ ฯ โง ๐ฆ โ ฯ) โ (๐ต ยทo ๐ฆ) โ
ฯ) |
34 | | nndi 6487 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ ฯ โง (๐ต ยทo ๐ฆ) โ ฯ โง ๐ต โ ฯ) โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
35 | 33, 34 | syl3an2 1272 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ ฯ โง (๐ต โ ฯ โง ๐ฆ โ ฯ) โง ๐ต โ ฯ) โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
36 | 35 | 3exp 1202 |
. . . . . . . . . . . . . . 15
โข (๐ด โ ฯ โ ((๐ต โ ฯ โง ๐ฆ โ ฯ) โ (๐ต โ ฯ โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))))) |
37 | 36 | expd 258 |
. . . . . . . . . . . . . 14
โข (๐ด โ ฯ โ (๐ต โ ฯ โ (๐ฆ โ ฯ โ (๐ต โ ฯ โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต)))))) |
38 | 37 | com34 83 |
. . . . . . . . . . . . 13
โข (๐ด โ ฯ โ (๐ต โ ฯ โ (๐ต โ ฯ โ (๐ฆ โ ฯ โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต)))))) |
39 | 38 | pm2.43d 50 |
. . . . . . . . . . . 12
โข (๐ด โ ฯ โ (๐ต โ ฯ โ (๐ฆ โ ฯ โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))))) |
40 | 39 | 3imp 1193 |
. . . . . . . . . . 11
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ฆ โ ฯ) โ (๐ด ยทo ((๐ต ยทo ๐ฆ) +o ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
41 | 32, 40 | eqtrd 2210 |
. . . . . . . . . 10
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ฆ โ ฯ) โ (๐ด ยทo (๐ต ยทo suc ๐ฆ)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต))) |
42 | 29, 41 | eqeq12d 2192 |
. . . . . . . . 9
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ฆ โ ฯ) โ (((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)) โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) +o (๐ด ยทo ๐ต)) = ((๐ด ยทo (๐ต ยทo ๐ฆ)) +o (๐ด ยทo ๐ต)))) |
43 | 26, 42 | imbitrrid 156 |
. . . . . . . 8
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ฆ โ ฯ) โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)))) |
44 | 43 | 3exp 1202 |
. . . . . . 7
โข (๐ด โ ฯ โ (๐ต โ ฯ โ (๐ฆ โ ฯ โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)))))) |
45 | 44 | com3r 79 |
. . . . . 6
โข (๐ฆ โ ฯ โ (๐ด โ ฯ โ (๐ต โ ฯ โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ)))))) |
46 | 45 | impd 254 |
. . . . 5
โข (๐ฆ โ ฯ โ ((๐ด โ ฯ โง ๐ต โ ฯ) โ (((๐ด ยทo ๐ต) ยทo ๐ฆ) = (๐ด ยทo (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ต) ยทo suc ๐ฆ) = (๐ด ยทo (๐ต ยทo suc ๐ฆ))))) |
47 | 9, 13, 17, 25, 46 | finds2 4601 |
. . . 4
โข (๐ฅ โ ฯ โ ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) ยทo ๐ฅ) = (๐ด ยทo (๐ต ยทo ๐ฅ)))) |
48 | 5, 47 | vtoclga 2804 |
. . 3
โข (๐ถ โ ฯ โ ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ)))) |
49 | 48 | expdcom 1442 |
. 2
โข (๐ด โ ฯ โ (๐ต โ ฯ โ (๐ถ โ ฯ โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ))))) |
50 | 49 | 3imp 1193 |
1
โข ((๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ) โ ((๐ด ยทo ๐ต) ยทo ๐ถ) = (๐ด ยทo (๐ต ยทo ๐ถ))) |