Metamath Proof Explorer

Theorem knoppndvlem10

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem10.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem10.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem10.a 
 |-  A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
4 knoppndvlem10.b 
 |-  B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) )
5 knoppndvlem10.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
6 knoppndvlem10.j 
 |-  ( ph -> J e. NN0 )
7 knoppndvlem10.m 
 |-  ( ph -> M e. ZZ )
8 knoppndvlem10.n 
 |-  ( ph -> N e. NN )
9 5 adantr 
 |-  ( ( ph /\ 2 || M ) -> C e. ( -u 1 (,) 1 ) )
10 6 adantr 
 |-  ( ( ph /\ 2 || M ) -> J e. NN0 )
11 7 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
12 11 adantr 
 |-  ( ( ph /\ 2 || M ) -> ( M + 1 ) e. ZZ )
13 8 adantr 
 |-  ( ( ph /\ 2 || M ) -> N e. NN )
14 notnot 
 |-  ( 2 || M -> -. -. 2 || M )
15 14 adantl 
 |-  ( ( ph /\ 2 || M ) -> -. -. 2 || M )
16 7 adantr 
 |-  ( ( ph /\ 2 || M ) -> M e. ZZ )
17 oddp1even 
 |-  ( M e. ZZ -> ( -. 2 || M <-> 2 || ( M + 1 ) ) )
18 16 17 syl 
 |-  ( ( ph /\ 2 || M ) -> ( -. 2 || M <-> 2 || ( M + 1 ) ) )
19 15 18 mtbid 
 |-  ( ( ph /\ 2 || M ) -> -. 2 || ( M + 1 ) )
20 1 2 4 9 10 12 13 19 knoppndvlem9 
 |-  ( ( ph /\ 2 || M ) -> ( ( F ` B ) ` J ) = ( ( C ^ J ) / 2 ) )
21 15 notnotrd 
 |-  ( ( ph /\ 2 || M ) -> 2 || M )
22 1 2 3 9 10 16 13 21 knoppndvlem8 
 |-  ( ( ph /\ 2 || M ) -> ( ( F ` A ) ` J ) = 0 )
23 20 22 oveq12d 
 |-  ( ( ph /\ 2 || M ) -> ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) = ( ( ( C ^ J ) / 2 ) - 0 ) )
24 5 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
25 24 simpld 
 |-  ( ph -> C e. RR )
26 25 recnd 
 |-  ( ph -> C e. CC )
27 26 6 expcld 
 |-  ( ph -> ( C ^ J ) e. CC )
28 2cnd 
 |-  ( ph -> 2 e. CC )
29 2ne0 
 |-  2 =/= 0
30 29 a1i 
 |-  ( ph -> 2 =/= 0 )
31 27 28 30 divcld 
 |-  ( ph -> ( ( C ^ J ) / 2 ) e. CC )
32 31 subid1d 
 |-  ( ph -> ( ( ( C ^ J ) / 2 ) - 0 ) = ( ( C ^ J ) / 2 ) )
33 32 adantr 
 |-  ( ( ph /\ 2 || M ) -> ( ( ( C ^ J ) / 2 ) - 0 ) = ( ( C ^ J ) / 2 ) )
34 23 33 eqtrd 
 |-  ( ( ph /\ 2 || M ) -> ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) = ( ( C ^ J ) / 2 ) )
35 34 fveq2d 
 |-  ( ( ph /\ 2 || M ) -> ( abs ` ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) ) = ( abs ` ( ( C ^ J ) / 2 ) ) )
36 4 a1i 
 |-  ( ph -> B = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) )
37 6 nn0zd 
 |-  ( ph -> J e. ZZ )
38 8 37 11 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. ( M + 1 ) ) e. RR )
39 36 38 eqeltrd 
 |-  ( ph -> B e. RR )
40 1 2 8 25 39 6 knoppcnlem3 
 |-  ( ph -> ( ( F ` B ) ` J ) e. RR )
41 40 recnd 
 |-  ( ph -> ( ( F ` B ) ` J ) e. CC )
42 3 a1i 
 |-  ( ph -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) )
43 8 37 7 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) e. RR )
44 42 43 eqeltrd 
 |-  ( ph -> A e. RR )
45 1 2 8 25 44 6 knoppcnlem3 
 |-  ( ph -> ( ( F ` A ) ` J ) e. RR )
46 45 recnd 
 |-  ( ph -> ( ( F ` A ) ` J ) e. CC )
47 41 46 abssubd 
 |-  ( ph -> ( abs ` ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) ) = ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) )
48 47 adantr 
 |-  ( ( ph /\ -. 2 || M ) -> ( abs ` ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) ) = ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) )
49 5 adantr 
 |-  ( ( ph /\ -. 2 || M ) -> C e. ( -u 1 (,) 1 ) )
50 6 adantr 
 |-  ( ( ph /\ -. 2 || M ) -> J e. NN0 )
51 7 adantr 
 |-  ( ( ph /\ -. 2 || M ) -> M e. ZZ )
52 8 adantr 
 |-  ( ( ph /\ -. 2 || M ) -> N e. NN )
53 simpr 
 |-  ( ( ph /\ -. 2 || M ) -> -. 2 || M )
54 1 2 3 49 50 51 52 53 knoppndvlem9 
 |-  ( ( ph /\ -. 2 || M ) -> ( ( F ` A ) ` J ) = ( ( C ^ J ) / 2 ) )
55 11 adantr 
 |-  ( ( ph /\ -. 2 || M ) -> ( M + 1 ) e. ZZ )
56 51 17 syl 
 |-  ( ( ph /\ -. 2 || M ) -> ( -. 2 || M <-> 2 || ( M + 1 ) ) )
57 53 56 mpbid 
 |-  ( ( ph /\ -. 2 || M ) -> 2 || ( M + 1 ) )
58 1 2 4 49 50 55 52 57 knoppndvlem8 
 |-  ( ( ph /\ -. 2 || M ) -> ( ( F ` B ) ` J ) = 0 )
59 54 58 oveq12d 
 |-  ( ( ph /\ -. 2 || M ) -> ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) = ( ( ( C ^ J ) / 2 ) - 0 ) )
60 32 adantr 
 |-  ( ( ph /\ -. 2 || M ) -> ( ( ( C ^ J ) / 2 ) - 0 ) = ( ( C ^ J ) / 2 ) )
61 59 60 eqtrd 
 |-  ( ( ph /\ -. 2 || M ) -> ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) = ( ( C ^ J ) / 2 ) )
62 61 fveq2d 
 |-  ( ( ph /\ -. 2 || M ) -> ( abs ` ( ( ( F ` A ) ` J ) - ( ( F ` B ) ` J ) ) ) = ( abs ` ( ( C ^ J ) / 2 ) ) )
63 48 62 eqtrd 
 |-  ( ( ph /\ -. 2 || M ) -> ( abs ` ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) ) = ( abs ` ( ( C ^ J ) / 2 ) ) )
64 35 63 pm2.61dan 
 |-  ( ph -> ( abs ` ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) ) = ( abs ` ( ( C ^ J ) / 2 ) ) )
65 27 28 30 absdivd 
 |-  ( ph -> ( abs ` ( ( C ^ J ) / 2 ) ) = ( ( abs ` ( C ^ J ) ) / ( abs ` 2 ) ) )
66 26 6 absexpd 
 |-  ( ph -> ( abs ` ( C ^ J ) ) = ( ( abs ` C ) ^ J ) )
67 0le2 
 |-  0 <_ 2
68 2re 
 |-  2 e. RR
69 68 absidi 
 |-  ( 0 <_ 2 -> ( abs ` 2 ) = 2 )
70 67 69 ax-mp 
 |-  ( abs ` 2 ) = 2
71 70 a1i 
 |-  ( ph -> ( abs ` 2 ) = 2 )
72 66 71 oveq12d 
 |-  ( ph -> ( ( abs ` ( C ^ J ) ) / ( abs ` 2 ) ) = ( ( ( abs ` C ) ^ J ) / 2 ) )
73 65 72 eqtrd 
 |-  ( ph -> ( abs ` ( ( C ^ J ) / 2 ) ) = ( ( ( abs ` C ) ^ J ) / 2 ) )
74 64 73 eqtrd 
 |-  ( ph -> ( abs ` ( ( ( F ` B ) ` J ) - ( ( F ` A ) ` J ) ) ) = ( ( ( abs ` C ) ^ J ) / 2 ) )