Metamath Proof Explorer


Theorem 2lgslem3a

Description: Lemma for 2lgslem3a1 . (Contributed by AV, 14-Jul-2021)

Ref Expression
Hypothesis 2lgslem2.n N=P12P4
Assertion 2lgslem3a K0P=8K+1N=2K

Proof

Step Hyp Ref Expression
1 2lgslem2.n N=P12P4
2 oveq1 P=8K+1P1=8K+1-1
3 2 oveq1d P=8K+1P12=8K+1-12
4 fvoveq1 P=8K+1P4=8K+14
5 3 4 oveq12d P=8K+1P12P4=8K+1-128K+14
6 1 5 eqtrid P=8K+1N=8K+1-128K+14
7 8nn0 80
8 7 a1i K080
9 id K0K0
10 8 9 nn0mulcld K08K0
11 10 nn0cnd K08K
12 pncan1 8K8K+1-1=8K
13 11 12 syl K08K+1-1=8K
14 13 oveq1d K08K+1-12=8K2
15 4cn 4
16 2cn 2
17 4t2e8 42=8
18 15 16 17 mulcomli 24=8
19 18 eqcomi 8=24
20 19 a1i K08=24
21 20 oveq1d K08K=24K
22 16 a1i K02
23 15 a1i K04
24 nn0cn K0K
25 22 23 24 mulassd K024K=24K
26 21 25 eqtrd K08K=24K
27 26 oveq1d K08K2=24K2
28 4nn0 40
29 28 a1i K040
30 29 9 nn0mulcld K04K0
31 30 nn0cnd K04K
32 2ne0 20
33 32 a1i K020
34 31 22 33 divcan3d K024K2=4K
35 14 27 34 3eqtrd K08K+1-12=4K
36 1cnd K01
37 4ne0 40
38 15 37 pm3.2i 440
39 38 a1i K0440
40 divdir 8K14408K+14=8K4+14
41 11 36 39 40 syl3anc K08K+14=8K4+14
42 8cn 8
43 42 a1i K08
44 div23 8K4408K4=84K
45 43 24 39 44 syl3anc K08K4=84K
46 17 eqcomi 8=42
47 46 oveq1i 84=424
48 16 15 37 divcan3i 424=2
49 47 48 eqtri 84=2
50 49 a1i K084=2
51 50 oveq1d K084K=2K
52 45 51 eqtrd K08K4=2K
53 52 oveq1d K08K4+14=2K+14
54 41 53 eqtrd K08K+14=2K+14
55 54 fveq2d K08K+14=2K+14
56 1lt4 1<4
57 2nn0 20
58 57 a1i K020
59 58 9 nn0mulcld K02K0
60 59 nn0zd K02K
61 1nn0 10
62 61 a1i K010
63 4nn 4
64 63 a1i K04
65 adddivflid 2K1041<42K+14=2K
66 60 62 64 65 syl3anc K01<42K+14=2K
67 56 66 mpbii K02K+14=2K
68 55 67 eqtrd K08K+14=2K
69 35 68 oveq12d K08K+1-128K+14=4K2K
70 2t2e4 22=4
71 70 eqcomi 4=22
72 71 a1i K04=22
73 72 oveq1d K04K=22K
74 22 22 24 mulassd K022K=22K
75 73 74 eqtrd K04K=22K
76 75 oveq1d K04K2K=22K2K
77 59 nn0cnd K02K
78 2txmxeqx 2K22K2K=2K
79 77 78 syl K022K2K=2K
80 69 76 79 3eqtrd K08K+1-128K+14=2K
81 6 80 sylan9eqr K0P=8K+1N=2K