This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem stirlinglem8

Description: If A converges to C , then F converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem8.1 ⊢ Ⅎ 𝑛 𝜑
stirlinglem8.2 ⊢ Ⅎ 𝑛 𝐴
stirlinglem8.3 ⊢ Ⅎ 𝑛 𝐷
stirlinglem8.4 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
stirlinglem8.5 ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ ℝ+ )
stirlinglem8.6 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
stirlinglem8.7 ⊢ 𝐿 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) )
stirlinglem8.8 ⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) )
stirlinglem8.9 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) ∈ ℝ+ )
stirlinglem8.10 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
stirlinglem8.11 ⊢ ( 𝜑 → 𝐴 ⇝ 𝐶 )
Assertion stirlinglem8 ( 𝜑 → 𝐹 ⇝ ( 𝐶 ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 stirlinglem8.1 ⊢ Ⅎ 𝑛 𝜑
2 stirlinglem8.2 ⊢ Ⅎ 𝑛 𝐴
3 stirlinglem8.3 ⊢ Ⅎ 𝑛 𝐷
4 stirlinglem8.4 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
5 stirlinglem8.5 ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ ℝ+ )
6 stirlinglem8.6 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
7 stirlinglem8.7 ⊢ 𝐿 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) )
8 stirlinglem8.8 ⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) )
9 stirlinglem8.9 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) ∈ ℝ+ )
10 stirlinglem8.10 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
11 stirlinglem8.11 ⊢ ( 𝜑 → 𝐴 ⇝ 𝐶 )
12 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) )
13 7 12 nfcxfr ⊢ Ⅎ 𝑛 𝐿
14 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) )
15 8 14 nfcxfr ⊢ Ⅎ 𝑛 𝑀
16 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
17 6 16 nfcxfr ⊢ Ⅎ 𝑛 𝐹
18 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
19 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
20 rrpsscn ⊢ ℝ+ ⊆ ℂ
21 fss ⊢ ( ( 𝐴 : ℕ ⟶ ℝ+ ∧ ℝ+ ⊆ ℂ ) → 𝐴 : ℕ ⟶ ℂ )
22 5 20 21 sylancl ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ ℂ )
23 4nn0 ⊢ 4 ∈ ℕ0
24 23 a1i ⊢ ( 𝜑 → 4 ∈ ℕ0 )
25 nnex ⊢ ℕ ∈ V
26 25 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) ) ∈ V
27 7 26 eqeltri ⊢ 𝐿 ∈ V
28 27 a1i ⊢ ( 𝜑 → 𝐿 ∈ V )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
30 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ ℝ+ )
31 30 rpcnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
32 23 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 4 ∈ ℕ0 )
33 31 32 expcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) ∈ ℂ )
34 7 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) ∈ ℂ ) → ( 𝐿 ‘ 𝑛 ) = ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) )
35 29 33 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐿 ‘ 𝑛 ) = ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) )
36 1 2 13 18 19 22 11 24 28 35 climexp ⊢ ( 𝜑 → 𝐿 ⇝ ( 𝐶 ↑ 4 ) )
37 25 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) ) ∈ V
38 6 37 eqeltri ⊢ 𝐹 ∈ V
39 38 a1i ⊢ ( 𝜑 → 𝐹 ∈ V )
40 22 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 : ℕ ⟶ ℂ )
41 2nn ⊢ 2 ∈ ℕ
42 41 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℕ )
43 id ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
44 42 43 nnmulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℕ )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 · 𝑛 ) ∈ ℕ )
46 40 45 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ ( 2 · 𝑛 ) ) ∈ ℂ )
47 1 46 4 fmptdf ⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ℂ )
48 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) )
49 fex ⊢ ( ( 𝐴 : ℕ ⟶ ℂ ∧ ℕ ∈ V ) → 𝐴 ∈ V )
50 22 25 49 sylancl ⊢ ( 𝜑 → 𝐴 ∈ V )
51 1nn ⊢ 1 ∈ ℕ
52 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
53 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
54 52 53 mulcld ⊢ ( 𝜑 → ( 2 · 1 ) ∈ ℂ )
55 oveq2 ⊢ ( 𝑛 = 1 → ( 2 · 𝑛 ) = ( 2 · 1 ) )
56 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) )
57 55 56 fvmptg ⊢ ( ( 1 ∈ ℕ ∧ ( 2 · 1 ) ∈ ℂ ) → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 1 ) = ( 2 · 1 ) )
58 51 54 57 sylancr ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 1 ) = ( 2 · 1 ) )
59 41 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
60 51 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
61 59 60 nnmulcld ⊢ ( 𝜑 → ( 2 · 1 ) ∈ ℕ )
62 58 61 eqeltrd ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 1 ) ∈ ℕ )
63 1red ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℝ )
64 42 nnred ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ )
65 44 nnred ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ )
66 42 nnge1d ⊢ ( 𝑛 ∈ ℕ → 1 ≤ 2 )
67 63 64 65 66 leadd2dd ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ≤ ( ( 2 · 𝑛 ) + 2 ) )
68 56 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 2 · 𝑛 ) ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) = ( 2 · 𝑛 ) )
69 44 68 mpdan ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) = ( 2 · 𝑛 ) )
70 69 oveq1d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) = ( ( 2 · 𝑛 ) + 1 ) )
71 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 2 · 𝑛 ) = ( 2 · 𝑘 ) )
72 71 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) = ( 𝑘 ∈ ℕ ↦ ( 2 · 𝑘 ) )
73 72 a1i ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) = ( 𝑘 ∈ ℕ ↦ ( 2 · 𝑘 ) ) )
74 simpr ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 = ( 𝑛 + 1 ) ) → 𝑘 = ( 𝑛 + 1 ) )
75 74 oveq2d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 = ( 𝑛 + 1 ) ) → ( 2 · 𝑘 ) = ( 2 · ( 𝑛 + 1 ) ) )
76 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
77 42 76 nnmulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · ( 𝑛 + 1 ) ) ∈ ℕ )
78 73 75 76 77 fvmptd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) = ( 2 · ( 𝑛 + 1 ) ) )
79 2cnd ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℂ )
80 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
81 1cnd ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℂ )
82 79 80 81 adddid ⊢ ( 𝑛 ∈ ℕ → ( 2 · ( 𝑛 + 1 ) ) = ( ( 2 · 𝑛 ) + ( 2 · 1 ) ) )
83 79 mulridd ⊢ ( 𝑛 ∈ ℕ → ( 2 · 1 ) = 2 )
84 83 oveq2d ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + ( 2 · 1 ) ) = ( ( 2 · 𝑛 ) + 2 ) )
85 78 82 84 3eqtrd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( 2 · 𝑛 ) + 2 ) )
86 67 70 85 3brtr4d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) )
87 44 nnzd ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℤ )
88 69 87 eqeltrd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) ∈ ℤ )
89 88 peano2zd ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) ∈ ℤ )
90 77 nnzd ⊢ ( 𝑛 ∈ ℕ → ( 2 · ( 𝑛 + 1 ) ) ∈ ℤ )
91 78 90 eqeltrd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) ∈ ℤ )
92 eluz ⊢ ( ( ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) ∈ ℤ ∧ ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) ∈ ℤ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) ) ↔ ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) ) )
93 89 91 92 syl2anc ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) ) ↔ ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) ) )
94 86 93 mpbird ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) ) )
95 94 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) + 1 ) ) )
96 25 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝐴 ‘ ( 2 · 𝑛 ) ) ) ∈ V
97 4 96 eqeltri ⊢ 𝐷 ∈ V
98 97 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
99 4 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐴 ‘ ( 2 · 𝑛 ) ) ∈ ℂ ) → ( 𝐷 ‘ 𝑛 ) = ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
100 29 46 99 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) = ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
101 69 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) = ( 2 · 𝑛 ) )
102 101 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 · 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) )
103 102 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ ( 2 · 𝑛 ) ) = ( 𝐴 ‘ ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) ) )
104 100 103 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) = ( 𝐴 ‘ ( ( 𝑛 ∈ ℕ ↦ ( 2 · 𝑛 ) ) ‘ 𝑛 ) ) )
105 1 2 3 48 18 19 50 31 11 62 95 98 104 climsuse ⊢ ( 𝜑 → 𝐷 ⇝ 𝐶 )
106 2nn0 ⊢ 2 ∈ ℕ0
107 106 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
108 25 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) ∈ V
109 8 108 eqeltri ⊢ 𝑀 ∈ V
110 109 a1i ⊢ ( 𝜑 → 𝑀 ∈ V )
111 9 rpcnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) ∈ ℂ )
112 111 sqcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ∈ ℂ )
113 8 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ∈ ℂ ) → ( 𝑀 ‘ 𝑛 ) = ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) )
114 29 112 113 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ 𝑛 ) = ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) )
115 1 3 15 18 19 47 105 107 110 114 climexp ⊢ ( 𝜑 → 𝑀 ⇝ ( 𝐶 ↑ 2 ) )
116 10 rpcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
117 10 rpne0d ⊢ ( 𝜑 → 𝐶 ≠ 0 )
118 2z ⊢ 2 ∈ ℤ
119 118 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
120 116 117 119 expne0d ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ≠ 0 )
121 1 33 7 fmptdf ⊢ ( 𝜑 → 𝐿 : ℕ ⟶ ℂ )
122 121 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐿 ‘ 𝑛 ) ∈ ℂ )
123 114 112 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ 𝑛 ) ∈ ℂ )
124 100 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) = ( ( 𝐴 ‘ ( 2 · 𝑛 ) ) ↑ 2 ) )
125 114 124 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ 𝑛 ) = ( ( 𝐴 ‘ ( 2 · 𝑛 ) ) ↑ 2 ) )
126 100 9 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ ( 2 · 𝑛 ) ) ∈ ℝ+ )
127 118 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 2 ∈ ℤ )
128 126 127 rpexpcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ∈ ℝ+ )
129 125 128 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ 𝑛 ) ∈ ℝ+ )
130 129 rpne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ 𝑛 ) ≠ 0 )
131 130 neneqd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ¬ ( 𝑀 ‘ 𝑛 ) = 0 )
132 0cn ⊢ 0 ∈ ℂ
133 elsn2g ⊢ ( 0 ∈ ℂ → ( ( 𝑀 ‘ 𝑛 ) ∈ { 0 } ↔ ( 𝑀 ‘ 𝑛 ) = 0 ) )
134 132 133 ax-mp ⊢ ( ( 𝑀 ‘ 𝑛 ) ∈ { 0 } ↔ ( 𝑀 ‘ 𝑛 ) = 0 )
135 131 134 sylnibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ¬ ( 𝑀 ‘ 𝑛 ) ∈ { 0 } )
136 123 135 eldifd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ 𝑛 ) ∈ ( ℂ ∖ { 0 } ) )
137 32 nn0zd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 4 ∈ ℤ )
138 30 137 rpexpcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) ∈ ℝ+ )
139 9 127 rpexpcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ∈ ℝ+ )
140 138 139 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) ∈ ℝ+ )
141 6 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) ∈ ℝ+ ) → ( 𝐹 ‘ 𝑛 ) = ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
142 29 140 141 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
143 7 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) ∈ ℝ+ ) → ( 𝐿 ‘ 𝑛 ) = ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) )
144 29 138 143 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐿 ‘ 𝑛 ) = ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) )
145 144 114 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐿 ‘ 𝑛 ) / ( 𝑀 ‘ 𝑛 ) ) = ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) )
146 142 145 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐿 ‘ 𝑛 ) / ( 𝑀 ‘ 𝑛 ) ) )
147 1 13 15 17 18 19 36 39 115 120 122 136 146 climdivf ⊢ ( 𝜑 → 𝐹 ⇝ ( ( 𝐶 ↑ 4 ) / ( 𝐶 ↑ 2 ) ) )
148 2cn ⊢ 2 ∈ ℂ
149 2p2e4 ⊢ ( 2 + 2 ) = 4
150 148 148 149 mvlladdi ⊢ 2 = ( 4 − 2 )
151 150 a1i ⊢ ( 𝜑 → 2 = ( 4 − 2 ) )
152 151 oveq2d ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = ( 𝐶 ↑ ( 4 − 2 ) ) )
153 24 nn0zd ⊢ ( 𝜑 → 4 ∈ ℤ )
154 116 117 119 153 expsubd ⊢ ( 𝜑 → ( 𝐶 ↑ ( 4 − 2 ) ) = ( ( 𝐶 ↑ 4 ) / ( 𝐶 ↑ 2 ) ) )
155 152 154 eqtrd ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = ( ( 𝐶 ↑ 4 ) / ( 𝐶 ↑ 2 ) ) )
156 147 155 breqtrrd ⊢ ( 𝜑 → 𝐹 ⇝ ( 𝐶 ↑ 2 ) )