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 ) / 𝐵 ) ) ) ) )