Step | Hyp | Ref
| Expression |
1 | | nnuz 12813 |
. . 3
โข โ =
(โคโฅโ1) |
2 | | 1zzd 12541 |
. . 3
โข ((๐ โง ๐ด = 0) โ 1 โ
โค) |
3 | | nn0ex 12426 |
. . . . 5
โข
โ0 โ V |
4 | 3 | mptex 7178 |
. . . 4
โข (๐ โ โ0
โฆ (๐ดโ๐)) โ V |
5 | 4 | a1i 11 |
. . 3
โข ((๐ โง ๐ด = 0) โ (๐ โ โ0 โฆ (๐ดโ๐)) โ V) |
6 | | 0cnd 11155 |
. . 3
โข ((๐ โง ๐ด = 0) โ 0 โ
โ) |
7 | | nnnn0 12427 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ0) |
8 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
9 | | eqid 2737 |
. . . . . . 7
โข (๐ โ โ0
โฆ (๐ดโ๐)) = (๐ โ โ0 โฆ (๐ดโ๐)) |
10 | | ovex 7395 |
. . . . . . 7
โข (๐ดโ๐) โ V |
11 | 8, 9, 10 | fvmpt 6953 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
12 | 7, 11 | syl 17 |
. . . . 5
โข (๐ โ โ โ ((๐ โ โ0
โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
13 | | simpr 486 |
. . . . . 6
โข ((๐ โง ๐ด = 0) โ ๐ด = 0) |
14 | 13 | oveq1d 7377 |
. . . . 5
โข ((๐ โง ๐ด = 0) โ (๐ดโ๐) = (0โ๐)) |
15 | 12, 14 | sylan9eqr 2799 |
. . . 4
โข (((๐ โง ๐ด = 0) โง ๐ โ โ) โ ((๐ โ โ0 โฆ (๐ดโ๐))โ๐) = (0โ๐)) |
16 | | 0exp 14010 |
. . . . 5
โข (๐ โ โ โ
(0โ๐) =
0) |
17 | 16 | adantl 483 |
. . . 4
โข (((๐ โง ๐ด = 0) โง ๐ โ โ) โ (0โ๐) = 0) |
18 | 15, 17 | eqtrd 2777 |
. . 3
โข (((๐ โง ๐ด = 0) โง ๐ โ โ) โ ((๐ โ โ0 โฆ (๐ดโ๐))โ๐) = 0) |
19 | 1, 2, 5, 6, 18 | climconst 15432 |
. 2
โข ((๐ โง ๐ด = 0) โ (๐ โ โ0 โฆ (๐ดโ๐)) โ 0) |
20 | | 1zzd 12541 |
. . . 4
โข ((๐ โง ๐ด โ 0) โ 1 โ
โค) |
21 | | expcnv.2 |
. . . . . . . . . 10
โข (๐ โ (absโ๐ด) < 1) |
22 | 21 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ด โ 0) โ (absโ๐ด) < 1) |
23 | | expcnv.1 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โ) |
24 | | absrpcl 15180 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0) โ (absโ๐ด) โ
โ+) |
25 | 23, 24 | sylan 581 |
. . . . . . . . . 10
โข ((๐ โง ๐ด โ 0) โ (absโ๐ด) โ
โ+) |
26 | 25 | reclt1d 12977 |
. . . . . . . . 9
โข ((๐ โง ๐ด โ 0) โ ((absโ๐ด) < 1 โ 1 < (1 /
(absโ๐ด)))) |
27 | 22, 26 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง ๐ด โ 0) โ 1 < (1 / (absโ๐ด))) |
28 | | 1re 11162 |
. . . . . . . . 9
โข 1 โ
โ |
29 | 25 | rpreccld 12974 |
. . . . . . . . . 10
โข ((๐ โง ๐ด โ 0) โ (1 / (absโ๐ด)) โ
โ+) |
30 | 29 | rpred 12964 |
. . . . . . . . 9
โข ((๐ โง ๐ด โ 0) โ (1 / (absโ๐ด)) โ
โ) |
31 | | difrp 12960 |
. . . . . . . . 9
โข ((1
โ โ โง (1 / (absโ๐ด)) โ โ) โ (1 < (1 /
(absโ๐ด)) โ ((1 /
(absโ๐ด)) โ 1)
โ โ+)) |
32 | 28, 30, 31 | sylancr 588 |
. . . . . . . 8
โข ((๐ โง ๐ด โ 0) โ (1 < (1 /
(absโ๐ด)) โ ((1 /
(absโ๐ด)) โ 1)
โ โ+)) |
33 | 27, 32 | mpbid 231 |
. . . . . . 7
โข ((๐ โง ๐ด โ 0) โ ((1 / (absโ๐ด)) โ 1) โ
โ+) |
34 | 33 | rpreccld 12974 |
. . . . . 6
โข ((๐ โง ๐ด โ 0) โ (1 / ((1 / (absโ๐ด)) โ 1)) โ
โ+) |
35 | 34 | rpcnd 12966 |
. . . . 5
โข ((๐ โง ๐ด โ 0) โ (1 / ((1 / (absโ๐ด)) โ 1)) โ
โ) |
36 | | divcnv 15745 |
. . . . 5
โข ((1 / ((1
/ (absโ๐ด)) โ
1)) โ โ โ (๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐)) โ
0) |
37 | 35, 36 | syl 17 |
. . . 4
โข ((๐ โง ๐ด โ 0) โ (๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐)) โ
0) |
38 | | nnex 12166 |
. . . . . 6
โข โ
โ V |
39 | 38 | mptex 7178 |
. . . . 5
โข (๐ โ โ โฆ
((absโ๐ด)โ๐)) โ V |
40 | 39 | a1i 11 |
. . . 4
โข ((๐ โง ๐ด โ 0) โ (๐ โ โ โฆ ((absโ๐ด)โ๐)) โ V) |
41 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ โ ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐) = ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐)) |
42 | | eqid 2737 |
. . . . . . 7
โข (๐ โ โ โฆ ((1 /
((1 / (absโ๐ด))
โ 1)) / ๐)) = (๐ โ โ โฆ ((1 /
((1 / (absโ๐ด))
โ 1)) / ๐)) |
43 | | ovex 7395 |
. . . . . . 7
โข ((1 / ((1
/ (absโ๐ด)) โ
1)) / ๐) โ
V |
44 | 41, 42, 43 | fvmpt 6953 |
. . . . . 6
โข (๐ โ โ โ ((๐ โ โ โฆ ((1 /
((1 / (absโ๐ด))
โ 1)) / ๐))โ๐) = ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐)) |
45 | 44 | adantl 483 |
. . . . 5
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐))โ๐) = ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐)) |
46 | 34 | rpred 12964 |
. . . . . 6
โข ((๐ โง ๐ด โ 0) โ (1 / ((1 / (absโ๐ด)) โ 1)) โ
โ) |
47 | | nndivre 12201 |
. . . . . 6
โข (((1 /
((1 / (absโ๐ด))
โ 1)) โ โ โง ๐ โ โ) โ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐) โ
โ) |
48 | 46, 47 | sylan 581 |
. . . . 5
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐) โ
โ) |
49 | 45, 48 | eqeltrd 2838 |
. . . 4
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐))โ๐) โ
โ) |
50 | | oveq2 7370 |
. . . . . . . 8
โข (๐ = ๐ โ ((absโ๐ด)โ๐) = ((absโ๐ด)โ๐)) |
51 | | eqid 2737 |
. . . . . . . 8
โข (๐ โ โ โฆ
((absโ๐ด)โ๐)) = (๐ โ โ โฆ ((absโ๐ด)โ๐)) |
52 | | ovex 7395 |
. . . . . . . 8
โข
((absโ๐ด)โ๐) โ V |
53 | 50, 51, 52 | fvmpt 6953 |
. . . . . . 7
โข (๐ โ โ โ ((๐ โ โ โฆ
((absโ๐ด)โ๐))โ๐) = ((absโ๐ด)โ๐)) |
54 | 53 | adantl 483 |
. . . . . 6
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) = ((absโ๐ด)โ๐)) |
55 | | nnz 12527 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
56 | | rpexpcl 13993 |
. . . . . . 7
โข
(((absโ๐ด)
โ โ+ โง ๐ โ โค) โ ((absโ๐ด)โ๐) โ
โ+) |
57 | 25, 55, 56 | syl2an 597 |
. . . . . 6
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((absโ๐ด)โ๐) โ
โ+) |
58 | 54, 57 | eqeltrd 2838 |
. . . . 5
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) โ
โ+) |
59 | 58 | rpred 12964 |
. . . 4
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) โ โ) |
60 | | nnrp 12933 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ+) |
61 | | rpmulcl 12945 |
. . . . . . . 8
โข ((((1 /
(absโ๐ด)) โ 1)
โ โ+ โง ๐ โ โ+) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โ
โ+) |
62 | 33, 60, 61 | syl2an 597 |
. . . . . . 7
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โ
โ+) |
63 | 62 | rpred 12964 |
. . . . . . . . 9
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โ
โ) |
64 | | peano2re 11335 |
. . . . . . . . . 10
โข ((((1 /
(absโ๐ด)) โ 1)
ยท ๐) โ โ
โ ((((1 / (absโ๐ด)) โ 1) ยท ๐) + 1) โ โ) |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((((1 /
(absโ๐ด)) โ 1)
ยท ๐) + 1) โ
โ) |
66 | | rpexpcl 13993 |
. . . . . . . . . . 11
โข (((1 /
(absโ๐ด)) โ
โ+ โง ๐
โ โค) โ ((1 / (absโ๐ด))โ๐) โ
โ+) |
67 | 29, 55, 66 | syl2an 597 |
. . . . . . . . . 10
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((1 /
(absโ๐ด))โ๐) โ
โ+) |
68 | 67 | rpred 12964 |
. . . . . . . . 9
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((1 /
(absโ๐ด))โ๐) โ
โ) |
69 | 63 | lep1d 12093 |
. . . . . . . . 9
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โค ((((1 /
(absโ๐ด)) โ 1)
ยท ๐) +
1)) |
70 | 30 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ (1 / (absโ๐ด)) โ
โ) |
71 | 7 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ๐ โ โ0) |
72 | 29 | rpge0d 12968 |
. . . . . . . . . . 11
โข ((๐ โง ๐ด โ 0) โ 0 โค (1 / (absโ๐ด))) |
73 | 72 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ 0 โค (1 /
(absโ๐ด))) |
74 | | bernneq2 14140 |
. . . . . . . . . 10
โข (((1 /
(absโ๐ด)) โ
โ โง ๐ โ
โ0 โง 0 โค (1 / (absโ๐ด))) โ ((((1 / (absโ๐ด)) โ 1) ยท ๐) + 1) โค ((1 /
(absโ๐ด))โ๐)) |
75 | 70, 71, 73, 74 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((((1 /
(absโ๐ด)) โ 1)
ยท ๐) + 1) โค ((1 /
(absโ๐ด))โ๐)) |
76 | 63, 65, 68, 69, 75 | letrd 11319 |
. . . . . . . 8
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โค ((1 /
(absโ๐ด))โ๐)) |
77 | 25 | rpcnne0d 12973 |
. . . . . . . . 9
โข ((๐ โง ๐ด โ 0) โ ((absโ๐ด) โ โ โง
(absโ๐ด) โ
0)) |
78 | | exprec 14016 |
. . . . . . . . . 10
โข
(((absโ๐ด)
โ โ โง (absโ๐ด) โ 0 โง ๐ โ โค) โ ((1 /
(absโ๐ด))โ๐) = (1 / ((absโ๐ด)โ๐))) |
79 | 78 | 3expa 1119 |
. . . . . . . . 9
โข
((((absโ๐ด)
โ โ โง (absโ๐ด) โ 0) โง ๐ โ โค) โ ((1 /
(absโ๐ด))โ๐) = (1 / ((absโ๐ด)โ๐))) |
80 | 77, 55, 79 | syl2an 597 |
. . . . . . . 8
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((1 /
(absโ๐ด))โ๐) = (1 / ((absโ๐ด)โ๐))) |
81 | 76, 80 | breqtrd 5136 |
. . . . . . 7
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โค (1 /
((absโ๐ด)โ๐))) |
82 | 62, 57, 81 | lerec2d 12985 |
. . . . . 6
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((absโ๐ด)โ๐) โค (1 / (((1 / (absโ๐ด)) โ 1) ยท ๐))) |
83 | 33 | rpcnne0d 12973 |
. . . . . . 7
โข ((๐ โง ๐ด โ 0) โ (((1 / (absโ๐ด)) โ 1) โ โ
โง ((1 / (absโ๐ด))
โ 1) โ 0)) |
84 | | nncn 12168 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
85 | | nnne0 12194 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ 0) |
86 | 84, 85 | jca 513 |
. . . . . . 7
โข (๐ โ โ โ (๐ โ โ โง ๐ โ 0)) |
87 | | recdiv2 11875 |
. . . . . . 7
โข (((((1 /
(absโ๐ด)) โ 1)
โ โ โง ((1 / (absโ๐ด)) โ 1) โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐) = (1 / (((1 /
(absโ๐ด)) โ 1)
ยท ๐))) |
88 | 83, 86, 87 | syl2an 597 |
. . . . . 6
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐) = (1 / (((1 /
(absโ๐ด)) โ 1)
ยท ๐))) |
89 | 82, 88 | breqtrrd 5138 |
. . . . 5
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((absโ๐ด)โ๐) โค ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐)) |
90 | 89, 54, 45 | 3brtr4d 5142 |
. . . 4
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) โค ((๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐))โ๐)) |
91 | 58 | rpge0d 12968 |
. . . 4
โข (((๐ โง ๐ด โ 0) โง ๐ โ โ) โ 0 โค ((๐ โ โ โฆ
((absโ๐ด)โ๐))โ๐)) |
92 | 1, 20, 37, 40, 49, 59, 90, 91 | climsqz2 15531 |
. . 3
โข ((๐ โง ๐ด โ 0) โ (๐ โ โ โฆ ((absโ๐ด)โ๐)) โ 0) |
93 | | 1zzd 12541 |
. . . . 5
โข (๐ โ 1 โ
โค) |
94 | 4 | a1i 11 |
. . . . 5
โข (๐ โ (๐ โ โ0 โฆ (๐ดโ๐)) โ V) |
95 | 39 | a1i 11 |
. . . . 5
โข (๐ โ (๐ โ โ โฆ ((absโ๐ด)โ๐)) โ V) |
96 | 7 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ๐ โ โ0) |
97 | 96, 11 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ0 โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
98 | | expcl 13992 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
99 | 23, 7, 98 | syl2an 597 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
100 | 97, 99 | eqeltrd 2838 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ0 โฆ (๐ดโ๐))โ๐) โ โ) |
101 | | absexp 15196 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |
102 | 23, 7, 101 | syl2an 597 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |
103 | 97 | fveq2d 6851 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (absโ((๐ โ โ0
โฆ (๐ดโ๐))โ๐)) = (absโ(๐ดโ๐))) |
104 | 53 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) = ((absโ๐ด)โ๐)) |
105 | 102, 103,
104 | 3eqtr4rd 2788 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) = (absโ((๐ โ โ0 โฆ (๐ดโ๐))โ๐))) |
106 | 1, 93, 94, 95, 100, 105 | climabs0 15474 |
. . . 4
โข (๐ โ ((๐ โ โ0 โฆ (๐ดโ๐)) โ 0 โ (๐ โ โ โฆ ((absโ๐ด)โ๐)) โ 0)) |
107 | 106 | biimpar 479 |
. . 3
โข ((๐ โง (๐ โ โ โฆ ((absโ๐ด)โ๐)) โ 0) โ (๐ โ โ0 โฆ (๐ดโ๐)) โ 0) |
108 | 92, 107 | syldan 592 |
. 2
โข ((๐ โง ๐ด โ 0) โ (๐ โ โ0 โฆ (๐ดโ๐)) โ 0) |
109 | 19, 108 | pm2.61dane 3033 |
1
โข (๐ โ (๐ โ โ0 โฆ (๐ดโ๐)) โ 0) |