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+1BM+11+M+1B=1+1BM1+MB⁢1+MB⁢1+1B1+M+1B

Proof

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