Metamath Proof Explorer

Theorem knoppndvlem16

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 19-Jul-2021)

Ref Expression
Hypotheses knoppndvlem16.a 
|- A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
knoppndvlem16.b 
|- B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) )
knoppndvlem16.j 
|- ( ph -> J e. NN0 )
knoppndvlem16.m 
|- ( ph -> M e. ZZ )
knoppndvlem16.n 
|- ( ph -> N e. NN )
Assertion knoppndvlem16 
|- ( ph -> ( B - A ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem16.a 
 |-  A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
2 knoppndvlem16.b 
 |-  B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) )
3 knoppndvlem16.j 
 |-  ( ph -> J e. NN0 )
4 knoppndvlem16.m 
 |-  ( ph -> M e. ZZ )
5 knoppndvlem16.n 
 |-  ( ph -> N e. NN )
6 2 a1i 
 |-  ( ph -> B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) )
7 1 a1i 
 |-  ( ph -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) )
8 6 7 oveq12d 
 |-  ( ph -> ( B - A ) = ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) )
9 2cnd 
 |-  ( ph -> 2 e. CC )
10 5 nncnd 
 |-  ( ph -> N e. CC )
11 9 10 mulcld 
 |-  ( ph -> ( 2 x. N ) e. CC )
12 2ne0 
 |-  2 =/= 0
13 12 a1i 
 |-  ( ph -> 2 =/= 0 )
14 5 nnne0d 
 |-  ( ph -> N =/= 0 )
15 9 10 13 14 mulne0d 
 |-  ( ph -> ( 2 x. N ) =/= 0 )
16 3 nn0zd 
 |-  ( ph -> J e. ZZ )
17 16 znegcld 
 |-  ( ph -> -u J e. ZZ )
18 11 15 17 expclzd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) e. CC )
19 9 10 15 mulne0bad 
 |-  ( ph -> 2 =/= 0 )
20 18 9 19 divcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. CC )
21 4 zcnd 
 |-  ( ph -> M e. CC )
22 1cnd 
 |-  ( ph -> 1 e. CC )
23 21 22 addcld 
 |-  ( ph -> ( M + 1 ) e. CC )
24 20 23 21 subdid 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( M + 1 ) - M ) ) = ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) )
25 24 eqcomd 
 |-  ( ph -> ( ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) - ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( M + 1 ) - M ) ) )
26 21 22 pncan2d 
 |-  ( ph -> ( ( M + 1 ) - M ) = 1 )
27 26 oveq2d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( M + 1 ) - M ) ) = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. 1 ) )
28 20 mulid1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. 1 ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
29 27 28 eqtrd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( ( M + 1 ) - M ) ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )
30 8 25 29 3eqtrd 
 |-  ( ph -> ( B - A ) = ( ( ( 2 x. N ) ^ -u J ) / 2 ) )