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	\|- A = ( n e. NN \|-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
	stirlinglem4.2	\|- B = ( n e. NN \|-> ( log ` ( A ` n ) ) )
	stirlinglem4.3	\|- J = ( n e. NN \|-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )
Assertion	stirlinglem4	\|- ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) = ( J ` N ) )

Proof

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

Metamath Proof Explorer

Theorem stirlinglem4

Proof