Step | Hyp | Ref
| Expression |
1 | | faclim2.1 |
. 2
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀)))) |
2 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑎 = 0 → ((𝑛 + 1)↑𝑎) = ((𝑛 + 1)↑0)) |
3 | 2 | oveq2d 6565 |
. . . . . 6
⊢ (𝑎 = 0 → ((!‘𝑛) · ((𝑛 + 1)↑𝑎)) = ((!‘𝑛) · ((𝑛 + 1)↑0))) |
4 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑎 = 0 → (𝑛 + 𝑎) = (𝑛 + 0)) |
5 | 4 | fveq2d 6107 |
. . . . . 6
⊢ (𝑎 = 0 → (!‘(𝑛 + 𝑎)) = (!‘(𝑛 + 0))) |
6 | 3, 5 | oveq12d 6567 |
. . . . 5
⊢ (𝑎 = 0 → (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎))) = (((!‘𝑛) · ((𝑛 + 1)↑0)) / (!‘(𝑛 + 0)))) |
7 | 6 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = 0 → (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎)))) = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑0)) / (!‘(𝑛 + 0))))) |
8 | 7 | breq1d 4593 |
. . 3
⊢ (𝑎 = 0 → ((𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎)))) ⇝ 1 ↔ (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑0)) / (!‘(𝑛 + 0)))) ⇝ 1)) |
9 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑎 = 𝑚 → ((𝑛 + 1)↑𝑎) = ((𝑛 + 1)↑𝑚)) |
10 | 9 | oveq2d 6565 |
. . . . . 6
⊢ (𝑎 = 𝑚 → ((!‘𝑛) · ((𝑛 + 1)↑𝑎)) = ((!‘𝑛) · ((𝑛 + 1)↑𝑚))) |
11 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑎 = 𝑚 → (𝑛 + 𝑎) = (𝑛 + 𝑚)) |
12 | 11 | fveq2d 6107 |
. . . . . 6
⊢ (𝑎 = 𝑚 → (!‘(𝑛 + 𝑎)) = (!‘(𝑛 + 𝑚))) |
13 | 10, 12 | oveq12d 6567 |
. . . . 5
⊢ (𝑎 = 𝑚 → (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎))) = (((!‘𝑛) · ((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚)))) |
14 | 13 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = 𝑚 → (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎)))) = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚))))) |
15 | 14 | breq1d 4593 |
. . 3
⊢ (𝑎 = 𝑚 → ((𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎)))) ⇝ 1 ↔ (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚)))) ⇝ 1)) |
16 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑎 = (𝑚 + 1) → ((𝑛 + 1)↑𝑎) = ((𝑛 + 1)↑(𝑚 + 1))) |
17 | 16 | oveq2d 6565 |
. . . . . 6
⊢ (𝑎 = (𝑚 + 1) → ((!‘𝑛) · ((𝑛 + 1)↑𝑎)) = ((!‘𝑛) · ((𝑛 + 1)↑(𝑚 + 1)))) |
18 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑎 = (𝑚 + 1) → (𝑛 + 𝑎) = (𝑛 + (𝑚 + 1))) |
19 | 18 | fveq2d 6107 |
. . . . . 6
⊢ (𝑎 = (𝑚 + 1) → (!‘(𝑛 + 𝑎)) = (!‘(𝑛 + (𝑚 + 1)))) |
20 | 17, 19 | oveq12d 6567 |
. . . . 5
⊢ (𝑎 = (𝑚 + 1) → (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎))) = (((!‘𝑛) · ((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1))))) |
21 | 20 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = (𝑚 + 1) → (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎)))) = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1)))))) |
22 | 21 | breq1d 4593 |
. . 3
⊢ (𝑎 = (𝑚 + 1) → ((𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎)))) ⇝ 1 ↔ (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1))))) ⇝ 1)) |
23 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑎 = 𝑀 → ((𝑛 + 1)↑𝑎) = ((𝑛 + 1)↑𝑀)) |
24 | 23 | oveq2d 6565 |
. . . . . 6
⊢ (𝑎 = 𝑀 → ((!‘𝑛) · ((𝑛 + 1)↑𝑎)) = ((!‘𝑛) · ((𝑛 + 1)↑𝑀))) |
25 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑎 = 𝑀 → (𝑛 + 𝑎) = (𝑛 + 𝑀)) |
26 | 25 | fveq2d 6107 |
. . . . . 6
⊢ (𝑎 = 𝑀 → (!‘(𝑛 + 𝑎)) = (!‘(𝑛 + 𝑀))) |
27 | 24, 26 | oveq12d 6567 |
. . . . 5
⊢ (𝑎 = 𝑀 → (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎))) = (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀)))) |
28 | 27 | mpteq2dv 4673 |
. . . 4
⊢ (𝑎 = 𝑀 → (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎)))) = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀))))) |
29 | 28 | breq1d 4593 |
. . 3
⊢ (𝑎 = 𝑀 → ((𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑎)) / (!‘(𝑛 + 𝑎)))) ⇝ 1 ↔ (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀)))) ⇝ 1)) |
30 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
31 | | 1zzd 11285 |
. . . . 5
⊢ (⊤
→ 1 ∈ ℤ) |
32 | | nnex 10903 |
. . . . . . 7
⊢ ℕ
∈ V |
33 | 32 | mptex 6390 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑0)) /
(!‘(𝑛 + 0)))) ∈
V |
34 | 33 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 + 1)↑0))
/ (!‘(𝑛 + 0))))
∈ V) |
35 | | 1cnd 9935 |
. . . . 5
⊢ (⊤
→ 1 ∈ ℂ) |
36 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (!‘𝑛) = (!‘𝑚)) |
37 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑛 + 1) = (𝑚 + 1)) |
38 | 37 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((𝑛 + 1)↑0) = ((𝑚 + 1)↑0)) |
39 | 36, 38 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → ((!‘𝑛) · ((𝑛 + 1)↑0)) = ((!‘𝑚) · ((𝑚 + 1)↑0))) |
40 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝑛 + 0) = (𝑚 + 0)) |
41 | 40 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (!‘(𝑛 + 0)) = (!‘(𝑚 + 0))) |
42 | 39, 41 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (((!‘𝑛) · ((𝑛 + 1)↑0)) / (!‘(𝑛 + 0))) = (((!‘𝑚) · ((𝑚 + 1)↑0)) / (!‘(𝑚 + 0)))) |
43 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑0)) /
(!‘(𝑛 + 0)))) =
(𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑0)) /
(!‘(𝑛 +
0)))) |
44 | | ovex 6577 |
. . . . . . . 8
⊢
(((!‘𝑚)
· ((𝑚 + 1)↑0))
/ (!‘(𝑚 + 0))) ∈
V |
45 | 42, 43, 44 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑0)) /
(!‘(𝑛 +
0))))‘𝑚) =
(((!‘𝑚) ·
((𝑚 + 1)↑0)) /
(!‘(𝑚 +
0)))) |
46 | | peano2nn 10909 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
47 | 46 | nncnd 10913 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℂ) |
48 | 47 | exp0d 12864 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → ((𝑚 + 1)↑0) =
1) |
49 | 48 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ →
((!‘𝑚) ·
((𝑚 + 1)↑0)) =
((!‘𝑚) ·
1)) |
50 | | nnnn0 11176 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ0) |
51 | | faccl 12932 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ (!‘𝑚) ∈
ℕ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ →
(!‘𝑚) ∈
ℕ) |
53 | 52 | nncnd 10913 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ →
(!‘𝑚) ∈
ℂ) |
54 | 53 | mulid1d 9936 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ →
((!‘𝑚) · 1) =
(!‘𝑚)) |
55 | 49, 54 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ →
((!‘𝑚) ·
((𝑚 + 1)↑0)) =
(!‘𝑚)) |
56 | | nncn 10905 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
57 | 56 | addid1d 10115 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → (𝑚 + 0) = 𝑚) |
58 | 57 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ →
(!‘(𝑚 + 0)) =
(!‘𝑚)) |
59 | 55, 58 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ →
(((!‘𝑚) ·
((𝑚 + 1)↑0)) /
(!‘(𝑚 + 0))) =
((!‘𝑚) /
(!‘𝑚))) |
60 | 52 | nnne0d 10942 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ →
(!‘𝑚) ≠
0) |
61 | 53, 60 | dividd 10678 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ →
((!‘𝑚) /
(!‘𝑚)) =
1) |
62 | 45, 59, 61 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑0)) /
(!‘(𝑛 +
0))))‘𝑚) =
1) |
63 | 62 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑚
∈ ℕ) → ((𝑛
∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑0)) / (!‘(𝑛 + 0))))‘𝑚) = 1) |
64 | 30, 31, 34, 35, 63 | climconst 14122 |
. . . 4
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 + 1)↑0))
/ (!‘(𝑛 + 0))))
⇝ 1) |
65 | 64 | trud 1484 |
. . 3
⊢ (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑0)) /
(!‘(𝑛 + 0)))) ⇝
1 |
66 | | 1zzd 11285 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1) → 1 ∈
ℤ) |
67 | | simpr 476 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1) → (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚)))) ⇝ 1) |
68 | 32 | mptex 6390 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1))))) ∈ V |
69 | 68 | a1i 11 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1) → (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1))))) ∈ V) |
70 | | 1zzd 11285 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ 1 ∈ ℤ) |
71 | | 1cnd 9935 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ 1 ∈ ℂ) |
72 | | nn0p1nn 11209 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ) |
73 | 72 | nnzd 11357 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℤ) |
74 | 32 | mptex 6390 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1)))) ∈ V |
75 | 74 | a1i 11 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ (𝑛 ∈ ℕ
↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1)))) ∈ V) |
76 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) |
77 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛 + (𝑚 + 1)) = (𝑘 + (𝑚 + 1))) |
78 | 76, 77 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝑛 + 1) / (𝑛 + (𝑚 + 1))) = ((𝑘 + 1) / (𝑘 + (𝑚 + 1)))) |
79 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1)))) = (𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1)))) |
80 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝑘 + 1) / (𝑘 + (𝑚 + 1))) ∈ V |
81 | 78, 79, 80 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))))‘𝑘) = ((𝑘 + 1) / (𝑘 + (𝑚 + 1)))) |
82 | 81 | adantl 481 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))))‘𝑘) = ((𝑘 + 1) / (𝑘 + (𝑚 + 1)))) |
83 | 30, 70, 71, 73, 75, 82 | divcnvlin 30871 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ (𝑛 ∈ ℕ
↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1)))) ⇝ 1) |
84 | 83 | adantr 480 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1) → (𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1)))) ⇝ 1) |
85 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ 𝑛 ∈
ℕ) |
86 | 85 | nnnn0d 11228 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ 𝑛 ∈
ℕ0) |
87 | | faccl 12932 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
→ (!‘𝑛) ∈
ℕ) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (!‘𝑛) ∈
ℕ) |
89 | | peano2nn 10909 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
90 | | nnexpcl 12735 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 + 1) ∈ ℕ ∧ 𝑚 ∈ ℕ0)
→ ((𝑛 + 1)↑𝑚) ∈
ℕ) |
91 | 89, 90 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ0)
→ ((𝑛 + 1)↑𝑚) ∈
ℕ) |
92 | 91 | ancoms 468 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((𝑛 + 1)↑𝑚) ∈
ℕ) |
93 | 88, 92 | nnmulcld 10945 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) ∈
ℕ) |
94 | 93 | nnred 10912 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) ∈
ℝ) |
95 | | nnnn0addcl 11200 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ0)
→ (𝑛 + 𝑚) ∈
ℕ) |
96 | 95 | ancoms 468 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑛 + 𝑚) ∈
ℕ) |
97 | 96 | nnnn0d 11228 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑛 + 𝑚) ∈
ℕ0) |
98 | | faccl 12932 |
. . . . . . . . . . . 12
⊢ ((𝑛 + 𝑚) ∈ ℕ0 →
(!‘(𝑛 + 𝑚)) ∈
ℕ) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (!‘(𝑛 + 𝑚)) ∈
ℕ) |
100 | 94, 99 | nndivred 10946 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚))) ∈
ℝ) |
101 | 100 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚))) ∈
ℂ) |
102 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚)))) = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚)))) |
103 | 101, 102 | fmptd 6292 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))):ℕ⟶ℂ) |
104 | 103 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚))))‘𝑘) ∈ ℂ) |
105 | 104 | adantlr 747 |
. . . . . 6
⊢ (((𝑚 ∈ ℕ0
∧ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚))))‘𝑘) ∈ ℂ) |
106 | 89 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑛 + 1) ∈
ℕ) |
107 | 106 | nnred 10912 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑛 + 1) ∈
ℝ) |
108 | 72 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑚 + 1) ∈
ℕ) |
109 | 85, 108 | nnaddcld 10944 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑛 + (𝑚 + 1)) ∈
ℕ) |
110 | 107, 109 | nndivred 10946 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))) ∈ ℝ) |
111 | 110 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))) ∈ ℂ) |
112 | 111, 79 | fmptd 6292 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ (𝑛 ∈ ℕ
↦ ((𝑛 + 1) / (𝑛 + (𝑚 +
1)))):ℕ⟶ℂ) |
113 | 112 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))))‘𝑘) ∈ ℂ) |
114 | 113 | adantlr 747 |
. . . . . 6
⊢ (((𝑚 ∈ ℕ0
∧ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))))‘𝑘) ∈ ℂ) |
115 | | peano2nn 10909 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
116 | 115 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℕ) |
117 | 116 | nncnd 10913 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℂ) |
118 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ 𝑚 ∈
ℕ0) |
119 | 117, 118 | expp1d 12871 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1)↑(𝑚 + 1)) = (((𝑘 + 1)↑𝑚) · (𝑘 + 1))) |
120 | 119 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((!‘𝑘)
· ((𝑘 +
1)↑(𝑚 + 1))) =
((!‘𝑘) ·
(((𝑘 + 1)↑𝑚) · (𝑘 + 1)))) |
121 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ) |
122 | 121 | nnnn0d 11228 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ0) |
123 | | faccl 12932 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (!‘𝑘) ∈
ℕ) |
125 | 124 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (!‘𝑘) ∈
ℂ) |
126 | | nnexpcl 12735 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑚 ∈ ℕ0)
→ ((𝑘 + 1)↑𝑚) ∈
ℕ) |
127 | 115, 126 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ0)
→ ((𝑘 + 1)↑𝑚) ∈
ℕ) |
128 | 127 | ancoms 468 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1)↑𝑚) ∈
ℕ) |
129 | 128 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1)↑𝑚) ∈
ℂ) |
130 | 125, 129,
117 | mulassd 9942 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (((!‘𝑘)
· ((𝑘 +
1)↑𝑚)) · (𝑘 + 1)) = ((!‘𝑘) · (((𝑘 + 1)↑𝑚) · (𝑘 + 1)))) |
131 | 120, 130 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((!‘𝑘)
· ((𝑘 +
1)↑(𝑚 + 1))) =
(((!‘𝑘) ·
((𝑘 + 1)↑𝑚)) · (𝑘 + 1))) |
132 | 122, 118 | nn0addcld 11232 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 𝑚) ∈
ℕ0) |
133 | | facp1 12927 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 𝑚) ∈ ℕ0 →
(!‘((𝑘 + 𝑚) + 1)) = ((!‘(𝑘 + 𝑚)) · ((𝑘 + 𝑚) + 1))) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (!‘((𝑘 + 𝑚) + 1)) = ((!‘(𝑘 + 𝑚)) · ((𝑘 + 𝑚) + 1))) |
135 | 121 | nncnd 10913 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℂ) |
136 | 118 | nn0cnd 11230 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ 𝑚 ∈
ℂ) |
137 | | 1cnd 9935 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ 1 ∈ ℂ) |
138 | 135, 136,
137 | addassd 9941 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 𝑚) + 1) = (𝑘 + (𝑚 + 1))) |
139 | 138 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (!‘((𝑘 + 𝑚) + 1)) = (!‘(𝑘 + (𝑚 + 1)))) |
140 | 138 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((!‘(𝑘 + 𝑚)) · ((𝑘 + 𝑚) + 1)) = ((!‘(𝑘 + 𝑚)) · (𝑘 + (𝑚 + 1)))) |
141 | 134, 139,
140 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (!‘(𝑘 + (𝑚 + 1))) = ((!‘(𝑘 + 𝑚)) · (𝑘 + (𝑚 + 1)))) |
142 | 131, 141 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (((!‘𝑘)
· ((𝑘 +
1)↑(𝑚 + 1))) /
(!‘(𝑘 + (𝑚 + 1)))) = ((((!‘𝑘) · ((𝑘 + 1)↑𝑚)) · (𝑘 + 1)) / ((!‘(𝑘 + 𝑚)) · (𝑘 + (𝑚 + 1))))) |
143 | 124, 128 | nnmulcld 10945 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((!‘𝑘)
· ((𝑘 +
1)↑𝑚)) ∈
ℕ) |
144 | 143 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((!‘𝑘)
· ((𝑘 +
1)↑𝑚)) ∈
ℂ) |
145 | | faccl 12932 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 𝑚) ∈ ℕ0 →
(!‘(𝑘 + 𝑚)) ∈
ℕ) |
146 | 132, 145 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (!‘(𝑘 + 𝑚)) ∈
ℕ) |
147 | 146 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (!‘(𝑘 + 𝑚)) ∈
ℂ) |
148 | 72 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (𝑚 + 1) ∈
ℕ) |
149 | 121, 148 | nnaddcld 10944 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (𝑘 + (𝑚 + 1)) ∈
ℕ) |
150 | 149 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (𝑘 + (𝑚 + 1)) ∈
ℂ) |
151 | 146 | nnne0d 10942 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (!‘(𝑘 + 𝑚)) ≠ 0) |
152 | 149 | nnne0d 10942 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (𝑘 + (𝑚 + 1)) ≠ 0) |
153 | 144, 147,
117, 150, 151, 152 | divmuldivd 10721 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((((!‘𝑘)
· ((𝑘 +
1)↑𝑚)) /
(!‘(𝑘 + 𝑚))) · ((𝑘 + 1) / (𝑘 + (𝑚 + 1)))) = ((((!‘𝑘) · ((𝑘 + 1)↑𝑚)) · (𝑘 + 1)) / ((!‘(𝑘 + 𝑚)) · (𝑘 + (𝑚 + 1))))) |
154 | 142, 153 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (((!‘𝑘)
· ((𝑘 +
1)↑(𝑚 + 1))) /
(!‘(𝑘 + (𝑚 + 1)))) = ((((!‘𝑘) · ((𝑘 + 1)↑𝑚)) / (!‘(𝑘 + 𝑚))) · ((𝑘 + 1) / (𝑘 + (𝑚 + 1))))) |
155 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘)) |
156 | 76 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → ((𝑛 + 1)↑(𝑚 + 1)) = ((𝑘 + 1)↑(𝑚 + 1))) |
157 | 155, 156 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((!‘𝑛) · ((𝑛 + 1)↑(𝑚 + 1))) = ((!‘𝑘) · ((𝑘 + 1)↑(𝑚 + 1)))) |
158 | 77 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (!‘(𝑛 + (𝑚 + 1))) = (!‘(𝑘 + (𝑚 + 1)))) |
159 | 157, 158 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (((!‘𝑛) · ((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1)))) = (((!‘𝑘) · ((𝑘 + 1)↑(𝑚 + 1))) / (!‘(𝑘 + (𝑚 + 1))))) |
160 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1))))) = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1))))) |
161 | | ovex 6577 |
. . . . . . . . . 10
⊢
(((!‘𝑘)
· ((𝑘 +
1)↑(𝑚 + 1))) /
(!‘(𝑘 + (𝑚 + 1)))) ∈
V |
162 | 159, 160,
161 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1)))))‘𝑘) = (((!‘𝑘) · ((𝑘 + 1)↑(𝑚 + 1))) / (!‘(𝑘 + (𝑚 + 1))))) |
163 | 162 | adantl 481 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑(𝑚 + 1))) /
(!‘(𝑛 + (𝑚 + 1)))))‘𝑘) = (((!‘𝑘) · ((𝑘 + 1)↑(𝑚 + 1))) / (!‘(𝑘 + (𝑚 + 1))))) |
164 | 76 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → ((𝑛 + 1)↑𝑚) = ((𝑘 + 1)↑𝑚)) |
165 | 155, 164 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → ((!‘𝑛) · ((𝑛 + 1)↑𝑚)) = ((!‘𝑘) · ((𝑘 + 1)↑𝑚))) |
166 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝑛 + 𝑚) = (𝑘 + 𝑚)) |
167 | 166 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (!‘(𝑛 + 𝑚)) = (!‘(𝑘 + 𝑚))) |
168 | 165, 167 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (((!‘𝑛) · ((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚))) = (((!‘𝑘) · ((𝑘 + 1)↑𝑚)) / (!‘(𝑘 + 𝑚)))) |
169 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(((!‘𝑘)
· ((𝑘 +
1)↑𝑚)) /
(!‘(𝑘 + 𝑚))) ∈ V |
170 | 168, 102,
169 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚))))‘𝑘) = (((!‘𝑘) · ((𝑘 + 1)↑𝑚)) / (!‘(𝑘 + 𝑚)))) |
171 | 170, 81 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (((𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚))))‘𝑘) · ((𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))))‘𝑘)) = ((((!‘𝑘) · ((𝑘 + 1)↑𝑚)) / (!‘(𝑘 + 𝑚))) · ((𝑘 + 1) / (𝑘 + (𝑚 + 1))))) |
172 | 171 | adantl 481 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ (((𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚))))‘𝑘) · ((𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))))‘𝑘)) = ((((!‘𝑘) · ((𝑘 + 1)↑𝑚)) / (!‘(𝑘 + 𝑚))) · ((𝑘 + 1) / (𝑘 + (𝑚 + 1))))) |
173 | 154, 163,
172 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝑘 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑(𝑚 + 1))) /
(!‘(𝑛 + (𝑚 + 1)))))‘𝑘) = (((𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚))))‘𝑘) · ((𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))))‘𝑘))) |
174 | 173 | adantlr 747 |
. . . . . 6
⊢ (((𝑚 ∈ ℕ0
∧ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1)))))‘𝑘) = (((𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑚)) / (!‘(𝑛 + 𝑚))))‘𝑘) · ((𝑛 ∈ ℕ ↦ ((𝑛 + 1) / (𝑛 + (𝑚 + 1))))‘𝑘))) |
175 | 30, 66, 67, 69, 84, 105, 114, 174 | climmul 14211 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1) → (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1))))) ⇝ (1 ·
1)) |
176 | | 1t1e1 11052 |
. . . . 5
⊢ (1
· 1) = 1 |
177 | 175, 176 | syl6breq 4624 |
. . . 4
⊢ ((𝑚 ∈ ℕ0
∧ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1) → (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1))))) ⇝ 1) |
178 | 177 | ex 449 |
. . 3
⊢ (𝑚 ∈ ℕ0
→ ((𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑚)) /
(!‘(𝑛 + 𝑚)))) ⇝ 1 → (𝑛 ∈ ℕ ↦
(((!‘𝑛) ·
((𝑛 + 1)↑(𝑚 + 1))) / (!‘(𝑛 + (𝑚 + 1))))) ⇝ 1)) |
179 | 8, 15, 22, 29, 65, 178 | nn0ind 11348 |
. 2
⊢ (𝑀 ∈ ℕ0
→ (𝑛 ∈ ℕ
↦ (((!‘𝑛)
· ((𝑛 +
1)↑𝑀)) /
(!‘(𝑛 + 𝑀)))) ⇝ 1) |
180 | 1, 179 | syl5eqbr 4618 |
1
⊢ (𝑀 ∈ ℕ0
→ 𝐹 ⇝
1) |