Step | Hyp | Ref
| Expression |
1 | | df-ne 2941 |
. . . . 5
โข (๐ด โ 0 โ ยฌ ๐ด = 0) |
2 | | oveq2 7366 |
. . . . . . . 8
โข ((๐ด
ยทโ ๐ต) = 0โ โ ((1 / ๐ด)
ยทโ (๐ด ยทโ ๐ต)) = ((1 / ๐ด) ยทโ
0โ)) |
3 | 2 | ad2antlr 726 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด
ยทโ ๐ต) = 0โ) โง ๐ด โ 0) โ ((1 / ๐ด)
ยทโ (๐ด ยทโ ๐ต)) = ((1 / ๐ด) ยทโ
0โ)) |
4 | | recid2 11833 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0) โ ((1 / ๐ด) ยท ๐ด) = 1) |
5 | 4 | oveq1d 7373 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0) โ (((1 / ๐ด) ยท ๐ด) ยทโ ๐ต) = (1
ยทโ ๐ต)) |
6 | 5 | adantlr 714 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (((1 / ๐ด) ยท ๐ด) ยทโ ๐ต) = (1
ยทโ ๐ต)) |
7 | | reccl 11825 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / ๐ด) โ
โ) |
8 | 7 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (1 / ๐ด) โ
โ) |
9 | | simpll 766 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ ๐ด โ
โ) |
10 | | simplr 768 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ ๐ต โ
โ) |
11 | | ax-hvmulass 29991 |
. . . . . . . . . 10
โข (((1 /
๐ด) โ โ โง
๐ด โ โ โง
๐ต โ โ) โ
(((1 / ๐ด) ยท ๐ด)
ยทโ ๐ต) = ((1 / ๐ด) ยทโ (๐ด
ยทโ ๐ต))) |
12 | 8, 9, 10, 11 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (((1 / ๐ด) ยท ๐ด) ยทโ ๐ต) = ((1 / ๐ด) ยทโ (๐ด
ยทโ ๐ต))) |
13 | | ax-hvmulid 29990 |
. . . . . . . . . 10
โข (๐ต โ โ โ (1
ยทโ ๐ต) = ๐ต) |
14 | 13 | ad2antlr 726 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ (1
ยทโ ๐ต) = ๐ต) |
15 | 6, 12, 14 | 3eqtr3d 2781 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ ((1 / ๐ด)
ยทโ (๐ด ยทโ ๐ต)) = ๐ต) |
16 | 15 | adantlr 714 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด
ยทโ ๐ต) = 0โ) โง ๐ด โ 0) โ ((1 / ๐ด)
ยทโ (๐ด ยทโ ๐ต)) = ๐ต) |
17 | | hvmul0 30008 |
. . . . . . . . . 10
โข ((1 /
๐ด) โ โ โ
((1 / ๐ด)
ยทโ 0โ) =
0โ) |
18 | 7, 17 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0) โ ((1 / ๐ด)
ยทโ 0โ) =
0โ) |
19 | 18 | adantlr 714 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด โ 0) โ ((1 / ๐ด)
ยทโ 0โ) =
0โ) |
20 | 19 | adantlr 714 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด
ยทโ ๐ต) = 0โ) โง ๐ด โ 0) โ ((1 / ๐ด)
ยทโ 0โ) =
0โ) |
21 | 3, 16, 20 | 3eqtr3d 2781 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ด
ยทโ ๐ต) = 0โ) โง ๐ด โ 0) โ ๐ต =
0โ) |
22 | 21 | ex 414 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด
ยทโ ๐ต) = 0โ) โ (๐ด โ 0 โ ๐ต = 0โ)) |
23 | 1, 22 | biimtrrid 242 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด
ยทโ ๐ต) = 0โ) โ (ยฌ
๐ด = 0 โ ๐ต =
0โ)) |
24 | 23 | orrd 862 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด
ยทโ ๐ต) = 0โ) โ (๐ด = 0 โจ ๐ต = 0โ)) |
25 | 24 | ex 414 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด
ยทโ ๐ต) = 0โ โ (๐ด = 0 โจ ๐ต = 0โ))) |
26 | | ax-hvmul0 29994 |
. . . . 5
โข (๐ต โ โ โ (0
ยทโ ๐ต) = 0โ) |
27 | | oveq1 7365 |
. . . . . 6
โข (๐ด = 0 โ (๐ด ยทโ ๐ต) = (0
ยทโ ๐ต)) |
28 | 27 | eqeq1d 2735 |
. . . . 5
โข (๐ด = 0 โ ((๐ด ยทโ ๐ต) = 0โ โ
(0 ยทโ ๐ต) = 0โ)) |
29 | 26, 28 | syl5ibrcom 247 |
. . . 4
โข (๐ต โ โ โ (๐ด = 0 โ (๐ด ยทโ ๐ต) =
0โ)) |
30 | 29 | adantl 483 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด = 0 โ (๐ด ยทโ ๐ต) =
0โ)) |
31 | | hvmul0 30008 |
. . . . 5
โข (๐ด โ โ โ (๐ด
ยทโ 0โ) =
0โ) |
32 | | oveq2 7366 |
. . . . . 6
โข (๐ต = 0โ โ
(๐ด
ยทโ ๐ต) = (๐ด ยทโ
0โ)) |
33 | 32 | eqeq1d 2735 |
. . . . 5
โข (๐ต = 0โ โ
((๐ด
ยทโ ๐ต) = 0โ โ (๐ด
ยทโ 0โ) =
0โ)) |
34 | 31, 33 | syl5ibrcom 247 |
. . . 4
โข (๐ด โ โ โ (๐ต = 0โ โ
(๐ด
ยทโ ๐ต) = 0โ)) |
35 | 34 | adantr 482 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ต = 0โ โ
(๐ด
ยทโ ๐ต) = 0โ)) |
36 | 30, 35 | jaod 858 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด = 0 โจ ๐ต = 0โ) โ (๐ด
ยทโ ๐ต) = 0โ)) |
37 | 25, 36 | impbid 211 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด
ยทโ ๐ต) = 0โ โ (๐ด = 0 โจ ๐ต = 0โ))) |