Step | Hyp | Ref
| Expression |
1 | | muls0ord.2 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ No
) |
2 | | muls02 27981 |
. . . . . . . . . . 11
โข (๐ต โ
No โ ( 0s ยทs ๐ต) = 0s ) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ( 0s
ยทs ๐ต) =
0s ) |
4 | 3 | adantr 480 |
. . . . . . . . 9
โข ((๐ โง ๐ต โ 0s ) โ ( 0s
ยทs ๐ต) =
0s ) |
5 | 4 | eqeq2d 2735 |
. . . . . . . 8
โข ((๐ โง ๐ต โ 0s ) โ ((๐ด ยทs ๐ต) = ( 0s
ยทs ๐ต)
โ (๐ด
ยทs ๐ต) =
0s )) |
6 | | muls0ord.1 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ No
) |
7 | 6 | adantr 480 |
. . . . . . . . 9
โข ((๐ โง ๐ต โ 0s ) โ ๐ด โ
No ) |
8 | | 0sno 27699 |
. . . . . . . . . 10
โข
0s โ No |
9 | 8 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ต โ 0s ) โ 0s
โ No ) |
10 | 1 | adantr 480 |
. . . . . . . . 9
โข ((๐ โง ๐ต โ 0s ) โ ๐ต โ
No ) |
11 | | simpr 484 |
. . . . . . . . 9
โข ((๐ โง ๐ต โ 0s ) โ ๐ต โ 0s
) |
12 | 7, 9, 10, 11 | mulscan2d 28019 |
. . . . . . . 8
โข ((๐ โง ๐ต โ 0s ) โ ((๐ด ยทs ๐ต) = ( 0s
ยทs ๐ต)
โ ๐ด = 0s
)) |
13 | 5, 12 | bitr3d 281 |
. . . . . . 7
โข ((๐ โง ๐ต โ 0s ) โ ((๐ด ยทs ๐ต) = 0s โ ๐ด = 0s
)) |
14 | 13 | biimpd 228 |
. . . . . 6
โข ((๐ โง ๐ต โ 0s ) โ ((๐ด ยทs ๐ต) = 0s โ ๐ด = 0s
)) |
15 | 14 | impancom 451 |
. . . . 5
โข ((๐ โง (๐ด ยทs ๐ต) = 0s ) โ (๐ต โ 0s โ ๐ด = 0s
)) |
16 | 15 | necon1bd 2950 |
. . . 4
โข ((๐ โง (๐ด ยทs ๐ต) = 0s ) โ (ยฌ ๐ด = 0s โ ๐ต = 0s
)) |
17 | 16 | orrd 860 |
. . 3
โข ((๐ โง (๐ด ยทs ๐ต) = 0s ) โ (๐ด = 0s โจ ๐ต = 0s
)) |
18 | 17 | ex 412 |
. 2
โข (๐ โ ((๐ด ยทs ๐ต) = 0s โ (๐ด = 0s โจ ๐ต = 0s ))) |
19 | | oveq1 7409 |
. . . . 5
โข (๐ด = 0s โ (๐ด ยทs ๐ต) = ( 0s
ยทs ๐ต)) |
20 | 19 | eqeq1d 2726 |
. . . 4
โข (๐ด = 0s โ ((๐ด ยทs ๐ต) = 0s โ (
0s ยทs ๐ต) = 0s )) |
21 | 3, 20 | syl5ibrcom 246 |
. . 3
โข (๐ โ (๐ด = 0s โ (๐ด ยทs ๐ต) = 0s )) |
22 | | muls01 27952 |
. . . . 5
โข (๐ด โ
No โ (๐ด
ยทs 0s ) = 0s ) |
23 | 6, 22 | syl 17 |
. . . 4
โข (๐ โ (๐ด ยทs 0s ) =
0s ) |
24 | | oveq2 7410 |
. . . . 5
โข (๐ต = 0s โ (๐ด ยทs ๐ต) = (๐ด ยทs 0s
)) |
25 | 24 | eqeq1d 2726 |
. . . 4
โข (๐ต = 0s โ ((๐ด ยทs ๐ต) = 0s โ (๐ด ยทs
0s ) = 0s )) |
26 | 23, 25 | syl5ibrcom 246 |
. . 3
โข (๐ โ (๐ต = 0s โ (๐ด ยทs ๐ต) = 0s )) |
27 | 21, 26 | jaod 856 |
. 2
โข (๐ โ ((๐ด = 0s โจ ๐ต = 0s ) โ (๐ด ยทs ๐ต) = 0s )) |
28 | 18, 27 | impbid 211 |
1
โข (๐ โ ((๐ด ยทs ๐ต) = 0s โ (๐ด = 0s โจ ๐ต = 0s ))) |