Step | Hyp | Ref
| Expression |
1 | | nnuz 12811 |
. . . . 5
β’ β =
(β€β₯β1) |
2 | | 1zzd 12539 |
. . . . 5
β’ (π β 1 β
β€) |
3 | | stirlinglem5.1 |
. . . . . . . . 9
β’ π· = (π β β β¦ ((-1β(π β 1)) Β· ((πβπ) / π))) |
4 | 3 | a1i 11 |
. . . . . . . 8
β’ (π β π· = (π β β β¦ ((-1β(π β 1)) Β· ((πβπ) / π)))) |
5 | | 1cnd 11155 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β 1 β
β) |
6 | 5 | negcld 11504 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β -1 β
β) |
7 | | nnm1nn0 12459 |
. . . . . . . . . . . . 13
β’ (π β β β (π β 1) β
β0) |
8 | 7 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π β 1) β
β0) |
9 | 6, 8 | expcld 14057 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (-1β(π β 1)) β
β) |
10 | | nncn 12166 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
11 | 10 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β) |
12 | | stirlinglem5.6 |
. . . . . . . . . . . . . . 15
β’ (π β π β
β+) |
13 | 12 | rpred 12962 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
14 | 13 | recnd 11188 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
15 | 14 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
16 | | nnnn0 12425 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β0) |
17 | 16 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β0) |
18 | 15, 17 | expcld 14057 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβπ) β β) |
19 | | nnne0 12192 |
. . . . . . . . . . . 12
β’ (π β β β π β 0) |
20 | 19 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β 0) |
21 | 9, 11, 18, 20 | div32d 11959 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (((-1β(π β 1)) / π) Β· (πβπ)) = ((-1β(π β 1)) Β· ((πβπ) / π))) |
22 | 5, 15 | pncan2d 11519 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((1 + π) β 1) = π) |
23 | 22 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π = ((1 + π) β 1)) |
24 | 23 | oveq1d 7373 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβπ) = (((1 + π) β 1)βπ)) |
25 | 24 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (((-1β(π β 1)) / π) Β· (πβπ)) = (((-1β(π β 1)) / π) Β· (((1 + π) β 1)βπ))) |
26 | 21, 25 | eqtr3d 2775 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((-1β(π β 1)) Β· ((πβπ) / π)) = (((-1β(π β 1)) / π) Β· (((1 + π) β 1)βπ))) |
27 | 26 | mpteq2dva 5206 |
. . . . . . . 8
β’ (π β (π β β β¦ ((-1β(π β 1)) Β· ((πβπ) / π))) = (π β β β¦ (((-1β(π β 1)) / π) Β· (((1 + π) β 1)βπ)))) |
28 | 4, 27 | eqtrd 2773 |
. . . . . . 7
β’ (π β π· = (π β β β¦ (((-1β(π β 1)) / π) Β· (((1 + π) β 1)βπ)))) |
29 | 28 | seqeq3d 13920 |
. . . . . 6
β’ (π β seq1( + , π·) = seq1( + , (π β β β¦
(((-1β(π β 1)) /
π) Β· (((1 + π) β 1)βπ))))) |
30 | | 1cnd 11155 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
31 | 30, 14 | addcld 11179 |
. . . . . . . . . 10
β’ (π β (1 + π) β β) |
32 | | eqid 2733 |
. . . . . . . . . . 11
β’ (abs
β β ) = (abs β β ) |
33 | 32 | cnmetdval 24150 |
. . . . . . . . . 10
β’ ((1
β β β§ (1 + π) β β) β (1(abs β
β )(1 + π)) =
(absβ(1 β (1 + π)))) |
34 | 30, 31, 33 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (1(abs β β )(1
+ π)) = (absβ(1
β (1 + π)))) |
35 | | 1m1e0 12230 |
. . . . . . . . . . . . . 14
β’ (1
β 1) = 0 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (1 β 1) =
0) |
37 | 36 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π β ((1 β 1) β
π) = (0 β π)) |
38 | 30, 30, 14 | subsub4d 11548 |
. . . . . . . . . . . 12
β’ (π β ((1 β 1) β
π) = (1 β (1 + π))) |
39 | | df-neg 11393 |
. . . . . . . . . . . . . 14
β’ -π = (0 β π) |
40 | 39 | eqcomi 2742 |
. . . . . . . . . . . . 13
β’ (0
β π) = -π |
41 | 40 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (0 β π) = -π) |
42 | 37, 38, 41 | 3eqtr3d 2781 |
. . . . . . . . . . 11
β’ (π β (1 β (1 + π)) = -π) |
43 | 42 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π β (absβ(1 β (1 +
π))) = (absβ-π)) |
44 | 14 | absnegd 15340 |
. . . . . . . . . . 11
β’ (π β (absβ-π) = (absβπ)) |
45 | | stirlinglem5.7 |
. . . . . . . . . . 11
β’ (π β (absβπ) < 1) |
46 | 44, 45 | eqbrtrd 5128 |
. . . . . . . . . 10
β’ (π β (absβ-π) < 1) |
47 | 43, 46 | eqbrtrd 5128 |
. . . . . . . . 9
β’ (π β (absβ(1 β (1 +
π))) <
1) |
48 | 34, 47 | eqbrtrd 5128 |
. . . . . . . 8
β’ (π β (1(abs β β )(1
+ π)) <
1) |
49 | | cnxmet 24152 |
. . . . . . . . . 10
β’ (abs
β β ) β (βMetββ) |
50 | 49 | a1i 11 |
. . . . . . . . 9
β’ (π β (abs β β )
β (βMetββ)) |
51 | | 1red 11161 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
52 | 51 | rexrd 11210 |
. . . . . . . . 9
β’ (π β 1 β
β*) |
53 | | elbl2 23759 |
. . . . . . . . 9
β’ ((((abs
β β ) β (βMetββ) β§ 1 β
β*) β§ (1 β β β§ (1 + π) β β)) β ((1 + π) β (1(ballβ(abs
β β ))1) β (1(abs β β )(1 + π)) < 1)) |
54 | 50, 52, 30, 31, 53 | syl22anc 838 |
. . . . . . . 8
β’ (π β ((1 + π) β (1(ballβ(abs β β
))1) β (1(abs β β )(1 + π)) < 1)) |
55 | 48, 54 | mpbird 257 |
. . . . . . 7
β’ (π β (1 + π) β (1(ballβ(abs β β
))1)) |
56 | | eqid 2733 |
. . . . . . . 8
β’
(1(ballβ(abs β β ))1) = (1(ballβ(abs β
β ))1) |
57 | 56 | logtayl2 26033 |
. . . . . . 7
β’ ((1 +
π) β
(1(ballβ(abs β β ))1) β seq1( + , (π β β β¦ (((-1β(π β 1)) / π) Β· (((1 + π) β 1)βπ)))) β (logβ(1 +
π))) |
58 | 55, 57 | syl 17 |
. . . . . 6
β’ (π β seq1( + , (π β β β¦
(((-1β(π β 1)) /
π) Β· (((1 + π) β 1)βπ)))) β (logβ(1 +
π))) |
59 | 29, 58 | eqbrtrd 5128 |
. . . . 5
β’ (π β seq1( + , π·) β (logβ(1 + π))) |
60 | | seqex 13914 |
. . . . . 6
β’ seq1( + ,
πΉ) β
V |
61 | 60 | a1i 11 |
. . . . 5
β’ (π β seq1( + , πΉ) β V) |
62 | | stirlinglem5.2 |
. . . . . . . 8
β’ πΈ = (π β β β¦ ((πβπ) / π)) |
63 | 62 | a1i 11 |
. . . . . . 7
β’ (π β πΈ = (π β β β¦ ((πβπ) / π))) |
64 | 63 | seqeq3d 13920 |
. . . . . 6
β’ (π β seq1( + , πΈ) = seq1( + , (π β β β¦ ((πβπ) / π)))) |
65 | | logtayl 26031 |
. . . . . . 7
β’ ((π β β β§
(absβπ) < 1)
β seq1( + , (π β
β β¦ ((πβπ) / π))) β -(logβ(1 β π))) |
66 | 14, 45, 65 | syl2anc 585 |
. . . . . 6
β’ (π β seq1( + , (π β β β¦ ((πβπ) / π))) β -(logβ(1 β π))) |
67 | 64, 66 | eqbrtrd 5128 |
. . . . 5
β’ (π β seq1( + , πΈ) β -(logβ(1 β
π))) |
68 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β β) β π β β) |
69 | 68, 1 | eleqtrdi 2844 |
. . . . . 6
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
70 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = π β (π β 1) = (π β 1)) |
71 | 70 | oveq2d 7374 |
. . . . . . . . 9
β’ (π = π β (-1β(π β 1)) = (-1β(π β 1))) |
72 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
73 | | id 22 |
. . . . . . . . . 10
β’ (π = π β π = π) |
74 | 72, 73 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = π β ((πβπ) / π) = ((πβπ) / π)) |
75 | 71, 74 | oveq12d 7376 |
. . . . . . . 8
β’ (π = π β ((-1β(π β 1)) Β· ((πβπ) / π)) = ((-1β(π β 1)) Β· ((πβπ) / π))) |
76 | | elfznn 13476 |
. . . . . . . . 9
β’ (π β (1...π) β π β β) |
77 | 76 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
78 | | 1cnd 11155 |
. . . . . . . . . . . 12
β’ (π β β β 1 β
β) |
79 | 78 | negcld 11504 |
. . . . . . . . . . 11
β’ (π β β β -1 β
β) |
80 | | nnm1nn0 12459 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
β0) |
81 | 79, 80 | expcld 14057 |
. . . . . . . . . 10
β’ (π β β β
(-1β(π β 1))
β β) |
82 | 77, 81 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β (-1β(π β 1)) β β) |
83 | 14 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
84 | 77 | nnnn0d 12478 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β π β β0) |
85 | 83, 84 | expcld 14057 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β (πβπ) β β) |
86 | 77 | nncnd 12174 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
87 | 77 | nnne0d 12208 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β π β 0) |
88 | 85, 86, 87 | divcld 11936 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β ((πβπ) / π) β β) |
89 | 82, 88 | mulcld 11180 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β ((-1β(π β 1)) Β· ((πβπ) / π)) β β) |
90 | 3, 75, 77, 89 | fvmptd3 6972 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...π)) β (π·βπ) = ((-1β(π β 1)) Β· ((πβπ) / π))) |
91 | 90, 89 | eqeltrd 2834 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...π)) β (π·βπ) β β) |
92 | | addcl 11138 |
. . . . . . 7
β’ ((π β β β§ π β β) β (π + π) β β) |
93 | 92 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ (π β β β§ π β β)) β (π + π) β β) |
94 | 69, 91, 93 | seqcl 13934 |
. . . . 5
β’ ((π β§ π β β) β (seq1( + , π·)βπ) β β) |
95 | 62, 74, 77, 88 | fvmptd3 6972 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...π)) β (πΈβπ) = ((πβπ) / π)) |
96 | 95, 88 | eqeltrd 2834 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...π)) β (πΈβπ) β β) |
97 | 69, 96, 93 | seqcl 13934 |
. . . . 5
β’ ((π β§ π β β) β (seq1( + , πΈ)βπ) β β) |
98 | | simpll 766 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...π)) β π) |
99 | | stirlinglem5.3 |
. . . . . . . . 9
β’ πΉ = (π β β β¦ (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π))) |
100 | 75, 74 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = π β (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π)) = (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π))) |
101 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
102 | 81 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (-1β(π β 1)) β
β) |
103 | 14 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β) |
104 | 101 | nnnn0d 12478 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β0) |
105 | 103, 104 | expcld 14057 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβπ) β β) |
106 | 101 | nncnd 12174 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
107 | 101 | nnne0d 12208 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β 0) |
108 | 105, 106,
107 | divcld 11936 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((πβπ) / π) β β) |
109 | 102, 108 | mulcld 11180 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((-1β(π β 1)) Β· ((πβπ) / π)) β β) |
110 | 109, 108 | addcld 11179 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π)) β β) |
111 | 99, 100, 101, 110 | fvmptd3 6972 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΉβπ) = (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π))) |
112 | 3, 75, 101, 109 | fvmptd3 6972 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π·βπ) = ((-1β(π β 1)) Β· ((πβπ) / π))) |
113 | 112 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((-1β(π β 1)) Β· ((πβπ) / π)) = (π·βπ)) |
114 | 62, 74, 101, 108 | fvmptd3 6972 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΈβπ) = ((πβπ) / π)) |
115 | 114 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβπ) / π) = (πΈβπ)) |
116 | 113, 115 | oveq12d 7376 |
. . . . . . . 8
β’ ((π β§ π β β) β (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π)) = ((π·βπ) + (πΈβπ))) |
117 | 111, 116 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π β β) β (πΉβπ) = ((π·βπ) + (πΈβπ))) |
118 | 98, 77, 117 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...π)) β (πΉβπ) = ((π·βπ) + (πΈβπ))) |
119 | 69, 91, 96, 118 | seradd 13956 |
. . . . 5
β’ ((π β§ π β β) β (seq1( + , πΉ)βπ) = ((seq1( + , π·)βπ) + (seq1( + , πΈ)βπ))) |
120 | 1, 2, 59, 61, 67, 94, 97, 119 | climadd 15520 |
. . . 4
β’ (π β seq1( + , πΉ) β ((logβ(1 + π)) + -(logβ(1 β
π)))) |
121 | | 1rp 12924 |
. . . . . . . . 9
β’ 1 β
β+ |
122 | 121 | a1i 11 |
. . . . . . . 8
β’ (π β 1 β
β+) |
123 | 122, 12 | rpaddcld 12977 |
. . . . . . 7
β’ (π β (1 + π) β
β+) |
124 | 123 | rpne0d 12967 |
. . . . . 6
β’ (π β (1 + π) β 0) |
125 | 31, 124 | logcld 25942 |
. . . . 5
β’ (π β (logβ(1 + π)) β
β) |
126 | 30, 14 | subcld 11517 |
. . . . . 6
β’ (π β (1 β π) β
β) |
127 | 13, 51 | absltd 15320 |
. . . . . . . . . 10
β’ (π β ((absβπ) < 1 β (-1 < π β§ π < 1))) |
128 | 45, 127 | mpbid 231 |
. . . . . . . . 9
β’ (π β (-1 < π β§ π < 1)) |
129 | 128 | simprd 497 |
. . . . . . . 8
β’ (π β π < 1) |
130 | 13, 129 | gtned 11295 |
. . . . . . 7
β’ (π β 1 β π) |
131 | 30, 14, 130 | subne0d 11526 |
. . . . . 6
β’ (π β (1 β π) β 0) |
132 | 126, 131 | logcld 25942 |
. . . . 5
β’ (π β (logβ(1 β
π)) β
β) |
133 | 125, 132 | negsubd 11523 |
. . . 4
β’ (π β ((logβ(1 + π)) + -(logβ(1 β
π))) = ((logβ(1 +
π)) β (logβ(1
β π)))) |
134 | 120, 133 | breqtrd 5132 |
. . 3
β’ (π β seq1( + , πΉ) β ((logβ(1 + π)) β (logβ(1 β
π)))) |
135 | | nn0uz 12810 |
. . . 4
β’
β0 = (β€β₯β0) |
136 | | 0zd 12516 |
. . . 4
β’ (π β 0 β
β€) |
137 | | stirlinglem5.5 |
. . . . . 6
β’ πΊ = (π β β0 β¦ ((2
Β· π) +
1)) |
138 | | 2nn0 12435 |
. . . . . . . . 9
β’ 2 β
β0 |
139 | 138 | a1i 11 |
. . . . . . . 8
β’ (π β β0
β 2 β β0) |
140 | | id 22 |
. . . . . . . 8
β’ (π β β0
β π β
β0) |
141 | 139, 140 | nn0mulcld 12483 |
. . . . . . 7
β’ (π β β0
β (2 Β· π)
β β0) |
142 | | nn0p1nn 12457 |
. . . . . . 7
β’ ((2
Β· π) β
β0 β ((2 Β· π) + 1) β β) |
143 | 141, 142 | syl 17 |
. . . . . 6
β’ (π β β0
β ((2 Β· π) + 1)
β β) |
144 | 137, 143 | fmpti 7061 |
. . . . 5
β’ πΊ:β0βΆβ |
145 | 144 | a1i 11 |
. . . 4
β’ (π β πΊ:β0βΆβ) |
146 | | 2re 12232 |
. . . . . . . . 9
β’ 2 β
β |
147 | 146 | a1i 11 |
. . . . . . . 8
β’ (π β β0
β 2 β β) |
148 | | nn0re 12427 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
149 | 147, 148 | remulcld 11190 |
. . . . . . 7
β’ (π β β0
β (2 Β· π)
β β) |
150 | | 1red 11161 |
. . . . . . . . 9
β’ (π β β0
β 1 β β) |
151 | 148, 150 | readdcld 11189 |
. . . . . . . 8
β’ (π β β0
β (π + 1) β
β) |
152 | 147, 151 | remulcld 11190 |
. . . . . . 7
β’ (π β β0
β (2 Β· (π + 1))
β β) |
153 | | 2rp 12925 |
. . . . . . . . 9
β’ 2 β
β+ |
154 | 153 | a1i 11 |
. . . . . . . 8
β’ (π β β0
β 2 β β+) |
155 | 148 | ltp1d 12090 |
. . . . . . . 8
β’ (π β β0
β π < (π + 1)) |
156 | 148, 151,
154, 155 | ltmul2dd 13018 |
. . . . . . 7
β’ (π β β0
β (2 Β· π) <
(2 Β· (π +
1))) |
157 | 149, 152,
150, 156 | ltadd1dd 11771 |
. . . . . 6
β’ (π β β0
β ((2 Β· π) + 1)
< ((2 Β· (π + 1))
+ 1)) |
158 | 137 | a1i 11 |
. . . . . . 7
β’ (π β β0
β πΊ = (π β β0
β¦ ((2 Β· π) +
1))) |
159 | | simpr 486 |
. . . . . . . . 9
β’ ((π β β0
β§ π = π) β π = π) |
160 | 159 | oveq2d 7374 |
. . . . . . . 8
β’ ((π β β0
β§ π = π) β (2 Β· π) = (2 Β· π)) |
161 | 160 | oveq1d 7373 |
. . . . . . 7
β’ ((π β β0
β§ π = π) β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
162 | | id 22 |
. . . . . . 7
β’ (π β β0
β π β
β0) |
163 | | 2cnd 12236 |
. . . . . . . . 9
β’ (π β β0
β 2 β β) |
164 | | nn0cn 12428 |
. . . . . . . . 9
β’ (π β β0
β π β
β) |
165 | 163, 164 | mulcld 11180 |
. . . . . . . 8
β’ (π β β0
β (2 Β· π)
β β) |
166 | | 1cnd 11155 |
. . . . . . . 8
β’ (π β β0
β 1 β β) |
167 | 165, 166 | addcld 11179 |
. . . . . . 7
β’ (π β β0
β ((2 Β· π) + 1)
β β) |
168 | 158, 161,
162, 167 | fvmptd 6956 |
. . . . . 6
β’ (π β β0
β (πΊβπ) = ((2 Β· π) + 1)) |
169 | | simpr 486 |
. . . . . . . . 9
β’ ((π β β0
β§ π = (π + 1)) β π = (π + 1)) |
170 | 169 | oveq2d 7374 |
. . . . . . . 8
β’ ((π β β0
β§ π = (π + 1)) β (2 Β· π) = (2 Β· (π + 1))) |
171 | 170 | oveq1d 7373 |
. . . . . . 7
β’ ((π β β0
β§ π = (π + 1)) β ((2 Β· π) + 1) = ((2 Β· (π + 1)) + 1)) |
172 | | peano2nn0 12458 |
. . . . . . 7
β’ (π β β0
β (π + 1) β
β0) |
173 | 164, 166 | addcld 11179 |
. . . . . . . . 9
β’ (π β β0
β (π + 1) β
β) |
174 | 163, 173 | mulcld 11180 |
. . . . . . . 8
β’ (π β β0
β (2 Β· (π + 1))
β β) |
175 | 174, 166 | addcld 11179 |
. . . . . . 7
β’ (π β β0
β ((2 Β· (π +
1)) + 1) β β) |
176 | 158, 171,
172, 175 | fvmptd 6956 |
. . . . . 6
β’ (π β β0
β (πΊβ(π + 1)) = ((2 Β· (π + 1)) + 1)) |
177 | 157, 168,
176 | 3brtr4d 5138 |
. . . . 5
β’ (π β β0
β (πΊβπ) < (πΊβ(π + 1))) |
178 | 177 | adantl 483 |
. . . 4
β’ ((π β§ π β β0) β (πΊβπ) < (πΊβ(π + 1))) |
179 | | eldifi 4087 |
. . . . . . 7
β’ (π β (β β ran
πΊ) β π β
β) |
180 | 179 | adantl 483 |
. . . . . 6
β’ ((π β§ π β (β β ran πΊ)) β π β β) |
181 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ (π β (β β ran
πΊ) β 1 β
β) |
182 | 181 | negcld 11504 |
. . . . . . . . . 10
β’ (π β (β β ran
πΊ) β -1 β
β) |
183 | 179, 80 | syl 17 |
. . . . . . . . . 10
β’ (π β (β β ran
πΊ) β (π β 1) β
β0) |
184 | 182, 183 | expcld 14057 |
. . . . . . . . 9
β’ (π β (β β ran
πΊ) β (-1β(π β 1)) β
β) |
185 | 184 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (β β ran πΊ)) β (-1β(π β 1)) β
β) |
186 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (β β ran πΊ)) β π β β) |
187 | 180 | nnnn0d 12478 |
. . . . . . . . . 10
β’ ((π β§ π β (β β ran πΊ)) β π β β0) |
188 | 186, 187 | expcld 14057 |
. . . . . . . . 9
β’ ((π β§ π β (β β ran πΊ)) β (πβπ) β β) |
189 | 180 | nncnd 12174 |
. . . . . . . . 9
β’ ((π β§ π β (β β ran πΊ)) β π β β) |
190 | 180 | nnne0d 12208 |
. . . . . . . . 9
β’ ((π β§ π β (β β ran πΊ)) β π β 0) |
191 | 188, 189,
190 | divcld 11936 |
. . . . . . . 8
β’ ((π β§ π β (β β ran πΊ)) β ((πβπ) / π) β β) |
192 | 185, 191 | mulcld 11180 |
. . . . . . 7
β’ ((π β§ π β (β β ran πΊ)) β ((-1β(π β 1)) Β· ((πβπ) / π)) β β) |
193 | 192, 191 | addcld 11179 |
. . . . . 6
β’ ((π β§ π β (β β ran πΊ)) β (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π)) β β) |
194 | 99, 100, 180, 193 | fvmptd3 6972 |
. . . . 5
β’ ((π β§ π β (β β ran πΊ)) β (πΉβπ) = (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π))) |
195 | | eldifn 4088 |
. . . . . . . . . . . 12
β’ (π β (β β ran
πΊ) β Β¬ π β ran πΊ) |
196 | | 0nn0 12433 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β0 |
197 | | 1nn0 12434 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β0 |
198 | 138, 197 | num0h 12635 |
. . . . . . . . . . . . . . . 16
β’ 1 = ((2
Β· 0) + 1) |
199 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (2 Β· π) = (2 Β·
0)) |
200 | 199 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β ((2 Β· π) + 1) = ((2 Β· 0) +
1)) |
201 | 200 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (1 = ((2 Β·
π) + 1) β 1 = ((2
Β· 0) + 1))) |
202 | 201 | rspcev 3580 |
. . . . . . . . . . . . . . . 16
β’ ((0
β β0 β§ 1 = ((2 Β· 0) + 1)) β βπ β β0 1 =
((2 Β· π) +
1)) |
203 | 196, 198,
202 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’
βπ β
β0 1 = ((2 Β· π) + 1) |
204 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
205 | 137 | elrnmpt 5912 |
. . . . . . . . . . . . . . . 16
β’ (1 β
β β (1 β ran πΊ β βπ β β0 1 = ((2 Β·
π) + 1))) |
206 | 204, 205 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (1 β
ran πΊ β βπ β β0 1 =
((2 Β· π) +
1)) |
207 | 203, 206 | mpbir 230 |
. . . . . . . . . . . . . 14
β’ 1 β
ran πΊ |
208 | 207 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π = 1 β 1 β ran πΊ) |
209 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π β ran πΊ β 1 β ran πΊ)) |
210 | 208, 209 | mpbird 257 |
. . . . . . . . . . . 12
β’ (π = 1 β π β ran πΊ) |
211 | 195, 210 | nsyl 140 |
. . . . . . . . . . 11
β’ (π β (β β ran
πΊ) β Β¬ π = 1) |
212 | | nn1m1nn 12179 |
. . . . . . . . . . . . 13
β’ (π β β β (π = 1 β¨ (π β 1) β β)) |
213 | 179, 212 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (β β ran
πΊ) β (π = 1 β¨ (π β 1) β β)) |
214 | 213 | ord 863 |
. . . . . . . . . . 11
β’ (π β (β β ran
πΊ) β (Β¬ π = 1 β (π β 1) β β)) |
215 | 211, 214 | mpd 15 |
. . . . . . . . . 10
β’ (π β (β β ran
πΊ) β (π β 1) β
β) |
216 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . 18
β’
β²πβ |
217 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(π β β0 β¦ ((2
Β· π) +
1)) |
218 | 137, 217 | nfcxfr 2902 |
. . . . . . . . . . . . . . . . . . 19
β’
β²ππΊ |
219 | 218 | nfrn 5908 |
. . . . . . . . . . . . . . . . . 18
β’
β²πran
πΊ |
220 | 216, 219 | nfdif 4086 |
. . . . . . . . . . . . . . . . 17
β’
β²π(β β ran πΊ) |
221 | 220 | nfcri 2891 |
. . . . . . . . . . . . . . . 16
β’
β²π π β (β β ran
πΊ) |
222 | 137 | elrnmpt 5912 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (β β ran
πΊ) β (π β ran πΊ β βπ β β0 π = ((2 Β· π) + 1))) |
223 | 195, 222 | mtbid 324 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (β β ran
πΊ) β Β¬
βπ β
β0 π = ((2
Β· π) +
1)) |
224 | | ralnex 3072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ β
β0 Β¬ π
= ((2 Β· π) + 1)
β Β¬ βπ
β β0 π = ((2 Β· π) + 1)) |
225 | 223, 224 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (β β ran
πΊ) β βπ β β0
Β¬ π = ((2 Β·
π) + 1)) |
226 | 225 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (β β ran
πΊ) β§ π β β0) β Β¬
π = ((2 Β· π) + 1)) |
227 | 226 | neqned 2947 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (β β ran
πΊ) β§ π β β0) β π β ((2 Β· π) + 1)) |
228 | 227 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (β β ran
πΊ) β§ π β β0) β ((2
Β· π) + 1) β π) |
229 | 228 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (β β ran
πΊ) β§ π β β€) β§ π β β0) β ((2
Β· π) + 1) β π) |
230 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (β β ran
πΊ) β§ π β β€) β§ Β¬ π β β0)
β π β
β€) |
231 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (β β ran
πΊ) β§ π β β€) β§ Β¬ π β β0)
β Β¬ π β
β0) |
232 | 179 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (β β ran
πΊ) β§ π β β€) β§ Β¬ π β β0)
β π β
β) |
233 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β€ β§ Β¬
π β
β0) β 2 β β) |
234 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β€ β§ Β¬
π β
β0) β π β β€) |
235 | 234 | zred 12612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β€ β§ Β¬
π β
β0) β π β β) |
236 | 233, 235 | remulcld 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β€ β§ Β¬
π β
β0) β (2 Β· π) β β) |
237 | | 0red 11163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β€ β§ Β¬
π β
β0) β 0 β β) |
238 | | 1red 11161 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β€ β§ Β¬
π β
β0) β 1 β β) |
239 | | 2cnd 12236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β€ β§ Β¬
π β
β0) β 2 β β) |
240 | 235 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β€ β§ Β¬
π β
β0) β π β β) |
241 | 239, 240 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β€ β§ Β¬
π β
β0) β (2 Β· π) = (π Β· 2)) |
242 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β β€ β§ Β¬
π β
β0) β Β¬ π β β0) |
243 | | elnn0z 12517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β β0
β (π β β€
β§ 0 β€ π)) |
244 | 242, 243 | sylnib 328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β β€ β§ Β¬
π β
β0) β Β¬ (π β β€ β§ 0 β€ π)) |
245 | | nan 829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β β€ β§ Β¬
π β
β0) β Β¬ (π β β€ β§ 0 β€ π)) β (((π β β€ β§ Β¬ π β β0)
β§ π β β€)
β Β¬ 0 β€ π)) |
246 | 244, 245 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β β€ β§ Β¬
π β
β0) β§ π β β€) β Β¬ 0 β€ π) |
247 | 246 | anabss1 665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β β€ β§ Β¬
π β
β0) β Β¬ 0 β€ π) |
248 | 235, 237 | ltnled 11307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β β€ β§ Β¬
π β
β0) β (π < 0 β Β¬ 0 β€ π)) |
249 | 247, 248 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β€ β§ Β¬
π β
β0) β π < 0) |
250 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β β€ β§ Β¬
π β
β0) β 2 β β+) |
251 | 250 | rpregt0d 12968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β€ β§ Β¬
π β
β0) β (2 β β β§ 0 < 2)) |
252 | | mulltgt0 43315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β β β§ π < 0) β§ (2 β β
β§ 0 < 2)) β (π
Β· 2) < 0) |
253 | 235, 249,
251, 252 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β€ β§ Β¬
π β
β0) β (π Β· 2) < 0) |
254 | 241, 253 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β€ β§ Β¬
π β
β0) β (2 Β· π) < 0) |
255 | 236, 237,
238, 254 | ltadd1dd 11771 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β€ β§ Β¬
π β
β0) β ((2 Β· π) + 1) < (0 + 1)) |
256 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β€ β§ Β¬
π β
β0) β 1 β β) |
257 | 256 | addid2d 11361 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β€ β§ Β¬
π β
β0) β (0 + 1) = 1) |
258 | 255, 257 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β€ β§ Β¬
π β
β0) β ((2 Β· π) + 1) < 1) |
259 | 236, 238 | readdcld 11189 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β€ β§ Β¬
π β
β0) β ((2 Β· π) + 1) β β) |
260 | 259, 238 | ltnled 11307 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β€ β§ Β¬
π β
β0) β (((2 Β· π) + 1) < 1 β Β¬ 1 β€ ((2
Β· π) +
1))) |
261 | 258, 260 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β€ β§ Β¬
π β
β0) β Β¬ 1 β€ ((2 Β· π) + 1)) |
262 | | nnge1 12186 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((2
Β· π) + 1) β
β β 1 β€ ((2 Β· π) + 1)) |
263 | 261, 262 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β€ β§ Β¬
π β
β0) β Β¬ ((2 Β· π) + 1) β β) |
264 | 263 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β€ β§ Β¬
π β
β0) β§ π β β) β Β¬ ((2 Β·
π) + 1) β
β) |
265 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ ((2
Β· π) + 1) = π) β ((2 Β· π) + 1) = π) |
266 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ ((2
Β· π) + 1) = π) β π β β) |
267 | 265, 266 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ ((2
Β· π) + 1) = π) β ((2 Β· π) + 1) β
β) |
268 | 267 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β β€ β§ Β¬
π β
β0) β§ π β β) β§ ((2 Β· π) + 1) = π) β ((2 Β· π) + 1) β β) |
269 | 264, 268 | mtand 815 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β€ β§ Β¬
π β
β0) β§ π β β) β Β¬ ((2 Β·
π) + 1) = π) |
270 | 269 | neqned 2947 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β€ β§ Β¬
π β
β0) β§ π β β) β ((2 Β· π) + 1) β π) |
271 | 230, 231,
232, 270 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (β β ran
πΊ) β§ π β β€) β§ Β¬ π β β0)
β ((2 Β· π) + 1)
β π) |
272 | 229, 271 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (β β ran
πΊ) β§ π β β€) β ((2 Β· π) + 1) β π) |
273 | 272 | neneqd 2945 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (β β ran
πΊ) β§ π β β€) β Β¬ ((2 Β·
π) + 1) = π) |
274 | 273 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (π β (β β ran
πΊ) β (π β β€ β Β¬ ((2
Β· π) + 1) = π)) |
275 | 221, 274 | ralrimi 3239 |
. . . . . . . . . . . . . . 15
β’ (π β (β β ran
πΊ) β βπ β β€ Β¬ ((2
Β· π) + 1) = π) |
276 | | ralnex 3072 |
. . . . . . . . . . . . . . 15
β’
(βπ β
β€ Β¬ ((2 Β· π) + 1) = π β Β¬ βπ β β€ ((2 Β· π) + 1) = π) |
277 | 275, 276 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β (β β ran
πΊ) β Β¬
βπ β β€ ((2
Β· π) + 1) = π) |
278 | 179 | nnzd 12531 |
. . . . . . . . . . . . . . 15
β’ (π β (β β ran
πΊ) β π β
β€) |
279 | | odd2np1 16228 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β (Β¬ 2
β₯ π β
βπ β β€ ((2
Β· π) + 1) = π)) |
280 | 278, 279 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (β β ran
πΊ) β (Β¬ 2 β₯
π β βπ β β€ ((2 Β·
π) + 1) = π)) |
281 | 277, 280 | mtbird 325 |
. . . . . . . . . . . . 13
β’ (π β (β β ran
πΊ) β Β¬ Β¬ 2
β₯ π) |
282 | 281 | notnotrd 133 |
. . . . . . . . . . . 12
β’ (π β (β β ran
πΊ) β 2 β₯ π) |
283 | 179 | nncnd 12174 |
. . . . . . . . . . . . 13
β’ (π β (β β ran
πΊ) β π β
β) |
284 | 283, 181 | npcand 11521 |
. . . . . . . . . . . 12
β’ (π β (β β ran
πΊ) β ((π β 1) + 1) = π) |
285 | 282, 284 | breqtrrd 5134 |
. . . . . . . . . . 11
β’ (π β (β β ran
πΊ) β 2 β₯ ((π β 1) +
1)) |
286 | 183 | nn0zd 12530 |
. . . . . . . . . . . 12
β’ (π β (β β ran
πΊ) β (π β 1) β
β€) |
287 | | oddp1even 16231 |
. . . . . . . . . . . 12
β’ ((π β 1) β β€
β (Β¬ 2 β₯ (π
β 1) β 2 β₯ ((π β 1) + 1))) |
288 | 286, 287 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β β ran
πΊ) β (Β¬ 2 β₯
(π β 1) β 2
β₯ ((π β 1) +
1))) |
289 | 285, 288 | mpbird 257 |
. . . . . . . . . 10
β’ (π β (β β ran
πΊ) β Β¬ 2 β₯
(π β
1)) |
290 | | oexpneg 16232 |
. . . . . . . . . 10
β’ ((1
β β β§ (π
β 1) β β β§ Β¬ 2 β₯ (π β 1)) β (-1β(π β 1)) = -(1β(π β 1))) |
291 | 181, 215,
289, 290 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (β β ran
πΊ) β (-1β(π β 1)) = -(1β(π β 1))) |
292 | | 1exp 14003 |
. . . . . . . . . . 11
β’ ((π β 1) β β€
β (1β(π β
1)) = 1) |
293 | 286, 292 | syl 17 |
. . . . . . . . . 10
β’ (π β (β β ran
πΊ) β (1β(π β 1)) =
1) |
294 | 293 | negeqd 11400 |
. . . . . . . . 9
β’ (π β (β β ran
πΊ) β -(1β(π β 1)) =
-1) |
295 | 291, 294 | eqtrd 2773 |
. . . . . . . 8
β’ (π β (β β ran
πΊ) β (-1β(π β 1)) =
-1) |
296 | 295 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (β β ran πΊ)) β (-1β(π β 1)) =
-1) |
297 | 296 | oveq1d 7373 |
. . . . . 6
β’ ((π β§ π β (β β ran πΊ)) β ((-1β(π β 1)) Β· ((πβπ) / π)) = (-1 Β· ((πβπ) / π))) |
298 | 297 | oveq1d 7373 |
. . . . 5
β’ ((π β§ π β (β β ran πΊ)) β (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π)) = ((-1 Β· ((πβπ) / π)) + ((πβπ) / π))) |
299 | 191 | mulm1d 11612 |
. . . . . . 7
β’ ((π β§ π β (β β ran πΊ)) β (-1 Β· ((πβπ) / π)) = -((πβπ) / π)) |
300 | 299 | oveq1d 7373 |
. . . . . 6
β’ ((π β§ π β (β β ran πΊ)) β ((-1 Β· ((πβπ) / π)) + ((πβπ) / π)) = (-((πβπ) / π) + ((πβπ) / π))) |
301 | 191 | negcld 11504 |
. . . . . . 7
β’ ((π β§ π β (β β ran πΊ)) β -((πβπ) / π) β β) |
302 | 301, 191 | addcomd 11362 |
. . . . . 6
β’ ((π β§ π β (β β ran πΊ)) β (-((πβπ) / π) + ((πβπ) / π)) = (((πβπ) / π) + -((πβπ) / π))) |
303 | 191 | negidd 11507 |
. . . . . 6
β’ ((π β§ π β (β β ran πΊ)) β (((πβπ) / π) + -((πβπ) / π)) = 0) |
304 | 300, 302,
303 | 3eqtrd 2777 |
. . . . 5
β’ ((π β§ π β (β β ran πΊ)) β ((-1 Β· ((πβπ) / π)) + ((πβπ) / π)) = 0) |
305 | 194, 298,
304 | 3eqtrd 2777 |
. . . 4
β’ ((π β§ π β (β β ran πΊ)) β (πΉβπ) = 0) |
306 | 111, 110 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β β) β (πΉβπ) β β) |
307 | 99 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β0) β πΉ = (π β β β¦ (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π)))) |
308 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π = ((2 Β· π) + 1)) β π = ((2 Β· π) + 1)) |
309 | 308 | oveq1d 7373 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π = ((2 Β· π) + 1)) β (π β 1) = (((2 Β·
π) + 1) β
1)) |
310 | 309 | oveq2d 7374 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π = ((2 Β· π) + 1)) β (-1β(π β 1)) = (-1β(((2
Β· π) + 1) β
1))) |
311 | 308 | oveq2d 7374 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π = ((2 Β· π) + 1)) β (πβπ) = (πβ((2 Β· π) + 1))) |
312 | 311, 308 | oveq12d 7376 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π = ((2 Β· π) + 1)) β ((πβπ) / π) = ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) |
313 | 310, 312 | oveq12d 7376 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π = ((2 Β· π) + 1)) β ((-1β(π β 1)) Β· ((πβπ) / π)) = ((-1β(((2 Β· π) + 1) β 1)) Β·
((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
314 | 313, 312 | oveq12d 7376 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π = ((2 Β· π) + 1)) β (((-1β(π β 1)) Β· ((πβπ) / π)) + ((πβπ) / π)) = (((-1β(((2 Β· π) + 1) β 1)) Β·
((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) + ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
315 | 138 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β β0) β 2 β
β0) |
316 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β β0) β π β
β0) |
317 | 315, 316 | nn0mulcld 12483 |
. . . . . . . 8
β’ ((π β§ π β β0) β (2
Β· π) β
β0) |
318 | | nn0p1nn 12457 |
. . . . . . . 8
β’ ((2
Β· π) β
β0 β ((2 Β· π) + 1) β β) |
319 | 317, 318 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β0) β ((2
Β· π) + 1) β
β) |
320 | 166 | negcld 11504 |
. . . . . . . . . . 11
β’ (π β β0
β -1 β β) |
321 | 165, 166 | pncand 11518 |
. . . . . . . . . . . 12
β’ (π β β0
β (((2 Β· π) +
1) β 1) = (2 Β· π)) |
322 | 138 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β0
β 2 β β0) |
323 | 322, 162 | nn0mulcld 12483 |
. . . . . . . . . . . 12
β’ (π β β0
β (2 Β· π)
β β0) |
324 | 321, 323 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (π β β0
β (((2 Β· π) +
1) β 1) β β0) |
325 | 320, 324 | expcld 14057 |
. . . . . . . . . 10
β’ (π β β0
β (-1β(((2 Β· π) + 1) β 1)) β
β) |
326 | 325 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
(-1β(((2 Β· π) +
1) β 1)) β β) |
327 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β π β
β) |
328 | 197 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β 1 β
β0) |
329 | 317, 328 | nn0addcld 12482 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β ((2
Β· π) + 1) β
β0) |
330 | 327, 329 | expcld 14057 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (πβ((2 Β· π) + 1)) β
β) |
331 | | 2cnd 12236 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β 2 β
β) |
332 | 164 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β π β
β) |
333 | 331, 332 | mulcld 11180 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (2
Β· π) β
β) |
334 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β 1 β
β) |
335 | 333, 334 | addcld 11179 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β ((2
Β· π) + 1) β
β) |
336 | | 0red 11163 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β 0 β
β) |
337 | 146 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β 2 β
β) |
338 | 148 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β π β
β) |
339 | 337, 338 | remulcld 11190 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β (2
Β· π) β
β) |
340 | | 1red 11161 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β 1 β
β) |
341 | | 0le2 12260 |
. . . . . . . . . . . . . 14
β’ 0 β€
2 |
342 | 341 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β 0 β€
2) |
343 | 316 | nn0ge0d 12481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β 0 β€
π) |
344 | 337, 338,
342, 343 | mulge0d 11737 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β 0 β€ (2
Β· π)) |
345 | | 0lt1 11682 |
. . . . . . . . . . . . 13
β’ 0 <
1 |
346 | 345 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β 0 <
1) |
347 | 339, 340,
344, 346 | addgegt0d 11733 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β 0 <
((2 Β· π) +
1)) |
348 | 336, 347 | gtned 11295 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β ((2
Β· π) + 1) β
0) |
349 | 330, 335,
348 | divcld 11936 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1)) β
β) |
350 | 326, 349 | mulcld 11180 |
. . . . . . . 8
β’ ((π β§ π β β0) β
((-1β(((2 Β· π)
+ 1) β 1)) Β· ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) β β) |
351 | 350, 349 | addcld 11179 |
. . . . . . 7
β’ ((π β§ π β β0) β
(((-1β(((2 Β· π)
+ 1) β 1)) Β· ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) + ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) β β) |
352 | 307, 314,
319, 351 | fvmptd 6956 |
. . . . . 6
β’ ((π β§ π β β0) β (πΉβ((2 Β· π) + 1)) = (((-1β(((2
Β· π) + 1) β
1)) Β· ((πβ((2
Β· π) + 1)) / ((2
Β· π) + 1))) +
((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
353 | 321 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β (((2
Β· π) + 1) β 1)
= (2 Β· π)) |
354 | 353 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β
(-1β(((2 Β· π) +
1) β 1)) = (-1β(2 Β· π))) |
355 | | nn0z 12529 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β€) |
356 | | m1expeven 14021 |
. . . . . . . . . . . . 13
β’ (π β β€ β
(-1β(2 Β· π)) =
1) |
357 | 355, 356 | syl 17 |
. . . . . . . . . . . 12
β’ (π β β0
β (-1β(2 Β· π)) = 1) |
358 | 357 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β
(-1β(2 Β· π)) =
1) |
359 | 354, 358 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β
(-1β(((2 Β· π) +
1) β 1)) = 1) |
360 | 359 | oveq1d 7373 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
((-1β(((2 Β· π)
+ 1) β 1)) Β· ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) = (1 Β· ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
361 | 349 | mulid2d 11178 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (1
Β· ((πβ((2
Β· π) + 1)) / ((2
Β· π) + 1))) =
((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) |
362 | 360, 361 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π β β0) β
((-1β(((2 Β· π)
+ 1) β 1)) Β· ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) = ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) |
363 | 362 | oveq1d 7373 |
. . . . . . 7
β’ ((π β§ π β β0) β
(((-1β(((2 Β· π)
+ 1) β 1)) Β· ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) + ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) = (((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1)) + ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
364 | 349 | 2timesd 12401 |
. . . . . . 7
β’ ((π β§ π β β0) β (2
Β· ((πβ((2
Β· π) + 1)) / ((2
Β· π) + 1))) =
(((πβ((2 Β·
π) + 1)) / ((2 Β·
π) + 1)) + ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
365 | 330, 335,
348 | divrec2d 11940 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1)) = ((1 / ((2 Β·
π) + 1)) Β· (πβ((2 Β· π) + 1)))) |
366 | 365 | oveq2d 7374 |
. . . . . . 7
β’ ((π β§ π β β0) β (2
Β· ((πβ((2
Β· π) + 1)) / ((2
Β· π) + 1))) = (2
Β· ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1))))) |
367 | 363, 364,
366 | 3eqtr2d 2779 |
. . . . . 6
β’ ((π β§ π β β0) β
(((-1β(((2 Β· π)
+ 1) β 1)) Β· ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) + ((πβ((2 Β· π) + 1)) / ((2 Β· π) + 1))) = (2 Β· ((1 / ((2 Β·
π) + 1)) Β· (πβ((2 Β· π) + 1))))) |
368 | 352, 367 | eqtr2d 2774 |
. . . . 5
β’ ((π β§ π β β0) β (2
Β· ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1)))) = (πΉβ((2 Β· π) + 1))) |
369 | | stirlinglem5.4 |
. . . . . . 7
β’ π» = (π β β0 β¦ (2
Β· ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1))))) |
370 | 369 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β0) β π» = (π β β0 β¦ (2
Β· ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1)))))) |
371 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π = π) β π = π) |
372 | 371 | oveq2d 7374 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π = π) β (2 Β· π) = (2 Β· π)) |
373 | 372 | oveq1d 7373 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π = π) β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
374 | 373 | oveq2d 7374 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π = π) β (1 / ((2 Β· π) + 1)) = (1 / ((2 Β· π) + 1))) |
375 | 373 | oveq2d 7374 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π = π) β (πβ((2 Β· π) + 1)) = (πβ((2 Β· π) + 1))) |
376 | 374, 375 | oveq12d 7376 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π = π) β ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1))) = ((1 / ((2 Β·
π) + 1)) Β· (πβ((2 Β· π) + 1)))) |
377 | 376 | oveq2d 7374 |
. . . . . 6
β’ (((π β§ π β β0) β§ π = π) β (2 Β· ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1)))) = (2 Β· ((1 /
((2 Β· π) + 1))
Β· (πβ((2
Β· π) +
1))))) |
378 | 335, 348 | reccld 11929 |
. . . . . . . 8
β’ ((π β§ π β β0) β (1 / ((2
Β· π) + 1)) β
β) |
379 | 378, 330 | mulcld 11180 |
. . . . . . 7
β’ ((π β§ π β β0) β ((1 / ((2
Β· π) + 1)) Β·
(πβ((2 Β· π) + 1))) β
β) |
380 | 331, 379 | mulcld 11180 |
. . . . . 6
β’ ((π β§ π β β0) β (2
Β· ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1)))) β β) |
381 | 370, 377,
316, 380 | fvmptd 6956 |
. . . . 5
β’ ((π β§ π β β0) β (π»βπ) = (2 Β· ((1 / ((2 Β· π) + 1)) Β· (πβ((2 Β· π) + 1))))) |
382 | 197 | a1i 11 |
. . . . . . . . 9
β’ (π β β0
β 1 β β0) |
383 | 323, 382 | nn0addcld 12482 |
. . . . . . . 8
β’ (π β β0
β ((2 Β· π) + 1)
β β0) |
384 | 158, 161,
162, 383 | fvmptd 6956 |
. . . . . . 7
β’ (π β β0
β (πΊβπ) = ((2 Β· π) + 1)) |
385 | 384 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β0) β (πΊβπ) = ((2 Β· π) + 1)) |
386 | 385 | fveq2d 6847 |
. . . . 5
β’ ((π β§ π β β0) β (πΉβ(πΊβπ)) = (πΉβ((2 Β· π) + 1))) |
387 | 368, 381,
386 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ π β β0) β (π»βπ) = (πΉβ(πΊβπ))) |
388 | 135, 1, 136, 2, 145, 178, 305, 306, 387 | isercoll2 15559 |
. . 3
β’ (π β (seq0( + , π») β ((logβ(1 + π)) β (logβ(1 β
π))) β seq1( + , πΉ) β ((logβ(1 + π)) β (logβ(1 β
π))))) |
389 | 134, 388 | mpbird 257 |
. 2
β’ (π β seq0( + , π») β ((logβ(1 + π)) β (logβ(1 β
π)))) |
390 | 51, 13 | resubcld 11588 |
. . . 4
β’ (π β (1 β π) β
β) |
391 | 14 | subidd 11505 |
. . . . . 6
β’ (π β (π β π) = 0) |
392 | 391 | eqcomd 2739 |
. . . . 5
β’ (π β 0 = (π β π)) |
393 | 13, 51, 13, 129 | ltsub1dd 11772 |
. . . . 5
β’ (π β (π β π) < (1 β π)) |
394 | 392, 393 | eqbrtrd 5128 |
. . . 4
β’ (π β 0 < (1 β π)) |
395 | 390, 394 | elrpd 12959 |
. . 3
β’ (π β (1 β π) β
β+) |
396 | 123, 395 | relogdivd 25997 |
. 2
β’ (π β (logβ((1 + π) / (1 β π))) = ((logβ(1 + π)) β (logβ(1 β π)))) |
397 | 389, 396 | breqtrrd 5134 |
1
β’ (π β seq0( + , π») β (logβ((1 + π) / (1 β π)))) |