Metamath Proof Explorer

Theorem knoppndvlem2

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

Ref Expression
Hypotheses knoppndvlem2.n 
|- ( ph -> N e. NN )
knoppndvlem2.i 
|- ( ph -> I e. ZZ )
knoppndvlem2.j 
|- ( ph -> J e. ZZ )
knoppndvlem2.m 
|- ( ph -> M e. ZZ )
knoppndvlem2.1 
|- ( ph -> J < I )
Assertion knoppndvlem2 
|- ( ph -> ( ( ( 2 x. N ) ^ I ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) e. ZZ )

Proof

Step Hyp Ref Expression
1 knoppndvlem2.n 
 |-  ( ph -> N e. NN )
2 knoppndvlem2.i 
 |-  ( ph -> I e. ZZ )
3 knoppndvlem2.j 
 |-  ( ph -> J e. ZZ )
4 knoppndvlem2.m 
 |-  ( ph -> M e. ZZ )
5 knoppndvlem2.1 
 |-  ( ph -> J < I )
6 2cnd 
 |-  ( ph -> 2 e. CC )
7 nnz 
 |-  ( N e. NN -> N e. ZZ )
8 1 7 syl 
 |-  ( ph -> N e. ZZ )
9 8 zcnd 
 |-  ( ph -> N e. CC )
10 6 9 mulcld 
 |-  ( ph -> ( 2 x. N ) e. CC )
11 2ne0 
 |-  2 =/= 0
12 11 a1i 
 |-  ( ph -> 2 =/= 0 )
13 0red 
 |-  ( ph -> 0 e. RR )
14 1red 
 |-  ( ph -> 1 e. RR )
15 8 zred 
 |-  ( ph -> N e. RR )
16 0lt1 
 |-  0 < 1
17 16 a1i 
 |-  ( ph -> 0 < 1 )
18 nnge1 
 |-  ( N e. NN -> 1 <_ N )
19 1 18 syl 
 |-  ( ph -> 1 <_ N )
20 13 14 15 17 19 ltletrd 
 |-  ( ph -> 0 < N )
21 13 20 ltned 
 |-  ( ph -> 0 =/= N )
22 21 necomd 
 |-  ( ph -> N =/= 0 )
23 6 9 12 22 mulne0d 
 |-  ( ph -> ( 2 x. N ) =/= 0 )
24 10 23 2 expclzd 
 |-  ( ph -> ( ( 2 x. N ) ^ I ) e. CC )
25 3 znegcld 
 |-  ( ph -> -u J e. ZZ )
26 10 23 25 expclzd 
 |-  ( ph -> ( ( 2 x. N ) ^ -u J ) e. CC )
27 26 6 12 divcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. CC )
28 4 zcnd 
 |-  ( ph -> M e. CC )
29 24 27 28 mulassd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ I ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) x. M ) = ( ( ( 2 x. N ) ^ I ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) )
30 29 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ I ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) = ( ( ( ( 2 x. N ) ^ I ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) x. M ) )
31 24 26 6 12 divassd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ I ) x. ( ( 2 x. N ) ^ -u J ) ) / 2 ) = ( ( ( 2 x. N ) ^ I ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) )
32 31 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ I ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( ( ( 2 x. N ) ^ I ) x. ( ( 2 x. N ) ^ -u J ) ) / 2 ) )
33 10 23 jca 
 |-  ( ph -> ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) )
34 2 25 jca 
 |-  ( ph -> ( I e. ZZ /\ -u J e. ZZ ) )
35 33 34 jca 
 |-  ( ph -> ( ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) /\ ( I e. ZZ /\ -u J e. ZZ ) ) )
36 expaddz 
 |-  ( ( ( ( 2 x. N ) e. CC /\ ( 2 x. N ) =/= 0 ) /\ ( I e. ZZ /\ -u J e. ZZ ) ) -> ( ( 2 x. N ) ^ ( I + -u J ) ) = ( ( ( 2 x. N ) ^ I ) x. ( ( 2 x. N ) ^ -u J ) ) )
37 35 36 syl 
 |-  ( ph -> ( ( 2 x. N ) ^ ( I + -u J ) ) = ( ( ( 2 x. N ) ^ I ) x. ( ( 2 x. N ) ^ -u J ) ) )
38 37 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ I ) x. ( ( 2 x. N ) ^ -u J ) ) = ( ( 2 x. N ) ^ ( I + -u J ) ) )
39 2 zcnd 
 |-  ( ph -> I e. CC )
40 3 zcnd 
 |-  ( ph -> J e. CC )
41 39 40 negsubd 
 |-  ( ph -> ( I + -u J ) = ( I - J ) )
42 41 oveq2d 
 |-  ( ph -> ( ( 2 x. N ) ^ ( I + -u J ) ) = ( ( 2 x. N ) ^ ( I - J ) ) )
43 3 2 jca 
 |-  ( ph -> ( J e. ZZ /\ I e. ZZ ) )
44 znnsub 
 |-  ( ( J e. ZZ /\ I e. ZZ ) -> ( J < I <-> ( I - J ) e. NN ) )
45 43 44 syl 
 |-  ( ph -> ( J < I <-> ( I - J ) e. NN ) )
46 5 45 mpbid 
 |-  ( ph -> ( I - J ) e. NN )
47 10 46 jca 
 |-  ( ph -> ( ( 2 x. N ) e. CC /\ ( I - J ) e. NN ) )
48 expm1t 
 |-  ( ( ( 2 x. N ) e. CC /\ ( I - J ) e. NN ) -> ( ( 2 x. N ) ^ ( I - J ) ) = ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. ( 2 x. N ) ) )
49 47 48 syl 
 |-  ( ph -> ( ( 2 x. N ) ^ ( I - J ) ) = ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. ( 2 x. N ) ) )
50 38 42 49 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ I ) x. ( ( 2 x. N ) ^ -u J ) ) = ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. ( 2 x. N ) ) )
51 50 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ I ) x. ( ( 2 x. N ) ^ -u J ) ) / 2 ) = ( ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. ( 2 x. N ) ) / 2 ) )
52 2 3 jca 
 |-  ( ph -> ( I e. ZZ /\ J e. ZZ ) )
53 zsubcl 
 |-  ( ( I e. ZZ /\ J e. ZZ ) -> ( I - J ) e. ZZ )
54 52 53 syl 
 |-  ( ph -> ( I - J ) e. ZZ )
55 peano2zm 
 |-  ( ( I - J ) e. ZZ -> ( ( I - J ) - 1 ) e. ZZ )
56 54 55 syl 
 |-  ( ph -> ( ( I - J ) - 1 ) e. ZZ )
57 3 zred 
 |-  ( ph -> J e. RR )
58 2 zred 
 |-  ( ph -> I e. RR )
59 57 58 posdifd 
 |-  ( ph -> ( J < I <-> 0 < ( I - J ) ) )
60 5 59 mpbid 
 |-  ( ph -> 0 < ( I - J ) )
61 0zd 
 |-  ( ph -> 0 e. ZZ )
62 61 54 jca 
 |-  ( ph -> ( 0 e. ZZ /\ ( I - J ) e. ZZ ) )
63 zltlem1 
 |-  ( ( 0 e. ZZ /\ ( I - J ) e. ZZ ) -> ( 0 < ( I - J ) <-> 0 <_ ( ( I - J ) - 1 ) ) )
64 62 63 syl 
 |-  ( ph -> ( 0 < ( I - J ) <-> 0 <_ ( ( I - J ) - 1 ) ) )
65 60 64 mpbid 
 |-  ( ph -> 0 <_ ( ( I - J ) - 1 ) )
66 56 65 jca 
 |-  ( ph -> ( ( ( I - J ) - 1 ) e. ZZ /\ 0 <_ ( ( I - J ) - 1 ) ) )
67 elnn0z 
 |-  ( ( ( I - J ) - 1 ) e. NN0 <-> ( ( ( I - J ) - 1 ) e. ZZ /\ 0 <_ ( ( I - J ) - 1 ) ) )
68 66 67 sylibr 
 |-  ( ph -> ( ( I - J ) - 1 ) e. NN0 )
69 10 68 expcld 
 |-  ( ph -> ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) e. CC )
70 69 10 6 12 divassd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. ( 2 x. N ) ) / 2 ) = ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. ( ( 2 x. N ) / 2 ) ) )
71 9 6 12 divcan3d 
 |-  ( ph -> ( ( 2 x. N ) / 2 ) = N )
72 71 oveq2d 
 |-  ( ph -> ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. ( ( 2 x. N ) / 2 ) ) = ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. N ) )
73 70 72 eqtrd 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. ( 2 x. N ) ) / 2 ) = ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. N ) )
74 32 51 73 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ I ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) = ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. N ) )
75 74 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ I ) x. ( ( ( 2 x. N ) ^ -u J ) / 2 ) ) x. M ) = ( ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. N ) x. M ) )
76 30 75 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ I ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) = ( ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. N ) x. M ) )
77 2z 
 |-  2 e. ZZ
78 77 a1i 
 |-  ( ph -> 2 e. ZZ )
79 78 8 jca 
 |-  ( ph -> ( 2 e. ZZ /\ N e. ZZ ) )
80 zmulcl 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 x. N ) e. ZZ )
81 79 80 syl 
 |-  ( ph -> ( 2 x. N ) e. ZZ )
82 81 68 jca 
 |-  ( ph -> ( ( 2 x. N ) e. ZZ /\ ( ( I - J ) - 1 ) e. NN0 ) )
83 zexpcl 
 |-  ( ( ( 2 x. N ) e. ZZ /\ ( ( I - J ) - 1 ) e. NN0 ) -> ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) e. ZZ )
84 82 83 syl 
 |-  ( ph -> ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) e. ZZ )
85 84 8 zmulcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. N ) e. ZZ )
86 85 4 zmulcld 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ ( ( I - J ) - 1 ) ) x. N ) x. M ) e. ZZ )
87 76 86 eqeltrd 
 |-  ( ph -> ( ( ( 2 x. N ) ^ I ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) e. ZZ )