Step | Hyp | Ref
| Expression |
1 | | cevathlem1.a |
. . . . 5
โข (๐ โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) |
2 | 1 | simp2d 1143 |
. . . 4
โข (๐ โ ๐ต โ โ) |
3 | | cevathlem1.b |
. . . . 5
โข (๐ โ (๐ท โ โ โง ๐ธ โ โ โง ๐น โ โ)) |
4 | 3 | simp3d 1144 |
. . . 4
โข (๐ โ ๐น โ โ) |
5 | 2, 4 | mulcld 11133 |
. . 3
โข (๐ โ (๐ต ยท ๐น) โ โ) |
6 | | cevathlem1.c |
. . . 4
โข (๐ โ (๐บ โ โ โง ๐ป โ โ โง ๐พ โ โ)) |
7 | 6 | simp2d 1143 |
. . 3
โข (๐ โ ๐ป โ โ) |
8 | 5, 7 | mulcld 11133 |
. 2
โข (๐ โ ((๐ต ยท ๐น) ยท ๐ป) โ โ) |
9 | 3 | simp1d 1142 |
. . . 4
โข (๐ โ ๐ท โ โ) |
10 | 6 | simp1d 1142 |
. . . 4
โข (๐ โ ๐บ โ โ) |
11 | 9, 10 | mulcld 11133 |
. . 3
โข (๐ โ (๐ท ยท ๐บ) โ โ) |
12 | 6 | simp3d 1144 |
. . 3
โข (๐ โ ๐พ โ โ) |
13 | 11, 12 | mulcld 11133 |
. 2
โข (๐ โ ((๐ท ยท ๐บ) ยท ๐พ) โ โ) |
14 | 1 | simp1d 1142 |
. . . 4
โข (๐ โ ๐ด โ โ) |
15 | 3 | simp2d 1143 |
. . . 4
โข (๐ โ ๐ธ โ โ) |
16 | 14, 15 | mulcld 11133 |
. . 3
โข (๐ โ (๐ด ยท ๐ธ) โ โ) |
17 | 1 | simp3d 1144 |
. . 3
โข (๐ โ ๐ถ โ โ) |
18 | 16, 17 | mulcld 11133 |
. 2
โข (๐ โ ((๐ด ยท ๐ธ) ยท ๐ถ) โ โ) |
19 | | cevathlem1.d |
. . . . 5
โข (๐ โ (๐ด โ 0 โง ๐ธ โ 0 โง ๐ถ โ 0)) |
20 | 19 | simp1d 1142 |
. . . 4
โข (๐ โ ๐ด โ 0) |
21 | 19 | simp2d 1143 |
. . . 4
โข (๐ โ ๐ธ โ 0) |
22 | 14, 15, 20, 21 | mulne0d 11765 |
. . 3
โข (๐ โ (๐ด ยท ๐ธ) โ 0) |
23 | 19 | simp3d 1144 |
. . 3
โข (๐ โ ๐ถ โ 0) |
24 | 16, 17, 22, 23 | mulne0d 11765 |
. 2
โข (๐ โ ((๐ด ยท ๐ธ) ยท ๐ถ) โ 0) |
25 | | cevathlem1.e |
. . . . . . . 8
โข (๐ โ ((๐ด ยท ๐ต) = (๐ถ ยท ๐ท) โง (๐ธ ยท ๐น) = (๐ด ยท ๐บ) โง (๐ถ ยท ๐ป) = (๐ธ ยท ๐พ))) |
26 | 25 | simp1d 1142 |
. . . . . . 7
โข (๐ โ (๐ด ยท ๐ต) = (๐ถ ยท ๐ท)) |
27 | 25 | simp2d 1143 |
. . . . . . 7
โข (๐ โ (๐ธ ยท ๐น) = (๐ด ยท ๐บ)) |
28 | 26, 27 | oveq12d 7369 |
. . . . . 6
โข (๐ โ ((๐ด ยท ๐ต) ยท (๐ธ ยท ๐น)) = ((๐ถ ยท ๐ท) ยท (๐ด ยท ๐บ))) |
29 | 14, 2, 15, 4 | mul4d 11325 |
. . . . . 6
โข (๐ โ ((๐ด ยท ๐ต) ยท (๐ธ ยท ๐น)) = ((๐ด ยท ๐ธ) ยท (๐ต ยท ๐น))) |
30 | 17, 9, 14, 10 | mul4d 11325 |
. . . . . 6
โข (๐ โ ((๐ถ ยท ๐ท) ยท (๐ด ยท ๐บ)) = ((๐ถ ยท ๐ด) ยท (๐ท ยท ๐บ))) |
31 | 28, 29, 30 | 3eqtr3d 2785 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐ธ) ยท (๐ต ยท ๐น)) = ((๐ถ ยท ๐ด) ยท (๐ท ยท ๐บ))) |
32 | 25 | simp3d 1144 |
. . . . 5
โข (๐ โ (๐ถ ยท ๐ป) = (๐ธ ยท ๐พ)) |
33 | 31, 32 | oveq12d 7369 |
. . . 4
โข (๐ โ (((๐ด ยท ๐ธ) ยท (๐ต ยท ๐น)) ยท (๐ถ ยท ๐ป)) = (((๐ถ ยท ๐ด) ยท (๐ท ยท ๐บ)) ยท (๐ธ ยท ๐พ))) |
34 | 16, 5, 17, 7 | mul4d 11325 |
. . . 4
โข (๐ โ (((๐ด ยท ๐ธ) ยท (๐ต ยท ๐น)) ยท (๐ถ ยท ๐ป)) = (((๐ด ยท ๐ธ) ยท ๐ถ) ยท ((๐ต ยท ๐น) ยท ๐ป))) |
35 | 17, 14 | mulcld 11133 |
. . . . 5
โข (๐ โ (๐ถ ยท ๐ด) โ โ) |
36 | 35, 11, 15, 12 | mul4d 11325 |
. . . 4
โข (๐ โ (((๐ถ ยท ๐ด) ยท (๐ท ยท ๐บ)) ยท (๐ธ ยท ๐พ)) = (((๐ถ ยท ๐ด) ยท ๐ธ) ยท ((๐ท ยท ๐บ) ยท ๐พ))) |
37 | 33, 34, 36 | 3eqtr3d 2785 |
. . 3
โข (๐ โ (((๐ด ยท ๐ธ) ยท ๐ถ) ยท ((๐ต ยท ๐น) ยท ๐ป)) = (((๐ถ ยท ๐ด) ยท ๐ธ) ยท ((๐ท ยท ๐บ) ยท ๐พ))) |
38 | 14, 15, 17 | mul32d 11323 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐ธ) ยท ๐ถ) = ((๐ด ยท ๐ถ) ยท ๐ธ)) |
39 | 14, 17 | mulcomd 11134 |
. . . . . 6
โข (๐ โ (๐ด ยท ๐ถ) = (๐ถ ยท ๐ด)) |
40 | 39 | oveq1d 7366 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐ถ) ยท ๐ธ) = ((๐ถ ยท ๐ด) ยท ๐ธ)) |
41 | 38, 40 | eqtrd 2777 |
. . . 4
โข (๐ โ ((๐ด ยท ๐ธ) ยท ๐ถ) = ((๐ถ ยท ๐ด) ยท ๐ธ)) |
42 | 41 | oveq1d 7366 |
. . 3
โข (๐ โ (((๐ด ยท ๐ธ) ยท ๐ถ) ยท ((๐ท ยท ๐บ) ยท ๐พ)) = (((๐ถ ยท ๐ด) ยท ๐ธ) ยท ((๐ท ยท ๐บ) ยท ๐พ))) |
43 | 37, 42 | eqtr4d 2780 |
. 2
โข (๐ โ (((๐ด ยท ๐ธ) ยท ๐ถ) ยท ((๐ต ยท ๐น) ยท ๐ป)) = (((๐ด ยท ๐ธ) ยท ๐ถ) ยท ((๐ท ยท ๐บ) ยท ๐พ))) |
44 | 8, 13, 18, 24, 43 | mulcanad 11748 |
1
โข (๐ โ ((๐ต ยท ๐น) ยท ๐ป) = ((๐ท ยท ๐บ) ยท ๐พ)) |