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 
|- ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( K ^ ( N - 2 ) ) - Y ) + ( K x. Y ) ) = ( ( ( K - 1 ) x. Y ) + ( K ^ ( N - 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 uznn0sub 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. NN0 )
2 expcl 
 |-  ( ( K e. CC /\ ( N - 2 ) e. NN0 ) -> ( K ^ ( N - 2 ) ) e. CC )
3 1 2 sylan2 
 |-  ( ( K e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( K ^ ( N - 2 ) ) e. CC )
4 3 3adant2 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( K ^ ( N - 2 ) ) e. CC )
5 simp2 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> Y e. CC )
6 mulcl 
 |-  ( ( K e. CC /\ Y e. CC ) -> ( K x. Y ) e. CC )
7 6 3adant3 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( K x. Y ) e. CC )
8 4 5 7 subadd23d 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( K ^ ( N - 2 ) ) - Y ) + ( K x. Y ) ) = ( ( K ^ ( N - 2 ) ) + ( ( K x. Y ) - Y ) ) )
9 7 5 subcld 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( ( K x. Y ) - Y ) e. CC )
10 4 9 addcomd 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( ( K ^ ( N - 2 ) ) + ( ( K x. Y ) - Y ) ) = ( ( ( K x. Y ) - Y ) + ( K ^ ( N - 2 ) ) ) )
11 simp1 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> K e. CC )
12 11 5 mulsubfacd 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( ( K x. Y ) - Y ) = ( ( K - 1 ) x. Y ) )
13 12 oveq1d 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( K x. Y ) - Y ) + ( K ^ ( N - 2 ) ) ) = ( ( ( K - 1 ) x. Y ) + ( K ^ ( N - 2 ) ) ) )
14 8 10 13 3eqtrd 
 |-  ( ( K e. CC /\ Y e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( K ^ ( N - 2 ) ) - Y ) + ( K x. Y ) ) = ( ( ( K - 1 ) x. Y ) + ( K ^ ( N - 2 ) ) ) )