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 pige0 ⊢ 0 ≤ π
183 182 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ π )
184 176 178 181 183 mulge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( 2 · π ) )
185 12 nn0red ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ )
186 12 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ 𝑛 )
187 179 184 185 186 sqrtmuld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) = ( ( √ ‘ ( 2 · π ) ) · ( √ ‘ 𝑛 ) ) )
188 176 181 178 183 sqrtmuld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( 2 · π ) ) = ( ( √ ‘ 2 ) · ( √ ‘ π ) ) )
189 188 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( 2 · π ) ) · ( √ ‘ 𝑛 ) ) = ( ( ( √ ‘ 2 ) · ( √ ‘ π ) ) · ( √ ‘ 𝑛 ) ) )
190 13 sqrtcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ 2 ) ∈ ℂ )
191 18 sqrtcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ 𝑛 ) ∈ ℂ )
192 190 34 191 mulassd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( √ ‘ 2 ) · ( √ ‘ π ) ) · ( √ ‘ 𝑛 ) ) = ( ( √ ‘ 2 ) · ( ( √ ‘ π ) · ( √ ‘ 𝑛 ) ) ) )
193 190 34 191 mul12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ 2 ) · ( ( √ ‘ π ) · ( √ ‘ 𝑛 ) ) ) = ( ( √ ‘ π ) · ( ( √ ‘ 2 ) · ( √ ‘ 𝑛 ) ) ) )
194 176 181 185 186 sqrtmuld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( 2 · 𝑛 ) ) = ( ( √ ‘ 2 ) · ( √ ‘ 𝑛 ) ) )
195 194 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ 2 ) · ( √ ‘ 𝑛 ) ) = ( √ ‘ ( 2 · 𝑛 ) ) )
196 195 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ π ) · ( ( √ ‘ 2 ) · ( √ ‘ 𝑛 ) ) ) = ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) )
197 193 196 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ 2 ) · ( ( √ ‘ π ) · ( √ ‘ 𝑛 ) ) ) = ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) )
198 189 192 197 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( 2 · π ) ) · ( √ ‘ 𝑛 ) ) = ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) )
199 187 198 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) = ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) )
200 199 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
201 200 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ! ‘ 𝑛 ) / ( ( ( √ ‘ π ) · ( √ ‘ ( 2 · 𝑛 ) ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
202 91 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ! ‘ 𝑛 ) ∈ ℂ )
203 94 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( 2 · 𝑛 ) ) ≠ 0 )
204 22 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → e ∈ ℂ )
205 25 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → e ≠ 0 )
206 18 204 205 divcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 / e ) ∈ ℂ )
207 95 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
208 18 204 207 205 divne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 / e ) ≠ 0 )
209 63 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ )
210 206 208 209 expne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 / e ) ↑ 𝑛 ) ≠ 0 )
211 38 29 203 210 mulne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ≠ 0 )
212 9 rpne0d ⊢ ( 𝜑 → 𝐶 ≠ 0 )
213 212 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ≠ 0 )
214 202 171 170 211 213 divdiv1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) / 𝐶 ) = ( ( ! ‘ 𝑛 ) / ( ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) · 𝐶 ) ) )
215 174 201 214 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) / 𝐶 ) )
216 99 ancli ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ∈ ℕ ∧ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ∈ ℂ ) )
217 216 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 ∈ ℕ ∧ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ∈ ℂ ) )
218 217 100 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) = ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
219 218 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( 𝐴 ‘ 𝑛 ) )
220 219 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) / 𝐶 ) = ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) )
221 33 215 220 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) )
222 1 221 mpteq2da ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) ) )
223 102 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
224 223 170 213 divrec2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) )
225 1 224 mpteq2da ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) )
226 146 212 reccld ⊢ ( 𝜑 → ( 1 / 𝐶 ) ∈ ℂ )
227 82 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ∈ V
228 227 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ∈ V )
229 3 a1i ⊢ ( 𝑘 ∈ ℕ → 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) )
230 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → 𝑛 = 𝑘 )
231 230 fveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑘 ) )
232 230 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 2 · 𝑛 ) = ( 2 · 𝑘 ) )
233 232 fveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( √ ‘ ( 2 · 𝑛 ) ) = ( √ ‘ ( 2 · 𝑘 ) ) )
234 230 oveq1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 𝑛 / e ) = ( 𝑘 / e ) )
235 234 230 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( 𝑛 / e ) ↑ 𝑛 ) = ( ( 𝑘 / e ) ↑ 𝑘 ) )
236 233 235 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) )
237 231 236 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) )
238 id ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ )
239 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
240 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
241 nncn ⊢ ( ( ! ‘ 𝑘 ) ∈ ℕ → ( ! ‘ 𝑘 ) ∈ ℂ )
242 239 240 241 3syl ⊢ ( 𝑘 ∈ ℕ → ( ! ‘ 𝑘 ) ∈ ℂ )
243 2cnd ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℂ )
244 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
245 243 244 mulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℂ )
246 245 sqrtcld ⊢ ( 𝑘 ∈ ℕ → ( √ ‘ ( 2 · 𝑘 ) ) ∈ ℂ )
247 22 a1i ⊢ ( 𝑘 ∈ ℕ → e ∈ ℂ )
248 25 a1i ⊢ ( 𝑘 ∈ ℕ → e ≠ 0 )
249 244 247 248 divcld ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 / e ) ∈ ℂ )
250 249 239 expcld ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 / e ) ↑ 𝑘 ) ∈ ℂ )
251 246 250 mulcld ⊢ ( 𝑘 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ∈ ℂ )
252 55 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℝ+ )
253 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
254 252 253 rpmulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℝ+ )
255 254 sqrtgt0d ⊢ ( 𝑘 ∈ ℕ → 0 < ( √ ‘ ( 2 · 𝑘 ) ) )
256 255 gt0ne0d ⊢ ( 𝑘 ∈ ℕ → ( √ ‘ ( 2 · 𝑘 ) ) ≠ 0 )
257 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
258 244 247 257 248 divne0d ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 / e ) ≠ 0 )
259 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
260 249 258 259 expne0d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 / e ) ↑ 𝑘 ) ≠ 0 )
261 246 250 256 260 mulne0d ⊢ ( 𝑘 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ≠ 0 )
262 242 251 261 divcld ⊢ ( 𝑘 ∈ ℕ → ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) ∈ ℂ )
263 229 237 238 262 fvmptd ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) = ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) )
264 263 262 eqeltrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
265 264 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
266 nfcv ⊢ Ⅎ 𝑘 ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) )
267 nfcv ⊢ Ⅎ 𝑛 1
268 nfcv ⊢ Ⅎ 𝑛 /
269 nfcv ⊢ Ⅎ 𝑛 𝐶
270 267 268 269 nfov ⊢ Ⅎ 𝑛 ( 1 / 𝐶 )
271 nfcv ⊢ Ⅎ 𝑛 ·
272 nfcv ⊢ Ⅎ 𝑛 𝑘
273 49 272 nffv ⊢ Ⅎ 𝑛 ( 𝐴 ‘ 𝑘 )
274 270 271 273 nfov ⊢ Ⅎ 𝑛 ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) )
275 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑘 ) )
276 275 oveq2d ⊢ ( 𝑛 = 𝑘 → ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
277 266 274 276 cbvmpt ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
278 277 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) )
279 278 fveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) ‘ 𝑘 ) )
280 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
281 146 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐶 ∈ ℂ )
282 212 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐶 ≠ 0 )
283 281 282 reccld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝐶 ) ∈ ℂ )
284 283 265 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ )
285 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
286 285 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ∈ ℂ ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) ‘ 𝑘 ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
287 280 284 286 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) ) ‘ 𝑘 ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
288 279 287 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑘 ) ) )
289 46 47 10 226 228 265 288 climmulc2 ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ⇝ ( ( 1 / 𝐶 ) · 𝐶 ) )
290 146 212 recid2d ⊢ ( 𝜑 → ( ( 1 / 𝐶 ) · 𝐶 ) = 1 )
291 289 290 breqtrd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝐶 ) · ( 𝐴 ‘ 𝑛 ) ) ) ⇝ 1 )
292 225 291 eqbrtrd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) / 𝐶 ) ) ⇝ 1 )
293 222 292 eqbrtrd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 )