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	bilani	$⊢ (N \in ℕ \land j \in ℕ) \to j \in ℤ_{\geq 1}$
132		oveq2	$⊢ k = n \to 2 k = 2 n$
133	132	oveq1d	$⊢ k = n \to 2 k + 1 = 2 n + 1$
134	133	oveq2d	$⊢ k = n \to \frac{1}{2 k + 1} = \frac{1}{2 n + 1}$
135	133	oveq2d	$⊢ k = n \to {(\frac{1}{2 \cdot N + 1})}^{2 k + 1} = {(\frac{1}{2 \cdot N + 1})}^{2 n + 1}$
136	134 135	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}$
137	136	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}$
138		elfzuz	$⊢ n \in (1 \dots j) \to n \in ℤ_{\geq 1}$
139		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
140	139	biimpri	$⊢ n \in ℤ_{\geq 1} \to n \in ℕ$
141		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
142	138 140 141	3syl	$⊢ n \in (1 \dots j) \to n \in ℕ_{0}$
143	142	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to n \in ℕ_{0}$
144		2cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \in ℂ$
145	143	nn0cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to n \in ℂ$
146	144 145	mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n \in ℂ$
147		1cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1 \in ℂ$
148	146 147	addcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n + 1 \in ℂ$
149		elfznn	$⊢ n \in (1 \dots j) \to n \in ℕ$
150		0red	$⊢ n \in ℕ \to 0 \in ℝ$
151		1red	$⊢ n \in ℕ \to 1 \in ℝ$
152	27	a1i	$⊢ n \in ℕ \to 2 \in ℝ$
153		nnre	$⊢ n \in ℕ \to n \in ℝ$
154	152 153	remulcld	$⊢ n \in ℕ \to 2 n \in ℝ$
155	154 151	readdcld	$⊢ n \in ℕ \to 2 n + 1 \in ℝ$
156	36	a1i	$⊢ n \in ℕ \to 0 < 1$
157		2rp	$⊢ 2 \in ℝ^{+}$
158	157	a1i	$⊢ n \in ℕ \to 2 \in ℝ^{+}$
159		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
160	158 159	rpmulcld	$⊢ n \in ℕ \to 2 n \in ℝ^{+}$
161	151 160	ltaddrp2d	$⊢ n \in ℕ \to 1 < 2 n + 1$
162	150 151 155 156 161	lttrd	$⊢ n \in ℕ \to 0 < 2 n + 1$
163	162	gt0ne0d	$⊢ n \in ℕ \to 2 n + 1 \neq 0$
164	149 163	syl	$⊢ n \in (1 \dots j) \to 2 n + 1 \neq 0$
165	164	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n + 1 \neq 0$
166	148 165	reccld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{1}{2 n + 1} \in ℂ$
167	101	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{1}{2 \cdot N + 1} \in ℂ$
168	62	a1i	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \in ℕ_{0}$
169	168 143	nn0mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n \in ℕ_{0}$
170	65	a1i	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1 \in ℕ_{0}$
171	169 170	nn0addcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n + 1 \in ℕ_{0}$
172	167 171	expcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n + 1} \in ℂ$
173	166 172	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 ℂ$
174	144 173	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 ℂ$
175	3 137 143 174	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}$
176	175 174	eqeltrd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to H (n) \in ℂ$
177		addcl	$⊢ (n \in ℂ \land i \in ℂ) \to n + i \in ℂ$
178	177	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to n + i \in ℂ$
179	131 176 178	seqcl	$⊢ (N \in ℕ \land j \in ℕ) \to seq 1 (+ H) (j) \in ℂ$
180		1cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to 1 \in ℂ$
181		2cnd	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to 2 \in ℂ$
182	43	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to N \in ℂ$
183	181 182	mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to 2 \cdot N \in ℂ$
184	180 183	addcld	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to 1 + 2 \cdot N \in ℂ$
185	184	halfcld	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to \frac{1 + 2 \cdot N}{2} \in ℂ$
186		simprl	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to n \in ℂ$
187		simprr	$⊢ ((N \in ℕ \land j \in ℕ) \land (n \in ℂ \land i \in ℂ)) \to i \in ℂ$
188	185 186 187	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$
189	132	oveq2d	$⊢ k = n \to {(\frac{1}{2 \cdot N + 1})}^{2 k} = {(\frac{1}{2 \cdot N + 1})}^{2 n}$
190	134 189	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}$
191	149	adantl	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to n \in ℕ$
192	167 169	expcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(\frac{1}{2 \cdot N + 1})}^{2 n} \in ℂ$
193	166 192	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 ℂ$
194	2 190 191 193	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}$
195	126	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1 + 2 \cdot N \in ℂ$
196		2ne0	$⊢ 2 \neq 0$
197	196	a1i	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \neq 0$
198	195 144 174 197	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})$
199	173 144 197	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}$
200	199	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}$
201	195 166 172	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}$
202	100	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \cdot N + 1 \in ℂ$
203	59	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \cdot N + 1 \neq 0$
204	171	nn0zd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n + 1 \in ℤ$
205	202 203 204	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}}$
206	205	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}})$
207	202 171	expcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n + 1} \in ℂ$
208	202 203 204	expne0d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n + 1} \neq 0$
209	195 207 208	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}})$
210	43	ad2antrr	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to N \in ℂ$
211	144 210	mulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \cdot N \in ℂ$
212	147 211	addcomd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1 + 2 \cdot N = 2 \cdot N + 1$
213	202 169	expcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n} \in ℂ$
214	213 202	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}$
215	212 214	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}}$
216	202 169	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)$
217	216	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)}$
218		2z	$⊢ 2 \in ℤ$
219	218	a1i	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 \in ℤ$
220	143	nn0zd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to n \in ℤ$
221	219 220	zmulcld	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 2 n \in ℤ$
222	202 203 221	expne0d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to {(2 \cdot N + 1)}^{2 n} \neq 0$
223	202 202 213 203 222	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}}$
224	215 217 223	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}}$
225	206 209 224	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}}$
226	225	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}})$
227	202 203	dividd	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{2 \cdot N + 1}{2 \cdot N + 1} = 1$
228		1exp	$⊢ 2 n \in ℤ \to 1^{2 n} = 1$
229	221 228	syl	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to 1^{2 n} = 1$
230	227 229	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}$
231	230	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}}$
232	147 202 203 169	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}}$
233	231 232	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}$
234	233	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}$
235	201 226 234	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}$
236	198 200 235	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}$
237	175	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)$
238	237	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)$
239	194 236 238	3eqtr2d	$⊢ ((N \in ℕ \land j \in ℕ) \land n \in (1 \dots j)) \to K (n) = (\frac{1 + 2 \cdot N}{2}) H (n)$
240	178 188 131 176 239	seqdistr	$⊢ (N \in ℕ \land j \in ℕ) \to seq 1 (+ K) (j) = (\frac{1 + 2 \cdot N}{2}) seq 1 (+ H) (j)$
241	4 5 125 127 129 179 240	climmulc2	$⊢ N \in ℕ \to seq 1 (+ K) ⇝ (\frac{1 + 2 \cdot N}{2}) (\log (\frac{N + 1}{N}) - (\frac{2}{2 \cdot N + 1}))$
242	90 99	addcomd	$⊢ N \in ℕ \to 1 + 2 \cdot N = 2 \cdot N + 1$
243	242	oveq1d	$⊢ N \in ℕ \to \frac{1 + 2 \cdot N}{2} = \frac{2 \cdot N + 1}{2}$
244	243	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}))$
245	243 127	eqeltrrd	$⊢ N \in ℕ \to \frac{2 \cdot N + 1}{2} \in ℂ$
246	43 90	addcld	$⊢ N \in ℕ \to N + 1 \in ℂ$
247		nnne0	$⊢ N \in ℕ \to N \neq 0$
248	246 43 247	divcld	$⊢ N \in ℕ \to \frac{N + 1}{N} \in ℂ$
249	49 51	readdcld	$⊢ N \in ℕ \to N + 1 \in ℝ$
250	49	ltp1d	$⊢ N \in ℕ \to N < N + 1$
251	53 49 249 54 250	lttrd	$⊢ N \in ℕ \to 0 < N + 1$
252	251	gt0ne0d	$⊢ N \in ℕ \to N + 1 \neq 0$
253	246 43 252 247	divne0d	$⊢ N \in ℕ \to \frac{N + 1}{N} \neq 0$
254	248 253	logcld	$⊢ N \in ℕ \to \log (\frac{N + 1}{N}) \in ℂ$
255	87 100 59	divcld	$⊢ N \in ℕ \to \frac{2}{2 \cdot N + 1} \in ℂ$
256	245 254 255	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})$
257	99 90	addcomd	$⊢ N \in ℕ \to 2 \cdot N + 1 = 1 + 2 \cdot N$
258	257	oveq1d	$⊢ N \in ℕ \to \frac{2 \cdot N + 1}{2} = \frac{1 + 2 \cdot N}{2}$
259	258	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})$
260	196	a1i	$⊢ N \in ℕ \to 2 \neq 0$
261	100 87 59 260	divcan6d	$⊢ N \in ℕ \to (\frac{2 \cdot N + 1}{2}) (\frac{2}{2 \cdot N + 1}) = 1$
262	259 261	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$
263	244 256 262	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$
264	241 263	breqtrd	$⊢ N \in ℕ \to seq 1 (+ K) ⇝ ((\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1)$
265		oveq2	$⊢ n = N \to 2 n = 2 \cdot N$
266	265	oveq2d	$⊢ n = N \to 1 + 2 n = 1 + 2 \cdot N$
267	266	oveq1d	$⊢ n = N \to \frac{1 + 2 n}{2} = \frac{1 + 2 \cdot N}{2}$
268		oveq1	$⊢ n = N \to n + 1 = N + 1$
269		id	$⊢ n = N \to n = N$
270	268 269	oveq12d	$⊢ n = N \to \frac{n + 1}{n} = \frac{N + 1}{N}$
271	270	fveq2d	$⊢ n = N \to \log (\frac{n + 1}{n}) = \log (\frac{N + 1}{N})$
272	267 271	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})$
273	272	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$
274		id	$⊢ N \in ℕ \to N \in ℕ$
275	127 254	mulcld	$⊢ N \in ℕ \to (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) \in ℂ$
276	275 90	subcld	$⊢ N \in ℕ \to (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ$
277	1 273 274 276	fvmptd3	$⊢ N \in ℕ \to J (N) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
278	264 277	breqtrrd	$⊢ N \in ℕ \to seq 1 (+ K) ⇝ J (N)$

Metamath Proof Explorer

Theorem stirlinglem7

Proof