Metamath Proof Explorer

Theorem faclim2

Description: Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017)

Ref Expression
Hypothesis faclim2.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑀 ) ) / ( ! ‘ ( 𝑛 + 𝑀 ) ) ) )
Assertion faclim2 ( 𝑀 ∈ ℕ0 → 𝐹 ⇝ 1 )

Proof

Step Hyp Ref Expression
1 faclim2.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑀 ) ) / ( ! ‘ ( 𝑛 + 𝑀 ) ) ) )
2 oveq2 ⊢ ( 𝑎 = 0 → ( ( 𝑛 + 1 ) ↑ 𝑎 ) = ( ( 𝑛 + 1 ) ↑ 0 ) )
3 2 oveq2d ⊢ ( 𝑎 = 0 → ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) = ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) )
4 oveq2 ⊢ ( 𝑎 = 0 → ( 𝑛 + 𝑎 ) = ( 𝑛 + 0 ) )
5 4 fveq2d ⊢ ( 𝑎 = 0 → ( ! ‘ ( 𝑛 + 𝑎 ) ) = ( ! ‘ ( 𝑛 + 0 ) ) )
6 3 5 oveq12d ⊢ ( 𝑎 = 0 → ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) = ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) )
7 6 mpteq2dv ⊢ ( 𝑎 = 0 → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) )
8 7 breq1d ⊢ ( 𝑎 = 0 → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) ) ⇝ 1 ↔ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) ⇝ 1 ) )
9 oveq2 ⊢ ( 𝑎 = 𝑚 → ( ( 𝑛 + 1 ) ↑ 𝑎 ) = ( ( 𝑛 + 1 ) ↑ 𝑚 ) )
10 9 oveq2d ⊢ ( 𝑎 = 𝑚 → ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) = ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) )
11 oveq2 ⊢ ( 𝑎 = 𝑚 → ( 𝑛 + 𝑎 ) = ( 𝑛 + 𝑚 ) )
12 11 fveq2d ⊢ ( 𝑎 = 𝑚 → ( ! ‘ ( 𝑛 + 𝑎 ) ) = ( ! ‘ ( 𝑛 + 𝑚 ) ) )
13 10 12 oveq12d ⊢ ( 𝑎 = 𝑚 → ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) = ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) )
14 13 mpteq2dv ⊢ ( 𝑎 = 𝑚 → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) )
15 14 breq1d ⊢ ( 𝑎 = 𝑚 → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) ) ⇝ 1 ↔ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) )
16 oveq2 ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( ( 𝑛 + 1 ) ↑ 𝑎 ) = ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) )
17 16 oveq2d ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) = ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) )
18 oveq2 ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( 𝑛 + 𝑎 ) = ( 𝑛 + ( 𝑚 + 1 ) ) )
19 18 fveq2d ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( ! ‘ ( 𝑛 + 𝑎 ) ) = ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) )
20 17 19 oveq12d ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) = ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) )
21 20 mpteq2dv ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) )
22 21 breq1d ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) ) ⇝ 1 ↔ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ⇝ 1 ) )
23 oveq2 ⊢ ( 𝑎 = 𝑀 → ( ( 𝑛 + 1 ) ↑ 𝑎 ) = ( ( 𝑛 + 1 ) ↑ 𝑀 ) )
24 23 oveq2d ⊢ ( 𝑎 = 𝑀 → ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) = ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑀 ) ) )
25 oveq2 ⊢ ( 𝑎 = 𝑀 → ( 𝑛 + 𝑎 ) = ( 𝑛 + 𝑀 ) )
26 25 fveq2d ⊢ ( 𝑎 = 𝑀 → ( ! ‘ ( 𝑛 + 𝑎 ) ) = ( ! ‘ ( 𝑛 + 𝑀 ) ) )
27 24 26 oveq12d ⊢ ( 𝑎 = 𝑀 → ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) = ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑀 ) ) / ( ! ‘ ( 𝑛 + 𝑀 ) ) ) )
28 27 mpteq2dv ⊢ ( 𝑎 = 𝑀 → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑀 ) ) / ( ! ‘ ( 𝑛 + 𝑀 ) ) ) ) )
29 28 breq1d ⊢ ( 𝑎 = 𝑀 → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑎 ) ) / ( ! ‘ ( 𝑛 + 𝑎 ) ) ) ) ⇝ 1 ↔ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑀 ) ) / ( ! ‘ ( 𝑛 + 𝑀 ) ) ) ) ⇝ 1 ) )
30 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
31 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
32 nnex ⊢ ℕ ∈ V
33 32 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) ∈ V
34 33 a1i ⊢ ( ⊤ → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) ∈ V )
35 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
36 fveq2 ⊢ ( 𝑛 = 𝑚 → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑚 ) )
37 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 + 1 ) = ( 𝑚 + 1 ) )
38 37 oveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 + 1 ) ↑ 0 ) = ( ( 𝑚 + 1 ) ↑ 0 ) )
39 36 38 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) = ( ( ! ‘ 𝑚 ) · ( ( 𝑚 + 1 ) ↑ 0 ) ) )
40 fvoveq1 ⊢ ( 𝑛 = 𝑚 → ( ! ‘ ( 𝑛 + 0 ) ) = ( ! ‘ ( 𝑚 + 0 ) ) )
41 39 40 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) = ( ( ( ! ‘ 𝑚 ) · ( ( 𝑚 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑚 + 0 ) ) ) )
42 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) )
43 ovex ⊢ ( ( ( ! ‘ 𝑚 ) · ( ( 𝑚 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑚 + 0 ) ) ) ∈ V
44 41 42 43 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) ‘ 𝑚 ) = ( ( ( ! ‘ 𝑚 ) · ( ( 𝑚 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑚 + 0 ) ) ) )
45 peano2nn ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
46 45 nncnd ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℂ )
47 46 exp0d ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑚 + 1 ) ↑ 0 ) = 1 )
48 47 oveq2d ⊢ ( 𝑚 ∈ ℕ → ( ( ! ‘ 𝑚 ) · ( ( 𝑚 + 1 ) ↑ 0 ) ) = ( ( ! ‘ 𝑚 ) · 1 ) )
49 nnnn0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
50 faccl ⊢ ( 𝑚 ∈ ℕ0 → ( ! ‘ 𝑚 ) ∈ ℕ )
51 49 50 syl ⊢ ( 𝑚 ∈ ℕ → ( ! ‘ 𝑚 ) ∈ ℕ )
52 51 nncnd ⊢ ( 𝑚 ∈ ℕ → ( ! ‘ 𝑚 ) ∈ ℂ )
53 52 mulid1d ⊢ ( 𝑚 ∈ ℕ → ( ( ! ‘ 𝑚 ) · 1 ) = ( ! ‘ 𝑚 ) )
54 48 53 eqtrd ⊢ ( 𝑚 ∈ ℕ → ( ( ! ‘ 𝑚 ) · ( ( 𝑚 + 1 ) ↑ 0 ) ) = ( ! ‘ 𝑚 ) )
55 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
56 55 addid1d ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 0 ) = 𝑚 )
57 56 fveq2d ⊢ ( 𝑚 ∈ ℕ → ( ! ‘ ( 𝑚 + 0 ) ) = ( ! ‘ 𝑚 ) )
58 54 57 oveq12d ⊢ ( 𝑚 ∈ ℕ → ( ( ( ! ‘ 𝑚 ) · ( ( 𝑚 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑚 + 0 ) ) ) = ( ( ! ‘ 𝑚 ) / ( ! ‘ 𝑚 ) ) )
59 51 nnne0d ⊢ ( 𝑚 ∈ ℕ → ( ! ‘ 𝑚 ) ≠ 0 )
60 52 59 dividd ⊢ ( 𝑚 ∈ ℕ → ( ( ! ‘ 𝑚 ) / ( ! ‘ 𝑚 ) ) = 1 )
61 44 58 60 3eqtrd ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) ‘ 𝑚 ) = 1 )
62 61 adantl ⊢ ( ( ⊤ ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) ‘ 𝑚 ) = 1 )
63 30 31 34 35 62 climconst ⊢ ( ⊤ → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) ⇝ 1 )
64 63 mptru ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 0 ) ) / ( ! ‘ ( 𝑛 + 0 ) ) ) ) ⇝ 1
65 1zzd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) → 1 ∈ ℤ )
66 simpr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 )
67 32 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ∈ V
68 67 a1i ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ∈ V )
69 1zzd ⊢ ( 𝑚 ∈ ℕ0 → 1 ∈ ℤ )
70 1cnd ⊢ ( 𝑚 ∈ ℕ0 → 1 ∈ ℂ )
71 nn0p1nn ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ )
72 71 nnzd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℤ )
73 32 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ∈ V
74 73 a1i ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ∈ V )
75 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 + 1 ) = ( 𝑘 + 1 ) )
76 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 + ( 𝑚 + 1 ) ) = ( 𝑘 + ( 𝑚 + 1 ) ) )
77 75 76 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) = ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑚 + 1 ) ) ) )
78 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) )
79 ovex ⊢ ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑚 + 1 ) ) ) ∈ V
80 77 78 79 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ‘ 𝑘 ) = ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑚 + 1 ) ) ) )
81 80 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ‘ 𝑘 ) = ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑚 + 1 ) ) ) )
82 30 69 70 72 74 81 divcnvlin ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ⇝ 1 )
83 82 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ⇝ 1 )
84 simpr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
85 84 nnnn0d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
86 faccl ⊢ ( 𝑛 ∈ ℕ0 → ( ! ‘ 𝑛 ) ∈ ℕ )
87 85 86 syl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ! ‘ 𝑛 ) ∈ ℕ )
88 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
89 nnexpcl ⊢ ( ( ( 𝑛 + 1 ) ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) ↑ 𝑚 ) ∈ ℕ )
90 88 89 sylan ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) ↑ 𝑚 ) ∈ ℕ )
91 90 ancoms ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) ↑ 𝑚 ) ∈ ℕ )
92 87 91 nnmulcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) ∈ ℕ )
93 92 nnred ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) ∈ ℝ )
94 nnnn0addcl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( 𝑛 + 𝑚 ) ∈ ℕ )
95 94 ancoms ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 𝑚 ) ∈ ℕ )
96 95 nnnn0d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 𝑚 ) ∈ ℕ0 )
97 faccl ⊢ ( ( 𝑛 + 𝑚 ) ∈ ℕ0 → ( ! ‘ ( 𝑛 + 𝑚 ) ) ∈ ℕ )
98 96 97 syl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ! ‘ ( 𝑛 + 𝑚 ) ) ∈ ℕ )
99 93 98 nndivred ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ∈ ℝ )
100 99 recnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ∈ ℂ )
101 100 fmpttd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) : ℕ ⟶ ℂ )
102 101 ffvelrnda ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ‘ 𝑘 ) ∈ ℂ )
103 102 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ‘ 𝑘 ) ∈ ℂ )
104 88 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ )
105 104 nnred ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℝ )
106 71 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
107 84 106 nnaddcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + ( 𝑚 + 1 ) ) ∈ ℕ )
108 105 107 nndivred ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ∈ ℝ )
109 108 recnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ∈ ℂ )
110 109 fmpttd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) : ℕ ⟶ ℂ )
111 110 ffvelrnda ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ‘ 𝑘 ) ∈ ℂ )
112 111 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ‘ 𝑘 ) ∈ ℂ )
113 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
114 113 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
115 114 nncnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℂ )
116 simpl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 𝑚 ∈ ℕ0 )
117 115 116 expp1d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) = ( ( ( 𝑘 + 1 ) ↑ 𝑚 ) · ( 𝑘 + 1 ) ) )
118 117 oveq2d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) ) = ( ( ! ‘ 𝑘 ) · ( ( ( 𝑘 + 1 ) ↑ 𝑚 ) · ( 𝑘 + 1 ) ) ) )
119 simpr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
120 119 nnnn0d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
121 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
122 120 121 syl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ! ‘ 𝑘 ) ∈ ℕ )
123 122 nncnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ! ‘ 𝑘 ) ∈ ℂ )
124 nnexpcl ⊢ ( ( ( 𝑘 + 1 ) ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ↑ 𝑚 ) ∈ ℕ )
125 113 124 sylan ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) ↑ 𝑚 ) ∈ ℕ )
126 125 ancoms ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 1 ) ↑ 𝑚 ) ∈ ℕ )
127 126 nncnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 1 ) ↑ 𝑚 ) ∈ ℂ )
128 123 127 115 mulassd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) · ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( ( ( 𝑘 + 1 ) ↑ 𝑚 ) · ( 𝑘 + 1 ) ) ) )
129 118 128 eqtr4d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) ) = ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) · ( 𝑘 + 1 ) ) )
130 120 116 nn0addcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 𝑚 ) ∈ ℕ0 )
131 facp1 ⊢ ( ( 𝑘 + 𝑚 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑘 + 𝑚 ) + 1 ) ) = ( ( ! ‘ ( 𝑘 + 𝑚 ) ) · ( ( 𝑘 + 𝑚 ) + 1 ) ) )
132 130 131 syl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ! ‘ ( ( 𝑘 + 𝑚 ) + 1 ) ) = ( ( ! ‘ ( 𝑘 + 𝑚 ) ) · ( ( 𝑘 + 𝑚 ) + 1 ) ) )
133 119 nncnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
134 116 nn0cnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 𝑚 ∈ ℂ )
135 1cnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℂ )
136 133 134 135 addassd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 𝑚 ) + 1 ) = ( 𝑘 + ( 𝑚 + 1 ) ) )
137 136 fveq2d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ! ‘ ( ( 𝑘 + 𝑚 ) + 1 ) ) = ( ! ‘ ( 𝑘 + ( 𝑚 + 1 ) ) ) )
138 136 oveq2d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ! ‘ ( 𝑘 + 𝑚 ) ) · ( ( 𝑘 + 𝑚 ) + 1 ) ) = ( ( ! ‘ ( 𝑘 + 𝑚 ) ) · ( 𝑘 + ( 𝑚 + 1 ) ) ) )
139 132 137 138 3eqtr3d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ! ‘ ( 𝑘 + ( 𝑚 + 1 ) ) ) = ( ( ! ‘ ( 𝑘 + 𝑚 ) ) · ( 𝑘 + ( 𝑚 + 1 ) ) ) )
140 129 139 oveq12d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑘 + ( 𝑚 + 1 ) ) ) ) = ( ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) · ( 𝑘 + 1 ) ) / ( ( ! ‘ ( 𝑘 + 𝑚 ) ) · ( 𝑘 + ( 𝑚 + 1 ) ) ) ) )
141 122 126 nnmulcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) ∈ ℕ )
142 141 nncnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) ∈ ℂ )
143 faccl ⊢ ( ( 𝑘 + 𝑚 ) ∈ ℕ0 → ( ! ‘ ( 𝑘 + 𝑚 ) ) ∈ ℕ )
144 130 143 syl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ! ‘ ( 𝑘 + 𝑚 ) ) ∈ ℕ )
145 144 nncnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ! ‘ ( 𝑘 + 𝑚 ) ) ∈ ℂ )
146 71 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
147 119 146 nnaddcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + ( 𝑚 + 1 ) ) ∈ ℕ )
148 147 nncnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + ( 𝑚 + 1 ) ) ∈ ℂ )
149 144 nnne0d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ! ‘ ( 𝑘 + 𝑚 ) ) ≠ 0 )
150 147 nnne0d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + ( 𝑚 + 1 ) ) ≠ 0 )
151 142 145 115 148 149 150 divmuldivd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑘 + 𝑚 ) ) ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑚 + 1 ) ) ) ) = ( ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) · ( 𝑘 + 1 ) ) / ( ( ! ‘ ( 𝑘 + 𝑚 ) ) · ( 𝑘 + ( 𝑚 + 1 ) ) ) ) )
152 140 151 eqtr4d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑘 + ( 𝑚 + 1 ) ) ) ) = ( ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑘 + 𝑚 ) ) ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑚 + 1 ) ) ) ) )
153 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑘 ) )
154 75 oveq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) = ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) )
155 153 154 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) = ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) ) )
156 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) = ( ! ‘ ( 𝑘 + ( 𝑚 + 1 ) ) ) )
157 155 156 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) = ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑘 + ( 𝑚 + 1 ) ) ) ) )
158 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) )
159 ovex ⊢ ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑘 + ( 𝑚 + 1 ) ) ) ) ∈ V
160 157 158 159 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ‘ 𝑘 ) = ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑘 + ( 𝑚 + 1 ) ) ) ) )
161 160 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ‘ 𝑘 ) = ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑘 + ( 𝑚 + 1 ) ) ) ) )
162 75 oveq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 + 1 ) ↑ 𝑚 ) = ( ( 𝑘 + 1 ) ↑ 𝑚 ) )
163 153 162 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) = ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) )
164 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( ! ‘ ( 𝑛 + 𝑚 ) ) = ( ! ‘ ( 𝑘 + 𝑚 ) ) )
165 163 164 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) = ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑘 + 𝑚 ) ) ) )
166 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) )
167 ovex ⊢ ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑘 + 𝑚 ) ) ) ∈ V
168 165 166 167 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ‘ 𝑘 ) = ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑘 + 𝑚 ) ) ) )
169 168 80 oveq12d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ‘ 𝑘 ) ) = ( ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑘 + 𝑚 ) ) ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑚 + 1 ) ) ) ) )
170 169 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ‘ 𝑘 ) ) = ( ( ( ( ! ‘ 𝑘 ) · ( ( 𝑘 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑘 + 𝑚 ) ) ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑚 + 1 ) ) ) ) )
171 152 161 170 3eqtr4d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ‘ 𝑘 ) ) )
172 171 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ‘ 𝑘 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 + 1 ) / ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ‘ 𝑘 ) ) )
173 30 65 66 68 83 103 112 172 climmul ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ⇝ ( 1 · 1 ) )
174 1t1e1 ⊢ ( 1 · 1 ) = 1
175 173 174 breqtrdi ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 ) → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ⇝ 1 )
176 175 ex ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑚 ) ) / ( ! ‘ ( 𝑛 + 𝑚 ) ) ) ) ⇝ 1 → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ ( 𝑚 + 1 ) ) ) / ( ! ‘ ( 𝑛 + ( 𝑚 + 1 ) ) ) ) ) ⇝ 1 ) )
177 8 15 22 29 64 176 nn0ind ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑛 ∈ ℕ ↦ ( ( ( ! ‘ 𝑛 ) · ( ( 𝑛 + 1 ) ↑ 𝑀 ) ) / ( ! ‘ ( 𝑛 + 𝑀 ) ) ) ) ⇝ 1 )
178 1 177 eqbrtrid ⊢ ( 𝑀 ∈ ℕ0 → 𝐹 ⇝ 1 )