Metamath Proof Explorer


Theorem numclwwlk3lem1

Description: Lemma 2 for numclwwlk3 . (Contributed by Alexander van der Vekens, 26-Aug-2018) (Proof shortened by AV, 23-Jan-2022)

Ref Expression
Assertion numclwwlk3lem1 ( ( 𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − 𝑌 ) + ( 𝐾 · 𝑌 ) ) = ( ( ( 𝐾 − 1 ) · 𝑌 ) + ( 𝐾 ↑ ( 𝑁 − 2 ) ) ) )

Proof

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