Step | Hyp | Ref
| Expression |
1 | | simp2 1138 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
๐ต โ
โ) |
2 | 1 | rexrd 11264 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
๐ต โ
โ*) |
3 | | simp1 1137 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
๐ด โ
โ*) |
4 | | 1xr 11273 |
. . . . . . . 8
โข 1 โ
โ* |
5 | 4 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ 1
โ โ*) |
6 | | simp3 1139 |
. . . . . . 7
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
๐ต โ 0) |
7 | 5, 1, 6 | xdivcld 32089 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ (1
/๐ ๐ต)
โ โ*) |
8 | 3, 7 | xmulcld 13281 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(๐ด ยทe (1
/๐ ๐ต))
โ โ*) |
9 | | xmulcom 13245 |
. . . . 5
โข ((๐ต โ โ*
โง (๐ด
ยทe (1 /๐ ๐ต)) โ โ*) โ (๐ต ยทe (๐ด ยทe (1
/๐ ๐ต)))
= ((๐ด ยทe
(1 /๐ ๐ต)) ยทe ๐ต)) |
10 | 2, 8, 9 | syl2anc 585 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(๐ต ยทe
(๐ด ยทe (1
/๐ ๐ต)))
= ((๐ด ยทe
(1 /๐ ๐ต)) ยทe ๐ต)) |
11 | | xmulass 13266 |
. . . . 5
โข ((๐ด โ โ*
โง (1 /๐ ๐ต) โ โ* โง ๐ต โ โ*)
โ ((๐ด
ยทe (1 /๐ ๐ต)) ยทe ๐ต) = (๐ด ยทe ((1
/๐ ๐ต)
ยทe ๐ต))) |
12 | 3, 7, 2, 11 | syl3anc 1372 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
((๐ด ยทe (1
/๐ ๐ต))
ยทe ๐ต) =
(๐ด ยทe ((1
/๐ ๐ต)
ยทe ๐ต))) |
13 | | xmulcom 13245 |
. . . . . . 7
โข (((1
/๐ ๐ต)
โ โ* โง ๐ต โ โ*) โ ((1
/๐ ๐ต)
ยทe ๐ต) =
(๐ต ยทe (1
/๐ ๐ต))) |
14 | 7, 2, 13 | syl2anc 585 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ ((1
/๐ ๐ต)
ยทe ๐ต) =
(๐ต ยทe (1
/๐ ๐ต))) |
15 | | eqid 2733 |
. . . . . . 7
โข (1
/๐ ๐ต) =
(1 /๐ ๐ต) |
16 | | xdivmul 32091 |
. . . . . . . 8
โข ((1
โ โ* โง (1 /๐ ๐ต) โ โ* โง (๐ต โ โ โง ๐ต โ 0)) โ ((1
/๐ ๐ต) =
(1 /๐ ๐ต)
โ (๐ต
ยทe (1 /๐ ๐ต)) = 1)) |
17 | 5, 7, 1, 6, 16 | syl112anc 1375 |
. . . . . . 7
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ ((1
/๐ ๐ต) =
(1 /๐ ๐ต)
โ (๐ต
ยทe (1 /๐ ๐ต)) = 1)) |
18 | 15, 17 | mpbii 232 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(๐ต ยทe (1
/๐ ๐ต)) =
1) |
19 | 14, 18 | eqtrd 2773 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ ((1
/๐ ๐ต)
ยทe ๐ต) =
1) |
20 | 19 | oveq2d 7425 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(๐ด ยทe ((1
/๐ ๐ต)
ยทe ๐ต)) =
(๐ด ยทe
1)) |
21 | 10, 12, 20 | 3eqtrd 2777 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(๐ต ยทe
(๐ด ยทe (1
/๐ ๐ต)))
= (๐ด ยทe
1)) |
22 | | xmulrid 13258 |
. . . 4
โข (๐ด โ โ*
โ (๐ด
ยทe 1) = ๐ด) |
23 | 3, 22 | syl 17 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(๐ด ยทe 1)
= ๐ด) |
24 | 21, 23 | eqtrd 2773 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(๐ต ยทe
(๐ด ยทe (1
/๐ ๐ต)))
= ๐ด) |
25 | | xdivmul 32091 |
. . 3
โข ((๐ด โ โ*
โง (๐ด
ยทe (1 /๐ ๐ต)) โ โ* โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ด /๐ ๐ต) = (๐ด ยทe (1
/๐ ๐ต))
โ (๐ต
ยทe (๐ด
ยทe (1 /๐ ๐ต))) = ๐ด)) |
26 | 3, 8, 1, 6, 25 | syl112anc 1375 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
((๐ด /๐
๐ต) = (๐ด ยทe (1
/๐ ๐ต))
โ (๐ต
ยทe (๐ด
ยทe (1 /๐ ๐ต))) = ๐ด)) |
27 | 24, 26 | mpbird 257 |
1
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(๐ด /๐
๐ต) = (๐ด ยทe (1
/๐ ๐ต))) |