Step | Hyp | Ref
| Expression |
1 | | redivcl 11882 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด / ๐ต) โ โ) |
2 | | recn 11149 |
. . . . . 6
โข (๐ด โ โ โ ๐ด โ
โ) |
3 | | recn 11149 |
. . . . . 6
โข (๐ต โ โ โ ๐ต โ
โ) |
4 | | id 22 |
. . . . . 6
โข (๐ต โ 0 โ ๐ต โ 0) |
5 | 2, 3, 4 | 3anim123i 1152 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0)) |
6 | | divcan2 11829 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ต ยท (๐ด / ๐ต)) = ๐ด) |
7 | 5, 6 | syl 17 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ต ยท (๐ด / ๐ต)) = ๐ด) |
8 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = (๐ด / ๐ต) โ (๐ต ยท ๐ฅ) = (๐ต ยท (๐ด / ๐ต))) |
9 | 8 | eqeq1d 2735 |
. . . . 5
โข (๐ฅ = (๐ด / ๐ต) โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท (๐ด / ๐ต)) = ๐ด)) |
10 | 9 | rspcev 3583 |
. . . 4
โข (((๐ด / ๐ต) โ โ โง (๐ต ยท (๐ด / ๐ต)) = ๐ด) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
11 | 1, 7, 10 | syl2anc 585 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
12 | | receu 11808 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ!๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
13 | 5, 12 | syl 17 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ!๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
14 | | ax-resscn 11116 |
. . . 4
โข โ
โ โ |
15 | | id 22 |
. . . . 5
โข ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท ๐ฅ) = ๐ด) |
16 | 15 | rgenw 3065 |
. . . 4
โข
โ๐ฅ โ
โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท ๐ฅ) = ๐ด) |
17 | | riotass2 7348 |
. . . 4
โข
(((โ โ โ โง โ๐ฅ โ โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท ๐ฅ) = ๐ด)) โง (โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด โง โ!๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) โ (โฉ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) = (โฉ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
18 | 14, 16, 17 | mpanl12 701 |
. . 3
โข
((โ๐ฅ โ
โ (๐ต ยท ๐ฅ) = ๐ด โง โ!๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) โ (โฉ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) = (โฉ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
19 | 11, 13, 18 | syl2anc 585 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ
(โฉ๐ฅ โ
โ (๐ต ยท ๐ฅ) = ๐ด) = (โฉ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
20 | | rexr 11209 |
. . . 4
โข (๐ด โ โ โ ๐ด โ
โ*) |
21 | | xdivval 31831 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(๐ด /๐
๐ต) = (โฉ๐ฅ โ โ*
(๐ต ยทe
๐ฅ) = ๐ด)) |
22 | 20, 21 | syl3an1 1164 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด /๐ ๐ต) = (โฉ๐ฅ โ โ*
(๐ต ยทe
๐ฅ) = ๐ด)) |
23 | | ressxr 11207 |
. . . . 5
โข โ
โ โ* |
24 | 23 | a1i 11 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ โ
โ*) |
25 | | rexmul 13199 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ฅ โ โ) โ (๐ต ยทe ๐ฅ) = (๐ต ยท ๐ฅ)) |
26 | 25 | eqeq1d 2735 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ฅ โ โ) โ ((๐ต ยทe ๐ฅ) = ๐ด โ (๐ต ยท ๐ฅ) = ๐ด)) |
27 | 26 | biimprd 248 |
. . . . . 6
โข ((๐ต โ โ โง ๐ฅ โ โ) โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยทe ๐ฅ) = ๐ด)) |
28 | 27 | ralrimiva 3140 |
. . . . 5
โข (๐ต โ โ โ
โ๐ฅ โ โ
((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยทe ๐ฅ) = ๐ด)) |
29 | 28 | 3ad2ant2 1135 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ๐ฅ โ โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยทe ๐ฅ) = ๐ด)) |
30 | | xreceu 31834 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
โ!๐ฅ โ
โ* (๐ต
ยทe ๐ฅ) =
๐ด) |
31 | 20, 30 | syl3an1 1164 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ!๐ฅ โ โ*
(๐ต ยทe
๐ฅ) = ๐ด) |
32 | | riotass2 7348 |
. . . 4
โข
(((โ โ โ* โง โ๐ฅ โ โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยทe ๐ฅ) = ๐ด)) โง (โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด โง โ!๐ฅ โ โ* (๐ต ยทe ๐ฅ) = ๐ด)) โ (โฉ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) = (โฉ๐ฅ โ โ* (๐ต ยทe ๐ฅ) = ๐ด)) |
33 | 24, 29, 11, 31, 32 | syl22anc 838 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ
(โฉ๐ฅ โ
โ (๐ต ยท ๐ฅ) = ๐ด) = (โฉ๐ฅ โ โ* (๐ต ยทe ๐ฅ) = ๐ด)) |
34 | 22, 33 | eqtr4d 2776 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด /๐ ๐ต) = (โฉ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
35 | | divval 11823 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด / ๐ต) = (โฉ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
36 | 5, 35 | syl 17 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด / ๐ต) = (โฉ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
37 | 19, 34, 36 | 3eqtr4d 2783 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด /๐ ๐ต) = (๐ด / ๐ต)) |