Theorem stirlinglem15

Description: The Stirling's formula is proven using a number of local definitions. The main theorem stirling will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem15.1	⊢ Ⅎ 𝑛 𝜑
	stirlinglem15.2	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
	stirlinglem15.3	⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
	stirlinglem15.4	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
	stirlinglem15.5	⊢ 𝐸 = ( 𝑛 ∈ ℕ ↦ ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
	stirlinglem15.6	⊢ 𝑉 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
	stirlinglem15.7	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
	stirlinglem15.8	⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
	stirlinglem15.9	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
	stirlinglem15.10	⊢ ( 𝜑 → 𝐴 ⇝ 𝐶 )
Assertion	stirlinglem15	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 )

Proof

Step	Hyp	Ref	Expression
1		stirlinglem15.1	⊢ Ⅎ 𝑛 𝜑
2		stirlinglem15.2	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
3		stirlinglem15.3	⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
4		stirlinglem15.4	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
5		stirlinglem15.5	⊢ 𝐸 = ( 𝑛 ∈ ℕ ↦ ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
6		stirlinglem15.6	⊢ 𝑉 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
7		stirlinglem15.7	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
8		stirlinglem15.8	⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
9		stirlinglem15.9	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
10		stirlinglem15.10	⊢ ( 𝜑 → 𝐴 ⇝ 𝐶 )
11		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
13		2cnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 2 ∈ ℂ )
14		picn	⊢ π ∈ ℂ
15	14	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ∈ ℂ )
16	13 15	mulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 · π ) ∈ ℂ )
17		nncn	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
19	16 18	mulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2 · π ) · 𝑛 ) ∈ ℂ )
20	19	sqrtcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) ∈ ℂ )
21		ere	⊢ e ∈ ℝ
22	21	recni	⊢ e ∈ ℂ
23	22	a1i	⊢ ( 𝑛 ∈ ℕ → e ∈ ℂ )
24		epos	⊢ 0 < e
25	21 24	gt0ne0ii	⊢ e ≠ 0
26	25	a1i	⊢ ( 𝑛 ∈ ℕ → e ≠ 0 )
27	17 23 26	divcld	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 / e ) ∈ ℂ )
28	27 11	expcld	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / e ) ↑ 𝑛 ) ∈ ℂ )
29	28	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 / e ) ↑ 𝑛 ) ∈ ℂ )
30	20 29	mulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ∈ ℂ )
31	2	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ∈ ℂ ) → ( 𝑆 ‘ 𝑛 ) = ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
32	12 30 31	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ‘ 𝑛 ) = ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
33	32	oveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) = ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
34	15	sqrtcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ π ) ∈ ℂ )
35		2cnd	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℂ )
36	35 17	mulcld	⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℂ )
37	36	sqrtcld	⊢ ( 𝑛 ∈ ℕ → ( √ ‘ ( 2 · 𝑛 ) ) ∈ ℂ )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( 2 · 𝑛 ) ) ∈ ℂ )
39	34 38 29	mulassd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( √ ‘ π ) · ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
40		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
41	7 40	nfcxfr	⊢ Ⅎ 𝑛 𝐹
42		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
43	8 42	nfcxfr	⊢ Ⅎ 𝑛 𝐻
44		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
45	6 44	nfcxfr	⊢ Ⅎ 𝑛 𝑉
46		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
47		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
48		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
49	3 48	nfcxfr	⊢ Ⅎ 𝑛 𝐴
50		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
51	4 50	nfcxfr	⊢ Ⅎ 𝑛 𝐷
52		faccl	⊢ ( 𝑛 ∈ ℕ0 → ( ! ‘ 𝑛 ) ∈ ℕ )
53	11 52	syl	⊢ ( 𝑛 ∈ ℕ → ( ! ‘ 𝑛 ) ∈ ℕ )
54	53	nnrpd	⊢ ( 𝑛 ∈ ℕ → ( ! ‘ 𝑛 ) ∈ ℝ+ )
55		2rp	⊢ 2 ∈ ℝ+
56	55	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ+ )
57		nnrp	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
58	56 57	rpmulcld	⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ+ )
59	58	rpsqrtcld	⊢ ( 𝑛 ∈ ℕ → ( √ ‘ ( 2 · 𝑛 ) ) ∈ ℝ+ )
60		epr	⊢ e ∈ ℝ+
61	60	a1i	⊢ ( 𝑛 ∈ ℕ → e ∈ ℝ+ )
62	57 61	rpdivcld	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 / e ) ∈ ℝ+ )
63		nnz	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
64	62 63	rpexpcld	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / e ) ↑ 𝑛 ) ∈ ℝ+ )
65	59 64	rpmulcld	⊢ ( 𝑛 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ∈ ℝ+ )
66	54 65	rpdivcld	⊢ ( 𝑛 ∈ ℕ → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ∈ ℝ+ )
67	3 66	fmpti	⊢ 𝐴 : ℕ ⟶ ℝ+
68	67	a1i	⊢ ( 𝜑 → 𝐴 : ℕ ⟶ ℝ+ )
69		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) )
70		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) )
71	67	a1i	⊢ ( 𝑛 ∈ ℕ → 𝐴 : ℕ ⟶ ℝ+ )
72		2nn	⊢ 2 ∈ ℕ
73	72	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℕ )
74		id	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
75	73 74	nnmulcld	⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℕ )
76	71 75	ffvelcdmd	⊢ ( 𝑛 ∈ ℕ → ( 𝐴 ‘ ( 2 · 𝑛 ) ) ∈ ℝ+ )
77	4	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐴 ‘ ( 2 · 𝑛 ) ) ∈ ℝ+ ) → ( 𝐷 ‘ 𝑛 ) = ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
78	76 77	mpdan	⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) = ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
79	78 76	eqeltrd	⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) ∈ ℝ+ )
80	79	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) ∈ ℝ+ )
81	1 49 51 4 68 7 69 70 80 9 10	stirlinglem8	⊢ ( 𝜑 → 𝐹 ⇝ ( 𝐶 ↑ 2 ) )
82		nnex	⊢ ℕ ∈ V
83	82	mptex	⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ V
84	6 83	eqeltri	⊢ 𝑉 ∈ V
85	84	a1i	⊢ ( 𝜑 → 𝑉 ∈ V )
86		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) )
87		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
88		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
89	8 86 87 88	stirlinglem1	⊢ 𝐻 ⇝ ( 1 / 2 )
90	89	a1i	⊢ ( 𝜑 → 𝐻 ⇝ ( 1 / 2 ) )
91	53	nncnd	⊢ ( 𝑛 ∈ ℕ → ( ! ‘ 𝑛 ) ∈ ℂ )
92	37 28	mulcld	⊢ ( 𝑛 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ∈ ℂ )
93	58	sqrtgt0d	⊢ ( 𝑛 ∈ ℕ → 0 < ( √ ‘ ( 2 · 𝑛 ) ) )
94	93	gt0ne0d	⊢ ( 𝑛 ∈ ℕ → ( √ ‘ ( 2 · 𝑛 ) ) ≠ 0 )
95		nnne0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
96	17 23 95 26	divne0d	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 / e ) ≠ 0 )
97	27 96 63	expne0d	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / e ) ↑ 𝑛 ) ≠ 0 )
98	37 28 94 97	mulne0d	⊢ ( 𝑛 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ≠ 0 )
99	91 92 98	divcld	⊢ ( 𝑛 ∈ ℕ → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ∈ ℂ )
100	3	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ∈ ℂ ) → ( 𝐴 ‘ 𝑛 ) = ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
101	99 100	mpdan	⊢ ( 𝑛 ∈ ℕ → ( 𝐴 ‘ 𝑛 ) = ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
102	101 99	eqeltrd	⊢ ( 𝑛 ∈ ℕ → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
103		4nn0	⊢ 4 ∈ ℕ0
104	103	a1i	⊢ ( 𝑛 ∈ ℕ → 4 ∈ ℕ0 )
105	102 104	expcld	⊢ ( 𝑛 ∈ ℕ → ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) ∈ ℂ )
106	79	rpcnd	⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) ∈ ℂ )
107	106	sqcld	⊢ ( 𝑛 ∈ ℕ → ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ∈ ℂ )
108	79	rpne0d	⊢ ( 𝑛 ∈ ℕ → ( 𝐷 ‘ 𝑛 ) ≠ 0 )
109		2z	⊢ 2 ∈ ℤ
110	109	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℤ )
111	106 108 110	expne0d	⊢ ( 𝑛 ∈ ℕ → ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ≠ 0 )
112	105 107 111	divcld	⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) ∈ ℂ )
113	7	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) ∈ ℂ ) → ( 𝐹 ‘ 𝑛 ) = ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
114	112 113	mpdan	⊢ ( 𝑛 ∈ ℕ → ( 𝐹 ‘ 𝑛 ) = ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
115	114 112	eqeltrd	⊢ ( 𝑛 ∈ ℕ → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
116	115	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
117	17	sqcld	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 2 ) ∈ ℂ )
118		1cnd	⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℂ )
119	36 118	addcld	⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℂ )
120	17 119	mulcld	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
121	75	nnred	⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ )
122		1red	⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℝ )
123	75	nngt0d	⊢ ( 𝑛 ∈ ℕ → 0 < ( 2 · 𝑛 ) )
124		0lt1	⊢ 0 < 1
125	124	a1i	⊢ ( 𝑛 ∈ ℕ → 0 < 1 )
126	121 122 123 125	addgt0d	⊢ ( 𝑛 ∈ ℕ → 0 < ( ( 2 · 𝑛 ) + 1 ) )
127	126	gt0ne0d	⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
128	17 119 95 127	mulne0d	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ≠ 0 )
129	117 120 128	divcld	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ ℂ )
130	8	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ ℂ ) → ( 𝐻 ‘ 𝑛 ) = ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
131	129 130	mpdan	⊢ ( 𝑛 ∈ ℕ → ( 𝐻 ‘ 𝑛 ) = ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
132	131 129	eqeltrd	⊢ ( 𝑛 ∈ ℕ → ( 𝐻 ‘ 𝑛 ) ∈ ℂ )
133	132	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐻 ‘ 𝑛 ) ∈ ℂ )
134	112 129	mulcld	⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) · ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) ∈ ℂ )
135	3 4 5 6	stirlinglem3	⊢ 𝑉 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) · ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
136	135	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) · ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) ∈ ℂ ) → ( 𝑉 ‘ 𝑛 ) = ( ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) · ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
137	134 136	mpdan	⊢ ( 𝑛 ∈ ℕ → ( 𝑉 ‘ 𝑛 ) = ( ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) · ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
138	114 131	oveq12d	⊢ ( 𝑛 ∈ ℕ → ( ( 𝐹 ‘ 𝑛 ) · ( 𝐻 ‘ 𝑛 ) ) = ( ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) · ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
139	137 138	eqtr4d	⊢ ( 𝑛 ∈ ℕ → ( 𝑉 ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑛 ) · ( 𝐻 ‘ 𝑛 ) ) )
140	139	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑉 ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑛 ) · ( 𝐻 ‘ 𝑛 ) ) )
141	1 41 43 45 46 47 81 85 90 116 133 140	climmulf	⊢ ( 𝜑 → 𝑉 ⇝ ( ( 𝐶 ↑ 2 ) · ( 1 / 2 ) ) )
142	6	wallispi2	⊢ 𝑉 ⇝ ( π / 2 )
143		climuni	⊢ ( ( 𝑉 ⇝ ( ( 𝐶 ↑ 2 ) · ( 1 / 2 ) ) ∧ 𝑉 ⇝ ( π / 2 ) ) → ( ( 𝐶 ↑ 2 ) · ( 1 / 2 ) ) = ( π / 2 ) )
144	141 142 143	sylancl	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) · ( 1 / 2 ) ) = ( π / 2 ) )
145	144	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) · ( 1 / 2 ) ) / ( 1 / 2 ) ) = ( ( π / 2 ) / ( 1 / 2 ) ) )
146	9	rpcnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
147	146	sqcld	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
148		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
149	148	halfcld	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
150		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
151		2pos	⊢ 0 < 2
152	151	a1i	⊢ ( 𝜑 → 0 < 2 )
153	152	gt0ne0d	⊢ ( 𝜑 → 2 ≠ 0 )
154	150 153	recne0d	⊢ ( 𝜑 → ( 1 / 2 ) ≠ 0 )
155	147 149 154	divcan4d	⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) · ( 1 / 2 ) ) / ( 1 / 2 ) ) = ( 𝐶 ↑ 2 ) )
156	14	a1i	⊢ ( 𝜑 → π ∈ ℂ )
157	124	a1i	⊢ ( 𝜑 → 0 < 1 )
158	157	gt0ne0d	⊢ ( 𝜑 → 1 ≠ 0 )
159	156 148 150 158 153	divcan7d	⊢ ( 𝜑 → ( ( π / 2 ) / ( 1 / 2 ) ) = ( π / 1 ) )
160	156	div1d	⊢ ( 𝜑 → ( π / 1 ) = π )
161	159 160	eqtrd	⊢ ( 𝜑 → ( ( π / 2 ) / ( 1 / 2 ) ) = π )
162	145 155 161	3eqtr3d	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = π )
163	162	fveq2d	⊢ ( 𝜑 → ( √ ‘ ( 𝐶 ↑ 2 ) ) = ( √ ‘ π ) )
164	9	rprege0d	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
165		sqrtsq	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) → ( √ ‘ ( 𝐶 ↑ 2 ) ) = 𝐶 )
166	164 165	syl	⊢ ( 𝜑 → ( √ ‘ ( 𝐶 ↑ 2 ) ) = 𝐶 )
167	163 166	eqtr3d	⊢ ( 𝜑 → ( √ ‘ π ) = 𝐶 )
168	167	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ π ) = 𝐶 )
169	168	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ π ) · ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( 𝐶 · ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
170	146	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℂ )
171	92	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ∈ ℂ )
172	170 171	mulcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 · ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) · 𝐶 ) )
173	39 169 172	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) · 𝐶 ) )
174	173	oveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ! ‘ 𝑛 ) / ( ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) · 𝐶 ) ) )
175		2re	⊢ 2 ∈ ℝ
176	175	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 2 ∈ ℝ )
177		pire	⊢ π ∈ ℝ
178	177	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → π ∈ ℝ )
179	176 178	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 · π ) ∈ ℝ )
180		0le2	⊢ 0 ≤ 2
181	180	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ 2 )
182		0re	⊢ 0 ∈ ℝ
183		pipos	⊢ 0 < π
184	182 177 183	ltleii	⊢ 0 ≤ π
185	184	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ π )
186	176 178 181 185	mulge0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( 2 · π ) )
187	12	nn0red	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ )
188	12	nn0ge0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ 𝑛 )
189	179 186 187 188	sqrtmuld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) = ( ( √ ‘ ( 2 · π ) ) · ( √ ‘ 𝑛 ) ) )
190	176 181 178 185	sqrtmuld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( 2 · π ) ) = ( ( √ ‘ 2 ) · ( √ ‘ π ) ) )
191	190	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( 2 · π ) ) · ( √ ‘ 𝑛 ) ) = ( ( ( √ ‘ 2 ) · ( √ ‘ π ) ) · ( √ ‘ 𝑛 ) ) )
192	13	sqrtcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ 2 ) ∈ ℂ )
193	18	sqrtcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ 𝑛 ) ∈ ℂ )
194	192 34 193	mulassd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( √ ‘ 2 ) · ( √ ‘ π ) ) · ( √ ‘ 𝑛 ) ) = ( ( √ ‘ 2 ) · ( ( √ ‘ π ) · ( √ ‘ 𝑛 ) ) ) )
195	192 34 193	mul12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ 2 ) · ( ( √ ‘ π ) · ( √ ‘ 𝑛 ) ) ) = ( ( √ ‘ π ) · ( ( √ ‘ 2 ) · ( √ ‘ 𝑛 ) ) ) )
196	176 181 187 188	sqrtmuld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( 2 · 𝑛 ) ) = ( ( √ ‘ 2 ) · ( √ ‘ 𝑛 ) ) )
197	196	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ 2 ) · ( √ ‘ 𝑛 ) ) = ( √ ‘ ( 2 · 𝑛 ) ) )
198	197	oveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ π ) · ( ( √ ‘ 2 ) · ( √ ‘ 𝑛 ) ) ) = ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) )
199	195 198	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ 2 ) · ( ( √ ‘ π ) · ( √ ‘ 𝑛 ) ) ) = ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) )
200	191 194 199	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( 2 · π ) ) · ( √ ‘ 𝑛 ) ) = ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) )
201	189 200	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) = ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) )
202	201	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
203	202	oveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ! ‘ 𝑛 ) / ( ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
204	91	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ! ‘ 𝑛 ) ∈ ℂ )
205	94	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( 2 · 𝑛 ) ) ≠ 0 )
206	22	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → e ∈ ℂ )
207	25	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → e ≠ 0 )
208	18 206 207	divcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 / e ) ∈ ℂ )
209	95	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
210	18 206 209 207	divne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 / e ) ≠ 0 )
211	63	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ )
212	208 210 211	expne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 / e ) ↑ 𝑛 ) ≠ 0 )
213	38 29 205 212	mulne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ≠ 0 )
214	9	rpne0d	⊢ ( 𝜑 → 𝐶 ≠ 0 )
215	214	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ≠ 0 )
216	204 171 170 213 215	divdiv1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) / 𝐶 ) = ( ( ! ‘ 𝑛 ) / ( ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) · 𝐶 ) ) )
217	174 203 216	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) / 𝐶 ) )
218	99	ancli	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ∈ ℕ ∧ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ∈ ℂ ) )
219	218	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 ∈ ℕ ∧ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ∈ ℂ ) )
220	219 100	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) = ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
221	220	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( 𝐴 ‘ 𝑛 ) )
222	221	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) / 𝐶 ) = ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) )
223	33 217 222	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) )
224	1 223	mpteq2da	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) ) )
225	102	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
226	225 170 215	divrec2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) )
227	1 226	mpteq2da	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) )
228	146 214	reccld	⊢ ( 𝜑 → ( 1 / 𝐶 ) ∈ ℂ )
229	82	mptex	⊢ ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ∈ V
230	229	a1i	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ∈ V )
231	3	a1i	⊢ ( 𝑘 ∈ ℕ → 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) )
232		simpr	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → 𝑛 = 𝑘 )
233	232	fveq2d	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑘 ) )
234	232	oveq2d	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 2 · 𝑛 ) = ( 2 · 𝑘 ) )
235	234	fveq2d	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( √ ‘ ( 2 · 𝑛 ) ) = ( √ ‘ ( 2 · 𝑘 ) ) )
236	232	oveq1d	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 𝑛 / e ) = ( 𝑘 / e ) )
237	236 232	oveq12d	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( 𝑛 / e ) ↑ 𝑛 ) = ( ( 𝑘 / e ) ↑ 𝑘 ) )
238	235 237	oveq12d	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) )
239	233 238	oveq12d	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) )
240		id	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ )
241		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
242		faccl	⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
243		nncn	⊢ ( ( ! ‘ 𝑘 ) ∈ ℕ → ( ! ‘ 𝑘 ) ∈ ℂ )
244	241 242 243	3syl	⊢ ( 𝑘 ∈ ℕ → ( ! ‘ 𝑘 ) ∈ ℂ )
245		2cnd	⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℂ )
246		nncn	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
247	245 246	mulcld	⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℂ )
248	247	sqrtcld	⊢ ( 𝑘 ∈ ℕ → ( √ ‘ ( 2 · 𝑘 ) ) ∈ ℂ )
249	22	a1i	⊢ ( 𝑘 ∈ ℕ → e ∈ ℂ )
250	25	a1i	⊢ ( 𝑘 ∈ ℕ → e ≠ 0 )
251	246 249 250	divcld	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 / e ) ∈ ℂ )
252	251 241	expcld	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 / e ) ↑ 𝑘 ) ∈ ℂ )
253	248 252	mulcld	⊢ ( 𝑘 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ∈ ℂ )
254	55	a1i	⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℝ+ )
255		nnrp	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
256	254 255	rpmulcld	⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℝ+ )
257	256	sqrtgt0d	⊢ ( 𝑘 ∈ ℕ → 0 < ( √ ‘ ( 2 · 𝑘 ) ) )
258	257	gt0ne0d	⊢ ( 𝑘 ∈ ℕ → ( √ ‘ ( 2 · 𝑘 ) ) ≠ 0 )
259		nnne0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
260	246 249 259 250	divne0d	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 / e ) ≠ 0 )
261		nnz	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
262	251 260 261	expne0d	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 / e ) ↑ 𝑘 ) ≠ 0 )
263	248 252 258 262	mulne0d	⊢ ( 𝑘 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ≠ 0 )
264	244 253 263	divcld	⊢ ( 𝑘 ∈ ℕ → ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) ∈ ℂ )
265	231 239 240 264	fvmptd	⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) = ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) )
266	265 264	eqeltrd	⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
267	266	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
268		nfcv	⊢ Ⅎ 𝑘 ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) )
269		nfcv	⊢ Ⅎ 𝑛 1
270		nfcv	⊢ Ⅎ 𝑛 /
271		nfcv	⊢ Ⅎ 𝑛 𝐶
272	269 270 271	nfov	⊢ Ⅎ 𝑛 ( 1 / 𝐶 )
273		nfcv	⊢ Ⅎ 𝑛 ·
274		nfcv	⊢ Ⅎ 𝑛 𝑘
275	49 274	nffv	⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑘 )
276	272 273 275	nfov	⊢ Ⅎ 𝑛 ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) )
277		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) )
278	277	oveq2d	⊢ ( 𝑛 = 𝑘 → ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
279	268 276 278	cbvmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
280	279	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) )
281	280	fveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) ‘ 𝑘 ) )
282		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
283	146	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐶 ∈ ℂ )
284	214	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐶 ≠ 0 )
285	283 284	reccld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝐶 ) ∈ ℂ )
286	285 267	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
287		eqid	⊢ ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
288	287	fvmpt2	⊢ ( ( 𝑘 ∈ ℕ ∧ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) ‘ 𝑘 ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
289	282 286 288	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) ‘ 𝑘 ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
290	281 289	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
291	46 47 10 228 230 267 290	climmulc2	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ⇝ ( ( 1 / 𝐶 ) · 𝐶 ) )
292	146 214	recid2d	⊢ ( 𝜑 → ( ( 1 / 𝐶 ) · 𝐶 ) = 1 )
293	291 292	breqtrd	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ⇝ 1 )
294	227 293	eqbrtrd	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) ) ⇝ 1 )
295	224 294	eqbrtrd	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 )