stirlinglem7

Description: Algebraic manipulation of the formula for J(n). (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem7.1	$⊢ J = (n \in ℕ ⟼ (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) - 1)$
	stirlinglem7.2	$⊢ K = (k \in ℕ ⟼ (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k})$
	stirlinglem7.3	$⊢ H = (k \in ℕ_{0} ⟼ 2 (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k + 1})$
Assertion	stirlinglem7	$⊢ N \in ℕ \to seq 1 (+ K) ⇝ J (N)$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem7.1	$⊢ J = (n \in ℕ ⟼ (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) - 1)$
2		stirlinglem7.2	$⊢ K = (k \in ℕ ⟼ (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k})$
3		stirlinglem7.3	$⊢ H = (k \in ℕ_{0} ⟼ 2 (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k + 1})$
4		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
5		1zzd	$⊢ N \in ℕ \to 1 \in ℤ$
6		1e0p1	$⊢ 1 = 0 + 1$
7	6	a1i	$⊢ N \in ℕ \to 1 = 0 + 1$
8	7	seqeq1d	$⊢ N \in ℕ \to seq 1 (+ H) = seq (0 + 1) (+ H)$
9		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
10		0nn0	$⊢ 0 \in ℕ_{0}$
11	10	a1i	$⊢ N \in ℕ \to 0 \in ℕ_{0}$
12		oveq2	$⊢ k = j \to 2 k = 2 j$
13	12	oveq1d	$⊢ k = j \to 2 k + 1 = 2 j + 1$
14	13	oveq2d	$⊢ k = j \to \frac{1}{2 k + 1} = \frac{1}{2 j + 1}$
15	13	oveq2d	$⊢ k = j \to {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = {(\frac{1}{2 \cdot N + 1})}^{2 j + 1}$
16	14 15	oveq12d	$⊢ k = j \to (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = (\frac{1}{2 j + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 j + 1}$
17	16	oveq2d	$⊢ k = j \to 2 (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = 2 (\frac{1}{2 j + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 j + 1}$
18		simpr	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to j \in ℕ_{0}$
19		2cnd	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 \in ℂ$
20		2cnd	$⊢ j \in ℕ_{0} \to 2 \in ℂ$
21		nn0cn	$⊢ j \in ℕ_{0} \to j \in ℂ$
22	20 21	mulcld	$⊢ j \in ℕ_{0} \to 2 j \in ℂ$
23		1cnd	$⊢ j \in ℕ_{0} \to 1 \in ℂ$
24	22 23	addcld	$⊢ j \in ℕ_{0} \to 2 j + 1 \in ℂ$
25	24	adantl	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 j + 1 \in ℂ$
26		0red	$⊢ j \in ℕ_{0} \to 0 \in ℝ$
27		2re	$⊢ 2 \in ℝ$
28	27	a1i	$⊢ j \in ℕ_{0} \to 2 \in ℝ$
29		nn0re	$⊢ j \in ℕ_{0} \to j \in ℝ$
30	28 29	remulcld	$⊢ j \in ℕ_{0} \to 2 j \in ℝ$
31		1red	$⊢ j \in ℕ_{0} \to 1 \in ℝ$
32		0le2	$⊢ 0 \leq 2$
33	32	a1i	$⊢ j \in ℕ_{0} \to 0 \leq 2$
34		nn0ge0	$⊢ j \in ℕ_{0} \to 0 \leq j$
35	28 29 33 34	mulge0d	$⊢ j \in ℕ_{0} \to 0 \leq 2 j$
36		0lt1	$⊢ 0 < 1$
37	36	a1i	$⊢ j \in ℕ_{0} \to 0 < 1$
38	30 31 35 37	addgegt0d	$⊢ j \in ℕ_{0} \to 0 < 2 j + 1$
39	26 38	ltned	$⊢ j \in ℕ_{0} \to 0 \neq 2 j + 1$
40	39	adantl	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 0 \neq 2 j + 1$
41	40	necomd	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 j + 1 \neq 0$
42	25 41	reccld	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to \frac{1}{2 j + 1} \in ℂ$
43		nncn	$⊢ N \in ℕ \to N \in ℂ$
44	43	adantr	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to N \in ℂ$
45	19 44	mulcld	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 \cdot N \in ℂ$
46		1cnd	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 1 \in ℂ$
47	45 46	addcld	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 \cdot N + 1 \in ℂ$
48	27	a1i	$⊢ N \in ℕ \to 2 \in ℝ$
49		nnre	$⊢ N \in ℕ \to N \in ℝ$
50	48 49	remulcld	$⊢ N \in ℕ \to 2 \cdot N \in ℝ$
51		1red	$⊢ N \in ℕ \to 1 \in ℝ$
52	32	a1i	$⊢ N \in ℕ \to 0 \leq 2$
53		0red	$⊢ N \in ℕ \to 0 \in ℝ$
54		nngt0	$⊢ N \in ℕ \to 0 < N$
55	53 49 54	ltled	$⊢ N \in ℕ \to 0 \leq N$
56	48 49 52 55	mulge0d	$⊢ N \in ℕ \to 0 \leq 2 \cdot N$
57	36	a1i	$⊢ N \in ℕ \to 0 < 1$
58	50 51 56 57	addgegt0d	$⊢ N \in ℕ \to 0 < 2 \cdot N + 1$
59	58	gt0ne0d	$⊢ N \in ℕ \to 2 \cdot N + 1 \neq 0$
60	59	adantr	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 \cdot N + 1 \neq 0$
61	47 60	reccld	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to \frac{1}{2 \cdot N + 1} \in ℂ$
62		2nn0	$⊢ 2 \in ℕ_{0}$
63	62	a1i	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 \in ℕ_{0}$
64	63 18	nn0mulcld	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 j \in ℕ_{0}$
65		1nn0	$⊢ 1 \in ℕ_{0}$
66	65	a1i	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 1 \in ℕ_{0}$
67	64 66	nn0addcld	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 j + 1 \in ℕ_{0}$
68	61 67	expcld	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to {(\frac{1}{2 \cdot N + 1})}^{2 j + 1} \in ℂ$
69	42 68	mulcld	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to (\frac{1}{2 j + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 j + 1} \in ℂ$
70	19 69	mulcld	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to 2 (\frac{1}{2 j + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 j + 1} \in ℂ$
71	3 17 18 70	fvmptd3	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to H (j) = 2 (\frac{1}{2 j + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 j + 1}$
72	71 70	eqeltrd	$⊢ (N \in ℕ \land j \in ℕ_{0}) \to H (j) \in ℂ$
73	3	stirlinglem6	$⊢ N \in ℕ \to seq 0 (+ H) ⇝ \log (\frac{N + 1}{N})$
74	9 11 72 73	clim2ser	$⊢ N \in ℕ \to seq (0 + 1) (+ H) ⇝ (\log (\frac{N + 1}{N}) - seq 0 (+ H) (0))$
75	8 74	eqbrtrd	$⊢ N \in ℕ \to seq 1 (+ H) ⇝ (\log (\frac{N + 1}{N}) - seq 0 (+ H) (0))$
76		0z	$⊢ 0 \in ℤ$
77		seq1	$⊢ 0 \in ℤ \to seq 0 (+ H) (0) = H (0)$
78	76 77	mp1i	$⊢ N \in ℕ \to seq 0 (+ H) (0) = H (0)$
79	3	a1i	$⊢ N \in ℕ \to H = (k \in ℕ_{0} ⟼ 2 (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k + 1})$
80		simpr	$⊢ (N \in ℕ \land k = 0) \to k = 0$
81	80	oveq2d	$⊢ (N \in ℕ \land k = 0) \to 2 k = 2 \cdot 0$
82	81	oveq1d	$⊢ (N \in ℕ \land k = 0) \to 2 k + 1 = 2 \cdot 0 + 1$
83	82	oveq2d	$⊢ (N \in ℕ \land k = 0) \to \frac{1}{2 k + 1} = \frac{1}{2 \cdot 0 + 1}$
84	82	oveq2d	$⊢ (N \in ℕ \land k = 0) \to {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1}$
85	83 84	oveq12d	$⊢ (N \in ℕ \land k = 0) \to (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = (\frac{1}{2 \cdot 0 + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1}$
86	85	oveq2d	$⊢ (N \in ℕ \land k = 0) \to 2 (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = 2 (\frac{1}{2 \cdot 0 + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1}$
87		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
88		0cnd	$⊢ N \in ℕ \to 0 \in ℂ$
89	87 88	mulcld	$⊢ N \in ℕ \to 2 \cdot 0 \in ℂ$
90		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
91	89 90	addcld	$⊢ N \in ℕ \to 2 \cdot 0 + 1 \in ℂ$
92	87	mul01d	$⊢ N \in ℕ \to 2 \cdot 0 = 0$
93	92	eqcomd	$⊢ N \in ℕ \to 0 = 2 \cdot 0$
94	93	oveq1d	$⊢ N \in ℕ \to 0 + 1 = 2 \cdot 0 + 1$
95	7 94	eqtrd	$⊢ N \in ℕ \to 1 = 2 \cdot 0 + 1$
96	57 95	breqtrd	$⊢ N \in ℕ \to 0 < 2 \cdot 0 + 1$
97	96	gt0ne0d	$⊢ N \in ℕ \to 2 \cdot 0 + 1 \neq 0$
98	91 97	reccld	$⊢ N \in ℕ \to \frac{1}{2 \cdot 0 + 1} \in ℂ$
99	87 43	mulcld	$⊢ N \in ℕ \to 2 \cdot N \in ℂ$
100	99 90	addcld	$⊢ N \in ℕ \to 2 \cdot N + 1 \in ℂ$
101	100 59	reccld	$⊢ N \in ℕ \to \frac{1}{2 \cdot N + 1} \in ℂ$
102	95 65	eqeltrrdi	$⊢ N \in ℕ \to 2 \cdot 0 + 1 \in ℕ_{0}$
103	101 102	expcld	$⊢ N \in ℕ \to {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1} \in ℂ$
104	98 103	mulcld	$⊢ N \in ℕ \to (\frac{1}{2 \cdot 0 + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1} \in ℂ$
105	87 104	mulcld	$⊢ N \in ℕ \to 2 (\frac{1}{2 \cdot 0 + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1} \in ℂ$
106	79 86 11 105	fvmptd	$⊢ N \in ℕ \to H (0) = 2 (\frac{1}{2 \cdot 0 + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1}$
107	92	oveq1d	$⊢ N \in ℕ \to 2 \cdot 0 + 1 = 0 + 1$
108	107 6	eqtr4di	$⊢ N \in ℕ \to 2 \cdot 0 + 1 = 1$
109	108	oveq2d	$⊢ N \in ℕ \to \frac{1}{2 \cdot 0 + 1} = \frac{1}{1}$
110	90	div1d	$⊢ N \in ℕ \to \frac{1}{1} = 1$
111	109 110	eqtrd	$⊢ N \in ℕ \to \frac{1}{2 \cdot 0 + 1} = 1$
112	108	oveq2d	$⊢ N \in ℕ \to {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1} = {(\frac{1}{2 \cdot N + 1})}^{1}$
113	101	exp1d	$⊢ N \in ℕ \to {(\frac{1}{2 \cdot N + 1})}^{1} = \frac{1}{2 \cdot N + 1}$
114	112 113	eqtrd	$⊢ N \in ℕ \to {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1} = \frac{1}{2 \cdot N + 1}$
115	111 114	oveq12d	$⊢ N \in ℕ \to (\frac{1}{2 \cdot 0 + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1} = 1 (\frac{1}{2 \cdot N + 1})$
116	101	mullidd	$⊢ N \in ℕ \to 1 (\frac{1}{2 \cdot N + 1}) = \frac{1}{2 \cdot N + 1}$
117	115 116	eqtrd	$⊢ N \in ℕ \to (\frac{1}{2 \cdot 0 + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1} = \frac{1}{2 \cdot N + 1}$
118	117	oveq2d	$⊢ N \in ℕ \to 2 (\frac{1}{2 \cdot 0 + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1} = 2 (\frac{1}{2 \cdot N + 1})$
119	87 90 100 59	divassd	$⊢ N \in ℕ \to \frac{2 \cdot 1}{2 \cdot N + 1} = 2 (\frac{1}{2 \cdot N + 1})$
120	87	mulridd	$⊢ N \in ℕ \to 2 \cdot 1 = 2$
121	120	oveq1d	$⊢ N \in ℕ \to \frac{2 \cdot 1}{2 \cdot N + 1} = \frac{2}{2 \cdot N + 1}$
122	118 119 121	3eqtr2d	$⊢ N \in ℕ \to 2 (\frac{1}{2 \cdot 0 + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 \cdot 0 + 1} = \frac{2}{2 \cdot N + 1}$
123	78 106 122	3eqtrd	$⊢ N \in ℕ \to seq 0 (+ H) (0) = \frac{2}{2 \cdot N + 1}$
124	123	oveq2d	$⊢ N \in ℕ \to \log (\frac{N + 1}{N}) - seq 0 (+ H) (0) = \log (\frac{N + 1}{N}) - (\frac{2}{2 \cdot N + 1})$
125	75 124	breqtrd	$⊢ N \in ℕ \to seq 1 (+ H) ⇝ (\log (\frac{N + 1}{N}) - (\frac{2}{2 \cdot N + 1}))$
126	90 99	addcld	$⊢ N \in ℕ \to 1 + 2 \cdot N \in ℂ$
127	126	halfcld	$⊢ N \in ℕ \to \frac{1 + 2 \cdot N}{2} \in ℂ$
128		seqex	$⊢ seq 1 (+ K) \in V$
129	128	a1i	$⊢ N \in ℕ \to seq 1 (+ K) \in V$
130		elnnuz	$⊢ j \in ℕ \leftrightarrow j \in ℤ_{\geq 1}$
131	130	biimpi	$⊢ j \in ℕ \to j \in ℤ_{\geq 1}$
132	131	adantl	$⊢ (N \in ℕ \land j \in ℕ) \to j \in ℤ_{\geq 1}$
133		oveq2	$⊢ k = n \to 2 k = 2 n$
134	133	oveq1d	$⊢ k = n \to 2 k + 1 = 2 n + 1$
135	134	oveq2d	$⊢ k = n \to \frac{1}{2 k + 1} = \frac{1}{2 n + 1}$
136	134	oveq2d	$⊢ k = n \to {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}$
137	135 136	oveq12d	$⊢ k = n \to (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}$
138	137	oveq2d	$⊢ k = n \to 2 (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = 2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}$
139		elfzuz	$⊢ n \in (1 \dots j) \to n \in ℤ_{\geq 1}$
140		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
141	140	biimpri	$⊢ n \in ℤ_{\geq 1} \to n \in ℕ$
142		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
143	139 141 142	3syl	$⊢ n \in (1 \dots j) \to n \in ℕ_{0}$
144	143	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to n \in ℕ_{0}$
145		2cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \in ℂ$
146	144	nn0cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to n \in ℂ$
147	145 146	mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n \in ℂ$
148		1cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1 \in ℂ$
149	147 148	addcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n + 1 \in ℂ$
150		elfznn	$⊢ n \in (1 \dots j) \to n \in ℕ$
151		0red	$⊢ n \in ℕ \to 0 \in ℝ$
152		1red	$⊢ n \in ℕ \to 1 \in ℝ$
153	27	a1i	$⊢ n \in ℕ \to 2 \in ℝ$
154		nnre	$⊢ n \in ℕ \to n \in ℝ$
155	153 154	remulcld	$⊢ n \in ℕ \to 2 n \in ℝ$
156	155 152	readdcld	$⊢ n \in ℕ \to 2 n + 1 \in ℝ$
157	36	a1i	$⊢ n \in ℕ \to 0 < 1$
158		2rp	$⊢ 2 \in ℝ^{+}$
159	158	a1i	$⊢ n \in ℕ \to 2 \in ℝ^{+}$
160		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
161	159 160	rpmulcld	$⊢ n \in ℕ \to 2 n \in ℝ^{+}$
162	152 161	ltaddrp2d	$⊢ n \in ℕ \to 1 < 2 n + 1$
163	151 152 156 157 162	lttrd	$⊢ n \in ℕ \to 0 < 2 n + 1$
164	163	gt0ne0d	$⊢ n \in ℕ \to 2 n + 1 \neq 0$
165	150 164	syl	$⊢ n \in (1 \dots j) \to 2 n + 1 \neq 0$
166	165	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n + 1 \neq 0$
167	149 166	reccld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{1}{2 n + 1} \in ℂ$
168	101	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{1}{2 \cdot N + 1} \in ℂ$
169	62	a1i	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \in ℕ_{0}$
170	169 144	nn0mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n \in ℕ_{0}$
171	65	a1i	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1 \in ℕ_{0}$
172	170 171	nn0addcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n + 1 \in ℕ_{0}$
173	168 172	expcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} \in ℂ$
174	167 173	mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} \in ℂ$
175	145 174	mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} \in ℂ$
176	3 138 144 175	fvmptd3	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to H (n) = 2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}$
177	176 175	eqeltrd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to H (n) \in ℂ$
178		addcl	$⊢ (n \in ℂ \land i \in ℂ) \to n + i \in ℂ$
179	178	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to n + i \in ℂ$
180	132 177 179	seqcl	$⊢ (N \in ℕ \land j \in ℕ) \to seq 1 (+ H) (j) \in ℂ$
181		1cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to 1 \in ℂ$
182		2cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to 2 \in ℂ$
183	43	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to N \in ℂ$
184	182 183	mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to 2 \cdot N \in ℂ$
185	181 184	addcld	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to 1 + 2 \cdot N \in ℂ$
186	185	halfcld	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to \frac{1 + 2 \cdot N}{2} \in ℂ$
187		simprl	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to n \in ℂ$
188		simprr	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to i \in ℂ$
189	186 187 188	adddid	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to (\frac{1 + 2 \cdot N}{2}) (n + i) = (\frac{1 + 2 \cdot N}{2}) n + (\frac{1 + 2 \cdot N}{2}) i$
190	133	oveq2d	$⊢ k = n \to {(\frac{1}{2 \cdot N + 1})}^{2 k} = {(\frac{1}{2 \cdot N + 1})}^{2 n}$
191	135 190	oveq12d	$⊢ k = n \to (\frac{1}{2 k + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 k} = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n}$
192	150	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to n \in ℕ$
193	168 170	expcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n} \in ℂ$
194	167 193	mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n} \in ℂ$
195	2 191 192 194	fvmptd3	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to K (n) = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n}$
196	126	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1 + 2 \cdot N \in ℂ$
197		2ne0	$⊢ 2 \neq 0$
198	197	a1i	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \neq 0$
199	196 145 175 198	div32d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (\frac{1 + 2 \cdot N}{2}) 2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = (1 + 2 \cdot N) (\frac{2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}}{2})$
200	174 145 198	divcan3d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}}{2} = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}$
201	200	oveq2d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (1 + 2 \cdot N) (\frac{2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}}{2}) = (1 + 2 \cdot N) (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}$
202	196 167 173	mul12d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (1 + 2 \cdot N) (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = (\frac{1}{2 n + 1}) (1 + 2 \cdot N) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}$
203	100	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \cdot N + 1 \in ℂ$
204	59	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \cdot N + 1 \neq 0$
205	172	nn0zd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n + 1 \in ℤ$
206	203 204 205	exprecd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = \frac{1}{{(2 \cdot N + 1)}^{2 n + 1}}$
207	206	oveq2d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (1 + 2 \cdot N) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = (1 + 2 \cdot N) (\frac{1}{{(2 \cdot N + 1)}^{2 n + 1}})$
208	203 172	expcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n + 1} \in ℂ$
209	203 204 205	expne0d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n + 1} \neq 0$
210	196 208 209	divrecd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{1 + 2 \cdot N}{{(2 \cdot N + 1)}^{2 n + 1}} = (1 + 2 \cdot N) (\frac{1}{{(2 \cdot N + 1)}^{2 n + 1}})$
211	43	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to N \in ℂ$
212	145 211	mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \cdot N \in ℂ$
213	148 212	addcomd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1 + 2 \cdot N = 2 \cdot N + 1$
214	203 170	expcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n} \in ℂ$
215	214 203	mulcomd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n} (2 \cdot N + 1) = (2 \cdot N + 1) {(2 \cdot N + 1)}^{2 n}$
216	213 215	oveq12d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{1 + 2 \cdot N}{{(2 \cdot N + 1)}^{2 n} (2 \cdot N + 1)} = \frac{2 \cdot N + 1}{(2 \cdot N + 1) {(2 \cdot N + 1)}^{2 n}}$
217	203 170	expp1d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n + 1} = {(2 \cdot N + 1)}^{2 n} (2 \cdot N + 1)$
218	217	oveq2d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{1 + 2 \cdot N}{{(2 \cdot N + 1)}^{2 n + 1}} = \frac{1 + 2 \cdot N}{{(2 \cdot N + 1)}^{2 n} (2 \cdot N + 1)}$
219		2z	$⊢ 2 \in ℤ$
220	219	a1i	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \in ℤ$
221	144	nn0zd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to n \in ℤ$
222	220 221	zmulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n \in ℤ$
223	203 204 222	expne0d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n} \neq 0$
224	203 203 214 204 223	divdiv1d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{\frac{2 \cdot N + 1}{2 \cdot N + 1}}{{(2 \cdot N + 1)}^{2 n}} = \frac{2 \cdot N + 1}{(2 \cdot N + 1) {(2 \cdot N + 1)}^{2 n}}$
225	216 218 224	3eqtr4d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{1 + 2 \cdot N}{{(2 \cdot N + 1)}^{2 n + 1}} = \frac{\frac{2 \cdot N + 1}{2 \cdot N + 1}}{{(2 \cdot N + 1)}^{2 n}}$
226	207 210 225	3eqtr2d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (1 + 2 \cdot N) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = \frac{\frac{2 \cdot N + 1}{2 \cdot N + 1}}{{(2 \cdot N + 1)}^{2 n}}$
227	226	oveq2d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) (1 + 2 \cdot N) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = (\frac{1}{2 n + 1}) (\frac{\frac{2 \cdot N + 1}{2 \cdot N + 1}}{{(2 \cdot N + 1)}^{2 n}})$
228	203 204	dividd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{2 \cdot N + 1}{2 \cdot N + 1} = 1$
229		1exp	$⊢ 2 n \in ℤ \to 1^{2 n} = 1$
230	222 229	syl	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1^{2 n} = 1$
231	228 230	eqtr4d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{2 \cdot N + 1}{2 \cdot N + 1} = 1^{2 n}$
232	231	oveq1d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{\frac{2 \cdot N + 1}{2 \cdot N + 1}}{{(2 \cdot N + 1)}^{2 n}} = \frac{1^{2 n}}{{(2 \cdot N + 1)}^{2 n}}$
233	148 203 204 170	expdivd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n} = \frac{1^{2 n}}{{(2 \cdot N + 1)}^{2 n}}$
234	232 233	eqtr4d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{\frac{2 \cdot N + 1}{2 \cdot N + 1}}{{(2 \cdot N + 1)}^{2 n}} = {(\frac{1}{2 \cdot N + 1})}^{2 n}$
235	234	oveq2d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (\frac{1}{2 n + 1}) (\frac{\frac{2 \cdot N + 1}{2 \cdot N + 1}}{{(2 \cdot N + 1)}^{2 n}}) = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n}$
236	202 227 235	3eqtrd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (1 + 2 \cdot N) (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n}$
237	199 201 236	3eqtrd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (\frac{1 + 2 \cdot N}{2}) 2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n}$
238	176	eqcomd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = H (n)$
239	238	oveq2d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to (\frac{1 + 2 \cdot N}{2}) 2 (\frac{1}{2 n + 1}) {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} = (\frac{1 + 2 \cdot N}{2}) H (n)$
240	195 237 239	3eqtr2d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to K (n) = (\frac{1 + 2 \cdot N}{2}) H (n)$
241	179 189 132 177 240	seqdistr	$⊢ (N \in ℕ \land j \in ℕ) \to seq 1 (+ K) (j) = (\frac{1 + 2 \cdot N}{2}) seq 1 (+ H) (j)$
242	4 5 125 127 129 180 241	climmulc2	$⊢ N \in ℕ \to seq 1 (+ K) ⇝ (\frac{1 + 2 \cdot N}{2}) (\log (\frac{N + 1}{N}) - (\frac{2}{2 \cdot N + 1}))$
243	90 99	addcomd	$⊢ N \in ℕ \to 1 + 2 \cdot N = 2 \cdot N + 1$
244	243	oveq1d	$⊢ N \in ℕ \to \frac{1 + 2 \cdot N}{2} = \frac{2 \cdot N + 1}{2}$
245	244	oveq1d	$⊢ N \in ℕ \to (\frac{1 + 2 \cdot N}{2}) (\log (\frac{N + 1}{N}) - (\frac{2}{2 \cdot N + 1})) = (\frac{2 \cdot N + 1}{2}) (\log (\frac{N + 1}{N}) - (\frac{2}{2 \cdot N + 1}))$
246	244 127	eqeltrrd	$⊢ N \in ℕ \to \frac{2 \cdot N + 1}{2} \in ℂ$
247	43 90	addcld	$⊢ N \in ℕ \to N + 1 \in ℂ$
248		nnne0	$⊢ N \in ℕ \to N \neq 0$
249	247 43 248	divcld	$⊢ N \in ℕ \to \frac{N + 1}{N} \in ℂ$
250	49 51	readdcld	$⊢ N \in ℕ \to N + 1 \in ℝ$
251	49	ltp1d	$⊢ N \in ℕ \to N < N + 1$
252	53 49 250 54 251	lttrd	$⊢ N \in ℕ \to 0 < N + 1$
253	252	gt0ne0d	$⊢ N \in ℕ \to N + 1 \neq 0$
254	247 43 253 248	divne0d	$⊢ N \in ℕ \to \frac{N + 1}{N} \neq 0$
255	249 254	logcld	$⊢ N \in ℕ \to \log (\frac{N + 1}{N}) \in ℂ$
256	87 100 59	divcld	$⊢ N \in ℕ \to \frac{2}{2 \cdot N + 1} \in ℂ$
257	246 255 256	subdid	$⊢ N \in ℕ \to (\frac{2 \cdot N + 1}{2}) (\log (\frac{N + 1}{N}) - (\frac{2}{2 \cdot N + 1})) = (\frac{2 \cdot N + 1}{2}) \log (\frac{N + 1}{N}) - (\frac{2 \cdot N + 1}{2}) (\frac{2}{2 \cdot N + 1})$
258	99 90	addcomd	$⊢ N \in ℕ \to 2 \cdot N + 1 = 1 + 2 \cdot N$
259	258	oveq1d	$⊢ N \in ℕ \to \frac{2 \cdot N + 1}{2} = \frac{1 + 2 \cdot N}{2}$
260	259	oveq1d	$⊢ N \in ℕ \to (\frac{2 \cdot N + 1}{2}) \log (\frac{N + 1}{N}) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N})$
261	197	a1i	$⊢ N \in ℕ \to 2 \neq 0$
262	100 87 59 261	divcan6d	$⊢ N \in ℕ \to (\frac{2 \cdot N + 1}{2}) (\frac{2}{2 \cdot N + 1}) = 1$
263	260 262	oveq12d	$⊢ N \in ℕ \to (\frac{2 \cdot N + 1}{2}) \log (\frac{N + 1}{N}) - (\frac{2 \cdot N + 1}{2}) (\frac{2}{2 \cdot N + 1}) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
264	245 257 263	3eqtrd	$⊢ N \in ℕ \to (\frac{1 + 2 \cdot N}{2}) (\log (\frac{N + 1}{N}) - (\frac{2}{2 \cdot N + 1})) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
265	242 264	breqtrd	$⊢ N \in ℕ \to seq 1 (+ K) ⇝ ((\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1)$
266		oveq2	$⊢ n = N \to 2 n = 2 \cdot N$
267	266	oveq2d	$⊢ n = N \to 1 + 2 n = 1 + 2 \cdot N$
268	267	oveq1d	$⊢ n = N \to \frac{1 + 2 n}{2} = \frac{1 + 2 \cdot N}{2}$
269		oveq1	$⊢ n = N \to n + 1 = N + 1$
270		id	$⊢ n = N \to n = N$
271	269 270	oveq12d	$⊢ n = N \to \frac{n + 1}{n} = \frac{N + 1}{N}$
272	271	fveq2d	$⊢ n = N \to \log (\frac{n + 1}{n}) = \log (\frac{N + 1}{N})$
273	268 272	oveq12d	$⊢ n = N \to (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N})$
274	273	oveq1d	$⊢ n = N \to (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) - 1 = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
275		id	$⊢ N \in ℕ \to N \in ℕ$
276	127 255	mulcld	$⊢ N \in ℕ \to (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) \in ℂ$
277	276 90	subcld	$⊢ N \in ℕ \to (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ$
278	1 274 275 277	fvmptd3	$⊢ N \in ℕ \to J (N) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
279	265 278	breqtrrd	$⊢ N \in ℕ \to seq 1 (+ K) ⇝ J (N)$

Metamath Proof Explorer

Theorem stirlinglem7

Proof