Metamath Proof Explorer


Theorem lighneallem2

Description: Lemma 2 for lighneal . (Contributed by AV, 13-Aug-2021)

Ref Expression
Assertion lighneallem2 P 2 M N 2 N 2 N 1 = P M M = 1

Proof

Step Hyp Ref Expression
1 evennn2n N 2 N k 2 k = N
2 1 3ad2ant3 P 2 M N 2 N k 2 k = N
3 oveq2 N = 2 k 2 N = 2 2 k
4 3 eqcoms 2 k = N 2 N = 2 2 k
5 2cnd k 2
6 nncn k k
7 5 6 mulcomd k 2 k = k 2
8 7 oveq2d k 2 2 k = 2 k 2
9 2nn0 2 0
10 9 a1i k 2 0
11 nnnn0 k k 0
12 5 10 11 expmuld k 2 k 2 = 2 k 2
13 8 12 eqtrd k 2 2 k = 2 k 2
14 13 adantl P 2 M N k 2 2 k = 2 k 2
15 4 14 sylan9eqr P 2 M N k 2 k = N 2 N = 2 k 2
16 15 oveq1d P 2 M N k 2 k = N 2 N 1 = 2 k 2 1
17 16 eqeq1d P 2 M N k 2 k = N 2 N 1 = P M 2 k 2 1 = P M
18 elnn1uz2 k k = 1 k 2
19 oveq2 k = 1 2 k = 2 1
20 2cn 2
21 exp1 2 2 1 = 2
22 20 21 ax-mp 2 1 = 2
23 19 22 eqtrdi k = 1 2 k = 2
24 23 oveq1d k = 1 2 k 2 = 2 2
25 24 oveq1d k = 1 2 k 2 1 = 2 2 1
26 sq2 2 2 = 4
27 26 oveq1i 2 2 1 = 4 1
28 4m1e3 4 1 = 3
29 27 28 eqtri 2 2 1 = 3
30 25 29 eqtrdi k = 1 2 k 2 1 = 3
31 30 eqeq1d k = 1 2 k 2 1 = P M 3 = P M
32 31 adantr k = 1 P 2 M N 2 k 2 1 = P M 3 = P M
33 eqcom 3 = P M P M = 3
34 eldifi P 2 P
35 prmnn P P
36 nnre P P
37 34 35 36 3syl P 2 P
38 37 3ad2ant1 P 2 M N P
39 nnnn0 M M 0
40 39 3ad2ant2 P 2 M N M 0
41 38 40 reexpcld P 2 M N P M
42 41 adantr P 2 M N P M = 3 P M
43 simpr P 2 M N P M = 3 P M = 3
44 42 43 eqled P 2 M N P M = 3 P M 3
45 44 ex P 2 M N P M = 3 P M 3
46 33 45 syl5bi P 2 M N 3 = P M P M 3
47 35 nnred P P
48 prmgt1 P 1 < P
49 47 48 jca P P 1 < P
50 34 49 syl P 2 P 1 < P
51 50 3ad2ant1 P 2 M N P 1 < P
52 nnz M M
53 52 3ad2ant2 P 2 M N M
54 3rp 3 +
55 54 a1i P 2 M N 3 +
56 efexple P 1 < P M 3 + P M 3 M log 3 log P
57 51 53 55 56 syl3anc P 2 M N P M 3 M log 3 log P
58 oddprmge3 P 2 P 3
59 eluzle P 3 3 P
60 58 59 syl P 2 3 P
61 54 a1i P 2 3 +
62 nnrp P P +
63 34 35 62 3syl P 2 P +
64 61 63 logled P 2 3 P log 3 log P
65 60 64 mpbid P 2 log 3 log P
66 65 3ad2ant1 P 2 M N log 3 log P
67 relogcl 3 + log 3
68 54 67 ax-mp log 3
69 rplogcl P 1 < P log P +
70 34 49 69 3syl P 2 log P +
71 70 3ad2ant1 P 2 M N log P +
72 divle1le log 3 log P + log 3 log P 1 log 3 log P
73 68 71 72 sylancr P 2 M N log 3 log P 1 log 3 log P
74 66 73 mpbird P 2 M N log 3 log P 1
75 fldivle log 3 log P + log 3 log P log 3 log P
76 68 71 75 sylancr P 2 M N log 3 log P log 3 log P
77 nnre M M
78 77 3ad2ant2 P 2 M N M
79 68 a1i P 2 log 3
80 62 relogcld P log P
81 34 35 80 3syl P 2 log P
82 35 nnrpd P P +
83 1red P 1
84 83 48 gtned P P 1
85 82 84 jca P P + P 1
86 logne0 P + P 1 log P 0
87 34 85 86 3syl P 2 log P 0
88 79 81 87 redivcld P 2 log 3 log P
89 88 flcld P 2 log 3 log P
90 89 zred P 2 log 3 log P
91 90 3ad2ant1 P 2 M N log 3 log P
92 88 3ad2ant1 P 2 M N log 3 log P
93 letr M log 3 log P log 3 log P M log 3 log P log 3 log P log 3 log P M log 3 log P
94 78 91 92 93 syl3anc P 2 M N M log 3 log P log 3 log P log 3 log P M log 3 log P
95 1red P 2 M N 1
96 letr M log 3 log P 1 M log 3 log P log 3 log P 1 M 1
97 78 92 95 96 syl3anc P 2 M N M log 3 log P log 3 log P 1 M 1
98 nnge1 M 1 M
99 eqcom M = 1 1 = M
100 1red M 1
101 100 77 letri3d M 1 = M 1 M M 1
102 99 101 bitr2id M 1 M M 1 M = 1
103 102 biimpd M 1 M M 1 M = 1
104 98 103 mpand M M 1 M = 1
105 104 3ad2ant2 P 2 M N M 1 M = 1
106 97 105 syld P 2 M N M log 3 log P log 3 log P 1 M = 1
107 106 expd P 2 M N M log 3 log P log 3 log P 1 M = 1
108 94 107 syld P 2 M N M log 3 log P log 3 log P log 3 log P log 3 log P 1 M = 1
109 76 108 mpan2d P 2 M N M log 3 log P log 3 log P 1 M = 1
110 74 109 mpid P 2 M N M log 3 log P M = 1
111 57 110 sylbid P 2 M N P M 3 M = 1
112 46 111 syld P 2 M N 3 = P M M = 1
113 112 adantl k = 1 P 2 M N 3 = P M M = 1
114 32 113 sylbid k = 1 P 2 M N 2 k 2 1 = P M M = 1
115 114 ex k = 1 P 2 M N 2 k 2 1 = P M M = 1
116 sq1 1 2 = 1
117 116 eqcomi 1 = 1 2
118 117 oveq2i 2 k 2 1 = 2 k 2 1 2
119 118 eqeq1i 2 k 2 1 = P M 2 k 2 1 2 = P M
120 eqcom 2 k 2 1 2 = P M P M = 2 k 2 1 2
121 9 a1i k 2 2 0
122 eluzge2nn0 k 2 k 0
123 121 122 nn0expcld k 2 2 k 0
124 123 adantr k 2 P 2 M N 2 k 0
125 1nn0 1 0
126 125 a1i k 2 P 2 M N 1 0
127 1p1e2 1 + 1 = 2
128 22 eqcomi 2 = 2 1
129 127 128 eqtri 1 + 1 = 2 1
130 eluz2gt1 k 2 1 < k
131 2re 2
132 131 a1i k 2 2
133 1zzd k 2 1
134 eluzelz k 2 k
135 1lt2 1 < 2
136 135 a1i k 2 1 < 2
137 132 133 134 136 ltexp2d k 2 1 < k 2 1 < 2 k
138 130 137 mpbid k 2 2 1 < 2 k
139 129 138 eqbrtrid k 2 1 + 1 < 2 k
140 139 adantr k 2 P 2 M N 1 + 1 < 2 k
141 34 39 anim12i P 2 M P M 0
142 141 3adant3 P 2 M N P M 0
143 142 adantl k 2 P 2 M N P M 0
144 difsqpwdvds 2 k 0 1 0 1 + 1 < 2 k P M 0 P M = 2 k 2 1 2 P 2 1
145 124 126 140 143 144 syl31anc k 2 P 2 M N P M = 2 k 2 1 2 P 2 1
146 2t1e2 2 1 = 2
147 146 breq2i P 2 1 P 2
148 prmuz2 P P 2
149 34 148 syl P 2 P 2
150 2prm 2
151 dvdsprm P 2 2 P 2 P = 2
152 149 150 151 sylancl P 2 P 2 P = 2
153 147 152 syl5bb P 2 P 2 1 P = 2
154 eldifsn P 2 P P 2
155 eqneqall P = 2 P 2 M = 1
156 155 com12 P 2 P = 2 M = 1
157 154 156 simplbiim P 2 P = 2 M = 1
158 153 157 sylbid P 2 P 2 1 M = 1
159 158 3ad2ant1 P 2 M N P 2 1 M = 1
160 159 adantl k 2 P 2 M N P 2 1 M = 1
161 145 160 syld k 2 P 2 M N P M = 2 k 2 1 2 M = 1
162 120 161 syl5bi k 2 P 2 M N 2 k 2 1 2 = P M M = 1
163 119 162 syl5bi k 2 P 2 M N 2 k 2 1 = P M M = 1
164 163 ex k 2 P 2 M N 2 k 2 1 = P M M = 1
165 115 164 jaoi k = 1 k 2 P 2 M N 2 k 2 1 = P M M = 1
166 18 165 sylbi k P 2 M N 2 k 2 1 = P M M = 1
167 166 impcom P 2 M N k 2 k 2 1 = P M M = 1
168 167 adantr P 2 M N k 2 k = N 2 k 2 1 = P M M = 1
169 17 168 sylbid P 2 M N k 2 k = N 2 N 1 = P M M = 1
170 169 rexlimdva2 P 2 M N k 2 k = N 2 N 1 = P M M = 1
171 2 170 sylbid P 2 M N 2 N 2 N 1 = P M M = 1
172 171 3imp P 2 M N 2 N 2 N 1 = P M M = 1