Metamath Proof Explorer

Theorem faclimlem3

Description: Lemma for faclim . Algebraic manipulation for the final induction. (Contributed by Scott Fenton, 15-Dec-2017)

Ref Expression
Assertion faclimlem3 ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ ( 𝑀 + 1 ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ) = ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( ( ( 1 + ( 𝑀 / 𝐵 ) ) · ( 1 + ( 1 / 𝐵 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 1rp ⊢ 1 ∈ ℝ+
2 1 a1i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → 1 ∈ ℝ+ )
3 nnrp ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
4 3 rpreccld ⊢ ( 𝐵 ∈ ℕ → ( 1 / 𝐵 ) ∈ ℝ+ )
5 4 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 / 𝐵 ) ∈ ℝ+ )
6 2 5 rpaddcld ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 + ( 1 / 𝐵 ) ) ∈ ℝ+ )
7 6 rpcnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 + ( 1 / 𝐵 ) ) ∈ ℂ )
8 simpl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → 𝑀 ∈ ℕ0 )
9 7 8 expp1d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( 1 + ( 1 / 𝐵 ) ) ↑ ( 𝑀 + 1 ) ) = ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) · ( 1 + ( 1 / 𝐵 ) ) ) )
10 1 a1i ⊢ ( 𝐵 ∈ ℕ → 1 ∈ ℝ+ )
11 10 4 rpaddcld ⊢ ( 𝐵 ∈ ℕ → ( 1 + ( 1 / 𝐵 ) ) ∈ ℝ+ )
12 nn0z ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
13 rpexpcl ⊢ ( ( ( 1 + ( 1 / 𝐵 ) ) ∈ ℝ+ ∧ 𝑀 ∈ ℤ ) → ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) ∈ ℝ+ )
14 11 12 13 syl2anr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) ∈ ℝ+ )
15 14 rpcnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) ∈ ℂ )
16 1cnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → 1 ∈ ℂ )
17 nn0nndivcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝑀 / 𝐵 ) ∈ ℝ )
18 17 recnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝑀 / 𝐵 ) ∈ ℂ )
19 16 18 addcomd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 + ( 𝑀 / 𝐵 ) ) = ( ( 𝑀 / 𝐵 ) + 1 ) )
20 nn0ge0div ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → 0 ≤ ( 𝑀 / 𝐵 ) )
21 17 20 ge0p1rpd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( 𝑀 / 𝐵 ) + 1 ) ∈ ℝ+ )
22 19 21 eqeltrd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 + ( 𝑀 / 𝐵 ) ) ∈ ℝ+ )
23 22 rpcnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 + ( 𝑀 / 𝐵 ) ) ∈ ℂ )
24 22 rpne0d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 + ( 𝑀 / 𝐵 ) ) ≠ 0 )
25 15 23 24 divcan1d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( 1 + ( 𝑀 / 𝐵 ) ) ) = ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) )
26 25 oveq1d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( 1 + ( 1 / 𝐵 ) ) ) = ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) · ( 1 + ( 1 / 𝐵 ) ) ) )
27 14 22 rpdivcld ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) ∈ ℝ+ )
28 27 rpcnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) ∈ ℂ )
29 28 23 7 mulassd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( 1 + ( 1 / 𝐵 ) ) ) = ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( ( 1 + ( 𝑀 / 𝐵 ) ) · ( 1 + ( 1 / 𝐵 ) ) ) ) )
30 9 26 29 3eqtr2d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( 1 + ( 1 / 𝐵 ) ) ↑ ( 𝑀 + 1 ) ) = ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( ( 1 + ( 𝑀 / 𝐵 ) ) · ( 1 + ( 1 / 𝐵 ) ) ) ) )
31 30 oveq1d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ ( 𝑀 + 1 ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ) = ( ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( ( 1 + ( 𝑀 / 𝐵 ) ) · ( 1 + ( 1 / 𝐵 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ) )
32 22 6 rpmulcld ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( 1 + ( 𝑀 / 𝐵 ) ) · ( 1 + ( 1 / 𝐵 ) ) ) ∈ ℝ+ )
33 32 rpcnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( 1 + ( 𝑀 / 𝐵 ) ) · ( 1 + ( 1 / 𝐵 ) ) ) ∈ ℂ )
34 nn0p1nn ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ )
35 34 nnrpd ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℝ+ )
36 35 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝑀 + 1 ) ∈ ℝ+ )
37 3 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℝ+ )
38 36 37 rpdivcld ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( 𝑀 + 1 ) / 𝐵 ) ∈ ℝ+ )
39 2 38 rpaddcld ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ∈ ℝ+ )
40 39 rpcnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ∈ ℂ )
41 39 rpne0d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ≠ 0 )
42 28 33 40 41 divassd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( ( 1 + ( 𝑀 / 𝐵 ) ) · ( 1 + ( 1 / 𝐵 ) ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ) = ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( ( ( 1 + ( 𝑀 / 𝐵 ) ) · ( 1 + ( 1 / 𝐵 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ) ) )
43 31 42 eqtrd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ ( 𝑀 + 1 ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ) = ( ( ( ( 1 + ( 1 / 𝐵 ) ) ↑ 𝑀 ) / ( 1 + ( 𝑀 / 𝐵 ) ) ) · ( ( ( 1 + ( 𝑀 / 𝐵 ) ) · ( 1 + ( 1 / 𝐵 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝐵 ) ) ) ) )