Step | Hyp | Ref
| Expression |
1 | | divmulassap 8665 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ ((๐ด ยท (๐ต / ๐ท)) ยท ๐ถ) = ((๐ด ยท ๐ต) ยท (๐ถ / ๐ท))) |
2 | | mulcom 7953 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
3 | 2 | 3adant3 1018 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
4 | 3 | adantr 276 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
5 | 4 | oveq1d 5903 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ ((๐ด ยท ๐ต) ยท (๐ถ / ๐ท)) = ((๐ต ยท ๐ด) ยท (๐ถ / ๐ท))) |
6 | | simpl2 1002 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ ๐ต โ โ) |
7 | | simpl1 1001 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ ๐ด โ โ) |
8 | | simp3 1000 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ถ โ
โ) |
9 | 8 | anim1i 340 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ (๐ถ โ โ โง (๐ท โ โ โง ๐ท # 0))) |
10 | | 3anass 983 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ท โ โ โง ๐ท # 0) โ (๐ถ โ โ โง (๐ท โ โ โง ๐ท # 0))) |
11 | 9, 10 | sylibr 134 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ (๐ถ โ โ โง ๐ท โ โ โง ๐ท # 0)) |
12 | | divclap 8648 |
. . . . 5
โข ((๐ถ โ โ โง ๐ท โ โ โง ๐ท # 0) โ (๐ถ / ๐ท) โ โ) |
13 | 11, 12 | syl 14 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ (๐ถ / ๐ท) โ โ) |
14 | 6, 7, 13 | mulassd 7994 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ ((๐ต ยท ๐ด) ยท (๐ถ / ๐ท)) = (๐ต ยท (๐ด ยท (๐ถ / ๐ท)))) |
15 | 8 | adantr 276 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ ๐ถ โ โ) |
16 | | simpr 110 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ (๐ท โ โ โง ๐ท # 0)) |
17 | | divassap 8660 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ โง (๐ท โ โ โง ๐ท # 0)) โ ((๐ด ยท ๐ถ) / ๐ท) = (๐ด ยท (๐ถ / ๐ท))) |
18 | 7, 15, 16, 17 | syl3anc 1248 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ ((๐ด ยท ๐ถ) / ๐ท) = (๐ด ยท (๐ถ / ๐ท))) |
19 | 18 | eqcomd 2193 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ (๐ด ยท (๐ถ / ๐ท)) = ((๐ด ยท ๐ถ) / ๐ท)) |
20 | 19 | oveq2d 5904 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ (๐ต ยท (๐ด ยท (๐ถ / ๐ท))) = (๐ต ยท ((๐ด ยท ๐ถ) / ๐ท))) |
21 | 14, 20 | eqtrd 2220 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ ((๐ต ยท ๐ด) ยท (๐ถ / ๐ท)) = (๐ต ยท ((๐ด ยท ๐ถ) / ๐ท))) |
22 | 1, 5, 21 | 3eqtrd 2224 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ท # 0)) โ ((๐ด ยท (๐ต / ๐ท)) ยท ๐ถ) = (๐ต ยท ((๐ด ยท ๐ถ) / ๐ท))) |