stirlinglem4 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > stirlinglem4		Structured version Visualization version GIF version

Theorem stirlinglem4 40294

Description: Algebraic manipulation of ((𝐵 n ) - ( B (𝑛 + 1))). It will be used in other theorems to show that 𝐵 is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

**Hypotheses**
Ref	Expression
stirlinglem4.1	⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
stirlinglem4.2	⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))
stirlinglem4.3	⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))

**Assertion**
Ref	Expression
stirlinglem4	⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) = (𝐽‘𝑁))

Distinct variable group: 𝑛,𝑁 Allowed substitution hints: 𝐴(𝑛) 𝐵(𝑛) 𝐽(𝑛)

Proof of Theorem stirlinglem4 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnre 11027	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		nnnn0 11299	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
3	2	nn0ge0d 11354	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 0 ≤ 𝑁)
4	1, 3	ge0p1rpd 11902	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ⁺)
5		nnrp 11842	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
6	4, 5	rpdivcld 11889	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℝ⁺)
7	6	rpsqrtcld 14150	. . . . 5 ⊢ (𝑁 ∈ ℕ → (√‘((𝑁 + 1) / 𝑁)) ∈ ℝ⁺)
8		nnz 11399	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
9	6, 8	rpexpcld 13032	. . . . 5 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 𝑁)↑𝑁) ∈ ℝ⁺)
10	7, 9	rpmulcld 11888	. . . 4 ⊢ (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) ∈ ℝ⁺)
11		epr 14936	. . . . 5 ⊢ e ∈ ℝ⁺
12	11	a1i 11	. . . 4 ⊢ (𝑁 ∈ ℕ → e ∈ ℝ⁺)
13	10, 12	relogdivd 24372	. . 3 ⊢ (𝑁 ∈ ℕ → (log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)) = ((log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) − (log‘e)))
14	7, 9	relogmuld 24371	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) = ((log‘(√‘((𝑁 + 1) / 𝑁))) + (log‘(((𝑁 + 1) / 𝑁)↑𝑁))))
15		logsqrt 24450	. . . . . . . 8 ⊢ (((𝑁 + 1) / 𝑁) ∈ ℝ⁺ → (log‘(√‘((𝑁 + 1) / 𝑁))) = ((log‘((𝑁 + 1) / 𝑁)) / 2))
16	6, 15	syl 17	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (log‘(√‘((𝑁 + 1) / 𝑁))) = ((log‘((𝑁 + 1) / 𝑁)) / 2))
17		relogexp 24342	. . . . . . . 8 ⊢ ((((𝑁 + 1) / 𝑁) ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ) → (log‘(((𝑁 + 1) / 𝑁)↑𝑁)) = (𝑁 · (log‘((𝑁 + 1) / 𝑁))))
18	6, 8, 17	syl2anc 693	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (log‘(((𝑁 + 1) / 𝑁)↑𝑁)) = (𝑁 · (log‘((𝑁 + 1) / 𝑁))))
19	16, 18	oveq12d 6668	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((log‘(√‘((𝑁 + 1) / 𝑁))) + (log‘(((𝑁 + 1) / 𝑁)↑𝑁))) = (((log‘((𝑁 + 1) / 𝑁)) / 2) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))))
20	14, 19	eqtrd 2656	. . . . 5 ⊢ (𝑁 ∈ ℕ → (log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) = (((log‘((𝑁 + 1) / 𝑁)) / 2) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))))
21		peano2nn 11032	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
22	21	nncnd 11036	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
23		nncn 11028	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
24		nnne0 11053	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
25	22, 23, 24	divcld 10801	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
26	21	nnne0d 11065	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0)
27	22, 23, 26, 24	divne0d 10817	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ≠ 0)
28	25, 27	logcld 24317	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (log‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
29		2cnd 11093	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℂ)
30		2rp 11837	. . . . . . . . 9 ⊢ 2 ∈ ℝ⁺
31	30	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℝ⁺)
32	31	rpne0d 11877	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 2 ≠ 0)
33	28, 29, 32	divrec2d 10805	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((log‘((𝑁 + 1) / 𝑁)) / 2) = ((1 / 2) · (log‘((𝑁 + 1) / 𝑁))))
34	33	oveq1d 6665	. . . . 5 ⊢ (𝑁 ∈ ℕ → (((log‘((𝑁 + 1) / 𝑁)) / 2) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))) = (((1 / 2) · (log‘((𝑁 + 1) / 𝑁))) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))))
35		1cnd 10056	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
36	35	halfcld 11277	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (1 / 2) ∈ ℂ)
37	36, 23, 28	adddird 10065	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (((1 / 2) + 𝑁) · (log‘((𝑁 + 1) / 𝑁))) = (((1 / 2) · (log‘((𝑁 + 1) / 𝑁))) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))))
38	23, 29, 32	divcan4d 10807	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 · 2) / 2) = 𝑁)
39	23, 29	mulcomd 10061	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 · 2) = (2 · 𝑁))
40	39	oveq1d 6665	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 · 2) / 2) = ((2 · 𝑁) / 2))
41	38, 40	eqtr3d 2658	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 = ((2 · 𝑁) / 2))
42	41	oveq2d 6666	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((1 / 2) + 𝑁) = ((1 / 2) + ((2 · 𝑁) / 2)))
43	29, 23	mulcld 10060	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
44	35, 43, 29, 32	divdird 10839	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) = ((1 / 2) + ((2 · 𝑁) / 2)))
45	42, 44	eqtr4d 2659	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((1 / 2) + 𝑁) = ((1 + (2 · 𝑁)) / 2))
46	45	oveq1d 6665	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (((1 / 2) + 𝑁) · (log‘((𝑁 + 1) / 𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
47	37, 46	eqtr3d 2658	. . . . 5 ⊢ (𝑁 ∈ ℕ → (((1 / 2) · (log‘((𝑁 + 1) / 𝑁))) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
48	20, 34, 47	3eqtrd 2660	. . . 4 ⊢ (𝑁 ∈ ℕ → (log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
49		loge 24333	. . . . 5 ⊢ (log‘e) = 1
50	49	a1i 11	. . . 4 ⊢ (𝑁 ∈ ℕ → (log‘e) = 1)
51	48, 50	oveq12d 6668	. . 3 ⊢ (𝑁 ∈ ℕ → ((log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) − (log‘e)) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
52	13, 51	eqtrd 2656	. 2 ⊢ (𝑁 ∈ ℕ → (log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
53		stirlinglem4.1	. . . . . . 7 ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
54	53	stirlinglem2 40292	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝐴‘𝑁) ∈ ℝ⁺)
55	54	relogcld 24369	. . . . 5 ⊢ (𝑁 ∈ ℕ → (log‘(𝐴‘𝑁)) ∈ ℝ)
56		nfcv 2764	. . . . . 6 ⊢ Ⅎ𝑛𝑁
57		nfcv 2764	. . . . . . 7 ⊢ Ⅎ𝑛log
58		nfmpt1 4747	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
59	53, 58	nfcxfr 2762	. . . . . . . 8 ⊢ Ⅎ𝑛𝐴
60	59, 56	nffv 6198	. . . . . . 7 ⊢ Ⅎ𝑛(𝐴‘𝑁)
61	57, 60	nffv 6198	. . . . . 6 ⊢ Ⅎ𝑛(log‘(𝐴‘𝑁))
62		fveq2 6191	. . . . . . 7 ⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁))
63	62	fveq2d 6195	. . . . . 6 ⊢ (𝑛 = 𝑁 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑁)))
64		stirlinglem4.2	. . . . . 6 ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))
65	56, 61, 63, 64	fvmptf 6301	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (log‘(𝐴‘𝑁)) ∈ ℝ) → (𝐵‘𝑁) = (log‘(𝐴‘𝑁)))
66	55, 65	mpdan 702	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) = (log‘(𝐴‘𝑁)))
67		nfcv 2764	. . . . . . . 8 ⊢ Ⅎ𝑘(log‘(𝐴‘𝑛))
68		nfcv 2764	. . . . . . . . . 10 ⊢ Ⅎ𝑛𝑘
69	59, 68	nffv 6198	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝐴‘𝑘)
70	57, 69	nffv 6198	. . . . . . . 8 ⊢ Ⅎ𝑛(log‘(𝐴‘𝑘))
71		fveq2 6191	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
72	71	fveq2d 6195	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑘)))
73	67, 70, 72	cbvmpt 4749	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛))) = (𝑘 ∈ ℕ ↦ (log‘(𝐴‘𝑘)))
74	64, 73	eqtri 2644	. . . . . 6 ⊢ 𝐵 = (𝑘 ∈ ℕ ↦ (log‘(𝐴‘𝑘)))
75	74	a1i 11	. . . . 5 ⊢ (𝑁 ∈ ℕ → 𝐵 = (𝑘 ∈ ℕ ↦ (log‘(𝐴‘𝑘))))
76		simpr 477	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → 𝑘 = (𝑁 + 1))
77	76	fveq2d 6195	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (𝐴‘𝑘) = (𝐴‘(𝑁 + 1)))
78	77	fveq2d 6195	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (log‘(𝐴‘𝑘)) = (log‘(𝐴‘(𝑁 + 1))))
79	53	stirlinglem2 40292	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ ℕ → (𝐴‘(𝑁 + 1)) ∈ ℝ⁺)
80	21, 79	syl 17	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝐴‘(𝑁 + 1)) ∈ ℝ⁺)
81	80	relogcld 24369	. . . . 5 ⊢ (𝑁 ∈ ℕ → (log‘(𝐴‘(𝑁 + 1))) ∈ ℝ)
82	75, 78, 21, 81	fvmptd 6288	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) = (log‘(𝐴‘(𝑁 + 1))))
83	66, 82	oveq12d 6668	. . 3 ⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) = ((log‘(𝐴‘𝑁)) − (log‘(𝐴‘(𝑁 + 1)))))
84	54, 80	relogdivd 24372	. . 3 ⊢ (𝑁 ∈ ℕ → (log‘((𝐴‘𝑁) / (𝐴‘(𝑁 + 1)))) = ((log‘(𝐴‘𝑁)) − (log‘(𝐴‘(𝑁 + 1)))))
85		faccl 13070	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (!‘𝑁) ∈ ℕ)
86		nnrp 11842	. . . . . . . . 9 ⊢ ((!‘𝑁) ∈ ℕ → (!‘𝑁) ∈ ℝ⁺)
87	2, 85, 86	3syl 18	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) ∈ ℝ⁺)
88	31, 5	rpmulcld 11888	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ⁺)
89	88	rpsqrtcld 14150	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (√‘(2 · 𝑁)) ∈ ℝ⁺)
90	5, 12	rpdivcld 11889	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 / e) ∈ ℝ⁺)
91	90, 8	rpexpcld 13032	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) ∈ ℝ⁺)
92	89, 91	rpmulcld 11888	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ∈ ℝ⁺)
93	87, 92	rpdivcld 11889	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺)
94	53	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))))
95		simpr 477	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁)
96	95	fveq2d 6195	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) ∧ 𝑛 = 𝑁) → (!‘𝑛) = (!‘𝑁))
97	95	oveq2d 6666	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) ∧ 𝑛 = 𝑁) → (2 · 𝑛) = (2 · 𝑁))
98	97	fveq2d 6195	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) ∧ 𝑛 = 𝑁) → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
99	95	oveq1d 6665	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) ∧ 𝑛 = 𝑁) → (𝑛 / e) = (𝑁 / e))
100	99, 95	oveq12d 6668	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) ∧ 𝑛 = 𝑁) → ((𝑛 / e)↑𝑛) = ((𝑁 / e)↑𝑁))
101	98, 100	oveq12d 6668	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) ∧ 𝑛 = 𝑁) → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)))
102	96, 101	oveq12d 6668	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) ∧ 𝑛 = 𝑁) → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
103		simpl 473	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → 𝑁 ∈ ℕ)
104	87	rpcnd 11874	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) ∈ ℂ)
105	104	adantr 481	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → (!‘𝑁) ∈ ℂ)
106		2cnd 11093	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → 2 ∈ ℂ)
107	103	nncnd 11036	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → 𝑁 ∈ ℂ)
108	106, 107	mulcld 10060	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → (2 · 𝑁) ∈ ℂ)
109	108	sqrtcld 14176	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → (√‘(2 · 𝑁)) ∈ ℂ)
110		ere 14819	. . . . . . . . . . . . . 14 ⊢ e ∈ ℝ
111	110	recni 10052	. . . . . . . . . . . . 13 ⊢ e ∈ ℂ
112	111	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → e ∈ ℂ)
113		0re 10040	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
114		epos 14935	. . . . . . . . . . . . . 14 ⊢ 0 < e
115	113, 114	gtneii 10149	. . . . . . . . . . . . 13 ⊢ e ≠ 0
116	115	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → e ≠ 0)
117	107, 112, 116	divcld 10801	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → (𝑁 / e) ∈ ℂ)
118	103	nnnn0d 11351	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → 𝑁 ∈ ℕ₀)
119	117, 118	expcld 13008	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → ((𝑁 / e)↑𝑁) ∈ ℂ)
120	109, 119	mulcld 10060	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ∈ ℂ)
121	89	rpne0d 11877	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (√‘(2 · 𝑁)) ≠ 0)
122	121	adantr 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → (√‘(2 · 𝑁)) ≠ 0)
123	103	nnne0d 11065	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → 𝑁 ≠ 0)
124	107, 112, 123, 116	divne0d 10817	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → (𝑁 / e) ≠ 0)
125	103	nnzd 11481	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → 𝑁 ∈ ℤ)
126	117, 124, 125	expne0d 13014	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → ((𝑁 / e)↑𝑁) ≠ 0)
127	109, 119, 122, 126	mulne0d 10679	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ≠ 0)
128	105, 120, 127	divcld 10801	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℂ)
129	94, 102, 103, 128	fvmptd 6288	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ⁺) → (𝐴‘𝑁) = ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
130	93, 129	mpdan 702	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝐴‘𝑁) = ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
131		nfcv 2764	. . . . . . . . . 10 ⊢ Ⅎ𝑘((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))
132		nfcv 2764	. . . . . . . . . 10 ⊢ Ⅎ𝑛((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)))
133		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘))
134		oveq2 6658	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘))
135	134	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑘)))
136		oveq1 6657	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (𝑛 / e) = (𝑘 / e))
137		id 22	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
138	136, 137	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → ((𝑛 / e)↑𝑛) = ((𝑘 / e)↑𝑘))
139	135, 138	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)))
140	133, 139	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))))
141	131, 132, 140	cbvmpt 4749	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) = (𝑘 ∈ ℕ ↦ ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))))
142	53, 141	eqtri 2644	. . . . . . . 8 ⊢ 𝐴 = (𝑘 ∈ ℕ ↦ ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))))
143	142	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝐴 = (𝑘 ∈ ℕ ↦ ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)))))
144	76	fveq2d 6195	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (!‘𝑘) = (!‘(𝑁 + 1)))
145	76	oveq2d 6666	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (2 · 𝑘) = (2 · (𝑁 + 1)))
146	145	fveq2d 6195	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (√‘(2 · 𝑘)) = (√‘(2 · (𝑁 + 1))))
147	76	oveq1d 6665	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (𝑘 / e) = ((𝑁 + 1) / e))
148	147, 76	oveq12d 6668	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → ((𝑘 / e)↑𝑘) = (((𝑁 + 1) / e)↑(𝑁 + 1)))
149	146, 148	oveq12d 6668	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)) = ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
150	144, 149	oveq12d 6668	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))) = ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))
151	21	nnnn0d 11351	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ₀)
152		faccl 13070	. . . . . . . . 9 ⊢ ((𝑁 + 1) ∈ ℕ₀ → (!‘(𝑁 + 1)) ∈ ℕ)
153		nnrp 11842	. . . . . . . . 9 ⊢ ((!‘(𝑁 + 1)) ∈ ℕ → (!‘(𝑁 + 1)) ∈ ℝ⁺)
154	151, 152, 153	3syl 18	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (!‘(𝑁 + 1)) ∈ ℝ⁺)
155	31, 4	rpmulcld 11888	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (2 · (𝑁 + 1)) ∈ ℝ⁺)
156	155	rpsqrtcld 14150	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (√‘(2 · (𝑁 + 1))) ∈ ℝ⁺)
157	4, 12	rpdivcld 11889	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / e) ∈ ℝ⁺)
158	8	peano2zd 11485	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℤ)
159	157, 158	rpexpcld 13032	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / e)↑(𝑁 + 1)) ∈ ℝ⁺)
160	156, 159	rpmulcld 11888	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ∈ ℝ⁺)
161	154, 160	rpdivcld 11889	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) ∈ ℝ⁺)
162	143, 150, 21, 161	fvmptd 6288	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝐴‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))
163	130, 162	oveq12d 6668	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((𝐴‘𝑁) / (𝐴‘(𝑁 + 1))) = (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
164		facp1 13065	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1)))
165	2, 164	syl 17	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1)))
166	165	oveq1d 6665	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) = (((!‘𝑁) · (𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))
167	160	rpcnd 11874	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ∈ ℂ)
168	160	rpne0d 11877	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ≠ 0)
169	104, 22, 167, 168	divassd 10836	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (((!‘𝑁) · (𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) = ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
170	166, 169	eqtrd 2656	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) = ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
171	170	oveq2d 6666	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))))
172	92	rpcnd 11874	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ∈ ℂ)
173	22, 167, 168	divcld 10801	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) ∈ ℂ)
174	104, 173	mulcld 10060	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) ∈ ℂ)
175	92	rpne0d 11877	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ≠ 0)
176	87	rpne0d 11877	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) ≠ 0)
177	22, 167, 26, 168	divne0d 10817	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) ≠ 0)
178	104, 173, 176, 177	mulne0d 10679	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) ≠ 0)
179	104, 172, 174, 175, 178	divdiv32d 10826	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) = (((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
180	104, 104, 173, 176, 177	divdiv1d 10832	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = ((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))))
181	180	eqcomd 2628	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) = (((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
182	181	oveq1d 6665	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
183	104, 176	dividd 10799	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((!‘𝑁) / (!‘𝑁)) = 1)
184	183	oveq1d 6665	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = (1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
185	184	oveq1d 6665	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
186	22, 167, 26, 168	recdivd 10818	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = (((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)))
187	186	oveq1d 6665	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
188	167, 22, 26	divcld 10801	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) ∈ ℂ)
189	89	rpcnd 11874	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (√‘(2 · 𝑁)) ∈ ℂ)
190	91	rpcnd 11874	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) ∈ ℂ)
191	91	rpne0d 11877	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) ≠ 0)
192	188, 189, 190, 121, 191	divdiv1d 10832	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) / ((𝑁 / e)↑𝑁)) = ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
193	167, 22, 189, 26, 121	divdiv32d 10826	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) = ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) / (𝑁 + 1)))
194	156	rpcnd 11874	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (√‘(2 · (𝑁 + 1))) ∈ ℂ)
195	159	rpcnd 11874	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / e)↑(𝑁 + 1)) ∈ ℂ)
196	194, 195, 189, 121	div23d 10838	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) = (((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
197	31	rpred 11872	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℝ)
198	31	rpge0d 11876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 0 ≤ 2)
199	21	nnred 11035	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
200	151	nn0ge0d 11354	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 0 ≤ (𝑁 + 1))
201	197, 198, 199, 200	sqrtmuld 14163	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (√‘(2 · (𝑁 + 1))) = ((√‘2) · (√‘(𝑁 + 1))))
202	197, 198, 1, 3	sqrtmuld 14163	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
203	201, 202	oveq12d 6668	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) = (((√‘2) · (√‘(𝑁 + 1))) / ((√‘2) · (√‘𝑁))))
204	29	sqrtcld 14176	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (√‘2) ∈ ℂ)
205	22	sqrtcld 14176	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (√‘(𝑁 + 1)) ∈ ℂ)
206	23	sqrtcld 14176	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (√‘𝑁) ∈ ℂ)
207	31	rpsqrtcld 14150	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (√‘2) ∈ ℝ⁺)
208	207	rpne0d 11877	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (√‘2) ≠ 0)
209	5	rpsqrtcld 14150	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (√‘𝑁) ∈ ℝ⁺)
210	209	rpne0d 11877	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (√‘𝑁) ≠ 0)
211	204, 204, 205, 206, 208, 210	divmuldivd 10842	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (((√‘2) / (√‘2)) · ((√‘(𝑁 + 1)) / (√‘𝑁))) = (((√‘2) · (√‘(𝑁 + 1))) / ((√‘2) · (√‘𝑁))))
212	204, 208	dividd 10799	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((√‘2) / (√‘2)) = 1)
213	199, 200, 5	sqrtdivd 14162	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (√‘((𝑁 + 1) / 𝑁)) = ((√‘(𝑁 + 1)) / (√‘𝑁)))
214	213	eqcomd 2628	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((√‘(𝑁 + 1)) / (√‘𝑁)) = (√‘((𝑁 + 1) / 𝑁)))
215	212, 214	oveq12d 6668	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (((√‘2) / (√‘2)) · ((√‘(𝑁 + 1)) / (√‘𝑁))) = (1 · (√‘((𝑁 + 1) / 𝑁))))
216	203, 211, 215	3eqtr2d 2662	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) = (1 · (√‘((𝑁 + 1) / 𝑁))))
217	216	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) = ((1 · (√‘((𝑁 + 1) / 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
218	25	sqrtcld 14176	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (√‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
219	218	mulid2d 10058	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (1 · (√‘((𝑁 + 1) / 𝑁))) = (√‘((𝑁 + 1) / 𝑁)))
220	219	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → ((1 · (√‘((𝑁 + 1) / 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
221	196, 217, 220	3eqtrd 2660	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
222	221	oveq1d 6665	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) / (𝑁 + 1)) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)))
223	193, 222	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)))
224	223	oveq1d 6665	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) / ((𝑁 / e)↑𝑁)) = ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)))
225	192, 224	eqtr3d 2658	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)))
226	218, 195	mulcld 10060	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ∈ ℂ)
227	226, 22, 190, 26, 191	divdiv32d 10826	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)) = ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) / (𝑁 + 1)))
228	218, 195, 190, 191	divassd 10836	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) = ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1) / e)↑(𝑁 + 1)) / ((𝑁 / e)↑𝑁))))
229	12	rpcnd 11874	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → e ∈ ℂ)
230	12	rpne0d 11877	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → e ≠ 0)
231	22, 229, 230, 151	expdivd 13022	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / e)↑(𝑁 + 1)) = (((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))))
232	23, 229, 230, 2	expdivd 13022	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) = ((𝑁↑𝑁) / (e↑𝑁)))
233	231, 232	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) / e)↑(𝑁 + 1)) / ((𝑁 / e)↑𝑁)) = ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁))))
234	233	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1) / e)↑(𝑁 + 1)) / ((𝑁 / e)↑𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁)))))
235	22, 151	expcld 13008	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1)↑(𝑁 + 1)) ∈ ℂ)
236	229, 151	expcld 13008	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (e↑(𝑁 + 1)) ∈ ℂ)
237	23, 2	expcld 13008	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (𝑁↑𝑁) ∈ ℂ)
238	229, 2	expcld 13008	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (e↑𝑁) ∈ ℂ)
239	229, 230, 158	expne0d 13014	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (e↑(𝑁 + 1)) ≠ 0)
240	229, 230, 8	expne0d 13014	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (e↑𝑁) ≠ 0)
241	23, 24, 8	expne0d 13014	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (𝑁↑𝑁) ≠ 0)
242	235, 236, 237, 238, 239, 240, 241	divdivdivd 10848	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁))) = ((((𝑁 + 1)↑(𝑁 + 1)) · (e↑𝑁)) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁))))
243	235, 238	mulcomd 10061	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) · (e↑𝑁)) = ((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))))
244	243	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) · (e↑𝑁)) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁))) = (((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁))))
245	238, 236, 235, 237, 239, 241	divmuldivd 10842	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (((e↑𝑁) / (e↑(𝑁 + 1))) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = (((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁))))
246	229, 2	expp1d 13009	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (e↑(𝑁 + 1)) = ((e↑𝑁) · e))
247	246	oveq2d 6666	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → ((e↑𝑁) / (e↑(𝑁 + 1))) = ((e↑𝑁) / ((e↑𝑁) · e)))
248	238, 238, 229, 240, 230	divdiv1d 10832	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (((e↑𝑁) / (e↑𝑁)) / e) = ((e↑𝑁) / ((e↑𝑁) · e)))
249	238, 240	dividd 10799	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → ((e↑𝑁) / (e↑𝑁)) = 1)
250	249	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (((e↑𝑁) / (e↑𝑁)) / e) = (1 / e))
251	247, 248, 250	3eqtr2d 2662	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → ((e↑𝑁) / (e↑(𝑁 + 1))) = (1 / e))
252	251	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → (((e↑𝑁) / (e↑(𝑁 + 1))) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))))
253	245, 252	eqtr3d 2658	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁))) = ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))))
254	242, 244, 253	3eqtrd 2660	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁))) = ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))))
255	254	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁)))) = ((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))))
256	228, 234, 255	3eqtrd 2660	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) = ((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))))
257	256	oveq1d 6665	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) / (𝑁 + 1)) = (((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) / (𝑁 + 1)))
258	235, 237, 241	divcld 10801	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) ∈ ℂ)
259	35, 229, 258, 230	div32d 10824	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = (1 · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e)))
260	258, 229, 230	divcld 10801	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e) ∈ ℂ)
261	260	mulid2d 10058	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (1 · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e)) = ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e))
262	259, 261	eqtrd 2656	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e))
263	262	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) = (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e)))
264	229, 230	reccld 10794	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (1 / e) ∈ ℂ)
265	264, 258	mulcld 10060	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) ∈ ℂ)
266	218, 265, 22, 26	div23d 10838	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) / (𝑁 + 1)) = (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))))
267	218, 22, 26	divcld 10801	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) ∈ ℂ)
268	267, 258, 229, 230	divassd 10836	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e) = (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e)))
269	263, 266, 268	3eqtr4d 2666	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) / (𝑁 + 1)) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e))
270	227, 257, 269	3eqtrd 2660	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e))
271	187, 225, 270	3eqtrd 2660	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e))
272	182, 185, 271	3eqtrd 2660	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e))
273	171, 179, 272	3eqtrd 2660	. . . . 5 ⊢ (𝑁 ∈ ℕ → (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e))
274	218, 22, 258, 26	div32d 10824	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / (𝑁 + 1))))
275	22, 2	expp1d 13009	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1)↑(𝑁 + 1)) = (((𝑁 + 1)↑𝑁) · (𝑁 + 1)))
276	275	oveq1d 6665	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) = ((((𝑁 + 1)↑𝑁) · (𝑁 + 1)) / (𝑁 + 1)))
277	22, 2	expcld 13008	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1)↑𝑁) ∈ ℂ)
278	277, 22, 26	divcan4d 10807	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑𝑁) · (𝑁 + 1)) / (𝑁 + 1)) = ((𝑁 + 1)↑𝑁))
279	276, 278	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) = ((𝑁 + 1)↑𝑁))
280	279	oveq1d 6665	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) / (𝑁↑𝑁)) = (((𝑁 + 1)↑𝑁) / (𝑁↑𝑁)))
281	235, 237, 22, 241, 26	divdiv32d 10826	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / (𝑁 + 1)) = ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) / (𝑁↑𝑁)))
282	22, 23, 24, 2	expdivd 13022	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 𝑁)↑𝑁) = (((𝑁 + 1)↑𝑁) / (𝑁↑𝑁)))
283	280, 281, 282	3eqtr4d 2666	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / (𝑁 + 1)) = (((𝑁 + 1) / 𝑁)↑𝑁))
284	283	oveq2d 6666	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / (𝑁 + 1))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)))
285	274, 284	eqtrd 2656	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)))
286	285	oveq1d 6665	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e))
287	163, 273, 286	3eqtrd 2660	. . . 4 ⊢ (𝑁 ∈ ℕ → ((𝐴‘𝑁) / (𝐴‘(𝑁 + 1))) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e))
288	287	fveq2d 6195	. . 3 ⊢ (𝑁 ∈ ℕ → (log‘((𝐴‘𝑁) / (𝐴‘(𝑁 + 1)))) = (log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)))
289	83, 84, 288	3eqtr2d 2662	. 2 ⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) = (log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)))
290	35, 43	addcld 10059	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) ∈ ℂ)
291	290	halfcld 11277	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
292	291, 28	mulcld 10060	. . . 4 ⊢ (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) ∈ ℂ)
293	292, 35	subcld 10392	. . 3 ⊢ (𝑁 ∈ ℕ → ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
294		stirlinglem4.3	. . . . 5 ⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))
295	294	a1i 11	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) → 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1)))
296		simpr 477	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁)
297	296	oveq2d 6666	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (2 · 𝑛) = (2 · 𝑁))
298	297	oveq2d 6666	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (1 + (2 · 𝑛)) = (1 + (2 · 𝑁)))
299	298	oveq1d 6665	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → ((1 + (2 · 𝑛)) / 2) = ((1 + (2 · 𝑁)) / 2))
300	296	oveq1d 6665	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (𝑛 + 1) = (𝑁 + 1))
301	300, 296	oveq12d 6668	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → ((𝑛 + 1) / 𝑛) = ((𝑁 + 1) / 𝑁))
302	301	fveq2d 6195	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (log‘((𝑛 + 1) / 𝑛)) = (log‘((𝑁 + 1) / 𝑁)))
303	299, 302	oveq12d 6668	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
304	303	oveq1d 6665	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
305		simpl 473	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) → 𝑁 ∈ ℕ)
306		simpr 477	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) → ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
307	295, 304, 305, 306	fvmptd 6288	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) → (𝐽‘𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
308	293, 307	mpdan 702	. 2 ⊢ (𝑁 ∈ ℕ → (𝐽‘𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
309	52, 289, 308	3eqtr4d 2666	1 ⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) = (𝐽‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ↦ cmpt 4729 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 − cmin 10266 / cdiv 10684 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℝ⁺crp 11832 ↑cexp 12860 !cfa 13060 √csqrt 13973 eceu 14793 logclog 24301

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-e 14799 df-sin 14800 df-cos 14801 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-log 24303 df-cxp 24304

This theorem is referenced by: stirlinglem9 40299

W3C validator