Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ ๐ด โ โ) |
2 | | simp3l 1025 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ ๐ถ โ โ) |
3 | | simp3r 1026 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ ๐ถ # 0) |
4 | 2, 3 | recclapd 8740 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (1 / ๐ถ) โ
โ) |
5 | 1, 2, 4 | mulassd 7983 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ ((๐ด ยท ๐ถ) ยท (1 / ๐ถ)) = (๐ด ยท (๐ถ ยท (1 / ๐ถ)))) |
6 | 2, 3 | recidapd 8742 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ถ ยท (1 / ๐ถ)) = 1) |
7 | 6 | oveq2d 5893 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ด ยท (๐ถ ยท (1 / ๐ถ))) = (๐ด ยท 1)) |
8 | 1 | mulridd 7976 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ด ยท 1) = ๐ด) |
9 | 5, 7, 8 | 3eqtrd 2214 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ ((๐ด ยท ๐ถ) ยท (1 / ๐ถ)) = ๐ด) |
10 | | simp2 998 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ ๐ต โ โ) |
11 | 10, 2, 4 | mulassd 7983 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ ((๐ต ยท ๐ถ) ยท (1 / ๐ถ)) = (๐ต ยท (๐ถ ยท (1 / ๐ถ)))) |
12 | 6 | oveq2d 5893 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ต ยท (๐ถ ยท (1 / ๐ถ))) = (๐ต ยท 1)) |
13 | 10 | mulridd 7976 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ต ยท 1) = ๐ต) |
14 | 11, 12, 13 | 3eqtrd 2214 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ ((๐ต ยท ๐ถ) ยท (1 / ๐ถ)) = ๐ต) |
15 | 9, 14 | breq12d 4018 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (((๐ด ยท ๐ถ) ยท (1 / ๐ถ)) # ((๐ต ยท ๐ถ) ยท (1 / ๐ถ)) โ ๐ด # ๐ต)) |
16 | 1, 2 | mulcld 7980 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ด ยท ๐ถ) โ โ) |
17 | 10, 2 | mulcld 7980 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ต ยท ๐ถ) โ โ) |
18 | | mulext1 8571 |
. . . 4
โข (((๐ด ยท ๐ถ) โ โ โง (๐ต ยท ๐ถ) โ โ โง (1 / ๐ถ) โ โ) โ
(((๐ด ยท ๐ถ) ยท (1 / ๐ถ)) # ((๐ต ยท ๐ถ) ยท (1 / ๐ถ)) โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
19 | 16, 17, 4, 18 | syl3anc 1238 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (((๐ด ยท ๐ถ) ยท (1 / ๐ถ)) # ((๐ต ยท ๐ถ) ยท (1 / ๐ถ)) โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
20 | 15, 19 | sylbird 170 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
21 | | mulext1 8571 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ถ) # (๐ต ยท ๐ถ) โ ๐ด # ๐ต)) |
22 | 21 | 3adant3r 1235 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ ((๐ด ยท ๐ถ) # (๐ต ยท ๐ถ) โ ๐ด # ๐ต)) |
23 | 20, 22 | impbid 129 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |