Proof of Theorem faclimlem3
| Step | Hyp | Ref
| Expression |
| 1 | | 1rp 13038 |
. . . . . . . 8
⊢ 1 ∈
ℝ+ |
| 2 | 1 | a1i 11 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 1 ∈ ℝ+) |
| 3 | | nnrp 13046 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ+) |
| 4 | 3 | rpreccld 13087 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → (1 /
𝐵) ∈
ℝ+) |
| 5 | 4 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 / 𝐵) ∈
ℝ+) |
| 6 | 2, 5 | rpaddcld 13092 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 + (1 / 𝐵)) ∈
ℝ+) |
| 7 | 6 | rpcnd 13079 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 + (1 / 𝐵)) ∈
ℂ) |
| 8 | | simpl 482 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑀 ∈
ℕ0) |
| 9 | 7, 8 | expp1d 14187 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((1 + (1 / 𝐵))↑(𝑀 + 1)) = (((1 + (1 / 𝐵))↑𝑀) · (1 + (1 / 𝐵)))) |
| 10 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 1 ∈
ℝ+) |
| 11 | 10, 4 | rpaddcld 13092 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → (1 + (1 /
𝐵)) ∈
ℝ+) |
| 12 | | nn0z 12638 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℤ) |
| 13 | | rpexpcl 14121 |
. . . . . . . 8
⊢ (((1 + (1
/ 𝐵)) ∈
ℝ+ ∧ 𝑀
∈ ℤ) → ((1 + (1 / 𝐵))↑𝑀) ∈
ℝ+) |
| 14 | 11, 12, 13 | syl2anr 597 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((1 + (1 / 𝐵))↑𝑀) ∈
ℝ+) |
| 15 | 14 | rpcnd 13079 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((1 + (1 / 𝐵))↑𝑀) ∈ ℂ) |
| 16 | | 1cnd 11256 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 1 ∈ ℂ) |
| 17 | | nn0nndivcl 12598 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑀 / 𝐵) ∈
ℝ) |
| 18 | 17 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑀 / 𝐵) ∈
ℂ) |
| 19 | 16, 18 | addcomd 11463 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 + (𝑀 / 𝐵)) = ((𝑀 / 𝐵) + 1)) |
| 20 | | nn0ge0div 12687 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 0 ≤ (𝑀 / 𝐵)) |
| 21 | 17, 20 | ge0p1rpd 13107 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝑀 / 𝐵) + 1) ∈
ℝ+) |
| 22 | 19, 21 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 + (𝑀 / 𝐵)) ∈
ℝ+) |
| 23 | 22 | rpcnd 13079 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 + (𝑀 / 𝐵)) ∈
ℂ) |
| 24 | 22 | rpne0d 13082 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 + (𝑀 / 𝐵)) ≠ 0) |
| 25 | 15, 23, 24 | divcan1d 12044 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (1 + (𝑀 / 𝐵))) = ((1 + (1 / 𝐵))↑𝑀)) |
| 26 | 25 | oveq1d 7446 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (1 + (𝑀 / 𝐵))) · (1 + (1 / 𝐵))) = (((1 + (1 / 𝐵))↑𝑀) · (1 + (1 / 𝐵)))) |
| 27 | 14, 22 | rpdivcld 13094 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) ∈
ℝ+) |
| 28 | 27 | rpcnd 13079 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) ∈ ℂ) |
| 29 | 28, 23, 7 | mulassd 11284 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (1 + (𝑀 / 𝐵))) · (1 + (1 / 𝐵))) = ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · ((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))))) |
| 30 | 9, 26, 29 | 3eqtr2d 2783 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((1 + (1 / 𝐵))↑(𝑀 + 1)) = ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · ((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))))) |
| 31 | 30 | oveq1d 7446 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (((1 + (1 / 𝐵))↑(𝑀 + 1)) / (1 + ((𝑀 + 1) / 𝐵))) = (((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · ((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵)))) / (1 + ((𝑀 + 1) / 𝐵)))) |
| 32 | 22, 6 | rpmulcld 13093 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))) ∈
ℝ+) |
| 33 | 32 | rpcnd 13079 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))) ∈
ℂ) |
| 34 | | nn0p1nn 12565 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ) |
| 35 | 34 | nnrpd 13075 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℝ+) |
| 36 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑀 + 1) ∈
ℝ+) |
| 37 | 3 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐵 ∈
ℝ+) |
| 38 | 36, 37 | rpdivcld 13094 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝑀 + 1) / 𝐵) ∈
ℝ+) |
| 39 | 2, 38 | rpaddcld 13092 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 + ((𝑀 + 1) /
𝐵)) ∈
ℝ+) |
| 40 | 39 | rpcnd 13079 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 + ((𝑀 + 1) /
𝐵)) ∈
ℂ) |
| 41 | 39 | rpne0d 13082 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (1 + ((𝑀 + 1) /
𝐵)) ≠
0) |
| 42 | 28, 33, 40, 41 | divassd 12078 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · ((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵)))) / (1 + ((𝑀 + 1) / 𝐵))) = ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))) / (1 + ((𝑀 + 1) / 𝐵))))) |
| 43 | 31, 42 | eqtrd 2777 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (((1 + (1 / 𝐵))↑(𝑀 + 1)) / (1 + ((𝑀 + 1) / 𝐵))) = ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))) / (1 + ((𝑀 + 1) / 𝐵))))) |