Metamath Proof Explorer

Theorem faclim

Description: An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 faclim.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) )
2 seqeq3 ⊢ ( 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) ) → seq 1 ( · , 𝐹 ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) ) ) )
3 1 2 ax-mp ⊢ seq 1 ( · , 𝐹 ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) ) )
4 oveq2 ⊢ ( 𝑎 = 0 → ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) = ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) )
5 oveq1 ⊢ ( 𝑎 = 0 → ( 𝑎 / 𝑛 ) = ( 0 / 𝑛 ) )
6 5 oveq2d ⊢ ( 𝑎 = 0 → ( 1 + ( 𝑎 / 𝑛 ) ) = ( 1 + ( 0 / 𝑛 ) ) )
7 4 6 oveq12d ⊢ ( 𝑎 = 0 → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) = ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) )
8 7 mpteq2dv ⊢ ( 𝑎 = 0 → ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) ) )
9 8 seqeq3d ⊢ ( 𝑎 = 0 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) ) ) )
10 fveq2 ⊢ ( 𝑎 = 0 → ( ! ‘ 𝑎 ) = ( ! ‘ 0 ) )
11 fac0 ⊢ ( ! ‘ 0 ) = 1
12 10 11 eqtrdi ⊢ ( 𝑎 = 0 → ( ! ‘ 𝑎 ) = 1 )
13 9 12 breq12d ⊢ ( 𝑎 = 0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑎 ) ↔ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) ) ) ⇝ 1 ) )
14 oveq2 ⊢ ( 𝑎 = 𝑚 → ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) = ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) )
15 oveq1 ⊢ ( 𝑎 = 𝑚 → ( 𝑎 / 𝑛 ) = ( 𝑚 / 𝑛 ) )
16 15 oveq2d ⊢ ( 𝑎 = 𝑚 → ( 1 + ( 𝑎 / 𝑛 ) ) = ( 1 + ( 𝑚 / 𝑛 ) ) )
17 14 16 oveq12d ⊢ ( 𝑎 = 𝑚 → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) = ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) )
18 17 mpteq2dv ⊢ ( 𝑎 = 𝑚 → ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) )
19 18 seqeq3d ⊢ ( 𝑎 = 𝑚 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) )
20 fveq2 ⊢ ( 𝑎 = 𝑚 → ( ! ‘ 𝑎 ) = ( ! ‘ 𝑚 ) )
21 19 20 breq12d ⊢ ( 𝑎 = 𝑚 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑎 ) ↔ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) )
22 oveq2 ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) = ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) )
23 oveq1 ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( 𝑎 / 𝑛 ) = ( ( 𝑚 + 1 ) / 𝑛 ) )
24 23 oveq2d ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( 1 + ( 𝑎 / 𝑛 ) ) = ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) )
25 22 24 oveq12d ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) = ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) )
26 25 mpteq2dv ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) )
27 26 seqeq3d ⊢ ( 𝑎 = ( 𝑚 + 1 ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) )
28 fveq2 ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( ! ‘ 𝑎 ) = ( ! ‘ ( 𝑚 + 1 ) ) )
29 27 28 breq12d ⊢ ( 𝑎 = ( 𝑚 + 1 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑎 ) ↔ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ ( 𝑚 + 1 ) ) ) )
30 oveq2 ⊢ ( 𝑎 = 𝐴 → ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) = ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) )
31 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 / 𝑛 ) = ( 𝐴 / 𝑛 ) )
32 31 oveq2d ⊢ ( 𝑎 = 𝐴 → ( 1 + ( 𝑎 / 𝑛 ) ) = ( 1 + ( 𝐴 / 𝑛 ) ) )
33 30 32 oveq12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) = ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) )
34 33 mpteq2dv ⊢ ( 𝑎 = 𝐴 → ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) ) )
35 34 seqeq3d ⊢ ( 𝑎 = 𝐴 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) ) ) )
36 fveq2 ⊢ ( 𝑎 = 𝐴 → ( ! ‘ 𝑎 ) = ( ! ‘ 𝐴 ) )
37 35 36 breq12d ⊢ ( 𝑎 = 𝐴 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑎 ) / ( 1 + ( 𝑎 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑎 ) ↔ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝐴 ) ) )
38 1red ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℝ )
39 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
40 38 39 readdcld ⊢ ( 𝑛 ∈ ℕ → ( 1 + ( 1 / 𝑛 ) ) ∈ ℝ )
41 40 recnd ⊢ ( 𝑛 ∈ ℕ → ( 1 + ( 1 / 𝑛 ) ) ∈ ℂ )
42 41 exp0d ⊢ ( 𝑛 ∈ ℕ → ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) = 1 )
43 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
44 nnne0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
45 43 44 div0d ⊢ ( 𝑛 ∈ ℕ → ( 0 / 𝑛 ) = 0 )
46 45 oveq2d ⊢ ( 𝑛 ∈ ℕ → ( 1 + ( 0 / 𝑛 ) ) = ( 1 + 0 ) )
47 1p0e1 ⊢ ( 1 + 0 ) = 1
48 46 47 eqtrdi ⊢ ( 𝑛 ∈ ℕ → ( 1 + ( 0 / 𝑛 ) ) = 1 )
49 42 48 oveq12d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) = ( 1 / 1 ) )
50 1div1e1 ⊢ ( 1 / 1 ) = 1
51 49 50 eqtrdi ⊢ ( 𝑛 ∈ ℕ → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) = 1 )
52 51 mpteq2ia ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ 1 )
53 fconstmpt ⊢ ( ℕ × { 1 } ) = ( 𝑛 ∈ ℕ ↦ 1 )
54 52 53 eqtr4i ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) ) = ( ℕ × { 1 } )
55 seqeq3 ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) ) = ( ℕ × { 1 } ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) ) ) = seq 1 ( · , ( ℕ × { 1 } ) ) )
56 54 55 ax-mp ⊢ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) ) ) = seq 1 ( · , ( ℕ × { 1 } ) )
57 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
58 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
59 57 58 climprod1 ⊢ ( ⊤ → seq 1 ( · , ( ℕ × { 1 } ) ) ⇝ 1 )
60 59 mptru ⊢ seq 1 ( · , ( ℕ × { 1 } ) ) ⇝ 1
61 56 60 eqbrtri ⊢ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 0 ) / ( 1 + ( 0 / 𝑛 ) ) ) ) ) ⇝ 1
62 1zzd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → 1 ∈ ℤ )
63 simpr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) )
64 seqex ⊢ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ∈ V
65 64 a1i ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ∈ V )
66 faclimlem2 ⊢ ( 𝑚 ∈ ℕ0 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( 𝑚 + 1 ) )
67 66 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( 𝑚 + 1 ) )
68 elnnuz ⊢ ( 𝑎 ∈ ℕ ↔ 𝑎 ∈ ( ℤ≥ ‘ 1 ) )
69 68 bilani ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) → 𝑎 ∈ ( ℤ≥ ‘ 1 ) )
70 1rp ⊢ 1 ∈ ℝ+
71 70 a1i ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℝ+ )
72 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
73 72 rpreccld ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
74 73 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
75 71 74 rpaddcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 + ( 1 / 𝑛 ) ) ∈ ℝ+ )
76 nn0z ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℤ )
77 76 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 𝑚 ∈ ℤ )
78 75 77 rpexpcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) ∈ ℝ+ )
79 1cnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℂ )
80 nn0nndivcl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑚 / 𝑛 ) ∈ ℝ )
81 80 recnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑚 / 𝑛 ) ∈ ℂ )
82 79 81 addcomd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 + ( 𝑚 / 𝑛 ) ) = ( ( 𝑚 / 𝑛 ) + 1 ) )
83 nn0ge0div ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( 𝑚 / 𝑛 ) )
84 80 83 ge0p1rpd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 / 𝑛 ) + 1 ) ∈ ℝ+ )
85 82 84 eqeltrd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 + ( 𝑚 / 𝑛 ) ) ∈ ℝ+ )
86 78 85 rpdivcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ∈ ℝ+ )
87 86 rpcnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ∈ ℂ )
88 87 fmpttd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) : ℕ ⟶ ℂ )
89 elfznn ⊢ ( 𝑏 ∈ ( 1 ... 𝑎 ) → 𝑏 ∈ ℕ )
90 ffvelcdm ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) : ℕ ⟶ ℂ ∧ 𝑏 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
91 88 89 90 syl2an ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
92 91 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
93 mulcl ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑏 · 𝑥 ) ∈ ℂ )
94 93 adantl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑏 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑏 · 𝑥 ) ∈ ℂ )
95 69 92 94 seqcl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ∈ ℂ )
96 95 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ∈ ℂ )
97 85 75 rpmulcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) ∈ ℝ+ )
98 nn0p1nn ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ )
99 98 nnrpd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℝ+ )
100 rpdivcl ⊢ ( ( ( 𝑚 + 1 ) ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑚 + 1 ) / 𝑛 ) ∈ ℝ+ )
101 99 72 100 syl2an ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 + 1 ) / 𝑛 ) ∈ ℝ+ )
102 71 101 rpaddcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ∈ ℝ+ )
103 97 102 rpdivcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ∈ ℝ+ )
104 103 rpcnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ∈ ℂ )
105 104 fmpttd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) : ℕ ⟶ ℂ )
106 ffvelcdm ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) : ℕ ⟶ ℂ ∧ 𝑏 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
107 105 89 106 syl2an ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
108 107 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
109 69 108 94 seqcl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ∈ ℂ )
110 109 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ∈ ℂ )
111 faclimlem3 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) = ( ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) · ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ) )
112 oveq2 ⊢ ( 𝑛 = 𝑏 → ( 1 / 𝑛 ) = ( 1 / 𝑏 ) )
113 112 oveq2d ⊢ ( 𝑛 = 𝑏 → ( 1 + ( 1 / 𝑛 ) ) = ( 1 + ( 1 / 𝑏 ) ) )
114 113 oveq1d ⊢ ( 𝑛 = 𝑏 → ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) = ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) )
115 oveq2 ⊢ ( 𝑛 = 𝑏 → ( ( 𝑚 + 1 ) / 𝑛 ) = ( ( 𝑚 + 1 ) / 𝑏 ) )
116 115 oveq2d ⊢ ( 𝑛 = 𝑏 → ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) = ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) )
117 114 116 oveq12d ⊢ ( 𝑛 = 𝑏 → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
118 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) )
119 ovex ⊢ ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ∈ V
120 117 118 119 fvmpt ⊢ ( 𝑏 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
121 120 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
122 113 oveq1d ⊢ ( 𝑛 = 𝑏 → ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) = ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) )
123 oveq2 ⊢ ( 𝑛 = 𝑏 → ( 𝑚 / 𝑛 ) = ( 𝑚 / 𝑏 ) )
124 123 oveq2d ⊢ ( 𝑛 = 𝑏 → ( 1 + ( 𝑚 / 𝑛 ) ) = ( 1 + ( 𝑚 / 𝑏 ) ) )
125 122 124 oveq12d ⊢ ( 𝑛 = 𝑏 → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) )
126 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) )
127 ovex ⊢ ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) ∈ V
128 125 126 127 fvmpt ⊢ ( 𝑏 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) )
129 124 113 oveq12d ⊢ ( 𝑛 = 𝑏 → ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) = ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) )
130 129 116 oveq12d ⊢ ( 𝑛 = 𝑏 → ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) = ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
131 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) )
132 ovex ⊢ ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ∈ V
133 130 131 132 fvmpt ⊢ ( 𝑏 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
134 128 133 oveq12d ⊢ ( 𝑏 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) = ( ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) · ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ) )
135 134 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) = ( ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) · ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ) )
136 111 121 135 3eqtr4d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) )
137 89 136 sylan2 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) )
138 137 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) )
139 69 92 108 138 prodfmul ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ‘ 𝑎 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ) )
140 139 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ‘ 𝑎 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ) )
141 57 62 63 65 67 96 110 140 climmul ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( ( ! ‘ 𝑚 ) · ( 𝑚 + 1 ) ) )
142 facp1 ⊢ ( 𝑚 ∈ ℕ0 → ( ! ‘ ( 𝑚 + 1 ) ) = ( ( ! ‘ 𝑚 ) · ( 𝑚 + 1 ) ) )
143 142 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → ( ! ‘ ( 𝑚 + 1 ) ) = ( ( ! ‘ 𝑚 ) · ( 𝑚 + 1 ) ) )
144 141 143 breqtrrd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ ( 𝑚 + 1 ) ) )
145 144 ex ⊢ ( 𝑚 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ ( 𝑚 + 1 ) ) ) )
146 13 21 29 37 61 145 nn0ind ⊢ ( 𝐴 ∈ ℕ0 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝐴 ) )
147 3 146 eqbrtrid ⊢ ( 𝐴 ∈ ℕ0 → seq 1 ( · , 𝐹 ) ⇝ ( ! ‘ 𝐴 ) )