Metamath Proof Explorer

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 )