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