Step |
Hyp |
Ref |
Expression |
1 |
|
uznn0sub |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 2 ) ∈ ℕ0 ) |
2 |
|
expcl |
⊢ ( ( 𝐾 ∈ ℂ ∧ ( 𝑁 − 2 ) ∈ ℕ0 ) → ( 𝐾 ↑ ( 𝑁 − 2 ) ) ∈ ℂ ) |
3 |
1 2
|
sylan2 |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐾 ↑ ( 𝑁 − 2 ) ) ∈ ℂ ) |
4 |
3
|
3adant2 |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐾 ↑ ( 𝑁 − 2 ) ) ∈ ℂ ) |
5 |
|
simp2 |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑌 ∈ ℂ ) |
6 |
|
mulcl |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( 𝐾 · 𝑌 ) ∈ ℂ ) |
7 |
6
|
3adant3 |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐾 · 𝑌 ) ∈ ℂ ) |
8 |
4 5 7
|
subadd23d |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − 𝑌 ) + ( 𝐾 · 𝑌 ) ) = ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) + ( ( 𝐾 · 𝑌 ) − 𝑌 ) ) ) |
9 |
7 5
|
subcld |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐾 · 𝑌 ) − 𝑌 ) ∈ ℂ ) |
10 |
4 9
|
addcomd |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) + ( ( 𝐾 · 𝑌 ) − 𝑌 ) ) = ( ( ( 𝐾 · 𝑌 ) − 𝑌 ) + ( 𝐾 ↑ ( 𝑁 − 2 ) ) ) ) |
11 |
|
simp1 |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐾 ∈ ℂ ) |
12 |
11 5
|
mulsubfacd |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐾 · 𝑌 ) − 𝑌 ) = ( ( 𝐾 − 1 ) · 𝑌 ) ) |
13 |
12
|
oveq1d |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝐾 · 𝑌 ) − 𝑌 ) + ( 𝐾 ↑ ( 𝑁 − 2 ) ) ) = ( ( ( 𝐾 − 1 ) · 𝑌 ) + ( 𝐾 ↑ ( 𝑁 − 2 ) ) ) ) |
14 |
8 10 13
|
3eqtrd |
⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − 𝑌 ) + ( 𝐾 · 𝑌 ) ) = ( ( ( 𝐾 − 1 ) · 𝑌 ) + ( 𝐾 ↑ ( 𝑁 − 2 ) ) ) ) |