Theorem stirlinglem4

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

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

Proof

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