Step | Hyp | Ref
| Expression |
1 | | zcn 9258 |
. . . 4
โข (๐ โ โค โ ๐ โ
โ) |
2 | | mulcom 7940 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด ยท ๐) = (๐ ยท ๐ด)) |
3 | 1, 2 | sylan2 286 |
. . 3
โข ((๐ด โ โ โง ๐ โ โค) โ (๐ด ยท ๐) = (๐ ยท ๐ด)) |
4 | 3 | fveq2d 5520 |
. 2
โข ((๐ด โ โ โง ๐ โ โค) โ
(expโ(๐ด ยท
๐)) = (expโ(๐ ยท ๐ด))) |
5 | | oveq2 5883 |
. . . . . 6
โข (๐ = 0 โ (๐ด ยท ๐) = (๐ด ยท 0)) |
6 | 5 | fveq2d 5520 |
. . . . 5
โข (๐ = 0 โ (expโ(๐ด ยท ๐)) = (expโ(๐ด ยท 0))) |
7 | | oveq2 5883 |
. . . . 5
โข (๐ = 0 โ ((expโ๐ด)โ๐) = ((expโ๐ด)โ0)) |
8 | 6, 7 | eqeq12d 2192 |
. . . 4
โข (๐ = 0 โ ((expโ(๐ด ยท ๐)) = ((expโ๐ด)โ๐) โ (expโ(๐ด ยท 0)) = ((expโ๐ด)โ0))) |
9 | | oveq2 5883 |
. . . . . 6
โข (๐ = ๐ โ (๐ด ยท ๐) = (๐ด ยท ๐)) |
10 | 9 | fveq2d 5520 |
. . . . 5
โข (๐ = ๐ โ (expโ(๐ด ยท ๐)) = (expโ(๐ด ยท ๐))) |
11 | | oveq2 5883 |
. . . . 5
โข (๐ = ๐ โ ((expโ๐ด)โ๐) = ((expโ๐ด)โ๐)) |
12 | 10, 11 | eqeq12d 2192 |
. . . 4
โข (๐ = ๐ โ ((expโ(๐ด ยท ๐)) = ((expโ๐ด)โ๐) โ (expโ(๐ด ยท ๐)) = ((expโ๐ด)โ๐))) |
13 | | oveq2 5883 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ด ยท ๐) = (๐ด ยท (๐ + 1))) |
14 | 13 | fveq2d 5520 |
. . . . 5
โข (๐ = (๐ + 1) โ (expโ(๐ด ยท ๐)) = (expโ(๐ด ยท (๐ + 1)))) |
15 | | oveq2 5883 |
. . . . 5
โข (๐ = (๐ + 1) โ ((expโ๐ด)โ๐) = ((expโ๐ด)โ(๐ + 1))) |
16 | 14, 15 | eqeq12d 2192 |
. . . 4
โข (๐ = (๐ + 1) โ ((expโ(๐ด ยท ๐)) = ((expโ๐ด)โ๐) โ (expโ(๐ด ยท (๐ + 1))) = ((expโ๐ด)โ(๐ + 1)))) |
17 | | oveq2 5883 |
. . . . . 6
โข (๐ = -๐ โ (๐ด ยท ๐) = (๐ด ยท -๐)) |
18 | 17 | fveq2d 5520 |
. . . . 5
โข (๐ = -๐ โ (expโ(๐ด ยท ๐)) = (expโ(๐ด ยท -๐))) |
19 | | oveq2 5883 |
. . . . 5
โข (๐ = -๐ โ ((expโ๐ด)โ๐) = ((expโ๐ด)โ-๐)) |
20 | 18, 19 | eqeq12d 2192 |
. . . 4
โข (๐ = -๐ โ ((expโ(๐ด ยท ๐)) = ((expโ๐ด)โ๐) โ (expโ(๐ด ยท -๐)) = ((expโ๐ด)โ-๐))) |
21 | | oveq2 5883 |
. . . . . 6
โข (๐ = ๐ โ (๐ด ยท ๐) = (๐ด ยท ๐)) |
22 | 21 | fveq2d 5520 |
. . . . 5
โข (๐ = ๐ โ (expโ(๐ด ยท ๐)) = (expโ(๐ด ยท ๐))) |
23 | | oveq2 5883 |
. . . . 5
โข (๐ = ๐ โ ((expโ๐ด)โ๐) = ((expโ๐ด)โ๐)) |
24 | 22, 23 | eqeq12d 2192 |
. . . 4
โข (๐ = ๐ โ ((expโ(๐ด ยท ๐)) = ((expโ๐ด)โ๐) โ (expโ(๐ด ยท ๐)) = ((expโ๐ด)โ๐))) |
25 | | ef0 11680 |
. . . . 5
โข
(expโ0) = 1 |
26 | | mul01 8346 |
. . . . . 6
โข (๐ด โ โ โ (๐ด ยท 0) =
0) |
27 | 26 | fveq2d 5520 |
. . . . 5
โข (๐ด โ โ โ
(expโ(๐ด ยท 0))
= (expโ0)) |
28 | | efcl 11672 |
. . . . . 6
โข (๐ด โ โ โ
(expโ๐ด) โ
โ) |
29 | 28 | exp0d 10648 |
. . . . 5
โข (๐ด โ โ โ
((expโ๐ด)โ0) =
1) |
30 | 25, 27, 29 | 3eqtr4a 2236 |
. . . 4
โข (๐ด โ โ โ
(expโ(๐ด ยท 0))
= ((expโ๐ด)โ0)) |
31 | | oveq1 5882 |
. . . . . . 7
โข
((expโ(๐ด
ยท ๐)) =
((expโ๐ด)โ๐) โ ((expโ(๐ด ยท ๐)) ยท (expโ๐ด)) = (((expโ๐ด)โ๐) ยท (expโ๐ด))) |
32 | 31 | adantl 277 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง (expโ(๐ด
ยท ๐)) =
((expโ๐ด)โ๐)) โ ((expโ(๐ด ยท ๐)) ยท (expโ๐ด)) = (((expโ๐ด)โ๐) ยท (expโ๐ด))) |
33 | | nn0cn 9186 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ๐ โ
โ) |
34 | | ax-1cn 7904 |
. . . . . . . . . . . 12
โข 1 โ
โ |
35 | | adddi 7943 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ โง 1 โ
โ) โ (๐ด ยท
(๐ + 1)) = ((๐ด ยท ๐) + (๐ด ยท 1))) |
36 | 34, 35 | mp3an3 1326 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด ยท (๐ + 1)) = ((๐ด ยท ๐) + (๐ด ยท 1))) |
37 | | mulrid 7954 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ (๐ด ยท 1) = ๐ด) |
38 | 37 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด ยท 1) = ๐ด) |
39 | 38 | oveq2d 5891 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ด ยท ๐) + (๐ด ยท 1)) = ((๐ด ยท ๐) + ๐ด)) |
40 | 36, 39 | eqtrd 2210 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด ยท (๐ + 1)) = ((๐ด ยท ๐) + ๐ด)) |
41 | 33, 40 | sylan2 286 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ด ยท (๐ + 1)) = ((๐ด ยท ๐) + ๐ด)) |
42 | 41 | fveq2d 5520 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ0)
โ (expโ(๐ด
ยท (๐ + 1))) =
(expโ((๐ด ยท
๐) + ๐ด))) |
43 | | mulcl 7938 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด ยท ๐) โ โ) |
44 | 33, 43 | sylan2 286 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ด ยท ๐) โ
โ) |
45 | | simpl 109 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ0)
โ ๐ด โ
โ) |
46 | | efadd 11683 |
. . . . . . . . 9
โข (((๐ด ยท ๐) โ โ โง ๐ด โ โ) โ (expโ((๐ด ยท ๐) + ๐ด)) = ((expโ(๐ด ยท ๐)) ยท (expโ๐ด))) |
47 | 44, 45, 46 | syl2anc 411 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ0)
โ (expโ((๐ด
ยท ๐) + ๐ด)) = ((expโ(๐ด ยท ๐)) ยท (expโ๐ด))) |
48 | 42, 47 | eqtrd 2210 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (expโ(๐ด
ยท (๐ + 1))) =
((expโ(๐ด ยท
๐)) ยท
(expโ๐ด))) |
49 | 48 | adantr 276 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง (expโ(๐ด
ยท ๐)) =
((expโ๐ด)โ๐)) โ (expโ(๐ด ยท (๐ + 1))) = ((expโ(๐ด ยท ๐)) ยท (expโ๐ด))) |
50 | | expp1 10527 |
. . . . . . . 8
โข
(((expโ๐ด)
โ โ โง ๐
โ โ0) โ ((expโ๐ด)โ(๐ + 1)) = (((expโ๐ด)โ๐) ยท (expโ๐ด))) |
51 | 28, 50 | sylan 283 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((expโ๐ด)โ(๐ + 1)) = (((expโ๐ด)โ๐) ยท (expโ๐ด))) |
52 | 51 | adantr 276 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง (expโ(๐ด
ยท ๐)) =
((expโ๐ด)โ๐)) โ ((expโ๐ด)โ(๐ + 1)) = (((expโ๐ด)โ๐) ยท (expโ๐ด))) |
53 | 32, 49, 52 | 3eqtr4d 2220 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ0)
โง (expโ(๐ด
ยท ๐)) =
((expโ๐ด)โ๐)) โ (expโ(๐ด ยท (๐ + 1))) = ((expโ๐ด)โ(๐ + 1))) |
54 | 53 | exp31 364 |
. . . 4
โข (๐ด โ โ โ (๐ โ โ0
โ ((expโ(๐ด
ยท ๐)) =
((expโ๐ด)โ๐) โ (expโ(๐ด ยท (๐ + 1))) = ((expโ๐ด)โ(๐ + 1))))) |
55 | | oveq2 5883 |
. . . . . 6
โข
((expโ(๐ด
ยท ๐)) =
((expโ๐ด)โ๐) โ (1 / (expโ(๐ด ยท ๐))) = (1 / ((expโ๐ด)โ๐))) |
56 | | nncn 8927 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
57 | | mulneg2 8353 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด ยท -๐) = -(๐ด ยท ๐)) |
58 | 56, 57 | sylan2 286 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด ยท -๐) = -(๐ด ยท ๐)) |
59 | 58 | fveq2d 5520 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ
(expโ(๐ด ยท
-๐)) = (expโ-(๐ด ยท ๐))) |
60 | 56, 43 | sylan2 286 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ด ยท ๐) โ โ) |
61 | | efneg 11687 |
. . . . . . . . 9
โข ((๐ด ยท ๐) โ โ โ (expโ-(๐ด ยท ๐)) = (1 / (expโ(๐ด ยท ๐)))) |
62 | 60, 61 | syl 14 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ
(expโ-(๐ด ยท
๐)) = (1 /
(expโ(๐ด ยท
๐)))) |
63 | 59, 62 | eqtrd 2210 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ
(expโ(๐ด ยท
-๐)) = (1 /
(expโ(๐ด ยท
๐)))) |
64 | | efap0 11685 |
. . . . . . . 8
โข (๐ด โ โ โ
(expโ๐ด) #
0) |
65 | | nnnn0 9183 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
66 | | expnegap0 10528 |
. . . . . . . 8
โข
(((expโ๐ด)
โ โ โง (expโ๐ด) # 0 โง ๐ โ โ0) โ
((expโ๐ด)โ-๐) = (1 / ((expโ๐ด)โ๐))) |
67 | 28, 64, 65, 66 | syl2an3an 1298 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ
((expโ๐ด)โ-๐) = (1 / ((expโ๐ด)โ๐))) |
68 | 63, 67 | eqeq12d 2192 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ
((expโ(๐ด ยท
-๐)) = ((expโ๐ด)โ-๐) โ (1 / (expโ(๐ด ยท ๐))) = (1 / ((expโ๐ด)โ๐)))) |
69 | 55, 68 | imbitrrid 156 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ
((expโ(๐ด ยท
๐)) = ((expโ๐ด)โ๐) โ (expโ(๐ด ยท -๐)) = ((expโ๐ด)โ-๐))) |
70 | 69 | ex 115 |
. . . 4
โข (๐ด โ โ โ (๐ โ โ โ
((expโ(๐ด ยท
๐)) = ((expโ๐ด)โ๐) โ (expโ(๐ด ยท -๐)) = ((expโ๐ด)โ-๐)))) |
71 | 8, 12, 16, 20, 24, 30, 54, 70 | zindd 9371 |
. . 3
โข (๐ด โ โ โ (๐ โ โค โ
(expโ(๐ด ยท
๐)) = ((expโ๐ด)โ๐))) |
72 | 71 | imp 124 |
. 2
โข ((๐ด โ โ โง ๐ โ โค) โ
(expโ(๐ด ยท
๐)) = ((expโ๐ด)โ๐)) |
73 | 4, 72 | eqtr3d 2212 |
1
โข ((๐ด โ โ โง ๐ โ โค) โ
(expโ(๐ ยท
๐ด)) = ((expโ๐ด)โ๐)) |