Step | Hyp | Ref
| Expression |
1 | | stirlinglem8.1 |
. . 3
β’
β²ππ |
2 | | stirlinglem8.7 |
. . . 4
β’ πΏ = (π β β β¦ ((π΄βπ)β4)) |
3 | | nfmpt1 5218 |
. . . 4
β’
β²π(π β β β¦ ((π΄βπ)β4)) |
4 | 2, 3 | nfcxfr 2906 |
. . 3
β’
β²ππΏ |
5 | | stirlinglem8.8 |
. . . 4
β’ π = (π β β β¦ ((π·βπ)β2)) |
6 | | nfmpt1 5218 |
. . . 4
β’
β²π(π β β β¦ ((π·βπ)β2)) |
7 | 5, 6 | nfcxfr 2906 |
. . 3
β’
β²ππ |
8 | | stirlinglem8.6 |
. . . 4
β’ πΉ = (π β β β¦ (((π΄βπ)β4) / ((π·βπ)β2))) |
9 | | nfmpt1 5218 |
. . . 4
β’
β²π(π β β β¦ (((π΄βπ)β4) / ((π·βπ)β2))) |
10 | 8, 9 | nfcxfr 2906 |
. . 3
β’
β²ππΉ |
11 | | nnuz 12813 |
. . 3
β’ β =
(β€β₯β1) |
12 | | 1zzd 12541 |
. . 3
β’ (π β 1 β
β€) |
13 | | stirlinglem8.2 |
. . . 4
β’
β²ππ΄ |
14 | | stirlinglem8.5 |
. . . . 5
β’ (π β π΄:ββΆβ+) |
15 | | rrpsscn 43903 |
. . . . 5
β’
β+ β β |
16 | | fss 6690 |
. . . . 5
β’ ((π΄:ββΆβ+ β§
β+ β β) β π΄:ββΆβ) |
17 | 14, 15, 16 | sylancl 587 |
. . . 4
β’ (π β π΄:ββΆβ) |
18 | | stirlinglem8.11 |
. . . 4
β’ (π β π΄ β πΆ) |
19 | | 4nn0 12439 |
. . . . 5
β’ 4 β
β0 |
20 | 19 | a1i 11 |
. . . 4
β’ (π β 4 β
β0) |
21 | | nnex 12166 |
. . . . . . 7
β’ β
β V |
22 | 21 | mptex 7178 |
. . . . . 6
β’ (π β β β¦ ((π΄βπ)β4)) β V |
23 | 2, 22 | eqeltri 2834 |
. . . . 5
β’ πΏ β V |
24 | 23 | a1i 11 |
. . . 4
β’ (π β πΏ β V) |
25 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
26 | 14 | ffvelcdmda 7040 |
. . . . . . 7
β’ ((π β§ π β β) β (π΄βπ) β
β+) |
27 | 26 | rpcnd 12966 |
. . . . . 6
β’ ((π β§ π β β) β (π΄βπ) β β) |
28 | 19 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β 4 β
β0) |
29 | 27, 28 | expcld 14058 |
. . . . 5
β’ ((π β§ π β β) β ((π΄βπ)β4) β β) |
30 | 2 | fvmpt2 6964 |
. . . . 5
β’ ((π β β β§ ((π΄βπ)β4) β β) β (πΏβπ) = ((π΄βπ)β4)) |
31 | 25, 29, 30 | syl2anc 585 |
. . . 4
β’ ((π β§ π β β) β (πΏβπ) = ((π΄βπ)β4)) |
32 | 1, 13, 4, 11, 12, 17, 18, 20, 24, 31 | climexp 43920 |
. . 3
β’ (π β πΏ β (πΆβ4)) |
33 | 21 | mptex 7178 |
. . . . 5
β’ (π β β β¦ (((π΄βπ)β4) / ((π·βπ)β2))) β V |
34 | 8, 33 | eqeltri 2834 |
. . . 4
β’ πΉ β V |
35 | 34 | a1i 11 |
. . 3
β’ (π β πΉ β V) |
36 | | stirlinglem8.3 |
. . . 4
β’
β²ππ· |
37 | 17 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π΄:ββΆβ) |
38 | | 2nn 12233 |
. . . . . . . . 9
β’ 2 β
β |
39 | 38 | a1i 11 |
. . . . . . . 8
β’ (π β β β 2 β
β) |
40 | | id 22 |
. . . . . . . 8
β’ (π β β β π β
β) |
41 | 39, 40 | nnmulcld 12213 |
. . . . . . 7
β’ (π β β β (2
Β· π) β
β) |
42 | 41 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β (2 Β· π) β
β) |
43 | 37, 42 | ffvelcdmd 7041 |
. . . . 5
β’ ((π β§ π β β) β (π΄β(2 Β· π)) β β) |
44 | | stirlinglem8.4 |
. . . . 5
β’ π· = (π β β β¦ (π΄β(2 Β· π))) |
45 | 1, 43, 44 | fmptdf 7070 |
. . . 4
β’ (π β π·:ββΆβ) |
46 | | nfmpt1 5218 |
. . . . 5
β’
β²π(π β β β¦ (2 Β· π)) |
47 | | fex 7181 |
. . . . . 6
β’ ((π΄:ββΆβ β§
β β V) β π΄
β V) |
48 | 17, 21, 47 | sylancl 587 |
. . . . 5
β’ (π β π΄ β V) |
49 | | 1nn 12171 |
. . . . . . 7
β’ 1 β
β |
50 | | 2cnd 12238 |
. . . . . . . 8
β’ (π β 2 β
β) |
51 | | 1cnd 11157 |
. . . . . . . 8
β’ (π β 1 β
β) |
52 | 50, 51 | mulcld 11182 |
. . . . . . 7
β’ (π β (2 Β· 1) β
β) |
53 | | oveq2 7370 |
. . . . . . . 8
β’ (π = 1 β (2 Β· π) = (2 Β·
1)) |
54 | | eqid 2737 |
. . . . . . . 8
β’ (π β β β¦ (2
Β· π)) = (π β β β¦ (2
Β· π)) |
55 | 53, 54 | fvmptg 6951 |
. . . . . . 7
β’ ((1
β β β§ (2 Β· 1) β β) β ((π β β β¦ (2 Β· π))β1) = (2 Β·
1)) |
56 | 49, 52, 55 | sylancr 588 |
. . . . . 6
β’ (π β ((π β β β¦ (2 Β· π))β1) = (2 Β·
1)) |
57 | 38 | a1i 11 |
. . . . . . 7
β’ (π β 2 β
β) |
58 | 49 | a1i 11 |
. . . . . . 7
β’ (π β 1 β
β) |
59 | 57, 58 | nnmulcld 12213 |
. . . . . 6
β’ (π β (2 Β· 1) β
β) |
60 | 56, 59 | eqeltrd 2838 |
. . . . 5
β’ (π β ((π β β β¦ (2 Β· π))β1) β
β) |
61 | | 1red 11163 |
. . . . . . . . 9
β’ (π β β β 1 β
β) |
62 | 39 | nnred 12175 |
. . . . . . . . 9
β’ (π β β β 2 β
β) |
63 | 41 | nnred 12175 |
. . . . . . . . 9
β’ (π β β β (2
Β· π) β
β) |
64 | 39 | nnge1d 12208 |
. . . . . . . . 9
β’ (π β β β 1 β€
2) |
65 | 61, 62, 63, 64 | leadd2dd 11777 |
. . . . . . . 8
β’ (π β β β ((2
Β· π) + 1) β€ ((2
Β· π) +
2)) |
66 | 54 | fvmpt2 6964 |
. . . . . . . . . 10
β’ ((π β β β§ (2
Β· π) β β)
β ((π β β
β¦ (2 Β· π))βπ) = (2 Β· π)) |
67 | 41, 66 | mpdan 686 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ (2
Β· π))βπ) = (2 Β· π)) |
68 | 67 | oveq1d 7377 |
. . . . . . . 8
β’ (π β β β (((π β β β¦ (2
Β· π))βπ) + 1) = ((2 Β· π) + 1)) |
69 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = π β (2 Β· π) = (2 Β· π)) |
70 | 69 | cbvmptv 5223 |
. . . . . . . . . . 11
β’ (π β β β¦ (2
Β· π)) = (π β β β¦ (2
Β· π)) |
71 | 70 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β (π β β β¦ (2
Β· π)) = (π β β β¦ (2
Β· π))) |
72 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β β β§ π = (π + 1)) β π = (π + 1)) |
73 | 72 | oveq2d 7378 |
. . . . . . . . . 10
β’ ((π β β β§ π = (π + 1)) β (2 Β· π) = (2 Β· (π + 1))) |
74 | | peano2nn 12172 |
. . . . . . . . . 10
β’ (π β β β (π + 1) β
β) |
75 | 39, 74 | nnmulcld 12213 |
. . . . . . . . . 10
β’ (π β β β (2
Β· (π + 1)) β
β) |
76 | 71, 73, 74, 75 | fvmptd 6960 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ (2
Β· π))β(π + 1)) = (2 Β· (π + 1))) |
77 | | 2cnd 12238 |
. . . . . . . . . 10
β’ (π β β β 2 β
β) |
78 | | nncn 12168 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
79 | | 1cnd 11157 |
. . . . . . . . . 10
β’ (π β β β 1 β
β) |
80 | 77, 78, 79 | adddid 11186 |
. . . . . . . . 9
β’ (π β β β (2
Β· (π + 1)) = ((2
Β· π) + (2 Β·
1))) |
81 | 77 | mulid1d 11179 |
. . . . . . . . . 10
β’ (π β β β (2
Β· 1) = 2) |
82 | 81 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β β β ((2
Β· π) + (2 Β·
1)) = ((2 Β· π) +
2)) |
83 | 76, 80, 82 | 3eqtrd 2781 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ (2
Β· π))β(π + 1)) = ((2 Β· π) + 2)) |
84 | 65, 68, 83 | 3brtr4d 5142 |
. . . . . . 7
β’ (π β β β (((π β β β¦ (2
Β· π))βπ) + 1) β€ ((π β β β¦ (2 Β· π))β(π + 1))) |
85 | 41 | nnzd 12533 |
. . . . . . . . . 10
β’ (π β β β (2
Β· π) β
β€) |
86 | 67, 85 | eqeltrd 2838 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ (2
Β· π))βπ) β
β€) |
87 | 86 | peano2zd 12617 |
. . . . . . . 8
β’ (π β β β (((π β β β¦ (2
Β· π))βπ) + 1) β
β€) |
88 | 75 | nnzd 12533 |
. . . . . . . . 9
β’ (π β β β (2
Β· (π + 1)) β
β€) |
89 | 76, 88 | eqeltrd 2838 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ (2
Β· π))β(π + 1)) β
β€) |
90 | | eluz 12784 |
. . . . . . . 8
β’
(((((π β
β β¦ (2 Β· π))βπ) + 1) β β€ β§ ((π β β β¦ (2
Β· π))β(π + 1)) β β€) β
(((π β β β¦
(2 Β· π))β(π + 1)) β
(β€β₯β(((π β β β¦ (2 Β· π))βπ) + 1)) β (((π β β β¦ (2 Β· π))βπ) + 1) β€ ((π β β β¦ (2 Β· π))β(π + 1)))) |
91 | 87, 89, 90 | syl2anc 585 |
. . . . . . 7
β’ (π β β β (((π β β β¦ (2
Β· π))β(π + 1)) β
(β€β₯β(((π β β β¦ (2 Β· π))βπ) + 1)) β (((π β β β¦ (2 Β· π))βπ) + 1) β€ ((π β β β¦ (2 Β· π))β(π + 1)))) |
92 | 84, 91 | mpbird 257 |
. . . . . 6
β’ (π β β β ((π β β β¦ (2
Β· π))β(π + 1)) β
(β€β₯β(((π β β β¦ (2 Β· π))βπ) + 1))) |
93 | 92 | adantl 483 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ (2 Β· π))β(π + 1)) β
(β€β₯β(((π β β β¦ (2 Β· π))βπ) + 1))) |
94 | 21 | mptex 7178 |
. . . . . . 7
β’ (π β β β¦ (π΄β(2 Β· π))) β V |
95 | 44, 94 | eqeltri 2834 |
. . . . . 6
β’ π· β V |
96 | 95 | a1i 11 |
. . . . 5
β’ (π β π· β V) |
97 | 44 | fvmpt2 6964 |
. . . . . . 7
β’ ((π β β β§ (π΄β(2 Β· π)) β β) β (π·βπ) = (π΄β(2 Β· π))) |
98 | 25, 43, 97 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β β) β (π·βπ) = (π΄β(2 Β· π))) |
99 | 67 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π β β β¦ (2 Β· π))βπ) = (2 Β· π)) |
100 | 99 | eqcomd 2743 |
. . . . . . 7
β’ ((π β§ π β β) β (2 Β· π) = ((π β β β¦ (2 Β· π))βπ)) |
101 | 100 | fveq2d 6851 |
. . . . . 6
β’ ((π β§ π β β) β (π΄β(2 Β· π)) = (π΄β((π β β β¦ (2 Β· π))βπ))) |
102 | 98, 101 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π β β) β (π·βπ) = (π΄β((π β β β¦ (2 Β· π))βπ))) |
103 | 1, 13, 36, 46, 11, 12, 48, 27, 18, 60, 93, 96, 102 | climsuse 43923 |
. . . 4
β’ (π β π· β πΆ) |
104 | | 2nn0 12437 |
. . . . 5
β’ 2 β
β0 |
105 | 104 | a1i 11 |
. . . 4
β’ (π β 2 β
β0) |
106 | 21 | mptex 7178 |
. . . . . 6
β’ (π β β β¦ ((π·βπ)β2)) β V |
107 | 5, 106 | eqeltri 2834 |
. . . . 5
β’ π β V |
108 | 107 | a1i 11 |
. . . 4
β’ (π β π β V) |
109 | | stirlinglem8.9 |
. . . . . . 7
β’ ((π β§ π β β) β (π·βπ) β
β+) |
110 | 109 | rpcnd 12966 |
. . . . . 6
β’ ((π β§ π β β) β (π·βπ) β β) |
111 | 110 | sqcld 14056 |
. . . . 5
β’ ((π β§ π β β) β ((π·βπ)β2) β β) |
112 | 5 | fvmpt2 6964 |
. . . . 5
β’ ((π β β β§ ((π·βπ)β2) β β) β (πβπ) = ((π·βπ)β2)) |
113 | 25, 111, 112 | syl2anc 585 |
. . . 4
β’ ((π β§ π β β) β (πβπ) = ((π·βπ)β2)) |
114 | 1, 36, 7, 11, 12, 45, 103, 105, 108, 113 | climexp 43920 |
. . 3
β’ (π β π β (πΆβ2)) |
115 | | stirlinglem8.10 |
. . . . 5
β’ (π β πΆ β
β+) |
116 | 115 | rpcnd 12966 |
. . . 4
β’ (π β πΆ β β) |
117 | 115 | rpne0d 12969 |
. . . 4
β’ (π β πΆ β 0) |
118 | | 2z 12542 |
. . . . 5
β’ 2 β
β€ |
119 | 118 | a1i 11 |
. . . 4
β’ (π β 2 β
β€) |
120 | 116, 117,
119 | expne0d 14064 |
. . 3
β’ (π β (πΆβ2) β 0) |
121 | 1, 29, 2 | fmptdf 7070 |
. . . 4
β’ (π β πΏ:ββΆβ) |
122 | 121 | ffvelcdmda 7040 |
. . 3
β’ ((π β§ π β β) β (πΏβπ) β β) |
123 | 113, 111 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π β β) β (πβπ) β β) |
124 | 98 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((π·βπ)β2) = ((π΄β(2 Β· π))β2)) |
125 | 113, 124 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβπ) = ((π΄β(2 Β· π))β2)) |
126 | 98, 109 | eqeltrrd 2839 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π΄β(2 Β· π)) β
β+) |
127 | 118 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β β) β 2 β
β€) |
128 | 126, 127 | rpexpcld 14157 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π΄β(2 Β· π))β2) β
β+) |
129 | 125, 128 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ π β β) β (πβπ) β
β+) |
130 | 129 | rpne0d 12969 |
. . . . . 6
β’ ((π β§ π β β) β (πβπ) β 0) |
131 | 130 | neneqd 2949 |
. . . . 5
β’ ((π β§ π β β) β Β¬ (πβπ) = 0) |
132 | | 0cn 11154 |
. . . . . 6
β’ 0 β
β |
133 | | elsn2g 4629 |
. . . . . 6
β’ (0 β
β β ((πβπ) β {0} β (πβπ) = 0)) |
134 | 132, 133 | ax-mp 5 |
. . . . 5
β’ ((πβπ) β {0} β (πβπ) = 0) |
135 | 131, 134 | sylnibr 329 |
. . . 4
β’ ((π β§ π β β) β Β¬ (πβπ) β {0}) |
136 | 123, 135 | eldifd 3926 |
. . 3
β’ ((π β§ π β β) β (πβπ) β (β β
{0})) |
137 | 28 | nn0zd 12532 |
. . . . . . 7
β’ ((π β§ π β β) β 4 β
β€) |
138 | 26, 137 | rpexpcld 14157 |
. . . . . 6
β’ ((π β§ π β β) β ((π΄βπ)β4) β
β+) |
139 | 109, 127 | rpexpcld 14157 |
. . . . . 6
β’ ((π β§ π β β) β ((π·βπ)β2) β
β+) |
140 | 138, 139 | rpdivcld 12981 |
. . . . 5
β’ ((π β§ π β β) β (((π΄βπ)β4) / ((π·βπ)β2)) β
β+) |
141 | 8 | fvmpt2 6964 |
. . . . 5
β’ ((π β β β§ (((π΄βπ)β4) / ((π·βπ)β2)) β β+) β
(πΉβπ) = (((π΄βπ)β4) / ((π·βπ)β2))) |
142 | 25, 140, 141 | syl2anc 585 |
. . . 4
β’ ((π β§ π β β) β (πΉβπ) = (((π΄βπ)β4) / ((π·βπ)β2))) |
143 | 2 | fvmpt2 6964 |
. . . . . 6
β’ ((π β β β§ ((π΄βπ)β4) β β+) β
(πΏβπ) = ((π΄βπ)β4)) |
144 | 25, 138, 143 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β β) β (πΏβπ) = ((π΄βπ)β4)) |
145 | 144, 113 | oveq12d 7380 |
. . . 4
β’ ((π β§ π β β) β ((πΏβπ) / (πβπ)) = (((π΄βπ)β4) / ((π·βπ)β2))) |
146 | 142, 145 | eqtr4d 2780 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = ((πΏβπ) / (πβπ))) |
147 | 1, 4, 7, 10, 11, 12, 32, 35, 114, 120, 122, 136, 146 | climdivf 43927 |
. 2
β’ (π β πΉ β ((πΆβ4) / (πΆβ2))) |
148 | | 2cn 12235 |
. . . . . 6
β’ 2 β
β |
149 | | 2p2e4 12295 |
. . . . . 6
β’ (2 + 2) =
4 |
150 | 148, 148,
149 | mvlladdi 11426 |
. . . . 5
β’ 2 = (4
β 2) |
151 | 150 | a1i 11 |
. . . 4
β’ (π β 2 = (4 β
2)) |
152 | 151 | oveq2d 7378 |
. . 3
β’ (π β (πΆβ2) = (πΆβ(4 β 2))) |
153 | 20 | nn0zd 12532 |
. . . 4
β’ (π β 4 β
β€) |
154 | 116, 117,
119, 153 | expsubd 14069 |
. . 3
β’ (π β (πΆβ(4 β 2)) = ((πΆβ4) / (πΆβ2))) |
155 | 152, 154 | eqtrd 2777 |
. 2
β’ (π β (πΆβ2) = ((πΆβ4) / (πΆβ2))) |
156 | 147, 155 | breqtrrd 5138 |
1
β’ (π β πΉ β (πΆβ2)) |