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 ⊢ M ∈ ℕ 0 ∧ B ∈ ℕ → 1 + 1 B M + 1 1 + M + 1 B = 1 + 1 B M 1 + M B ⁢ 1 + M B ⁢ 1 + 1 B 1 + M + 1 B

Proof

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