Step | Hyp | Ref
| Expression |
1 | | 0red 11165 |
. 2
โข (๐ด โ โ โ 0 โ
โ) |
2 | | imcl 15003 |
. 2
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
3 | | ax-icn 11117 |
. . . . . . . . 9
โข i โ
โ |
4 | | negcl 11408 |
. . . . . . . . . 10
โข (๐ด โ โ โ -๐ด โ
โ) |
5 | 4 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
-๐ด โ
โ) |
6 | | mulcl 11142 |
. . . . . . . . 9
โข ((i
โ โ โง -๐ด
โ โ) โ (i ยท -๐ด) โ โ) |
7 | 3, 5, 6 | sylancr 588 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(i ยท -๐ด) โ
โ) |
8 | | ax-1cn 11116 |
. . . . . . . . . 10
โข 1 โ
โ |
9 | 5 | sqcld 14056 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(-๐ดโ2) โ
โ) |
10 | | subcl 11407 |
. . . . . . . . . 10
โข ((1
โ โ โง (-๐ดโ2) โ โ) โ (1 โ
(-๐ดโ2)) โ
โ) |
11 | 8, 9, 10 | sylancr 588 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(1 โ (-๐ดโ2))
โ โ) |
12 | 11 | sqrtcld 15329 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ(1 โ (-๐ดโ2))) โ โ) |
13 | 7, 12 | addcld 11181 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
((i ยท -๐ด) +
(โโ(1 โ (-๐ดโ2)))) โ โ) |
14 | | asinlem 26234 |
. . . . . . . 8
โข (-๐ด โ โ โ ((i
ยท -๐ด) +
(โโ(1 โ (-๐ดโ2)))) โ 0) |
15 | 5, 14 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
((i ยท -๐ด) +
(โโ(1 โ (-๐ดโ2)))) โ 0) |
16 | 13, 15 | absrpcld 15340 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(absโ((i ยท -๐ด)
+ (โโ(1 โ (-๐ดโ2))))) โ
โ+) |
17 | | 2z 12542 |
. . . . . 6
โข 2 โ
โค |
18 | | rpexpcl 13993 |
. . . . . 6
โข
(((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2))))) โ
โ+ โง 2 โ โค) โ ((absโ((i ยท
-๐ด) + (โโ(1
โ (-๐ดโ2)))))โ2) โ
โ+) |
19 | 16, 17, 18 | sylancl 587 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2) โ
โ+) |
20 | 19 | rprecred 12975 |
. . . 4
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(1 / ((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2)) โ
โ) |
21 | 13 | cjcld 15088 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2))))) โ
โ) |
22 | 21 | recld 15086 |
. . . 4
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))) โ
โ) |
23 | 19 | rpreccld 12974 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(1 / ((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2)) โ
โ+) |
24 | 23 | rpge0d 12968 |
. . . 4
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ 0
โค (1 / ((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2))) |
25 | | imneg 15025 |
. . . . . . . 8
โข (๐ด โ โ โ
(โโ-๐ด) =
-(โโ๐ด)) |
26 | 25 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ-๐ด) =
-(โโ๐ด)) |
27 | 2 | le0neg2d 11734 |
. . . . . . . 8
โข (๐ด โ โ โ (0 โค
(โโ๐ด) โ
-(โโ๐ด) โค
0)) |
28 | 27 | biimpa 478 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
-(โโ๐ด) โค
0) |
29 | 26, 28 | eqbrtrd 5132 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ-๐ด) โค
0) |
30 | | asinlem3a 26236 |
. . . . . 6
โข ((-๐ด โ โ โง
(โโ-๐ด) โค 0)
โ 0 โค (โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))) |
31 | 5, 29, 30 | syl2anc 585 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ 0
โค (โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))) |
32 | 13 | recjd 15096 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))) =
(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))) |
33 | 31, 32 | breqtrrd 5138 |
. . . 4
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ 0
โค (โโ(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2))))))) |
34 | 20, 22, 24, 33 | mulge0d 11739 |
. . 3
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ 0
โค ((1 / ((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2)) ยท
(โโ(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))))) |
35 | | recval 15214 |
. . . . . . 7
โข ((((i
ยท -๐ด) +
(โโ(1 โ (-๐ดโ2)))) โ โ โง ((i
ยท -๐ด) +
(โโ(1 โ (-๐ดโ2)))) โ 0) โ (1 / ((i ยท
-๐ด) + (โโ(1
โ (-๐ดโ2))))) =
((โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2))))) / ((absโ((i
ยท -๐ด) +
(โโ(1 โ (-๐ดโ2)))))โ2))) |
36 | 13, 15, 35 | syl2anc 585 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(1 / ((i ยท -๐ด) +
(โโ(1 โ (-๐ดโ2))))) = ((โโ((i ยท
-๐ด) + (โโ(1
โ (-๐ดโ2))))) /
((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2))) |
37 | | asinlem2 26235 |
. . . . . . . . 9
โข (๐ด โ โ โ (((i
ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) ยท ((i ยท -๐ด) + (โโ(1 โ
(-๐ดโ2))))) =
1) |
38 | 37 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(((i ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) ยท ((i ยท -๐ด) + (โโ(1 โ
(-๐ดโ2))))) =
1) |
39 | 38 | eqcomd 2743 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ 1
= (((i ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) ยท ((i ยท -๐ด) + (โโ(1 โ
(-๐ดโ2)))))) |
40 | | 1cnd 11157 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ 1
โ โ) |
41 | | simpl 484 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
๐ด โ
โ) |
42 | | mulcl 11142 |
. . . . . . . . . 10
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
43 | 3, 41, 42 | sylancr 588 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(i ยท ๐ด) โ
โ) |
44 | | sqcl 14030 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ (๐ดโ2) โ
โ) |
45 | 44 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(๐ดโ2) โ
โ) |
46 | | subcl 11407 |
. . . . . . . . . . 11
โข ((1
โ โ โง (๐ดโ2) โ โ) โ (1 โ
(๐ดโ2)) โ
โ) |
47 | 8, 45, 46 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(1 โ (๐ดโ2))
โ โ) |
48 | 47 | sqrtcld 15329 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ(1 โ (๐ดโ2))) โ โ) |
49 | 43, 48 | addcld 11181 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
((i ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) โ โ) |
50 | 40, 49, 13, 15 | divmul3d 11972 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
((1 / ((i ยท -๐ด) +
(โโ(1 โ (-๐ดโ2))))) = ((i ยท ๐ด) + (โโ(1 โ
(๐ดโ2)))) โ 1 =
(((i ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) ยท ((i ยท -๐ด) + (โโ(1 โ
(-๐ดโ2))))))) |
51 | 39, 50 | mpbird 257 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(1 / ((i ยท -๐ด) +
(โโ(1 โ (-๐ดโ2))))) = ((i ยท ๐ด) + (โโ(1 โ
(๐ดโ2))))) |
52 | 19 | rpcnd 12966 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2) โ
โ) |
53 | 19 | rpne0d 12969 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2) โ
0) |
54 | 21, 52, 53 | divrec2d 11942 |
. . . . . 6
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
((โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2))))) / ((absโ((i
ยท -๐ด) +
(โโ(1 โ (-๐ดโ2)))))โ2)) = ((1 /
((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2)) ยท
(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2))))))) |
55 | 36, 51, 54 | 3eqtr3d 2785 |
. . . . 5
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
((i ยท ๐ด) +
(โโ(1 โ (๐ดโ2)))) = ((1 / ((absโ((i ยท
-๐ด) + (โโ(1
โ (-๐ดโ2)))))โ2)) ยท
(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2))))))) |
56 | 55 | fveq2d 6851 |
. . . 4
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ((i ยท ๐ด) + (โโ(1 โ (๐ดโ2))))) = (โโ((1
/ ((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2)) ยท
(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))))) |
57 | 20, 21 | remul2d 15119 |
. . . 4
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ((1 / ((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2)) ยท
(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2))))))) = ((1 /
((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2)) ยท
(โโ(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))))) |
58 | 56, 57 | eqtrd 2777 |
. . 3
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ
(โโ((i ยท ๐ด) + (โโ(1 โ (๐ดโ2))))) = ((1 /
((absโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))โ2)) ยท
(โโ(โโ((i ยท -๐ด) + (โโ(1 โ (-๐ดโ2)))))))) |
59 | 34, 58 | breqtrrd 5138 |
. 2
โข ((๐ด โ โ โง 0 โค
(โโ๐ด)) โ 0
โค (โโ((i ยท ๐ด) + (โโ(1 โ (๐ดโ2)))))) |
60 | | asinlem3a 26236 |
. 2
โข ((๐ด โ โ โง
(โโ๐ด) โค 0)
โ 0 โค (โโ((i ยท ๐ด) + (โโ(1 โ (๐ดโ2)))))) |
61 | 1, 2, 59, 60 | lecasei 11268 |
1
โข (๐ด โ โ โ 0 โค
(โโ((i ยท ๐ด) + (โโ(1 โ (๐ดโ2)))))) |