Step | Hyp | Ref
| Expression |
1 | | oveq2 7410 |
. . . . 5
โข (๐ = 0s โ (๐ด ยทs ๐) = (๐ด ยทs 0s
)) |
2 | 1 | eleq1d 2810 |
. . . 4
โข (๐ = 0s โ ((๐ด ยทs ๐) โ โ0s
โ (๐ด
ยทs 0s ) โ
โ0s)) |
3 | 2 | imbi2d 340 |
. . 3
โข (๐ = 0s โ ((๐ด โ โ0s
โ (๐ด
ยทs ๐)
โ โ0s) โ (๐ด โ โ0s โ (๐ด ยทs
0s ) โ โ0s))) |
4 | | oveq2 7410 |
. . . . 5
โข (๐ = ๐ โ (๐ด ยทs ๐) = (๐ด ยทs ๐)) |
5 | 4 | eleq1d 2810 |
. . . 4
โข (๐ = ๐ โ ((๐ด ยทs ๐) โ โ0s โ (๐ด ยทs ๐) โ
โ0s)) |
6 | 5 | imbi2d 340 |
. . 3
โข (๐ = ๐ โ ((๐ด โ โ0s โ (๐ด ยทs ๐) โ โ0s)
โ (๐ด โ
โ0s โ (๐ด ยทs ๐) โ
โ0s))) |
7 | | oveq2 7410 |
. . . . 5
โข (๐ = (๐ +s 1s ) โ (๐ด ยทs ๐) = (๐ด ยทs (๐ +s 1s
))) |
8 | 7 | eleq1d 2810 |
. . . 4
โข (๐ = (๐ +s 1s ) โ ((๐ด ยทs ๐) โ โ0s
โ (๐ด
ยทs (๐
+s 1s )) โ โ0s)) |
9 | 8 | imbi2d 340 |
. . 3
โข (๐ = (๐ +s 1s ) โ ((๐ด โ โ0s
โ (๐ด
ยทs ๐)
โ โ0s) โ (๐ด โ โ0s โ (๐ด ยทs (๐ +s 1s ))
โ โ0s))) |
10 | | oveq2 7410 |
. . . . 5
โข (๐ = ๐ต โ (๐ด ยทs ๐) = (๐ด ยทs ๐ต)) |
11 | 10 | eleq1d 2810 |
. . . 4
โข (๐ = ๐ต โ ((๐ด ยทs ๐) โ โ0s โ (๐ด ยทs ๐ต) โ
โ0s)) |
12 | 11 | imbi2d 340 |
. . 3
โข (๐ = ๐ต โ ((๐ด โ โ0s โ (๐ด ยทs ๐) โ โ0s)
โ (๐ด โ
โ0s โ (๐ด ยทs ๐ต) โ
โ0s))) |
13 | | n0sno 28114 |
. . . . 5
โข (๐ด โ โ0s
โ ๐ด โ No ) |
14 | | muls01 27931 |
. . . . 5
โข (๐ด โ
No โ (๐ด
ยทs 0s ) = 0s ) |
15 | 13, 14 | syl 17 |
. . . 4
โข (๐ด โ โ0s
โ (๐ด
ยทs 0s ) = 0s ) |
16 | | 0n0s 28118 |
. . . 4
โข
0s โ โ0s |
17 | 15, 16 | eqeltrdi 2833 |
. . 3
โข (๐ด โ โ0s
โ (๐ด
ยทs 0s ) โ
โ0s) |
18 | 13 | ad2antrr 723 |
. . . . . . . . 9
โข (((๐ด โ โ0s
โง ๐ โ
โ0s) โง (๐ด ยทs ๐) โ โ0s) โ ๐ด โ
No ) |
19 | | n0sno 28114 |
. . . . . . . . . 10
โข (๐ โ โ0s
โ ๐ โ No ) |
20 | 19 | ad2antlr 724 |
. . . . . . . . 9
โข (((๐ด โ โ0s
โง ๐ โ
โ0s) โง (๐ด ยทs ๐) โ โ0s) โ ๐ โ
No ) |
21 | | 1sno 27679 |
. . . . . . . . . 10
โข
1s โ No |
22 | 21 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ โ0s
โง ๐ โ
โ0s) โง (๐ด ยทs ๐) โ โ0s) โ
1s โ No ) |
23 | 18, 20, 22 | addsdid 27975 |
. . . . . . . 8
โข (((๐ด โ โ0s
โง ๐ โ
โ0s) โง (๐ด ยทs ๐) โ โ0s) โ (๐ด ยทs (๐ +s 1s ))
= ((๐ด ยทs
๐) +s (๐ด ยทs
1s ))) |
24 | 13 | mulsridd 27933 |
. . . . . . . . . 10
โข (๐ด โ โ0s
โ (๐ด
ยทs 1s ) = ๐ด) |
25 | 24 | oveq2d 7418 |
. . . . . . . . 9
โข (๐ด โ โ0s
โ ((๐ด
ยทs ๐)
+s (๐ด
ยทs 1s )) = ((๐ด ยทs ๐) +s ๐ด)) |
26 | 25 | ad2antrr 723 |
. . . . . . . 8
โข (((๐ด โ โ0s
โง ๐ โ
โ0s) โง (๐ด ยทs ๐) โ โ0s) โ ((๐ด ยทs ๐) +s (๐ด ยทs
1s )) = ((๐ด
ยทs ๐)
+s ๐ด)) |
27 | 23, 26 | eqtrd 2764 |
. . . . . . 7
โข (((๐ด โ โ0s
โง ๐ โ
โ0s) โง (๐ด ยทs ๐) โ โ0s) โ (๐ด ยทs (๐ +s 1s ))
= ((๐ด ยทs
๐) +s ๐ด)) |
28 | | n0addscl 28129 |
. . . . . . . . 9
โข (((๐ด ยทs ๐) โ โ0s
โง ๐ด โ
โ0s) โ ((๐ด ยทs ๐) +s ๐ด) โ
โ0s) |
29 | 28 | ancoms 458 |
. . . . . . . 8
โข ((๐ด โ โ0s
โง (๐ด
ยทs ๐)
โ โ0s) โ ((๐ด ยทs ๐) +s ๐ด) โ
โ0s) |
30 | 29 | adantlr 712 |
. . . . . . 7
โข (((๐ด โ โ0s
โง ๐ โ
โ0s) โง (๐ด ยทs ๐) โ โ0s) โ ((๐ด ยทs ๐) +s ๐ด) โ
โ0s) |
31 | 27, 30 | eqeltrd 2825 |
. . . . . 6
โข (((๐ด โ โ0s
โง ๐ โ
โ0s) โง (๐ด ยทs ๐) โ โ0s) โ (๐ด ยทs (๐ +s 1s ))
โ โ0s) |
32 | 31 | ex 412 |
. . . . 5
โข ((๐ด โ โ0s
โง ๐ โ
โ0s) โ ((๐ด ยทs ๐) โ โ0s โ (๐ด ยทs (๐ +s 1s ))
โ โ0s)) |
33 | 32 | expcom 413 |
. . . 4
โข (๐ โ โ0s
โ (๐ด โ
โ0s โ ((๐ด ยทs ๐) โ โ0s โ (๐ด ยทs (๐ +s 1s ))
โ โ0s))) |
34 | 33 | a2d 29 |
. . 3
โข (๐ โ โ0s
โ ((๐ด โ
โ0s โ (๐ด ยทs ๐) โ โ0s) โ (๐ด โ โ0s
โ (๐ด
ยทs (๐
+s 1s )) โ โ0s))) |
35 | 3, 6, 9, 12, 17, 34 | n0sind 28121 |
. 2
โข (๐ต โ โ0s
โ (๐ด โ
โ0s โ (๐ด ยทs ๐ต) โ
โ0s)) |
36 | 35 | impcom 407 |
1
โข ((๐ด โ โ0s
โง ๐ต โ
โ0s) โ (๐ด ยทs ๐ต) โ
โ0s) |