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	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to K^{N-2}-Y+KY=\left(K-1\right)Y+K^{N-2}$$

Proof

Step	Hyp	Ref	Expression
1		uznn0sub	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-2\in {\mathbb{N}}_0$$
2		expcl	$$⊢\left(K\in ℂ\wedge N-2\in {\mathbb{N}}_0\right)\to K^{N-2}\in ℂ$$
3	1 2	sylan2	$$⊢\left(K\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to K^{N-2}\in ℂ$$
4	3	3adant2	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to K^{N-2}\in ℂ$$
5		simp2	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to Y\in ℂ$$
6		mulcl	$$⊢\left(K\in ℂ\wedge Y\in ℂ\right)\to KY\in ℂ$$
7	6	3adant3	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to KY\in ℂ$$
8	4 5 7	subadd23d	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to K^{N-2}-Y+KY=K^{N-2}+KY-Y$$
9	7 5	subcld	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to KY-Y\in ℂ$$
10	4 9	addcomd	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to K^{N-2}+KY-Y=KY-Y+K^{N-2}$$
11		simp1	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to K\in ℂ$$
12	11 5	mulsubfacd	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to KY-Y=\left(K-1\right)Y$$
13	12	oveq1d	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to KY-Y+K^{N-2}=\left(K-1\right)Y+K^{N-2}$$
14	8 10 13	3eqtrd	$$⊢\left(K\in ℂ\wedge Y\in ℂ\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to K^{N-2}-Y+KY=\left(K-1\right)Y+K^{N-2}$$