Step | Hyp | Ref
| Expression |
1 | | nnuz 9563 |
. . 3
โข โ =
(โคโฅโ1) |
2 | | 1zzd 9280 |
. . 3
โข (๐ โ 1 โ
โค) |
3 | | expcnvap0.2 |
. . . . . . . 8
โข (๐ โ (absโ๐ด) < 1) |
4 | | expcnvap0.1 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
5 | | expcnvap0.0 |
. . . . . . . . . 10
โข (๐ โ ๐ด # 0) |
6 | 4, 5 | absrpclapd 11197 |
. . . . . . . . 9
โข (๐ โ (absโ๐ด) โ
โ+) |
7 | 6 | reclt1d 9710 |
. . . . . . . 8
โข (๐ โ ((absโ๐ด) < 1 โ 1 < (1 /
(absโ๐ด)))) |
8 | 3, 7 | mpbid 147 |
. . . . . . 7
โข (๐ โ 1 < (1 /
(absโ๐ด))) |
9 | | 1re 7956 |
. . . . . . . 8
โข 1 โ
โ |
10 | 6 | rpreccld 9707 |
. . . . . . . . 9
โข (๐ โ (1 / (absโ๐ด)) โ
โ+) |
11 | 10 | rpred 9696 |
. . . . . . . 8
โข (๐ โ (1 / (absโ๐ด)) โ
โ) |
12 | | difrp 9692 |
. . . . . . . 8
โข ((1
โ โ โง (1 / (absโ๐ด)) โ โ) โ (1 < (1 /
(absโ๐ด)) โ ((1 /
(absโ๐ด)) โ 1)
โ โ+)) |
13 | 9, 11, 12 | sylancr 414 |
. . . . . . 7
โข (๐ โ (1 < (1 /
(absโ๐ด)) โ ((1 /
(absโ๐ด)) โ 1)
โ โ+)) |
14 | 8, 13 | mpbid 147 |
. . . . . 6
โข (๐ โ ((1 / (absโ๐ด)) โ 1) โ
โ+) |
15 | 14 | rpreccld 9707 |
. . . . 5
โข (๐ โ (1 / ((1 /
(absโ๐ด)) โ 1))
โ โ+) |
16 | 15 | rpcnd 9698 |
. . . 4
โข (๐ โ (1 / ((1 /
(absโ๐ด)) โ 1))
โ โ) |
17 | | divcnv 11505 |
. . . 4
โข ((1 / ((1
/ (absโ๐ด)) โ
1)) โ โ โ (๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐)) โ
0) |
18 | 16, 17 | syl 14 |
. . 3
โข (๐ โ (๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐)) โ
0) |
19 | | nnex 8925 |
. . . . 5
โข โ
โ V |
20 | 19 | mptex 5743 |
. . . 4
โข (๐ โ โ โฆ
((absโ๐ด)โ๐)) โ V |
21 | 20 | a1i 9 |
. . 3
โข (๐ โ (๐ โ โ โฆ ((absโ๐ด)โ๐)) โ V) |
22 | | simpr 110 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ๐ โ โ) |
23 | 16 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (1 / ((1 /
(absโ๐ด)) โ 1))
โ โ) |
24 | 22 | nncnd 8933 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ๐ โ โ) |
25 | 22 | nnap0d 8965 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ๐ # 0) |
26 | 23, 24, 25 | divclapd 8747 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐) โ
โ) |
27 | | oveq2 5883 |
. . . . . 6
โข (๐ = ๐ โ ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐) = ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐)) |
28 | | eqid 2177 |
. . . . . 6
โข (๐ โ โ โฆ ((1 /
((1 / (absโ๐ด))
โ 1)) / ๐)) = (๐ โ โ โฆ ((1 /
((1 / (absโ๐ด))
โ 1)) / ๐)) |
29 | 27, 28 | fvmptg 5593 |
. . . . 5
โข ((๐ โ โ โง ((1 / ((1
/ (absโ๐ด)) โ
1)) / ๐) โ โ)
โ ((๐ โ โ
โฆ ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐))โ๐) = ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐)) |
30 | 22, 26, 29 | syl2anc 411 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐))โ๐) = ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐)) |
31 | 15 | rpred 9696 |
. . . . 5
โข (๐ โ (1 / ((1 /
(absโ๐ด)) โ 1))
โ โ) |
32 | | nndivre 8955 |
. . . . 5
โข (((1 /
((1 / (absโ๐ด))
โ 1)) โ โ โง ๐ โ โ) โ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐) โ
โ) |
33 | 31, 32 | sylan 283 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐) โ
โ) |
34 | 30, 33 | eqeltrd 2254 |
. . 3
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐))โ๐) โ
โ) |
35 | 6 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (absโ๐ด) โ
โ+) |
36 | 35 | rpcnd 9698 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (absโ๐ด) โ
โ) |
37 | | nnnn0 9183 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
38 | 37 | adantl 277 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ๐ โ โ0) |
39 | 36, 38 | expcld 10654 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((absโ๐ด)โ๐) โ โ) |
40 | | oveq2 5883 |
. . . . . . 7
โข (๐ = ๐ โ ((absโ๐ด)โ๐) = ((absโ๐ด)โ๐)) |
41 | | eqid 2177 |
. . . . . . 7
โข (๐ โ โ โฆ
((absโ๐ด)โ๐)) = (๐ โ โ โฆ ((absโ๐ด)โ๐)) |
42 | 40, 41 | fvmptg 5593 |
. . . . . 6
โข ((๐ โ โ โง
((absโ๐ด)โ๐) โ โ) โ ((๐ โ โ โฆ
((absโ๐ด)โ๐))โ๐) = ((absโ๐ด)โ๐)) |
43 | 22, 39, 42 | syl2anc 411 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) = ((absโ๐ด)โ๐)) |
44 | | nnz 9272 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
45 | | rpexpcl 10539 |
. . . . . 6
โข
(((absโ๐ด)
โ โ+ โง ๐ โ โค) โ ((absโ๐ด)โ๐) โ
โ+) |
46 | 6, 44, 45 | syl2an 289 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((absโ๐ด)โ๐) โ
โ+) |
47 | 43, 46 | eqeltrd 2254 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) โ
โ+) |
48 | 47 | rpred 9696 |
. . 3
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) โ โ) |
49 | | nnrp 9663 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ+) |
50 | | rpmulcl 9678 |
. . . . . . 7
โข ((((1 /
(absโ๐ด)) โ 1)
โ โ+ โง ๐ โ โ+) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โ
โ+) |
51 | 14, 49, 50 | syl2an 289 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โ
โ+) |
52 | 51 | rpred 9696 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โ
โ) |
53 | | peano2re 8093 |
. . . . . . . . 9
โข ((((1 /
(absโ๐ด)) โ 1)
ยท ๐) โ โ
โ ((((1 / (absโ๐ด)) โ 1) ยท ๐) + 1) โ โ) |
54 | 52, 53 | syl 14 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((((1 /
(absโ๐ด)) โ 1)
ยท ๐) + 1) โ
โ) |
55 | | rpexpcl 10539 |
. . . . . . . . . 10
โข (((1 /
(absโ๐ด)) โ
โ+ โง ๐
โ โค) โ ((1 / (absโ๐ด))โ๐) โ
โ+) |
56 | 10, 44, 55 | syl2an 289 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((1 /
(absโ๐ด))โ๐) โ
โ+) |
57 | 56 | rpred 9696 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((1 /
(absโ๐ด))โ๐) โ
โ) |
58 | 52 | lep1d 8888 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โค ((((1 /
(absโ๐ด)) โ 1)
ยท ๐) +
1)) |
59 | 11 | adantr 276 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (1 / (absโ๐ด)) โ
โ) |
60 | 10 | rpge0d 9700 |
. . . . . . . . . 10
โข (๐ โ 0 โค (1 /
(absโ๐ด))) |
61 | 60 | adantr 276 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ 0 โค (1 /
(absโ๐ด))) |
62 | | bernneq2 10642 |
. . . . . . . . 9
โข (((1 /
(absโ๐ด)) โ
โ โง ๐ โ
โ0 โง 0 โค (1 / (absโ๐ด))) โ ((((1 / (absโ๐ด)) โ 1) ยท ๐) + 1) โค ((1 /
(absโ๐ด))โ๐)) |
63 | 59, 38, 61, 62 | syl3anc 1238 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((((1 /
(absโ๐ด)) โ 1)
ยท ๐) + 1) โค ((1 /
(absโ๐ด))โ๐)) |
64 | 52, 54, 57, 58, 63 | letrd 8081 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โค ((1 /
(absโ๐ด))โ๐)) |
65 | 6 | rpcnd 9698 |
. . . . . . . 8
โข (๐ โ (absโ๐ด) โ
โ) |
66 | 6 | rpap0d 9702 |
. . . . . . . 8
โข (๐ โ (absโ๐ด) # 0) |
67 | | exprecap 10561 |
. . . . . . . 8
โข
(((absโ๐ด)
โ โ โง (absโ๐ด) # 0 โง ๐ โ โค) โ ((1 /
(absโ๐ด))โ๐) = (1 / ((absโ๐ด)โ๐))) |
68 | 65, 66, 44, 67 | syl2an3an 1298 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ((1 /
(absโ๐ด))โ๐) = (1 / ((absโ๐ด)โ๐))) |
69 | 64, 68 | breqtrd 4030 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (((1 /
(absโ๐ด)) โ 1)
ยท ๐) โค (1 /
((absโ๐ด)โ๐))) |
70 | 51, 46, 69 | lerec2d 9718 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((absโ๐ด)โ๐) โค (1 / (((1 / (absโ๐ด)) โ 1) ยท ๐))) |
71 | 14 | rpcnd 9698 |
. . . . . . 7
โข (๐ โ ((1 / (absโ๐ด)) โ 1) โ
โ) |
72 | 14 | rpap0d 9702 |
. . . . . . 7
โข (๐ โ ((1 / (absโ๐ด)) โ 1) #
0) |
73 | 71, 72 | jca 306 |
. . . . . 6
โข (๐ โ (((1 / (absโ๐ด)) โ 1) โ โ
โง ((1 / (absโ๐ด))
โ 1) # 0)) |
74 | | nncn 8927 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
75 | | nnap0 8948 |
. . . . . . 7
โข (๐ โ โ โ ๐ # 0) |
76 | 74, 75 | jca 306 |
. . . . . 6
โข (๐ โ โ โ (๐ โ โ โง ๐ # 0)) |
77 | | recdivap2 8682 |
. . . . . 6
โข (((((1 /
(absโ๐ด)) โ 1)
โ โ โง ((1 / (absโ๐ด)) โ 1) # 0) โง (๐ โ โ โง ๐ # 0)) โ ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐) = (1 / (((1 / (absโ๐ด)) โ 1) ยท ๐))) |
78 | 73, 76, 77 | syl2an 289 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐) = (1 / (((1 /
(absโ๐ด)) โ 1)
ยท ๐))) |
79 | 70, 78 | breqtrrd 4032 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ((absโ๐ด)โ๐) โค ((1 / ((1 / (absโ๐ด)) โ 1)) / ๐)) |
80 | 79, 43, 30 | 3brtr4d 4036 |
. . 3
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) โค ((๐ โ โ โฆ ((1 / ((1 /
(absโ๐ด)) โ 1))
/ ๐))โ๐)) |
81 | 47 | rpge0d 9700 |
. . 3
โข ((๐ โง ๐ โ โ) โ 0 โค ((๐ โ โ โฆ
((absโ๐ด)โ๐))โ๐)) |
82 | 1, 2, 18, 21, 34, 48, 80, 81 | climsqz2 11344 |
. 2
โข (๐ โ (๐ โ โ โฆ ((absโ๐ด)โ๐)) โ 0) |
83 | | nn0ex 9182 |
. . . . 5
โข
โ0 โ V |
84 | 83 | mptex 5743 |
. . . 4
โข (๐ โ โ0
โฆ (๐ดโ๐)) โ V |
85 | 84 | a1i 9 |
. . 3
โข (๐ โ (๐ โ โ0 โฆ (๐ดโ๐)) โ V) |
86 | 4 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ๐ด โ โ) |
87 | 86, 38 | expcld 10654 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
88 | | oveq2 5883 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
89 | | eqid 2177 |
. . . . . 6
โข (๐ โ โ0
โฆ (๐ดโ๐)) = (๐ โ โ0 โฆ (๐ดโ๐)) |
90 | 88, 89 | fvmptg 5593 |
. . . . 5
โข ((๐ โ โ0
โง (๐ดโ๐) โ โ) โ ((๐ โ โ0
โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
91 | 38, 87, 90 | syl2anc 411 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ0 โฆ (๐ดโ๐))โ๐) = (๐ดโ๐)) |
92 | | expcl 10538 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
93 | 4, 37, 92 | syl2an 289 |
. . . 4
โข ((๐ โง ๐ โ โ) โ (๐ดโ๐) โ โ) |
94 | 91, 93 | eqeltrd 2254 |
. . 3
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ0 โฆ (๐ดโ๐))โ๐) โ โ) |
95 | | absexp 11088 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |
96 | 4, 37, 95 | syl2an 289 |
. . . 4
โข ((๐ โง ๐ โ โ) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |
97 | 91 | fveq2d 5520 |
. . . 4
โข ((๐ โง ๐ โ โ) โ (absโ((๐ โ โ0
โฆ (๐ดโ๐))โ๐)) = (absโ(๐ดโ๐))) |
98 | 96, 97, 43 | 3eqtr4rd 2221 |
. . 3
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((absโ๐ด)โ๐))โ๐) = (absโ((๐ โ โ0 โฆ (๐ดโ๐))โ๐))) |
99 | 1, 2, 85, 21, 94, 98 | climabs0 11315 |
. 2
โข (๐ โ ((๐ โ โ0 โฆ (๐ดโ๐)) โ 0 โ (๐ โ โ โฆ ((absโ๐ด)โ๐)) โ 0)) |
100 | 82, 99 | mpbird 167 |
1
โข (๐ โ (๐ โ โ0 โฆ (๐ดโ๐)) โ 0) |