| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | stirlinglem8.1 | . . 3
⊢
Ⅎ𝑛𝜑 | 
| 2 |  | stirlinglem8.7 | . . . 4
⊢ 𝐿 = (𝑛 ∈ ℕ ↦ ((𝐴‘𝑛)↑4)) | 
| 3 |  | nfmpt1 5249 | . . . 4
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((𝐴‘𝑛)↑4)) | 
| 4 | 2, 3 | nfcxfr 2902 | . . 3
⊢
Ⅎ𝑛𝐿 | 
| 5 |  | stirlinglem8.8 | . . . 4
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ((𝐷‘𝑛)↑2)) | 
| 6 |  | nfmpt1 5249 | . . . 4
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((𝐷‘𝑛)↑2)) | 
| 7 | 5, 6 | nfcxfr 2902 | . . 3
⊢
Ⅎ𝑛𝑀 | 
| 8 |  | stirlinglem8.6 | . . . 4
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2))) | 
| 9 |  | nfmpt1 5249 | . . . 4
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2))) | 
| 10 | 8, 9 | nfcxfr 2902 | . . 3
⊢
Ⅎ𝑛𝐹 | 
| 11 |  | nnuz 12922 | . . 3
⊢ ℕ =
(ℤ≥‘1) | 
| 12 |  | 1zzd 12650 | . . 3
⊢ (𝜑 → 1 ∈
ℤ) | 
| 13 |  | stirlinglem8.2 | . . . 4
⊢
Ⅎ𝑛𝐴 | 
| 14 |  | stirlinglem8.5 | . . . . 5
⊢ (𝜑 → 𝐴:ℕ⟶ℝ+) | 
| 15 |  | rrpsscn 45608 | . . . . 5
⊢
ℝ+ ⊆ ℂ | 
| 16 |  | fss 6751 | . . . . 5
⊢ ((𝐴:ℕ⟶ℝ+ ∧
ℝ+ ⊆ ℂ) → 𝐴:ℕ⟶ℂ) | 
| 17 | 14, 15, 16 | sylancl 586 | . . . 4
⊢ (𝜑 → 𝐴:ℕ⟶ℂ) | 
| 18 |  | stirlinglem8.11 | . . . 4
⊢ (𝜑 → 𝐴 ⇝ 𝐶) | 
| 19 |  | 4nn0 12547 | . . . . 5
⊢ 4 ∈
ℕ0 | 
| 20 | 19 | a1i 11 | . . . 4
⊢ (𝜑 → 4 ∈
ℕ0) | 
| 21 |  | nnex 12273 | . . . . . . 7
⊢ ℕ
∈ V | 
| 22 | 21 | mptex 7244 | . . . . . 6
⊢ (𝑛 ∈ ℕ ↦ ((𝐴‘𝑛)↑4)) ∈ V | 
| 23 | 2, 22 | eqeltri 2836 | . . . . 5
⊢ 𝐿 ∈ V | 
| 24 | 23 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐿 ∈ V) | 
| 25 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) | 
| 26 | 14 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈
ℝ+) | 
| 27 | 26 | rpcnd 13080 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ ℂ) | 
| 28 | 19 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 4 ∈
ℕ0) | 
| 29 | 27, 28 | expcld 14187 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴‘𝑛)↑4) ∈ ℂ) | 
| 30 | 2 | fvmpt2 7026 | . . . . 5
⊢ ((𝑛 ∈ ℕ ∧ ((𝐴‘𝑛)↑4) ∈ ℂ) → (𝐿‘𝑛) = ((𝐴‘𝑛)↑4)) | 
| 31 | 25, 29, 30 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐿‘𝑛) = ((𝐴‘𝑛)↑4)) | 
| 32 | 1, 13, 4, 11, 12, 17, 18, 20, 24, 31 | climexp 45625 | . . 3
⊢ (𝜑 → 𝐿 ⇝ (𝐶↑4)) | 
| 33 | 21 | mptex 7244 | . . . . 5
⊢ (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2))) ∈ V | 
| 34 | 8, 33 | eqeltri 2836 | . . . 4
⊢ 𝐹 ∈ V | 
| 35 | 34 | a1i 11 | . . 3
⊢ (𝜑 → 𝐹 ∈ V) | 
| 36 |  | stirlinglem8.3 | . . . 4
⊢
Ⅎ𝑛𝐷 | 
| 37 | 17 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴:ℕ⟶ℂ) | 
| 38 |  | 2nn 12340 | . . . . . . . . 9
⊢ 2 ∈
ℕ | 
| 39 | 38 | a1i 11 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ) | 
| 40 |  | id 22 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) | 
| 41 | 39, 40 | nnmulcld 12320 | . . . . . . 7
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℕ) | 
| 42 | 41 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈
ℕ) | 
| 43 | 37, 42 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘(2 · 𝑛)) ∈ ℂ) | 
| 44 |  | stirlinglem8.4 | . . . . 5
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛))) | 
| 45 | 1, 43, 44 | fmptdf 7136 | . . . 4
⊢ (𝜑 → 𝐷:ℕ⟶ℂ) | 
| 46 |  | nfmpt1 5249 | . . . . 5
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ (2 · 𝑛)) | 
| 47 |  | fex 7247 | . . . . . 6
⊢ ((𝐴:ℕ⟶ℂ ∧
ℕ ∈ V) → 𝐴
∈ V) | 
| 48 | 17, 21, 47 | sylancl 586 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ V) | 
| 49 |  | 1nn 12278 | . . . . . . 7
⊢ 1 ∈
ℕ | 
| 50 |  | 2cnd 12345 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) | 
| 51 |  | 1cnd 11257 | . . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) | 
| 52 | 50, 51 | mulcld 11282 | . . . . . . 7
⊢ (𝜑 → (2 · 1) ∈
ℂ) | 
| 53 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑛 = 1 → (2 · 𝑛) = (2 ·
1)) | 
| 54 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (2
· 𝑛)) = (𝑛 ∈ ℕ ↦ (2
· 𝑛)) | 
| 55 | 53, 54 | fvmptg 7013 | . . . . . . 7
⊢ ((1
∈ ℕ ∧ (2 · 1) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘1) = (2 ·
1)) | 
| 56 | 49, 52, 55 | sylancr 587 | . . . . . 6
⊢ (𝜑 → ((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘1) = (2 ·
1)) | 
| 57 | 38 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 2 ∈
ℕ) | 
| 58 | 49 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 1 ∈
ℕ) | 
| 59 | 57, 58 | nnmulcld 12320 | . . . . . 6
⊢ (𝜑 → (2 · 1) ∈
ℕ) | 
| 60 | 56, 59 | eqeltrd 2840 | . . . . 5
⊢ (𝜑 → ((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘1) ∈
ℕ) | 
| 61 |  | 1red 11263 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ) | 
| 62 | 39 | nnred 12282 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ) | 
| 63 | 41 | nnred 12282 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ) | 
| 64 | 39 | nnge1d 12315 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 1 ≤
2) | 
| 65 | 61, 62, 63, 64 | leadd2dd 11879 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ≤ ((2
· 𝑛) +
2)) | 
| 66 | 54 | fvmpt2 7026 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (2
· 𝑛) ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ (2 · 𝑛))‘𝑛) = (2 · 𝑛)) | 
| 67 | 41, 66 | mpdan 687 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘𝑛) = (2 · 𝑛)) | 
| 68 | 67 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘𝑛) + 1) = ((2 · 𝑛) + 1)) | 
| 69 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘)) | 
| 70 | 69 | cbvmptv 5254 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ (2
· 𝑛)) = (𝑘 ∈ ℕ ↦ (2
· 𝑘)) | 
| 71 | 70 | a1i 11 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑛 ∈ ℕ ↦ (2
· 𝑛)) = (𝑘 ∈ ℕ ↦ (2
· 𝑘))) | 
| 72 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 = (𝑛 + 1)) → 𝑘 = (𝑛 + 1)) | 
| 73 | 72 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 = (𝑛 + 1)) → (2 · 𝑘) = (2 · (𝑛 + 1))) | 
| 74 |  | peano2nn 12279 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) | 
| 75 | 39, 74 | nnmulcld 12320 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (2
· (𝑛 + 1)) ∈
ℕ) | 
| 76 | 71, 73, 74, 75 | fvmptd 7022 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘(𝑛 + 1)) = (2 · (𝑛 + 1))) | 
| 77 |  | 2cnd 12345 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 2 ∈
ℂ) | 
| 78 |  | nncn 12275 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) | 
| 79 |  | 1cnd 11257 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 1 ∈
ℂ) | 
| 80 | 77, 78, 79 | adddid 11286 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (2
· (𝑛 + 1)) = ((2
· 𝑛) + (2 ·
1))) | 
| 81 | 77 | mulridd 11279 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (2
· 1) = 2) | 
| 82 | 81 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + (2 ·
1)) = ((2 · 𝑛) +
2)) | 
| 83 | 76, 80, 82 | 3eqtrd 2780 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘(𝑛 + 1)) = ((2 · 𝑛) + 2)) | 
| 84 | 65, 68, 83 | 3brtr4d 5174 | . . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘𝑛) + 1) ≤ ((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘(𝑛 + 1))) | 
| 85 | 41 | nnzd 12642 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℤ) | 
| 86 | 67, 85 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘𝑛) ∈
ℤ) | 
| 87 | 86 | peano2zd 12727 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘𝑛) + 1) ∈
ℤ) | 
| 88 | 75 | nnzd 12642 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (2
· (𝑛 + 1)) ∈
ℤ) | 
| 89 | 76, 88 | eqeltrd 2840 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘(𝑛 + 1)) ∈
ℤ) | 
| 90 |  | eluz 12893 | . . . . . . . 8
⊢
(((((𝑛 ∈
ℕ ↦ (2 · 𝑛))‘𝑛) + 1) ∈ ℤ ∧ ((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘(𝑛 + 1)) ∈ ℤ) →
(((𝑛 ∈ ℕ ↦
(2 · 𝑛))‘(𝑛 + 1)) ∈
(ℤ≥‘(((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛) + 1)) ↔ (((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛) + 1) ≤ ((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘(𝑛 + 1)))) | 
| 91 | 87, 89, 90 | syl2anc 584 | . . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘(𝑛 + 1)) ∈
(ℤ≥‘(((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛) + 1)) ↔ (((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛) + 1) ≤ ((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘(𝑛 + 1)))) | 
| 92 | 84, 91 | mpbird 257 | . . . . . 6
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (2
· 𝑛))‘(𝑛 + 1)) ∈
(ℤ≥‘(((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛) + 1))) | 
| 93 | 92 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘(𝑛 + 1)) ∈
(ℤ≥‘(((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛) + 1))) | 
| 94 | 21 | mptex 7244 | . . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛))) ∈ V | 
| 95 | 44, 94 | eqeltri 2836 | . . . . . 6
⊢ 𝐷 ∈ V | 
| 96 | 95 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝐷 ∈ V) | 
| 97 | 44 | fvmpt2 7026 | . . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ (𝐴‘(2 · 𝑛)) ∈ ℂ) → (𝐷‘𝑛) = (𝐴‘(2 · 𝑛))) | 
| 98 | 25, 43, 97 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = (𝐴‘(2 · 𝑛))) | 
| 99 | 67 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛) = (2 · 𝑛)) | 
| 100 | 99 | eqcomd 2742 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) = ((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛)) | 
| 101 | 100 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘(2 · 𝑛)) = (𝐴‘((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛))) | 
| 102 | 98, 101 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = (𝐴‘((𝑛 ∈ ℕ ↦ (2 · 𝑛))‘𝑛))) | 
| 103 | 1, 13, 36, 46, 11, 12, 48, 27, 18, 60, 93, 96, 102 | climsuse 45628 | . . . 4
⊢ (𝜑 → 𝐷 ⇝ 𝐶) | 
| 104 |  | 2nn0 12545 | . . . . 5
⊢ 2 ∈
ℕ0 | 
| 105 | 104 | a1i 11 | . . . 4
⊢ (𝜑 → 2 ∈
ℕ0) | 
| 106 | 21 | mptex 7244 | . . . . . 6
⊢ (𝑛 ∈ ℕ ↦ ((𝐷‘𝑛)↑2)) ∈ V | 
| 107 | 5, 106 | eqeltri 2836 | . . . . 5
⊢ 𝑀 ∈ V | 
| 108 | 107 | a1i 11 | . . . 4
⊢ (𝜑 → 𝑀 ∈ V) | 
| 109 |  | stirlinglem8.9 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) ∈
ℝ+) | 
| 110 | 109 | rpcnd 13080 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) ∈ ℂ) | 
| 111 | 110 | sqcld 14185 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐷‘𝑛)↑2) ∈ ℂ) | 
| 112 | 5 | fvmpt2 7026 | . . . . 5
⊢ ((𝑛 ∈ ℕ ∧ ((𝐷‘𝑛)↑2) ∈ ℂ) → (𝑀‘𝑛) = ((𝐷‘𝑛)↑2)) | 
| 113 | 25, 111, 112 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘𝑛) = ((𝐷‘𝑛)↑2)) | 
| 114 | 1, 36, 7, 11, 12, 45, 103, 105, 108, 113 | climexp 45625 | . . 3
⊢ (𝜑 → 𝑀 ⇝ (𝐶↑2)) | 
| 115 |  | stirlinglem8.10 | . . . . 5
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 116 | 115 | rpcnd 13080 | . . . 4
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 117 | 115 | rpne0d 13083 | . . . 4
⊢ (𝜑 → 𝐶 ≠ 0) | 
| 118 |  | 2z 12651 | . . . . 5
⊢ 2 ∈
ℤ | 
| 119 | 118 | a1i 11 | . . . 4
⊢ (𝜑 → 2 ∈
ℤ) | 
| 120 | 116, 117,
119 | expne0d 14193 | . . 3
⊢ (𝜑 → (𝐶↑2) ≠ 0) | 
| 121 | 1, 29, 2 | fmptdf 7136 | . . . 4
⊢ (𝜑 → 𝐿:ℕ⟶ℂ) | 
| 122 | 121 | ffvelcdmda 7103 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐿‘𝑛) ∈ ℂ) | 
| 123 | 113, 111 | eqeltrd 2840 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘𝑛) ∈ ℂ) | 
| 124 | 98 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐷‘𝑛)↑2) = ((𝐴‘(2 · 𝑛))↑2)) | 
| 125 | 113, 124 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘𝑛) = ((𝐴‘(2 · 𝑛))↑2)) | 
| 126 | 98, 109 | eqeltrrd 2841 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘(2 · 𝑛)) ∈
ℝ+) | 
| 127 | 118 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 2 ∈
ℤ) | 
| 128 | 126, 127 | rpexpcld 14287 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴‘(2 · 𝑛))↑2) ∈
ℝ+) | 
| 129 | 125, 128 | eqeltrd 2840 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘𝑛) ∈
ℝ+) | 
| 130 | 129 | rpne0d 13083 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘𝑛) ≠ 0) | 
| 131 | 130 | neneqd 2944 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ¬ (𝑀‘𝑛) = 0) | 
| 132 |  | 0cn 11254 | . . . . . 6
⊢ 0 ∈
ℂ | 
| 133 |  | elsn2g 4663 | . . . . . 6
⊢ (0 ∈
ℂ → ((𝑀‘𝑛) ∈ {0} ↔ (𝑀‘𝑛) = 0)) | 
| 134 | 132, 133 | ax-mp 5 | . . . . 5
⊢ ((𝑀‘𝑛) ∈ {0} ↔ (𝑀‘𝑛) = 0) | 
| 135 | 131, 134 | sylnibr 329 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ¬ (𝑀‘𝑛) ∈ {0}) | 
| 136 | 123, 135 | eldifd 3961 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘𝑛) ∈ (ℂ ∖
{0})) | 
| 137 | 28 | nn0zd 12641 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 4 ∈
ℤ) | 
| 138 | 26, 137 | rpexpcld 14287 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴‘𝑛)↑4) ∈
ℝ+) | 
| 139 | 109, 127 | rpexpcld 14287 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐷‘𝑛)↑2) ∈
ℝ+) | 
| 140 | 138, 139 | rpdivcld 13095 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) ∈
ℝ+) | 
| 141 | 8 | fvmpt2 7026 | . . . . 5
⊢ ((𝑛 ∈ ℕ ∧ (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) ∈ ℝ+) →
(𝐹‘𝑛) = (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2))) | 
| 142 | 25, 140, 141 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2))) | 
| 143 | 2 | fvmpt2 7026 | . . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ ((𝐴‘𝑛)↑4) ∈ ℝ+) →
(𝐿‘𝑛) = ((𝐴‘𝑛)↑4)) | 
| 144 | 25, 138, 143 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐿‘𝑛) = ((𝐴‘𝑛)↑4)) | 
| 145 | 144, 113 | oveq12d 7450 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐿‘𝑛) / (𝑀‘𝑛)) = (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2))) | 
| 146 | 142, 145 | eqtr4d 2779 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = ((𝐿‘𝑛) / (𝑀‘𝑛))) | 
| 147 | 1, 4, 7, 10, 11, 12, 32, 35, 114, 120, 122, 136, 146 | climdivf 45632 | . 2
⊢ (𝜑 → 𝐹 ⇝ ((𝐶↑4) / (𝐶↑2))) | 
| 148 |  | 2cn 12342 | . . . . . 6
⊢ 2 ∈
ℂ | 
| 149 |  | 2p2e4 12402 | . . . . . 6
⊢ (2 + 2) =
4 | 
| 150 | 148, 148,
149 | mvlladdi 11528 | . . . . 5
⊢ 2 = (4
− 2) | 
| 151 | 150 | a1i 11 | . . . 4
⊢ (𝜑 → 2 = (4 −
2)) | 
| 152 | 151 | oveq2d 7448 | . . 3
⊢ (𝜑 → (𝐶↑2) = (𝐶↑(4 − 2))) | 
| 153 | 20 | nn0zd 12641 | . . . 4
⊢ (𝜑 → 4 ∈
ℤ) | 
| 154 | 116, 117,
119, 153 | expsubd 14198 | . . 3
⊢ (𝜑 → (𝐶↑(4 − 2)) = ((𝐶↑4) / (𝐶↑2))) | 
| 155 | 152, 154 | eqtrd 2776 | . 2
⊢ (𝜑 → (𝐶↑2) = ((𝐶↑4) / (𝐶↑2))) | 
| 156 | 147, 155 | breqtrrd 5170 | 1
⊢ (𝜑 → 𝐹 ⇝ (𝐶↑2)) |