Metamath Proof Explorer

Theorem knoppndvlem7

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppndvlem7.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppndvlem7.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppndvlem7.a 
|- A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
knoppndvlem7.j 
|- ( ph -> J e. NN0 )
knoppndvlem7.m 
|- ( ph -> M e. ZZ )
knoppndvlem7.n 
|- ( ph -> N e. NN )
Assertion knoppndvlem7 
|- ( ph -> ( ( F ` A ) ` J ) = ( ( C ^ J ) x. ( T ` ( M / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem7.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem7.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem7.a 
 |-  A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
4 knoppndvlem7.j 
 |-  ( ph -> J e. NN0 )
5 knoppndvlem7.m 
 |-  ( ph -> M e. ZZ )
6 knoppndvlem7.n 
 |-  ( ph -> N e. NN )
7 3 a1i 
 |-  ( ph -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) )
8 4 nn0zd 
 |-  ( ph -> J e. ZZ )
9 6 8 5 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) e. RR )
10 7 9 eqeltrd 
 |-  ( ph -> A e. RR )
11 2 10 4 knoppcnlem1 
 |-  ( ph -> ( ( F ` A ) ` J ) = ( ( C ^ J ) x. ( T ` ( ( ( 2 x. N ) ^ J ) x. A ) ) ) )
12 3 oveq2i 
 |-  ( ( ( 2 x. N ) ^ J ) x. A ) = ( ( ( 2 x. N ) ^ J ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) )
13 12 a1i 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. A ) = ( ( ( 2 x. N ) ^ J ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) )
14 2cnd 
 |-  ( ph -> 2 e. CC )
15 nnz 
 |-  ( N e. NN -> N e. ZZ )
16 6 15 syl 
 |-  ( ph -> N e. ZZ )
17 16 zcnd 
 |-  ( ph -> N e. CC )
18 14 17 mulcld 
 |-  ( ph -> ( 2 x. N ) e. CC )
19 18 4 expcld 
 |-  ( ph -> ( ( 2 x. N ) ^ J ) e. CC )
20 2ne0 
 |-  2 =/= 0
21 20 a1i 
 |-  ( ph -> 2 =/= 0 )
22 0red 
 |-  ( ph -> 0 e. RR )
23 1red 
 |-  ( ph -> 1 e. RR )
24 16 zred 
 |-  ( ph -> N e. RR )
25 0lt1 
 |-  0 < 1
26 25 a1i 
 |-  ( ph -> 0 < 1 )
27 nnge1 
 |-  ( N e. NN -> 1 <_ N )
28 6 27 syl 
 |-  ( ph -> 1 <_ N )
29 22 23 24 26 28 ltletrd 
 |-  ( ph -> 0 < N )
30 22 29 ltned 
 |-  ( ph -> 0 =/= N )
31 30 necomd 
 |-  ( ph -> N =/= 0 )
32 14 17 21 31 mulne0d 
 |-  ( ph -> ( 2 x. N ) =/= 0 )
33 8 znegcld 
 |-  ( ph -> -u J e. ZZ )
34 18 32 33 expclzd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) e. CC )
35 34 14 21 divcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. CC )
36 5 zcnd 
 |-  ( ph -> M e. CC )
37 19 35 36 mulassd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ J ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) x. M ) = ( ( ( 2 x. N ) ^ J ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) )
38 37 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) = ( ( ( ( 2 x. N ) ^ J ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) x. M ) )
39 19 34 14 21 divassd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ J ) x. ( ( 2 x. N ) ^ -u J ) ) / 2 ) = ( ( ( 2 x. N ) ^ J ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) )
40 39 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( ( ( 2 x. N ) ^ J ) x. ( ( 2 x. N ) ^ -u J ) ) / 2 ) )
41 18 32 8 expnegd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) = ( 1 / ( ( 2 x. N ) ^ J ) ) )
42 41 oveq2d 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. ( ( 2 x. N ) ^ -u J ) ) = ( ( ( 2 x. N ) ^ J ) x. ( 1 / ( ( 2 x. N ) ^ J ) ) ) )
43 18 32 8 expne0d 
 |-  ( ph -> ( ( 2 x. N ) ^ J ) =/= 0 )
44 19 43 recidd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. ( 1 / ( ( 2 x. N ) ^ J ) ) ) = 1 )
45 42 44 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. ( ( 2 x. N ) ^ -u J ) ) = 1 )
46 45 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ J ) x. ( ( 2 x. N ) ^ -u J ) ) / 2 ) = ( 1 / 2 ) )
47 40 46 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( 1 / 2 ) )
48 47 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ J ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) x. M ) = ( ( 1 / 2 ) x. M ) )
49 36 14 21 divrec2d 
 |-  ( ph -> ( M / 2 ) = ( ( 1 / 2 ) x. M ) )
50 49 eqcomd 
 |-  ( ph -> ( ( 1 / 2 ) x. M ) = ( M / 2 ) )
51 38 48 50 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) = ( M / 2 ) )
52 13 51 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ J ) x. A ) = ( M / 2 ) )
53 52 fveq2d 
 |-  ( ph -> ( T ` ( ( ( 2 x. N ) ^ J ) x. A ) ) = ( T ` ( M / 2 ) ) )
54 53 oveq2d 
 |-  ( ph -> ( ( C ^ J ) x. ( T ` ( ( ( 2 x. N ) ^ J ) x. A ) ) ) = ( ( C ^ J ) x. ( T ` ( M / 2 ) ) ) )
55 11 54 eqtrd 
 |-  ( ph -> ( ( F ` A ) ` J ) = ( ( C ^ J ) x. ( T ` ( M / 2 ) ) ) )