Step | Hyp | Ref
| Expression |
1 | | nnuz 12811 |
. 2
โข โ =
(โคโฅโ1) |
2 | | 1zzd 12539 |
. 2
โข (๐ โ 1 โ
โค) |
3 | | oveq1 7365 |
. . . . 5
โข (๐ = ๐ โ (๐โ๐-(โโ๐)) = (๐โ๐-(โโ๐))) |
4 | | eqid 2733 |
. . . . 5
โข (๐ โ โ โฆ (๐โ๐-(โโ๐))) = (๐ โ โ โฆ (๐โ๐-(โโ๐))) |
5 | | ovex 7391 |
. . . . 5
โข (๐โ๐-(โโ๐)) โ V |
6 | 3, 4, 5 | fvmpt 6949 |
. . . 4
โข (๐ โ โ โ ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ๐) = (๐โ๐-(โโ๐))) |
7 | 6 | adantl 483 |
. . 3
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ๐) = (๐โ๐-(โโ๐))) |
8 | | zetacvg.3 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) = (๐โ๐-๐)) |
9 | | nncn 12166 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
10 | 9 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ๐ โ โ) |
11 | | nnne0 12192 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ 0) |
12 | 11 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ๐ โ 0) |
13 | | zetacvg.1 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
14 | 13 | negcld 11504 |
. . . . . . . 8
โข (๐ โ -๐ โ โ) |
15 | 14 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ -๐ โ โ) |
16 | 10, 12, 15 | cxpefd 26083 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (๐โ๐-๐) = (expโ(-๐ ยท (logโ๐)))) |
17 | 8, 16 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) = (expโ(-๐ ยท (logโ๐)))) |
18 | 17 | fveq2d 6847 |
. . . 4
โข ((๐ โง ๐ โ โ) โ (absโ(๐นโ๐)) = (absโ(expโ(-๐ ยท (logโ๐))))) |
19 | | nnrp 12931 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ+) |
20 | 19 | relogcld 25994 |
. . . . . . 7
โข (๐ โ โ โ
(logโ๐) โ
โ) |
21 | 20 | recnd 11188 |
. . . . . 6
โข (๐ โ โ โ
(logโ๐) โ
โ) |
22 | | mulcl 11140 |
. . . . . 6
โข ((-๐ โ โ โง
(logโ๐) โ
โ) โ (-๐
ยท (logโ๐))
โ โ) |
23 | 14, 21, 22 | syl2an 597 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (-๐ ยท (logโ๐)) โ โ) |
24 | | absef 16084 |
. . . . 5
โข ((-๐ ยท (logโ๐)) โ โ โ
(absโ(expโ(-๐
ยท (logโ๐)))) =
(expโ(โโ(-๐ ยท (logโ๐))))) |
25 | 23, 24 | syl 17 |
. . . 4
โข ((๐ โง ๐ โ โ) โ
(absโ(expโ(-๐
ยท (logโ๐)))) =
(expโ(โโ(-๐ ยท (logโ๐))))) |
26 | | remul 15020 |
. . . . . . . 8
โข ((-๐ โ โ โง
(logโ๐) โ
โ) โ (โโ(-๐ ยท (logโ๐))) = (((โโ-๐) ยท (โโ(logโ๐))) โ
((โโ-๐)
ยท (โโ(logโ๐))))) |
27 | 14, 21, 26 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (โโ(-๐ ยท (logโ๐))) = (((โโ-๐) ยท
(โโ(logโ๐))) โ ((โโ-๐) ยท
(โโ(logโ๐))))) |
28 | 13 | renegd 15100 |
. . . . . . . . 9
โข (๐ โ (โโ-๐) = -(โโ๐)) |
29 | 20 | rered 15115 |
. . . . . . . . 9
โข (๐ โ โ โ
(โโ(logโ๐)) = (logโ๐)) |
30 | 28, 29 | oveqan12d 7377 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((โโ-๐) ยท
(โโ(logโ๐))) = (-(โโ๐) ยท (logโ๐))) |
31 | 20 | reim0d 15116 |
. . . . . . . . . 10
โข (๐ โ โ โ
(โโ(logโ๐)) = 0) |
32 | 31 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ โ โ
((โโ-๐)
ยท (โโ(logโ๐))) = ((โโ-๐) ยท 0)) |
33 | | imcl 15002 |
. . . . . . . . . . . 12
โข (-๐ โ โ โ
(โโ-๐) โ
โ) |
34 | 33 | recnd 11188 |
. . . . . . . . . . 11
โข (-๐ โ โ โ
(โโ-๐) โ
โ) |
35 | 14, 34 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (โโ-๐) โ
โ) |
36 | 35 | mul01d 11359 |
. . . . . . . . 9
โข (๐ โ ((โโ-๐) ยท 0) =
0) |
37 | 32, 36 | sylan9eqr 2795 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ
((โโ-๐)
ยท (โโ(logโ๐))) = 0) |
38 | 30, 37 | oveq12d 7376 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ
(((โโ-๐)
ยท (โโ(logโ๐))) โ ((โโ-๐) ยท
(โโ(logโ๐)))) = ((-(โโ๐) ยท (logโ๐)) โ 0)) |
39 | 13 | recld 15085 |
. . . . . . . . . . 11
โข (๐ โ (โโ๐) โ
โ) |
40 | 39 | renegcld 11587 |
. . . . . . . . . 10
โข (๐ โ -(โโ๐) โ
โ) |
41 | 40 | recnd 11188 |
. . . . . . . . 9
โข (๐ โ -(โโ๐) โ
โ) |
42 | | mulcl 11140 |
. . . . . . . . 9
โข
((-(โโ๐)
โ โ โง (logโ๐) โ โ) โ
(-(โโ๐) ยท
(logโ๐)) โ
โ) |
43 | 41, 21, 42 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (-(โโ๐) ยท (logโ๐)) โ
โ) |
44 | 43 | subid1d 11506 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ
((-(โโ๐)
ยท (logโ๐))
โ 0) = (-(โโ๐) ยท (logโ๐))) |
45 | 27, 38, 44 | 3eqtrd 2777 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (โโ(-๐ ยท (logโ๐))) = (-(โโ๐) ยท (logโ๐))) |
46 | 45 | fveq2d 6847 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ
(expโ(โโ(-๐ ยท (logโ๐)))) = (expโ(-(โโ๐) ยท (logโ๐)))) |
47 | 41 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ -(โโ๐) โ
โ) |
48 | 10, 12, 47 | cxpefd 26083 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐โ๐-(โโ๐)) =
(expโ(-(โโ๐) ยท (logโ๐)))) |
49 | 46, 48 | eqtr4d 2776 |
. . . 4
โข ((๐ โง ๐ โ โ) โ
(expโ(โโ(-๐ ยท (logโ๐)))) = (๐โ๐-(โโ๐))) |
50 | 18, 25, 49 | 3eqtrd 2777 |
. . 3
โข ((๐ โง ๐ โ โ) โ (absโ(๐นโ๐)) = (๐โ๐-(โโ๐))) |
51 | 7, 50 | eqtr4d 2776 |
. 2
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ๐) = (absโ(๐นโ๐))) |
52 | 10, 15 | cxpcld 26079 |
. . 3
โข ((๐ โง ๐ โ โ) โ (๐โ๐-๐) โ โ) |
53 | 8, 52 | eqeltrd 2834 |
. 2
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) โ โ) |
54 | | 2rp 12925 |
. . . . . . 7
โข 2 โ
โ+ |
55 | | 1re 11160 |
. . . . . . . 8
โข 1 โ
โ |
56 | | resubcl 11470 |
. . . . . . . 8
โข ((1
โ โ โง (โโ๐) โ โ) โ (1 โ
(โโ๐)) โ
โ) |
57 | 55, 39, 56 | sylancr 588 |
. . . . . . 7
โข (๐ โ (1 โ
(โโ๐)) โ
โ) |
58 | | rpcxpcl 26047 |
. . . . . . 7
โข ((2
โ โ+ โง (1 โ (โโ๐)) โ โ) โ
(2โ๐(1 โ (โโ๐))) โ
โ+) |
59 | 54, 57, 58 | sylancr 588 |
. . . . . 6
โข (๐ โ
(2โ๐(1 โ (โโ๐))) โ
โ+) |
60 | 59 | rpcnd 12964 |
. . . . 5
โข (๐ โ
(2โ๐(1 โ (โโ๐))) โ โ) |
61 | | zetacvg.2 |
. . . . . . . . 9
โข (๐ โ 1 < (โโ๐)) |
62 | | recl 15001 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(โโ๐) โ
โ) |
63 | 62 | recnd 11188 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(โโ๐) โ
โ) |
64 | 13, 63 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (โโ๐) โ
โ) |
65 | 64 | addid2d 11361 |
. . . . . . . . 9
โข (๐ โ (0 + (โโ๐)) = (โโ๐)) |
66 | 61, 65 | breqtrrd 5134 |
. . . . . . . 8
โข (๐ โ 1 < (0 +
(โโ๐))) |
67 | | 0re 11162 |
. . . . . . . . . 10
โข 0 โ
โ |
68 | | ltsubadd 11630 |
. . . . . . . . . 10
โข ((1
โ โ โง (โโ๐) โ โ โง 0 โ โ)
โ ((1 โ (โโ๐)) < 0 โ 1 < (0 +
(โโ๐)))) |
69 | 55, 67, 68 | mp3an13 1453 |
. . . . . . . . 9
โข
((โโ๐)
โ โ โ ((1 โ (โโ๐)) < 0 โ 1 < (0 +
(โโ๐)))) |
70 | 39, 69 | syl 17 |
. . . . . . . 8
โข (๐ โ ((1 โ
(โโ๐)) < 0
โ 1 < (0 + (โโ๐)))) |
71 | 66, 70 | mpbird 257 |
. . . . . . 7
โข (๐ โ (1 โ
(โโ๐)) <
0) |
72 | | 2re 12232 |
. . . . . . . . 9
โข 2 โ
โ |
73 | | 1lt2 12329 |
. . . . . . . . 9
โข 1 <
2 |
74 | | cxplt 26065 |
. . . . . . . . 9
โข (((2
โ โ โง 1 < 2) โง ((1 โ (โโ๐)) โ โ โง 0 โ
โ)) โ ((1 โ (โโ๐)) < 0 โ
(2โ๐(1 โ (โโ๐))) <
(2โ๐0))) |
75 | 72, 73, 74 | mpanl12 701 |
. . . . . . . 8
โข (((1
โ (โโ๐))
โ โ โง 0 โ โ) โ ((1 โ (โโ๐)) < 0 โ
(2โ๐(1 โ (โโ๐))) <
(2โ๐0))) |
76 | 57, 67, 75 | sylancl 587 |
. . . . . . 7
โข (๐ โ ((1 โ
(โโ๐)) < 0
โ (2โ๐(1 โ (โโ๐))) <
(2โ๐0))) |
77 | 71, 76 | mpbid 231 |
. . . . . 6
โข (๐ โ
(2โ๐(1 โ (โโ๐))) <
(2โ๐0)) |
78 | 59 | rprege0d 12969 |
. . . . . . 7
โข (๐ โ
((2โ๐(1 โ (โโ๐))) โ โ โง 0 โค
(2โ๐(1 โ (โโ๐))))) |
79 | | absid 15187 |
. . . . . . 7
โข
(((2โ๐(1 โ (โโ๐))) โ โ โง 0 โค
(2โ๐(1 โ (โโ๐)))) โ
(absโ(2โ๐(1 โ (โโ๐)))) =
(2โ๐(1 โ (โโ๐)))) |
80 | 78, 79 | syl 17 |
. . . . . 6
โข (๐ โ
(absโ(2โ๐(1 โ (โโ๐)))) =
(2โ๐(1 โ (โโ๐)))) |
81 | | 2cn 12233 |
. . . . . . . . 9
โข 2 โ
โ |
82 | | cxp0 26041 |
. . . . . . . . 9
โข (2 โ
โ โ (2โ๐0) = 1) |
83 | 81, 82 | ax-mp 5 |
. . . . . . . 8
โข
(2โ๐0) = 1 |
84 | 83 | eqcomi 2742 |
. . . . . . 7
โข 1 =
(2โ๐0) |
85 | 84 | a1i 11 |
. . . . . 6
โข (๐ โ 1 =
(2โ๐0)) |
86 | 77, 80, 85 | 3brtr4d 5138 |
. . . . 5
โข (๐ โ
(absโ(2โ๐(1 โ (โโ๐)))) < 1) |
87 | | oveq2 7366 |
. . . . . . 7
โข (๐ = ๐ โ ((2โ๐(1
โ (โโ๐)))โ๐) = ((2โ๐(1 โ
(โโ๐)))โ๐)) |
88 | | eqid 2733 |
. . . . . . 7
โข (๐ โ โ0
โฆ ((2โ๐(1 โ (โโ๐)))โ๐)) = (๐ โ โ0 โฆ
((2โ๐(1 โ (โโ๐)))โ๐)) |
89 | | ovex 7391 |
. . . . . . 7
โข
((2โ๐(1 โ (โโ๐)))โ๐) โ V |
90 | 87, 88, 89 | fvmpt 6949 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((2โ๐(1 โ
(โโ๐)))โ๐))โ๐) = ((2โ๐(1 โ
(โโ๐)))โ๐)) |
91 | 90 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((2โ๐(1 โ (โโ๐)))โ๐))โ๐) = ((2โ๐(1 โ
(โโ๐)))โ๐)) |
92 | 60, 86, 91 | geolim 15760 |
. . . 4
โข (๐ โ seq0( + , (๐ โ โ0
โฆ ((2โ๐(1 โ (โโ๐)))โ๐))) โ (1 / (1 โ
(2โ๐(1 โ (โโ๐)))))) |
93 | | seqex 13914 |
. . . . 5
โข seq0( + ,
(๐ โ
โ0 โฆ ((2โ๐(1 โ
(โโ๐)))โ๐))) โ V |
94 | | ovex 7391 |
. . . . 5
โข (1 / (1
โ (2โ๐(1 โ (โโ๐))))) โ V |
95 | 93, 94 | breldm 5865 |
. . . 4
โข (seq0( +
, (๐ โ
โ0 โฆ ((2โ๐(1 โ
(โโ๐)))โ๐))) โ (1 / (1 โ
(2โ๐(1 โ (โโ๐))))) โ seq0( + , (๐ โ โ0 โฆ
((2โ๐(1 โ (โโ๐)))โ๐))) โ dom โ ) |
96 | 92, 95 | syl 17 |
. . 3
โข (๐ โ seq0( + , (๐ โ โ0
โฆ ((2โ๐(1 โ (โโ๐)))โ๐))) โ dom โ ) |
97 | | rpcxpcl 26047 |
. . . . . . 7
โข ((๐ โ โ+
โง -(โโ๐)
โ โ) โ (๐โ๐-(โโ๐)) โ
โ+) |
98 | 19, 40, 97 | syl2anr 598 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (๐โ๐-(โโ๐)) โ
โ+) |
99 | 98 | rpred 12962 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐โ๐-(โโ๐)) โ
โ) |
100 | 7, 99 | eqeltrd 2834 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ๐) โ โ) |
101 | 98 | rpge0d 12966 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ 0 โค (๐โ๐-(โโ๐))) |
102 | 101, 7 | breqtrrd 5134 |
. . . 4
โข ((๐ โง ๐ โ โ) โ 0 โค ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ๐)) |
103 | | nnre 12165 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
104 | 103 | lep1d 12091 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โค (๐ + 1)) |
105 | 19 | reeflogd 25995 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(expโ(logโ๐)) =
๐) |
106 | | peano2nn 12170 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ + 1) โ
โ) |
107 | 106 | nnrpd 12960 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ + 1) โ
โ+) |
108 | 107 | reeflogd 25995 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(expโ(logโ(๐ +
1))) = (๐ +
1)) |
109 | 104, 105,
108 | 3brtr4d 5138 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(expโ(logโ๐))
โค (expโ(logโ(๐ + 1)))) |
110 | 107 | relogcld 25994 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(logโ(๐ + 1)) โ
โ) |
111 | | efle 16005 |
. . . . . . . . . . . 12
โข
(((logโ๐)
โ โ โง (logโ(๐ + 1)) โ โ) โ
((logโ๐) โค
(logโ(๐ + 1)) โ
(expโ(logโ๐))
โค (expโ(logโ(๐ + 1))))) |
112 | 20, 110, 111 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((logโ๐) โค
(logโ(๐ + 1)) โ
(expโ(logโ๐))
โค (expโ(logโ(๐ + 1))))) |
113 | 109, 112 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ โ โ
(logโ๐) โค
(logโ(๐ +
1))) |
114 | 113 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (logโ๐) โค (logโ(๐ + 1))) |
115 | 20 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (logโ๐) โ
โ) |
116 | 106 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ (๐ + 1) โ โ) |
117 | 116 | nnrpd 12960 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (๐ + 1) โ
โ+) |
118 | 117 | relogcld 25994 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (logโ(๐ + 1)) โ
โ) |
119 | 39 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (โโ๐) โ
โ) |
120 | 67 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 0 โ
โ) |
121 | 55 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 1 โ
โ) |
122 | | 0lt1 11682 |
. . . . . . . . . . . . 13
โข 0 <
1 |
123 | 122 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 0 < 1) |
124 | 120, 121,
39, 123, 61 | lttrd 11321 |
. . . . . . . . . . 11
โข (๐ โ 0 < (โโ๐)) |
125 | 124 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ 0 <
(โโ๐)) |
126 | | lemul2 12013 |
. . . . . . . . . 10
โข
(((logโ๐)
โ โ โง (logโ(๐ + 1)) โ โ โง
((โโ๐) โ
โ โง 0 < (โโ๐))) โ ((logโ๐) โค (logโ(๐ + 1)) โ ((โโ๐) ยท (logโ๐)) โค ((โโ๐) ยท (logโ(๐ + 1))))) |
127 | 115, 118,
119, 125, 126 | syl112anc 1375 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((logโ๐) โค (logโ(๐ + 1)) โ
((โโ๐) ยท
(logโ๐)) โค
((โโ๐) ยท
(logโ(๐ +
1))))) |
128 | 114, 127 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((โโ๐) ยท (logโ๐)) โค ((โโ๐) ยท (logโ(๐ + 1)))) |
129 | | remulcl 11141 |
. . . . . . . . . 10
โข
(((โโ๐)
โ โ โง (logโ๐) โ โ) โ ((โโ๐) ยท (logโ๐)) โ
โ) |
130 | 39, 20, 129 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((โโ๐) ยท (logโ๐)) โ
โ) |
131 | | remulcl 11141 |
. . . . . . . . . 10
โข
(((โโ๐)
โ โ โง (logโ(๐ + 1)) โ โ) โ
((โโ๐) ยท
(logโ(๐ + 1))) โ
โ) |
132 | 39, 110, 131 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((โโ๐) ยท (logโ(๐ + 1))) โ
โ) |
133 | 130, 132 | lenegd 11739 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (((โโ๐) ยท (logโ๐)) โค ((โโ๐) ยท (logโ(๐ + 1))) โ
-((โโ๐) ยท
(logโ(๐ + 1))) โค
-((โโ๐) ยท
(logโ๐)))) |
134 | 128, 133 | mpbid 231 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ -((โโ๐) ยท (logโ(๐ + 1))) โค
-((โโ๐) ยท
(logโ๐))) |
135 | 110 | recnd 11188 |
. . . . . . . 8
โข (๐ โ โ โ
(logโ(๐ + 1)) โ
โ) |
136 | | mulneg1 11596 |
. . . . . . . 8
โข
(((โโ๐)
โ โ โง (logโ(๐ + 1)) โ โ) โ
(-(โโ๐) ยท
(logโ(๐ + 1))) =
-((โโ๐) ยท
(logโ(๐ +
1)))) |
137 | 64, 135, 136 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (-(โโ๐) ยท (logโ(๐ + 1))) = -((โโ๐) ยท (logโ(๐ + 1)))) |
138 | | mulneg1 11596 |
. . . . . . . 8
โข
(((โโ๐)
โ โ โง (logโ๐) โ โ) โ
(-(โโ๐) ยท
(logโ๐)) =
-((โโ๐) ยท
(logโ๐))) |
139 | 64, 21, 138 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (-(โโ๐) ยท (logโ๐)) = -((โโ๐) ยท (logโ๐))) |
140 | 134, 137,
139 | 3brtr4d 5138 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (-(โโ๐) ยท (logโ(๐ + 1))) โค
(-(โโ๐) ยท
(logโ๐))) |
141 | | remulcl 11141 |
. . . . . . . 8
โข
((-(โโ๐)
โ โ โง (logโ(๐ + 1)) โ โ) โ
(-(โโ๐) ยท
(logโ(๐ + 1))) โ
โ) |
142 | 40, 110, 141 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (-(โโ๐) ยท (logโ(๐ + 1))) โ
โ) |
143 | | remulcl 11141 |
. . . . . . . 8
โข
((-(โโ๐)
โ โ โง (logโ๐) โ โ) โ
(-(โโ๐) ยท
(logโ๐)) โ
โ) |
144 | 40, 20, 143 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (-(โโ๐) ยท (logโ๐)) โ
โ) |
145 | | efle 16005 |
. . . . . . 7
โข
(((-(โโ๐)
ยท (logโ(๐ +
1))) โ โ โง (-(โโ๐) ยท (logโ๐)) โ โ) โ
((-(โโ๐)
ยท (logโ(๐ +
1))) โค (-(โโ๐) ยท (logโ๐)) โ (expโ(-(โโ๐) ยท (logโ(๐ + 1)))) โค
(expโ(-(โโ๐) ยท (logโ๐))))) |
146 | 142, 144,
145 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ
((-(โโ๐)
ยท (logโ(๐ +
1))) โค (-(โโ๐) ยท (logโ๐)) โ (expโ(-(โโ๐) ยท (logโ(๐ + 1)))) โค
(expโ(-(โโ๐) ยท (logโ๐))))) |
147 | 140, 146 | mpbid 231 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ
(expโ(-(โโ๐) ยท (logโ(๐ + 1)))) โค
(expโ(-(โโ๐) ยท (logโ๐)))) |
148 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (๐โ๐-(โโ๐)) = ((๐ +
1)โ๐-(โโ๐))) |
149 | | ovex 7391 |
. . . . . . . 8
โข ((๐ +
1)โ๐-(โโ๐)) โ V |
150 | 148, 4, 149 | fvmpt 6949 |
. . . . . . 7
โข ((๐ + 1) โ โ โ
((๐ โ โ โฆ
(๐โ๐-(โโ๐)))โ(๐ + 1)) = ((๐ +
1)โ๐-(โโ๐))) |
151 | 116, 150 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ(๐ + 1)) = ((๐ +
1)โ๐-(โโ๐))) |
152 | 116 | nncnd 12174 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (๐ + 1) โ โ) |
153 | 116 | nnne0d 12208 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (๐ + 1) โ 0) |
154 | 152, 153,
47 | cxpefd 26083 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ +
1)โ๐-(โโ๐)) = (expโ(-(โโ๐) ยท (logโ(๐ + 1))))) |
155 | 151, 154 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ(๐ + 1)) = (expโ(-(โโ๐) ยท (logโ(๐ + 1))))) |
156 | 7, 48 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ๐) = (expโ(-(โโ๐) ยท (logโ๐)))) |
157 | 147, 155,
156 | 3brtr4d 5138 |
. . . 4
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ(๐ + 1)) โค ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ๐)) |
158 | 57 | recnd 11188 |
. . . . . . . . . . 11
โข (๐ โ (1 โ
(โโ๐)) โ
โ) |
159 | 158 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ (1
โ (โโ๐))
โ โ) |
160 | | nn0re 12427 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โ) |
161 | 160 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ) |
162 | 161 | recnd 11188 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ) |
163 | 159, 162 | mulcomd 11181 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ ((1
โ (โโ๐))
ยท ๐) = (๐ ยท (1 โ
(โโ๐)))) |
164 | 163 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(2โ๐((1 โ (โโ๐)) ยท ๐)) = (2โ๐(๐ ยท (1 โ
(โโ๐))))) |
165 | 54 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ 2 โ
โ+) |
166 | 165, 161,
159 | cxpmuld 26107 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(2โ๐(๐ ยท (1 โ (โโ๐)))) =
((2โ๐๐)โ๐(1 โ
(โโ๐)))) |
167 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ0) |
168 | | cxpexp 26039 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐๐) = (2โ๐)) |
169 | 81, 167, 168 | sylancr 588 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
(2โ๐๐) = (2โ๐)) |
170 | | ax-1cn 11114 |
. . . . . . . . . . 11
โข 1 โ
โ |
171 | 64 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ0) โ
(โโ๐) โ
โ) |
172 | | negsub 11454 |
. . . . . . . . . . 11
โข ((1
โ โ โง (โโ๐) โ โ) โ (1 +
-(โโ๐)) = (1
โ (โโ๐))) |
173 | 170, 171,
172 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ (1 +
-(โโ๐)) = (1
โ (โโ๐))) |
174 | 173 | eqcomd 2739 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (1
โ (โโ๐)) =
(1 + -(โโ๐))) |
175 | 169, 174 | oveq12d 7376 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
((2โ๐๐)โ๐(1 โ
(โโ๐))) =
((2โ๐)โ๐(1 +
-(โโ๐)))) |
176 | 164, 166,
175 | 3eqtrd 2777 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
(2โ๐((1 โ (โโ๐)) ยท ๐)) = ((2โ๐)โ๐(1 +
-(โโ๐)))) |
177 | 57 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (1
โ (โโ๐))
โ โ) |
178 | 165, 177,
162 | cxpmuld 26107 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
(2โ๐((1 โ (โโ๐)) ยท ๐)) = ((2โ๐(1 โ
(โโ๐)))โ๐๐)) |
179 | | 2nn 12231 |
. . . . . . . . . . 11
โข 2 โ
โ |
180 | | nnexpcl 13986 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
181 | 179, 180 | mpan 689 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (2โ๐) โ
โ) |
182 | 181 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
(2โ๐) โ
โ) |
183 | 182 | nncnd 12174 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(2โ๐) โ
โ) |
184 | 182 | nnne0d 12208 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(2โ๐) โ
0) |
185 | | 1cnd 11155 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ 1 โ
โ) |
186 | 41 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
-(โโ๐) โ
โ) |
187 | 183, 184,
185, 186 | cxpaddd 26088 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
((2โ๐)โ๐(1 +
-(โโ๐))) =
(((2โ๐)โ๐1) ยท
((2โ๐)โ๐-(โโ๐)))) |
188 | 176, 178,
187 | 3eqtr3d 2781 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
((2โ๐(1 โ (โโ๐)))โ๐๐) = (((2โ๐)โ๐1) ยท
((2โ๐)โ๐-(โโ๐)))) |
189 | | cxpexp 26039 |
. . . . . . 7
โข
(((2โ๐(1 โ (โโ๐))) โ โ โง ๐ โ โ0) โ
((2โ๐(1 โ (โโ๐)))โ๐๐) =
((2โ๐(1 โ (โโ๐)))โ๐)) |
190 | 60, 189 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
((2โ๐(1 โ (โโ๐)))โ๐๐) =
((2โ๐(1 โ (โโ๐)))โ๐)) |
191 | 183 | cxp1d 26077 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
((2โ๐)โ๐1) = (2โ๐)) |
192 | 191 | oveq1d 7373 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(((2โ๐)โ๐1) ยท
((2โ๐)โ๐-(โโ๐))) = ((2โ๐) ยท ((2โ๐)โ๐-(โโ๐)))) |
193 | 188, 190,
192 | 3eqtr3d 2781 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
((2โ๐(1 โ (โโ๐)))โ๐) = ((2โ๐) ยท ((2โ๐)โ๐-(โโ๐)))) |
194 | 179, 167,
180 | sylancr 588 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
(2โ๐) โ
โ) |
195 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = (2โ๐) โ (๐โ๐-(โโ๐)) = ((2โ๐)โ๐-(โโ๐))) |
196 | | ovex 7391 |
. . . . . . . 8
โข
((2โ๐)โ๐-(โโ๐)) โ V |
197 | 195, 4, 196 | fvmpt 6949 |
. . . . . . 7
โข
((2โ๐) โ
โ โ ((๐ โ
โ โฆ (๐โ๐-(โโ๐)))โ(2โ๐)) = ((2โ๐)โ๐-(โโ๐))) |
198 | 194, 197 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ(2โ๐)) = ((2โ๐)โ๐-(โโ๐))) |
199 | 198 | oveq2d 7374 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
((2โ๐) ยท
((๐ โ โ โฆ
(๐โ๐-(โโ๐)))โ(2โ๐))) = ((2โ๐) ยท ((2โ๐)โ๐-(โโ๐)))) |
200 | 193, 91, 199 | 3eqtr4d 2783 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((2โ๐(1 โ (โโ๐)))โ๐))โ๐) = ((2โ๐) ยท ((๐ โ โ โฆ (๐โ๐-(โโ๐)))โ(2โ๐)))) |
201 | 100, 102,
157, 200 | climcnds 15741 |
. . 3
โข (๐ โ (seq1( + , (๐ โ โ โฆ (๐โ๐-(โโ๐)))) โ dom โ โ
seq0( + , (๐ โ
โ0 โฆ ((2โ๐(1 โ
(โโ๐)))โ๐))) โ dom โ )) |
202 | 96, 201 | mpbird 257 |
. 2
โข (๐ โ seq1( + , (๐ โ โ โฆ (๐โ๐-(โโ๐)))) โ dom โ
) |
203 | 1, 2, 51, 53, 202 | abscvgcvg 15709 |
1
โข (๐ โ seq1( + , ๐น) โ dom โ
) |