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 biimpi ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ( ℤ≥ ‘ 1 ) )
70 69 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) → 𝑎 ∈ ( ℤ≥ ‘ 1 ) )
71 1rp ⊢ 1 ∈ ℝ+
72 71 a1i ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℝ+ )
73 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
74 73 rpreccld ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
75 74 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
76 72 75 rpaddcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 + ( 1 / 𝑛 ) ) ∈ ℝ+ )
77 nn0z ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℤ )
78 77 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 𝑚 ∈ ℤ )
79 76 78 rpexpcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) ∈ ℝ+ )
80 1cnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℂ )
81 nn0nndivcl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑚 / 𝑛 ) ∈ ℝ )
82 81 recnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑚 / 𝑛 ) ∈ ℂ )
83 80 82 addcomd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 + ( 𝑚 / 𝑛 ) ) = ( ( 𝑚 / 𝑛 ) + 1 ) )
84 nn0ge0div ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( 𝑚 / 𝑛 ) )
85 81 84 ge0p1rpd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 / 𝑛 ) + 1 ) ∈ ℝ+ )
86 83 85 eqeltrd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 + ( 𝑚 / 𝑛 ) ) ∈ ℝ+ )
87 79 86 rpdivcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ∈ ℝ+ )
88 87 rpcnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ∈ ℂ )
89 88 fmpttd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) : ℕ ⟶ ℂ )
90 elfznn ⊢ ( 𝑏 ∈ ( 1 ... 𝑎 ) → 𝑏 ∈ ℕ )
91 ffvelcdm ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) : ℕ ⟶ ℂ ∧ 𝑏 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
92 89 90 91 syl2an ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
93 92 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
94 mulcl ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑏 · 𝑥 ) ∈ ℂ )
95 94 adantl ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) ∧ ( 𝑏 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑏 · 𝑥 ) ∈ ℂ )
96 70 93 95 seqcl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ∈ ℂ )
97 96 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ∈ ℂ )
98 86 76 rpmulcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) ∈ ℝ+ )
99 nn0p1nn ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ )
100 99 nnrpd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℝ+ )
101 rpdivcl ⊢ ( ( ( 𝑚 + 1 ) ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑚 + 1 ) / 𝑛 ) ∈ ℝ+ )
102 100 73 101 syl2an ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 + 1 ) / 𝑛 ) ∈ ℝ+ )
103 72 102 rpaddcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ∈ ℝ+ )
104 98 103 rpdivcld ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ∈ ℝ+ )
105 104 rpcnd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ∈ ℂ )
106 105 fmpttd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) : ℕ ⟶ ℂ )
107 ffvelcdm ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) : ℕ ⟶ ℂ ∧ 𝑏 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
108 106 90 107 syl2an ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
109 108 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ∈ ℂ )
110 70 109 95 seqcl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ∈ ℂ )
111 110 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ∈ ℂ )
112 faclimlem3 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) = ( ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) · ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ) )
113 oveq2 ⊢ ( 𝑛 = 𝑏 → ( 1 / 𝑛 ) = ( 1 / 𝑏 ) )
114 113 oveq2d ⊢ ( 𝑛 = 𝑏 → ( 1 + ( 1 / 𝑛 ) ) = ( 1 + ( 1 / 𝑏 ) ) )
115 114 oveq1d ⊢ ( 𝑛 = 𝑏 → ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) = ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) )
116 oveq2 ⊢ ( 𝑛 = 𝑏 → ( ( 𝑚 + 1 ) / 𝑛 ) = ( ( 𝑚 + 1 ) / 𝑏 ) )
117 116 oveq2d ⊢ ( 𝑛 = 𝑏 → ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) = ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) )
118 115 117 oveq12d ⊢ ( 𝑛 = 𝑏 → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
119 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) )
120 ovex ⊢ ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ∈ V
121 118 119 120 fvmpt ⊢ ( 𝑏 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
122 121 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
123 114 oveq1d ⊢ ( 𝑛 = 𝑏 → ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) = ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) )
124 oveq2 ⊢ ( 𝑛 = 𝑏 → ( 𝑚 / 𝑛 ) = ( 𝑚 / 𝑏 ) )
125 124 oveq2d ⊢ ( 𝑛 = 𝑏 → ( 1 + ( 𝑚 / 𝑛 ) ) = ( 1 + ( 𝑚 / 𝑏 ) ) )
126 123 125 oveq12d ⊢ ( 𝑛 = 𝑏 → ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) )
127 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) )
128 ovex ⊢ ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) ∈ V
129 126 127 128 fvmpt ⊢ ( 𝑏 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) )
130 125 114 oveq12d ⊢ ( 𝑛 = 𝑏 → ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) = ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) )
131 130 117 oveq12d ⊢ ( 𝑛 = 𝑏 → ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) = ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
132 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) )
133 ovex ⊢ ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ∈ V
134 131 132 133 fvmpt ⊢ ( 𝑏 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) )
135 129 134 oveq12d ⊢ ( 𝑏 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) = ( ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) · ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ) )
136 135 adantl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) = ( ( ( ( 1 + ( 1 / 𝑏 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑏 ) ) ) · ( ( ( 1 + ( 𝑚 / 𝑏 ) ) · ( 1 + ( 1 / 𝑏 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑏 ) ) ) ) )
137 112 122 136 3eqtr4d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) )
138 90 137 sylan2 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) )
139 138 adantlr ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) ∧ 𝑏 ∈ ( 1 ... 𝑎 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ‘ 𝑏 ) · ( ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ‘ 𝑏 ) ) )
140 70 93 109 139 prodfmul ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑎 ∈ ℕ ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ‘ 𝑎 ) · ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑚 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ) )
141 140 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 ) / 𝑛 ) ) ) ) ) ‘ 𝑎 ) ) )
142 57 62 63 65 67 97 111 141 climmul ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( ( ! ‘ 𝑚 ) · ( 𝑚 + 1 ) ) )
143 facp1 ⊢ ( 𝑚 ∈ ℕ0 → ( ! ‘ ( 𝑚 + 1 ) ) = ( ( ! ‘ 𝑚 ) · ( 𝑚 + 1 ) ) )
144 143 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → ( ! ‘ ( 𝑚 + 1 ) ) = ( ( ! ‘ 𝑚 ) · ( 𝑚 + 1 ) ) )
145 142 144 breqtrrd ⊢ ( ( 𝑚 ∈ ℕ0 ∧ seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ ( 𝑚 + 1 ) ) )
146 145 ex ⊢ ( 𝑚 ∈ ℕ0 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝑚 ) / ( 1 + ( 𝑚 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝑚 ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ ( 𝑚 + 1 ) ) / ( 1 + ( ( 𝑚 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ ( 𝑚 + 1 ) ) ) )
147 13 21 29 37 61 146 nn0ind ⊢ ( 𝐴 ∈ ℕ0 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 1 / 𝑛 ) ) ↑ 𝐴 ) / ( 1 + ( 𝐴 / 𝑛 ) ) ) ) ) ⇝ ( ! ‘ 𝐴 ) )
148 3 147 eqbrtrid ⊢ ( 𝐴 ∈ ℕ0 → seq 1 ( · , 𝐹 ) ⇝ ( ! ‘ 𝐴 ) )