Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stirlinglem4 Structured version   Visualization version   GIF version

Theorem stirlinglem4 38970
Description: Algebraic manipulation of ((𝐵 n ) - ( B (𝑛 + 1))). It will be used in other theorems to show that 𝐵 is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem4.1 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
stirlinglem4.2 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴𝑛)))
stirlinglem4.3 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))
Assertion
Ref Expression
stirlinglem4 (𝑁 ∈ ℕ → ((𝐵𝑁) − (𝐵‘(𝑁 + 1))) = (𝐽𝑁))
Distinct variable group:   𝑛,𝑁
Allowed substitution hints:   𝐴(𝑛)   𝐵(𝑛)   𝐽(𝑛)

Proof of Theorem stirlinglem4
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 nnre 10904 . . . . . . . 8 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2 nnnn0 11176 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
32nn0ge0d 11231 . . . . . . . 8 (𝑁 ∈ ℕ → 0 ≤ 𝑁)
41, 3ge0p1rpd 11778 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ+)
5 nnrp 11718 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
64, 5rpdivcld 11765 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℝ+)
76rpsqrtcld 13998 . . . . 5 (𝑁 ∈ ℕ → (√‘((𝑁 + 1) / 𝑁)) ∈ ℝ+)
8 nnz 11276 . . . . . 6 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
96, 8rpexpcld 12894 . . . . 5 (𝑁 ∈ ℕ → (((𝑁 + 1) / 𝑁)↑𝑁) ∈ ℝ+)
107, 9rpmulcld 11764 . . . 4 (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) ∈ ℝ+)
11 epr 14775 . . . . 5 e ∈ ℝ+
1211a1i 11 . . . 4 (𝑁 ∈ ℕ → e ∈ ℝ+)
1310, 12relogdivd 24176 . . 3 (𝑁 ∈ ℕ → (log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)) = ((log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) − (log‘e)))
147, 9relogmuld 24175 . . . . . 6 (𝑁 ∈ ℕ → (log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) = ((log‘(√‘((𝑁 + 1) / 𝑁))) + (log‘(((𝑁 + 1) / 𝑁)↑𝑁))))
15 logsqrt 24250 . . . . . . . 8 (((𝑁 + 1) / 𝑁) ∈ ℝ+ → (log‘(√‘((𝑁 + 1) / 𝑁))) = ((log‘((𝑁 + 1) / 𝑁)) / 2))
166, 15syl 17 . . . . . . 7 (𝑁 ∈ ℕ → (log‘(√‘((𝑁 + 1) / 𝑁))) = ((log‘((𝑁 + 1) / 𝑁)) / 2))
17 relogexp 24146 . . . . . . . 8 ((((𝑁 + 1) / 𝑁) ∈ ℝ+𝑁 ∈ ℤ) → (log‘(((𝑁 + 1) / 𝑁)↑𝑁)) = (𝑁 · (log‘((𝑁 + 1) / 𝑁))))
186, 8, 17syl2anc 691 . . . . . . 7 (𝑁 ∈ ℕ → (log‘(((𝑁 + 1) / 𝑁)↑𝑁)) = (𝑁 · (log‘((𝑁 + 1) / 𝑁))))
1916, 18oveq12d 6567 . . . . . 6 (𝑁 ∈ ℕ → ((log‘(√‘((𝑁 + 1) / 𝑁))) + (log‘(((𝑁 + 1) / 𝑁)↑𝑁))) = (((log‘((𝑁 + 1) / 𝑁)) / 2) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))))
2014, 19eqtrd 2644 . . . . 5 (𝑁 ∈ ℕ → (log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) = (((log‘((𝑁 + 1) / 𝑁)) / 2) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))))
21 peano2nn 10909 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
2221nncnd 10913 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
23 nncn 10905 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
24 nnne0 10930 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
2522, 23, 24divcld 10680 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
2621nnne0d 10942 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0)
2722, 23, 26, 24divne0d 10696 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ≠ 0)
2825, 27logcld 24121 . . . . . . 7 (𝑁 ∈ ℕ → (log‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
29 2cnd 10970 . . . . . . 7 (𝑁 ∈ ℕ → 2 ∈ ℂ)
30 2rp 11713 . . . . . . . . 9 2 ∈ ℝ+
3130a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → 2 ∈ ℝ+)
3231rpne0d 11753 . . . . . . 7 (𝑁 ∈ ℕ → 2 ≠ 0)
3328, 29, 32divrec2d 10684 . . . . . 6 (𝑁 ∈ ℕ → ((log‘((𝑁 + 1) / 𝑁)) / 2) = ((1 / 2) · (log‘((𝑁 + 1) / 𝑁))))
3433oveq1d 6564 . . . . 5 (𝑁 ∈ ℕ → (((log‘((𝑁 + 1) / 𝑁)) / 2) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))) = (((1 / 2) · (log‘((𝑁 + 1) / 𝑁))) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))))
35 1cnd 9935 . . . . . . . 8 (𝑁 ∈ ℕ → 1 ∈ ℂ)
3635halfcld 11154 . . . . . . 7 (𝑁 ∈ ℕ → (1 / 2) ∈ ℂ)
3736, 23, 28adddird 9944 . . . . . 6 (𝑁 ∈ ℕ → (((1 / 2) + 𝑁) · (log‘((𝑁 + 1) / 𝑁))) = (((1 / 2) · (log‘((𝑁 + 1) / 𝑁))) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))))
3823, 29, 32divcan4d 10686 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((𝑁 · 2) / 2) = 𝑁)
3923, 29mulcomd 9940 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 · 2) = (2 · 𝑁))
4039oveq1d 6564 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((𝑁 · 2) / 2) = ((2 · 𝑁) / 2))
4138, 40eqtr3d 2646 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 = ((2 · 𝑁) / 2))
4241oveq2d 6565 . . . . . . . 8 (𝑁 ∈ ℕ → ((1 / 2) + 𝑁) = ((1 / 2) + ((2 · 𝑁) / 2)))
4329, 23mulcld 9939 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
4435, 43, 29, 32divdird 10718 . . . . . . . 8 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) = ((1 / 2) + ((2 · 𝑁) / 2)))
4542, 44eqtr4d 2647 . . . . . . 7 (𝑁 ∈ ℕ → ((1 / 2) + 𝑁) = ((1 + (2 · 𝑁)) / 2))
4645oveq1d 6564 . . . . . 6 (𝑁 ∈ ℕ → (((1 / 2) + 𝑁) · (log‘((𝑁 + 1) / 𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
4737, 46eqtr3d 2646 . . . . 5 (𝑁 ∈ ℕ → (((1 / 2) · (log‘((𝑁 + 1) / 𝑁))) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
4820, 34, 473eqtrd 2648 . . . 4 (𝑁 ∈ ℕ → (log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
49 loge 24137 . . . . 5 (log‘e) = 1
5049a1i 11 . . . 4 (𝑁 ∈ ℕ → (log‘e) = 1)
5148, 50oveq12d 6567 . . 3 (𝑁 ∈ ℕ → ((log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) − (log‘e)) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
5213, 51eqtrd 2644 . 2 (𝑁 ∈ ℕ → (log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
53 stirlinglem4.1 . . . . . . 7 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
5453stirlinglem2 38968 . . . . . 6 (𝑁 ∈ ℕ → (𝐴𝑁) ∈ ℝ+)
5554relogcld 24173 . . . . 5 (𝑁 ∈ ℕ → (log‘(𝐴𝑁)) ∈ ℝ)
56 nfcv 2751 . . . . . 6 𝑛𝑁
57 nfcv 2751 . . . . . . 7 𝑛log
58 nfmpt1 4675 . . . . . . . . 9 𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))
5953, 58nfcxfr 2749 . . . . . . . 8 𝑛𝐴
6059, 56nffv 6110 . . . . . . 7 𝑛(𝐴𝑁)
6157, 60nffv 6110 . . . . . 6 𝑛(log‘(𝐴𝑁))
62 fveq2 6103 . . . . . . 7 (𝑛 = 𝑁 → (𝐴𝑛) = (𝐴𝑁))
6362fveq2d 6107 . . . . . 6 (𝑛 = 𝑁 → (log‘(𝐴𝑛)) = (log‘(𝐴𝑁)))
64 stirlinglem4.2 . . . . . 6 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴𝑛)))
6556, 61, 63, 64fvmptf 6209 . . . . 5 ((𝑁 ∈ ℕ ∧ (log‘(𝐴𝑁)) ∈ ℝ) → (𝐵𝑁) = (log‘(𝐴𝑁)))
6655, 65mpdan 699 . . . 4 (𝑁 ∈ ℕ → (𝐵𝑁) = (log‘(𝐴𝑁)))
67 nfcv 2751 . . . . . . . 8 𝑘(log‘(𝐴𝑛))
68 nfcv 2751 . . . . . . . . . 10 𝑛𝑘
6959, 68nffv 6110 . . . . . . . . 9 𝑛(𝐴𝑘)
7057, 69nffv 6110 . . . . . . . 8 𝑛(log‘(𝐴𝑘))
71 fveq2 6103 . . . . . . . . 9 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
7271fveq2d 6107 . . . . . . . 8 (𝑛 = 𝑘 → (log‘(𝐴𝑛)) = (log‘(𝐴𝑘)))
7367, 70, 72cbvmpt 4677 . . . . . . 7 (𝑛 ∈ ℕ ↦ (log‘(𝐴𝑛))) = (𝑘 ∈ ℕ ↦ (log‘(𝐴𝑘)))
7464, 73eqtri 2632 . . . . . 6 𝐵 = (𝑘 ∈ ℕ ↦ (log‘(𝐴𝑘)))
7574a1i 11 . . . . 5 (𝑁 ∈ ℕ → 𝐵 = (𝑘 ∈ ℕ ↦ (log‘(𝐴𝑘))))
76 simpr 476 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → 𝑘 = (𝑁 + 1))
7776fveq2d 6107 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (𝐴𝑘) = (𝐴‘(𝑁 + 1)))
7877fveq2d 6107 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (log‘(𝐴𝑘)) = (log‘(𝐴‘(𝑁 + 1))))
7953stirlinglem2 38968 . . . . . . 7 ((𝑁 + 1) ∈ ℕ → (𝐴‘(𝑁 + 1)) ∈ ℝ+)
8021, 79syl 17 . . . . . 6 (𝑁 ∈ ℕ → (𝐴‘(𝑁 + 1)) ∈ ℝ+)
8180relogcld 24173 . . . . 5 (𝑁 ∈ ℕ → (log‘(𝐴‘(𝑁 + 1))) ∈ ℝ)
8275, 78, 21, 81fvmptd 6197 . . . 4 (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) = (log‘(𝐴‘(𝑁 + 1))))
8366, 82oveq12d 6567 . . 3 (𝑁 ∈ ℕ → ((𝐵𝑁) − (𝐵‘(𝑁 + 1))) = ((log‘(𝐴𝑁)) − (log‘(𝐴‘(𝑁 + 1)))))
8454, 80relogdivd 24176 . . 3 (𝑁 ∈ ℕ → (log‘((𝐴𝑁) / (𝐴‘(𝑁 + 1)))) = ((log‘(𝐴𝑁)) − (log‘(𝐴‘(𝑁 + 1)))))
85 faccl 12932 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
86 nnrp 11718 . . . . . . . . 9 ((!‘𝑁) ∈ ℕ → (!‘𝑁) ∈ ℝ+)
872, 85, 863syl 18 . . . . . . . 8 (𝑁 ∈ ℕ → (!‘𝑁) ∈ ℝ+)
8831, 5rpmulcld 11764 . . . . . . . . . 10 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ+)
8988rpsqrtcld 13998 . . . . . . . . 9 (𝑁 ∈ ℕ → (√‘(2 · 𝑁)) ∈ ℝ+)
905, 12rpdivcld 11765 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 / e) ∈ ℝ+)
9190, 8rpexpcld 12894 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) ∈ ℝ+)
9289, 91rpmulcld 11764 . . . . . . . 8 (𝑁 ∈ ℕ → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ∈ ℝ+)
9387, 92rpdivcld 11765 . . . . . . 7 (𝑁 ∈ ℕ → ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+)
9453a1i 11 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))))
95 simpr 476 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁)
9695fveq2d 6107 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → (!‘𝑛) = (!‘𝑁))
9795oveq2d 6565 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → (2 · 𝑛) = (2 · 𝑁))
9897fveq2d 6107 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
9995oveq1d 6564 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → (𝑛 / e) = (𝑁 / e))
10099, 95oveq12d 6567 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → ((𝑛 / e)↑𝑛) = ((𝑁 / e)↑𝑁))
10198, 100oveq12d 6567 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)))
10296, 101oveq12d 6567 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
103 simpl 472 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ∈ ℕ)
10487rpcnd 11750 . . . . . . . . . 10 (𝑁 ∈ ℕ → (!‘𝑁) ∈ ℂ)
105104adantr 480 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → (!‘𝑁) ∈ ℂ)
106 2cnd 10970 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 2 ∈ ℂ)
107103nncnd 10913 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ∈ ℂ)
108106, 107mulcld 9939 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → (2 · 𝑁) ∈ ℂ)
109108sqrtcld 14024 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → (√‘(2 · 𝑁)) ∈ ℂ)
110 ere 14658 . . . . . . . . . . . . . 14 e ∈ ℝ
111110recni 9931 . . . . . . . . . . . . 13 e ∈ ℂ
112111a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → e ∈ ℂ)
113 0re 9919 . . . . . . . . . . . . . 14 0 ∈ ℝ
114 epos 14774 . . . . . . . . . . . . . 14 0 < e
115113, 114gtneii 10028 . . . . . . . . . . . . 13 e ≠ 0
116115a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → e ≠ 0)
117107, 112, 116divcld 10680 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → (𝑁 / e) ∈ ℂ)
118103nnnn0d 11228 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ∈ ℕ0)
119117, 118expcld 12870 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → ((𝑁 / e)↑𝑁) ∈ ℂ)
120109, 119mulcld 9939 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ∈ ℂ)
12189rpne0d 11753 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (√‘(2 · 𝑁)) ≠ 0)
122121adantr 480 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → (√‘(2 · 𝑁)) ≠ 0)
123103nnne0d 10942 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ≠ 0)
124107, 112, 123, 116divne0d 10696 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → (𝑁 / e) ≠ 0)
125103nnzd 11357 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ∈ ℤ)
126117, 124, 125expne0d 12876 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → ((𝑁 / e)↑𝑁) ≠ 0)
127109, 119, 122, 126mulne0d 10558 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ≠ 0)
128105, 120, 127divcld 10680 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℂ)
12994, 102, 103, 128fvmptd 6197 . . . . . . 7 ((𝑁 ∈ ℕ ∧ ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → (𝐴𝑁) = ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
13093, 129mpdan 699 . . . . . 6 (𝑁 ∈ ℕ → (𝐴𝑁) = ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
131 nfcv 2751 . . . . . . . . . 10 𝑘((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))
132 nfcv 2751 . . . . . . . . . 10 𝑛((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)))
133 fveq2 6103 . . . . . . . . . . 11 (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘))
134 oveq2 6557 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘))
135134fveq2d 6107 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑘)))
136 oveq1 6556 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑛 / e) = (𝑘 / e))
137 id 22 . . . . . . . . . . . . 13 (𝑛 = 𝑘𝑛 = 𝑘)
138136, 137oveq12d 6567 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((𝑛 / e)↑𝑛) = ((𝑘 / e)↑𝑘))
139135, 138oveq12d 6567 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)))
140133, 139oveq12d 6567 . . . . . . . . . 10 (𝑛 = 𝑘 → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))))
141131, 132, 140cbvmpt 4677 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) = (𝑘 ∈ ℕ ↦ ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))))
14253, 141eqtri 2632 . . . . . . . 8 𝐴 = (𝑘 ∈ ℕ ↦ ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))))
143142a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 𝐴 = (𝑘 ∈ ℕ ↦ ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)))))
14476fveq2d 6107 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (!‘𝑘) = (!‘(𝑁 + 1)))
14576oveq2d 6565 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (2 · 𝑘) = (2 · (𝑁 + 1)))
146145fveq2d 6107 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (√‘(2 · 𝑘)) = (√‘(2 · (𝑁 + 1))))
14776oveq1d 6564 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (𝑘 / e) = ((𝑁 + 1) / e))
148147, 76oveq12d 6567 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → ((𝑘 / e)↑𝑘) = (((𝑁 + 1) / e)↑(𝑁 + 1)))
149146, 148oveq12d 6567 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)) = ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
150144, 149oveq12d 6567 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))) = ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))
15121nnnn0d 11228 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
152 faccl 12932 . . . . . . . . 9 ((𝑁 + 1) ∈ ℕ0 → (!‘(𝑁 + 1)) ∈ ℕ)
153 nnrp 11718 . . . . . . . . 9 ((!‘(𝑁 + 1)) ∈ ℕ → (!‘(𝑁 + 1)) ∈ ℝ+)
154151, 152, 1533syl 18 . . . . . . . 8 (𝑁 ∈ ℕ → (!‘(𝑁 + 1)) ∈ ℝ+)
15531, 4rpmulcld 11764 . . . . . . . . . 10 (𝑁 ∈ ℕ → (2 · (𝑁 + 1)) ∈ ℝ+)
156155rpsqrtcld 13998 . . . . . . . . 9 (𝑁 ∈ ℕ → (√‘(2 · (𝑁 + 1))) ∈ ℝ+)
1574, 12rpdivcld 11765 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((𝑁 + 1) / e) ∈ ℝ+)
1588peano2zd 11361 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℤ)
159157, 158rpexpcld 12894 . . . . . . . . 9 (𝑁 ∈ ℕ → (((𝑁 + 1) / e)↑(𝑁 + 1)) ∈ ℝ+)
160156, 159rpmulcld 11764 . . . . . . . 8 (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ∈ ℝ+)
161154, 160rpdivcld 11765 . . . . . . 7 (𝑁 ∈ ℕ → ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) ∈ ℝ+)
162143, 150, 21, 161fvmptd 6197 . . . . . 6 (𝑁 ∈ ℕ → (𝐴‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))
163130, 162oveq12d 6567 . . . . 5 (𝑁 ∈ ℕ → ((𝐴𝑁) / (𝐴‘(𝑁 + 1))) = (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
164 facp1 12927 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1)))
1652, 164syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1)))
166165oveq1d 6564 . . . . . . . 8 (𝑁 ∈ ℕ → ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) = (((!‘𝑁) · (𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))
167160rpcnd 11750 . . . . . . . . 9 (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ∈ ℂ)
168160rpne0d 11753 . . . . . . . . 9 (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ≠ 0)
169104, 22, 167, 168divassd 10715 . . . . . . . 8 (𝑁 ∈ ℕ → (((!‘𝑁) · (𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) = ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
170166, 169eqtrd 2644 . . . . . . 7 (𝑁 ∈ ℕ → ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) = ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
171170oveq2d 6565 . . . . . 6 (𝑁 ∈ ℕ → (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))))
17292rpcnd 11750 . . . . . . 7 (𝑁 ∈ ℕ → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ∈ ℂ)
17322, 167, 168divcld 10680 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) ∈ ℂ)
174104, 173mulcld 9939 . . . . . . 7 (𝑁 ∈ ℕ → ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) ∈ ℂ)
17592rpne0d 11753 . . . . . . 7 (𝑁 ∈ ℕ → ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ≠ 0)
17687rpne0d 11753 . . . . . . . 8 (𝑁 ∈ ℕ → (!‘𝑁) ≠ 0)
17722, 167, 26, 168divne0d 10696 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) ≠ 0)
178104, 173, 176, 177mulne0d 10558 . . . . . . 7 (𝑁 ∈ ℕ → ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) ≠ 0)
179104, 172, 174, 175, 178divdiv32d 10705 . . . . . 6 (𝑁 ∈ ℕ → (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) = (((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
180104, 104, 173, 176, 177divdiv1d 10711 . . . . . . . . 9 (𝑁 ∈ ℕ → (((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = ((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))))
181180eqcomd 2616 . . . . . . . 8 (𝑁 ∈ ℕ → ((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) = (((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
182181oveq1d 6564 . . . . . . 7 (𝑁 ∈ ℕ → (((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
183104, 176dividd 10678 . . . . . . . . 9 (𝑁 ∈ ℕ → ((!‘𝑁) / (!‘𝑁)) = 1)
184183oveq1d 6564 . . . . . . . 8 (𝑁 ∈ ℕ → (((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = (1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))
185184oveq1d 6564 . . . . . . 7 (𝑁 ∈ ℕ → ((((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
18622, 167, 26, 168recdivd 10697 . . . . . . . . 9 (𝑁 ∈ ℕ → (1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = (((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)))
187186oveq1d 6564 . . . . . . . 8 (𝑁 ∈ ℕ → ((1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
188167, 22, 26divcld 10680 . . . . . . . . . 10 (𝑁 ∈ ℕ → (((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) ∈ ℂ)
18989rpcnd 11750 . . . . . . . . . 10 (𝑁 ∈ ℕ → (√‘(2 · 𝑁)) ∈ ℂ)
19091rpcnd 11750 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) ∈ ℂ)
19191rpne0d 11753 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) ≠ 0)
192188, 189, 190, 121, 191divdiv1d 10711 . . . . . . . . 9 (𝑁 ∈ ℕ → (((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) / ((𝑁 / e)↑𝑁)) = ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))))
193167, 22, 189, 26, 121divdiv32d 10705 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) = ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) / (𝑁 + 1)))
194156rpcnd 11750 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (√‘(2 · (𝑁 + 1))) ∈ ℂ)
195159rpcnd 11750 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (((𝑁 + 1) / e)↑(𝑁 + 1)) ∈ ℂ)
196194, 195, 189, 121div23d 10717 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) = (((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
19731rpred 11748 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 2 ∈ ℝ)
19831rpge0d 11752 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 2)
19921nnred 10912 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
200151nn0ge0d 11231 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ (𝑁 + 1))
201197, 198, 199, 200sqrtmuld 14011 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (√‘(2 · (𝑁 + 1))) = ((√‘2) · (√‘(𝑁 + 1))))
202197, 198, 1, 3sqrtmuld 14011 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
203201, 202oveq12d 6567 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) = (((√‘2) · (√‘(𝑁 + 1))) / ((√‘2) · (√‘𝑁))))
20429sqrtcld 14024 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (√‘2) ∈ ℂ)
20522sqrtcld 14024 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (√‘(𝑁 + 1)) ∈ ℂ)
20623sqrtcld 14024 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (√‘𝑁) ∈ ℂ)
20731rpsqrtcld 13998 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (√‘2) ∈ ℝ+)
208207rpne0d 11753 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (√‘2) ≠ 0)
2095rpsqrtcld 13998 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (√‘𝑁) ∈ ℝ+)
210209rpne0d 11753 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (√‘𝑁) ≠ 0)
211204, 204, 205, 206, 208, 210divmuldivd 10721 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (((√‘2) / (√‘2)) · ((√‘(𝑁 + 1)) / (√‘𝑁))) = (((√‘2) · (√‘(𝑁 + 1))) / ((√‘2) · (√‘𝑁))))
212204, 208dividd 10678 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → ((√‘2) / (√‘2)) = 1)
213199, 200, 5sqrtdivd 14010 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (√‘((𝑁 + 1) / 𝑁)) = ((√‘(𝑁 + 1)) / (√‘𝑁)))
214213eqcomd 2616 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → ((√‘(𝑁 + 1)) / (√‘𝑁)) = (√‘((𝑁 + 1) / 𝑁)))
215212, 214oveq12d 6567 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (((√‘2) / (√‘2)) · ((√‘(𝑁 + 1)) / (√‘𝑁))) = (1 · (√‘((𝑁 + 1) / 𝑁))))
216203, 211, 2153eqtr2d 2650 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) = (1 · (√‘((𝑁 + 1) / 𝑁))))
217216oveq1d 6564 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) = ((1 · (√‘((𝑁 + 1) / 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
21825sqrtcld 14024 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → (√‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
219218mulid2d 9937 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (1 · (√‘((𝑁 + 1) / 𝑁))) = (√‘((𝑁 + 1) / 𝑁)))
220219oveq1d 6564 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((1 · (√‘((𝑁 + 1) / 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
221196, 217, 2203eqtrd 2648 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))))
222221oveq1d 6564 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) / (𝑁 + 1)) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)))
223193, 222eqtrd 2644 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)))
224223oveq1d 6564 . . . . . . . . 9 (𝑁 ∈ ℕ → (((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) / ((𝑁 / e)↑𝑁)) = ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)))
225192, 224eqtr3d 2646 . . . . . . . 8 (𝑁 ∈ ℕ → ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)))
226218, 195mulcld 9939 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ∈ ℂ)
227226, 22, 190, 26, 191divdiv32d 10705 . . . . . . . . 9 (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)) = ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) / (𝑁 + 1)))
228218, 195, 190, 191divassd 10715 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) = ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1) / e)↑(𝑁 + 1)) / ((𝑁 / e)↑𝑁))))
22912rpcnd 11750 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → e ∈ ℂ)
23012rpne0d 11753 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → e ≠ 0)
23122, 229, 230, 151expdivd 12884 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((𝑁 + 1) / e)↑(𝑁 + 1)) = (((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))))
23223, 229, 230, 2expdivd 12884 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) = ((𝑁𝑁) / (e↑𝑁)))
233231, 232oveq12d 6567 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((((𝑁 + 1) / e)↑(𝑁 + 1)) / ((𝑁 / e)↑𝑁)) = ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁𝑁) / (e↑𝑁))))
234233oveq2d 6565 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1) / e)↑(𝑁 + 1)) / ((𝑁 / e)↑𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁𝑁) / (e↑𝑁)))))
23522, 151expcld 12870 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((𝑁 + 1)↑(𝑁 + 1)) ∈ ℂ)
236229, 151expcld 12870 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (e↑(𝑁 + 1)) ∈ ℂ)
23723, 2expcld 12870 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (𝑁𝑁) ∈ ℂ)
238229, 2expcld 12870 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (e↑𝑁) ∈ ℂ)
239229, 230, 158expne0d 12876 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (e↑(𝑁 + 1)) ≠ 0)
240229, 230, 8expne0d 12876 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (e↑𝑁) ≠ 0)
24123, 24, 8expne0d 12876 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (𝑁𝑁) ≠ 0)
242235, 236, 237, 238, 239, 240, 241divdivdivd 10727 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁𝑁) / (e↑𝑁))) = ((((𝑁 + 1)↑(𝑁 + 1)) · (e↑𝑁)) / ((e↑(𝑁 + 1)) · (𝑁𝑁))))
243235, 238mulcomd 9940 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) · (e↑𝑁)) = ((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))))
244243oveq1d 6564 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) · (e↑𝑁)) / ((e↑(𝑁 + 1)) · (𝑁𝑁))) = (((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))) / ((e↑(𝑁 + 1)) · (𝑁𝑁))))
245238, 236, 235, 237, 239, 241divmuldivd 10721 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (((e↑𝑁) / (e↑(𝑁 + 1))) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) = (((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))) / ((e↑(𝑁 + 1)) · (𝑁𝑁))))
246229, 2expp1d 12871 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (e↑(𝑁 + 1)) = ((e↑𝑁) · e))
247246oveq2d 6565 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → ((e↑𝑁) / (e↑(𝑁 + 1))) = ((e↑𝑁) / ((e↑𝑁) · e)))
248238, 238, 229, 240, 230divdiv1d 10711 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (((e↑𝑁) / (e↑𝑁)) / e) = ((e↑𝑁) / ((e↑𝑁) · e)))
249238, 240dividd 10678 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → ((e↑𝑁) / (e↑𝑁)) = 1)
250249oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (((e↑𝑁) / (e↑𝑁)) / e) = (1 / e))
251247, 248, 2503eqtr2d 2650 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → ((e↑𝑁) / (e↑(𝑁 + 1))) = (1 / e))
252251oveq1d 6564 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (((e↑𝑁) / (e↑(𝑁 + 1))) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) = ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))))
253245, 252eqtr3d 2646 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))) / ((e↑(𝑁 + 1)) · (𝑁𝑁))) = ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))))
254242, 244, 2533eqtrd 2648 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁𝑁) / (e↑𝑁))) = ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))))
255254oveq2d 6565 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁𝑁) / (e↑𝑁)))) = ((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)))))
256228, 234, 2553eqtrd 2648 . . . . . . . . . 10 (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) = ((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)))))
257256oveq1d 6564 . . . . . . . . 9 (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) / (𝑁 + 1)) = (((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)))) / (𝑁 + 1)))
258235, 237, 241divcld 10680 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) ∈ ℂ)
25935, 229, 258, 230div32d 10703 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) = (1 · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / e)))
260258, 229, 230divcld 10680 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / e) ∈ ℂ)
261260mulid2d 9937 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / e)) = ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / e))
262259, 261eqtrd 2644 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) = ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / e))
263262oveq2d 6565 . . . . . . . . . 10 (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)))) = (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / e)))
264229, 230reccld 10673 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / e) ∈ ℂ)
265264, 258mulcld 9939 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) ∈ ℂ)
266218, 265, 22, 26div23d 10717 . . . . . . . . . 10 (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)))) / (𝑁 + 1)) = (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)))))
267218, 22, 26divcld 10680 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) ∈ ℂ)
268267, 258, 229, 230divassd 10715 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) / e) = (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / e)))
269263, 266, 2683eqtr4d 2654 . . . . . . . . 9 (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)))) / (𝑁 + 1)) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) / e))
270227, 257, 2693eqtrd 2648 . . . . . . . 8 (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) / e))
271187, 225, 2703eqtrd 2648 . . . . . . 7 (𝑁 ∈ ℕ → ((1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) / e))
272182, 185, 2713eqtrd 2648 . . . . . 6 (𝑁 ∈ ℕ → (((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) / e))
273171, 179, 2723eqtrd 2648 . . . . 5 (𝑁 ∈ ℕ → (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) / e))
274218, 22, 258, 26div32d 10703 . . . . . . 7 (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / (𝑁 + 1))))
27522, 2expp1d 12871 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((𝑁 + 1)↑(𝑁 + 1)) = (((𝑁 + 1)↑𝑁) · (𝑁 + 1)))
276275oveq1d 6564 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) = ((((𝑁 + 1)↑𝑁) · (𝑁 + 1)) / (𝑁 + 1)))
27722, 2expcld 12870 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((𝑁 + 1)↑𝑁) ∈ ℂ)
278277, 22, 26divcan4d 10686 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((((𝑁 + 1)↑𝑁) · (𝑁 + 1)) / (𝑁 + 1)) = ((𝑁 + 1)↑𝑁))
279276, 278eqtrd 2644 . . . . . . . . . 10 (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) = ((𝑁 + 1)↑𝑁))
280279oveq1d 6564 . . . . . . . . 9 (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) / (𝑁𝑁)) = (((𝑁 + 1)↑𝑁) / (𝑁𝑁)))
281235, 237, 22, 241, 26divdiv32d 10705 . . . . . . . . 9 (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / (𝑁 + 1)) = ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) / (𝑁𝑁)))
28222, 23, 24, 2expdivd 12884 . . . . . . . . 9 (𝑁 ∈ ℕ → (((𝑁 + 1) / 𝑁)↑𝑁) = (((𝑁 + 1)↑𝑁) / (𝑁𝑁)))
283280, 281, 2823eqtr4d 2654 . . . . . . . 8 (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / (𝑁 + 1)) = (((𝑁 + 1) / 𝑁)↑𝑁))
284283oveq2d 6565 . . . . . . 7 (𝑁 ∈ ℕ → ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁)) / (𝑁 + 1))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)))
285274, 284eqtrd 2644 . . . . . 6 (𝑁 ∈ ℕ → (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)))
286285oveq1d 6564 . . . . 5 (𝑁 ∈ ℕ → ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁𝑁))) / e) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e))
287163, 273, 2863eqtrd 2648 . . . 4 (𝑁 ∈ ℕ → ((𝐴𝑁) / (𝐴‘(𝑁 + 1))) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e))
288287fveq2d 6107 . . 3 (𝑁 ∈ ℕ → (log‘((𝐴𝑁) / (𝐴‘(𝑁 + 1)))) = (log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)))
28983, 84, 2883eqtr2d 2650 . 2 (𝑁 ∈ ℕ → ((𝐵𝑁) − (𝐵‘(𝑁 + 1))) = (log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)))
29035, 43addcld 9938 . . . . . 6 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) ∈ ℂ)
291290halfcld 11154 . . . . 5 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
292291, 28mulcld 9939 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) ∈ ℂ)
293292, 35subcld 10271 . . 3 (𝑁 ∈ ℕ → ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
294 stirlinglem4.3 . . . . 5 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))
295294a1i 11 . . . 4 ((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) → 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1)))
296 simpr 476 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁)
297296oveq2d 6565 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (2 · 𝑛) = (2 · 𝑁))
298297oveq2d 6565 . . . . . . 7 (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (1 + (2 · 𝑛)) = (1 + (2 · 𝑁)))
299298oveq1d 6564 . . . . . 6 (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → ((1 + (2 · 𝑛)) / 2) = ((1 + (2 · 𝑁)) / 2))
300296oveq1d 6564 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (𝑛 + 1) = (𝑁 + 1))
301300, 296oveq12d 6567 . . . . . . 7 (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → ((𝑛 + 1) / 𝑛) = ((𝑁 + 1) / 𝑁))
302301fveq2d 6107 . . . . . 6 (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (log‘((𝑛 + 1) / 𝑛)) = (log‘((𝑁 + 1) / 𝑁)))
303299, 302oveq12d 6567 . . . . 5 (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → (((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
304303oveq1d 6564 . . . 4 (((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) ∧ 𝑛 = 𝑁) → ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
305 simpl 472 . . . 4 ((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) → 𝑁 ∈ ℕ)
306 simpr 476 . . . 4 ((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) → ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
307295, 304, 305, 306fvmptd 6197 . . 3 ((𝑁 ∈ ℕ ∧ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ) → (𝐽𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
308293, 307mpdan 699 . 2 (𝑁 ∈ ℕ → (𝐽𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
30952, 289, 3083eqtr4d 2654 1 (𝑁 ∈ ℕ → ((𝐵𝑁) − (𝐵‘(𝑁 + 1))) = (𝐽𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  wne 2780  cmpt 4643  cfv 5804  (class class class)co 6549  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  cmin 10145   / cdiv 10563  cn 10897  2c2 10947  0cn0 11169  cz 11254  +crp 11708  cexp 12722  !cfa 12922  csqrt 13821  eceu 14632  logclog 24105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-e 14638  df-sin 14639  df-cos 14640  df-pi 14642  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437  df-log 24107  df-cxp 24108
This theorem is referenced by:  stirlinglem9  38975
  Copyright terms: Public domain W3C validator