Step | Hyp | Ref
| Expression |
1 | | oveq2 5883 |
. . . . . . 7
โข (๐ = 0 โ (๐ + ๐) = (๐ + 0)) |
2 | 1 | oveq2d 5891 |
. . . . . 6
โข (๐ = 0 โ (๐ดโ(๐ + ๐)) = (๐ดโ(๐ + 0))) |
3 | | oveq2 5883 |
. . . . . . 7
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
4 | 3 | oveq2d 5891 |
. . . . . 6
โข (๐ = 0 โ ((๐ดโ๐) ยท (๐ดโ๐)) = ((๐ดโ๐) ยท (๐ดโ0))) |
5 | 2, 4 | eqeq12d 2192 |
. . . . 5
โข (๐ = 0 โ ((๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)) โ (๐ดโ(๐ + 0)) = ((๐ดโ๐) ยท (๐ดโ0)))) |
6 | 5 | imbi2d 230 |
. . . 4
โข (๐ = 0 โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ + 0)) = ((๐ดโ๐) ยท (๐ดโ0))))) |
7 | | oveq2 5883 |
. . . . . . 7
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
8 | 7 | oveq2d 5891 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ(๐ + ๐)) = (๐ดโ(๐ + ๐))) |
9 | | oveq2 5883 |
. . . . . . 7
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
10 | 9 | oveq2d 5891 |
. . . . . 6
โข (๐ = ๐ โ ((๐ดโ๐) ยท (๐ดโ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
11 | 8, 10 | eqeq12d 2192 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
12 | 11 | imbi2d 230 |
. . . 4
โข (๐ = ๐ โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))))) |
13 | | oveq2 5883 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ + ๐) = (๐ + (๐ + 1))) |
14 | 13 | oveq2d 5891 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ดโ(๐ + ๐)) = (๐ดโ(๐ + (๐ + 1)))) |
15 | | oveq2 5883 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
16 | 15 | oveq2d 5891 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((๐ดโ๐) ยท (๐ดโ๐)) = ((๐ดโ๐) ยท (๐ดโ(๐ + 1)))) |
17 | 14, 16 | eqeq12d 2192 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)) โ (๐ดโ(๐ + (๐ + 1))) = ((๐ดโ๐) ยท (๐ดโ(๐ + 1))))) |
18 | 17 | imbi2d 230 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ + (๐ + 1))) = ((๐ดโ๐) ยท (๐ดโ(๐ + 1)))))) |
19 | | oveq2 5883 |
. . . . . . 7
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
20 | 19 | oveq2d 5891 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ(๐ + ๐)) = (๐ดโ(๐ + ๐))) |
21 | | oveq2 5883 |
. . . . . . 7
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
22 | 21 | oveq2d 5891 |
. . . . . 6
โข (๐ = ๐ โ ((๐ดโ๐) ยท (๐ดโ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |
23 | 20, 22 | eqeq12d 2192 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
24 | 23 | imbi2d 230 |
. . . 4
โข (๐ = ๐ โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))))) |
25 | | nn0cn 9186 |
. . . . . . . . 9
โข (๐ โ โ0
โ ๐ โ
โ) |
26 | 25 | addid1d 8106 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ + 0) = ๐) |
27 | 26 | adantl 277 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ + 0) = ๐) |
28 | 27 | oveq2d 5891 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 0)) = (๐ดโ๐)) |
29 | | expcl 10538 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
30 | 29 | mulridd 7974 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ดโ๐) ยท 1) = (๐ดโ๐)) |
31 | 28, 30 | eqtr4d 2213 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 0)) = ((๐ดโ๐) ยท 1)) |
32 | | exp0 10524 |
. . . . . . 7
โข (๐ด โ โ โ (๐ดโ0) = 1) |
33 | 32 | adantr 276 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ0) =
1) |
34 | 33 | oveq2d 5891 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ดโ๐) ยท (๐ดโ0)) = ((๐ดโ๐) ยท 1)) |
35 | 31, 34 | eqtr4d 2213 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 0)) = ((๐ดโ๐) ยท (๐ดโ0))) |
36 | | oveq1 5882 |
. . . . . . 7
โข ((๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)) โ ((๐ดโ(๐ + ๐)) ยท ๐ด) = (((๐ดโ๐) ยท (๐ดโ๐)) ยท ๐ด)) |
37 | | nn0cn 9186 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โ) |
38 | | ax-1cn 7904 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
39 | | addass 7941 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ โง 1 โ
โ) โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
40 | 38, 39 | mp3an3 1326 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
41 | 25, 37, 40 | syl2an 289 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
42 | 41 | adantll 476 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
43 | 42 | oveq2d 5891 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ((๐ + ๐) + 1)) = (๐ดโ(๐ + (๐ + 1)))) |
44 | | simpll 527 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ๐ด โ โ) |
45 | | nn0addcl 9211 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ
โ0) |
46 | 45 | adantll 476 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ + ๐) โ
โ0) |
47 | | expp1 10527 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ + ๐) โ โ0) โ (๐ดโ((๐ + ๐) + 1)) = ((๐ดโ(๐ + ๐)) ยท ๐ด)) |
48 | 44, 46, 47 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ((๐ + ๐) + 1)) = ((๐ดโ(๐ + ๐)) ยท ๐ด)) |
49 | 43, 48 | eqtr3d 2212 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ(๐ + (๐ + 1))) = ((๐ดโ(๐ + ๐)) ยท ๐ด)) |
50 | | expp1 10527 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
51 | 50 | adantlr 477 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
52 | 51 | oveq2d 5891 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ๐) ยท (๐ดโ(๐ + 1))) = ((๐ดโ๐) ยท ((๐ดโ๐) ยท ๐ด))) |
53 | 29 | adantr 276 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ๐) โ โ) |
54 | | expcl 10538 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
55 | 54 | adantlr 477 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ๐) โ โ) |
56 | 53, 55, 44 | mulassd 7981 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (((๐ดโ๐) ยท (๐ดโ๐)) ยท ๐ด) = ((๐ดโ๐) ยท ((๐ดโ๐) ยท ๐ด))) |
57 | 52, 56 | eqtr4d 2213 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ๐) ยท (๐ดโ(๐ + 1))) = (((๐ดโ๐) ยท (๐ดโ๐)) ยท ๐ด)) |
58 | 49, 57 | eqeq12d 2192 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ(๐ + (๐ + 1))) = ((๐ดโ๐) ยท (๐ดโ(๐ + 1))) โ ((๐ดโ(๐ + ๐)) ยท ๐ด) = (((๐ดโ๐) ยท (๐ดโ๐)) ยท ๐ด))) |
59 | 36, 58 | imbitrrid 156 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)) โ (๐ดโ(๐ + (๐ + 1))) = ((๐ดโ๐) ยท (๐ดโ(๐ + 1))))) |
60 | 59 | expcom 116 |
. . . . 5
โข (๐ โ โ0
โ ((๐ด โ โ
โง ๐ โ
โ0) โ ((๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)) โ (๐ดโ(๐ + (๐ + 1))) = ((๐ดโ๐) ยท (๐ดโ(๐ + 1)))))) |
61 | 60 | a2d 26 |
. . . 4
โข (๐ โ โ0
โ (((๐ด โ โ
โง ๐ โ
โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ + (๐ + 1))) = ((๐ดโ๐) ยท (๐ดโ(๐ + 1)))))) |
62 | 6, 12, 18, 24, 35, 61 | nn0ind 9367 |
. . 3
โข (๐ โ โ0
โ ((๐ด โ โ
โง ๐ โ
โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐)))) |
63 | 62 | expdcom 1442 |
. 2
โข (๐ด โ โ โ (๐ โ โ0
โ (๐ โ
โ0 โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))))) |
64 | 63 | 3imp 1193 |
1
โข ((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โ (๐ดโ(๐ + ๐)) = ((๐ดโ๐) ยท (๐ดโ๐))) |