numclwwlk3lem1

		Ref	Expression
	Assertion	numclwwlk3lem1	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K^{N - 2} - Y + K Y = (K - 1) Y + K^{N - 2}$

Step	Hyp	Ref	Expression
1		uznn0sub	$⊢ N \in ℤ_{\geq 2} \to N - 2 \in ℕ_{0}$
2		expcl	$⊢ (K \in ℂ \land N - 2 \in ℕ_{0}) \to K^{N - 2} \in ℂ$
3	1 2	sylan2	$⊢ (K \in ℂ \land N \in ℤ_{\geq 2}) \to K^{N - 2} \in ℂ$
4	3	3adant2	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K^{N - 2} \in ℂ$
5		simp2	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to Y \in ℂ$
6		mulcl	$⊢ (K \in ℂ \land Y \in ℂ) \to K Y \in ℂ$
7	6	3adant3	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K Y \in ℂ$
8	4 5 7	subadd23d	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K^{N - 2} - Y + K Y = K^{N - 2} + K Y - Y$
9	7 5	subcld	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K Y - Y \in ℂ$
10	4 9	addcomd	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K^{N - 2} + K Y - Y = K Y - Y + K^{N - 2}$
11		simp1	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K \in ℂ$
12	11 5	mulsubfacd	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K Y - Y = (K - 1) Y$
13	12	oveq1d	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K Y - Y + K^{N - 2} = (K - 1) Y + K^{N - 2}$
14	8 10 13	3eqtrd	$⊢ (K \in ℂ \land Y \in ℂ \land N \in ℤ_{\geq 2}) \to K^{N - 2} - Y + K Y = (K - 1) Y + K^{N - 2}$

Metamath Proof Explorer