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 φN
knoppndvlem2.i φI
knoppndvlem2.j φJ
knoppndvlem2.m φM
knoppndvlem2.1 φJ<I
Assertion knoppndvlem2 φ2 NI2 NJ2 M

Proof

Step Hyp Ref Expression
1 knoppndvlem2.n φN
2 knoppndvlem2.i φI
3 knoppndvlem2.j φJ
4 knoppndvlem2.m φM
5 knoppndvlem2.1 φJ<I
6 2cnd φ2
7 nnz NN
8 1 7 syl φN
9 8 zcnd φN
10 6 9 mulcld φ2 N
11 2ne0 20
12 11 a1i φ20
13 0red φ0
14 1red φ1
15 8 zred φN
16 0lt1 0<1
17 16 a1i φ0<1
18 nnge1 N1N
19 1 18 syl φ1N
20 13 14 15 17 19 ltletrd φ0<N
21 13 20 ltned φ0N
22 21 necomd φN0
23 6 9 12 22 mulne0d φ2 N0
24 10 23 2 expclzd φ2 NI
25 3 znegcld φJ
26 10 23 25 expclzd φ2 NJ
27 26 6 12 divcld φ2 NJ2
28 4 zcnd φM
29 24 27 28 mulassd φ2 NI2 NJ2 M=2 NI2 NJ2 M
30 29 eqcomd φ2 NI2 NJ2 M=2 NI2 NJ2 M
31 24 26 6 12 divassd φ2 NI2 NJ2=2 NI2 NJ2
32 31 eqcomd φ2 NI2 NJ2=2 NI2 NJ2
33 10 23 jca φ2 N2 N0
34 2 25 jca φIJ
35 33 34 jca φ2 N2 N0IJ
36 expaddz 2 N2 N0IJ2 NI+- J=2 NI2 NJ
37 35 36 syl φ2 NI+- J=2 NI2 NJ
38 37 eqcomd φ2 NI2 NJ=2 NI+- J
39 2 zcnd φI
40 3 zcnd φJ
41 39 40 negsubd φI+- J=IJ
42 41 oveq2d φ2 NI+- J=2 NIJ
43 3 2 jca φJI
44 znnsub JIJ<IIJ
45 43 44 syl φJ<IIJ
46 5 45 mpbid φIJ
47 10 46 jca φ2 NIJ
48 expm1t 2 NIJ2 NIJ=2 NI-J-12 N
49 47 48 syl φ2 NIJ=2 NI-J-12 N
50 38 42 49 3eqtrd φ2 NI2 NJ=2 NI-J-12 N
51 50 oveq1d φ2 NI2 NJ2=2 NI-J-12 N2
52 2 3 jca φIJ
53 zsubcl IJIJ
54 52 53 syl φIJ
55 peano2zm IJI-J-1
56 54 55 syl φI-J-1
57 3 zred φJ
58 2 zred φI
59 57 58 posdifd φJ<I0<IJ
60 5 59 mpbid φ0<IJ
61 0zd φ0
62 61 54 jca φ0IJ
63 zltlem1 0IJ0<IJ0I-J-1
64 62 63 syl φ0<IJ0I-J-1
65 60 64 mpbid φ0I-J-1
66 56 65 jca φI-J-10I-J-1
67 elnn0z I-J-10I-J-10I-J-1
68 66 67 sylibr φI-J-10
69 10 68 expcld φ2 NI-J-1
70 69 10 6 12 divassd φ2 NI-J-12 N2=2 NI-J-12 N2
71 9 6 12 divcan3d φ2 N2=N
72 71 oveq2d φ2 NI-J-12 N2=2 NI-J-1 N
73 70 72 eqtrd φ2 NI-J-12 N2=2 NI-J-1 N
74 32 51 73 3eqtrd φ2 NI2 NJ2=2 NI-J-1 N
75 74 oveq1d φ2 NI2 NJ2 M=2 NI-J-1 N M
76 30 75 eqtrd φ2 NI2 NJ2 M=2 NI-J-1 N M
77 2z 2
78 77 a1i φ2
79 78 8 jca φ2N
80 zmulcl 2N2 N
81 79 80 syl φ2 N
82 81 68 jca φ2 NI-J-10
83 zexpcl 2 NI-J-102 NI-J-1
84 82 83 syl φ2 NI-J-1
85 84 8 zmulcld φ2 NI-J-1 N
86 85 4 zmulcld φ2 NI-J-1 N M
87 76 86 eqeltrd φ2 NI2 NJ2 M