Metamath Proof Explorer


Theorem 2lgslem3a

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

Ref Expression
Hypothesis 2lgslem2.n N = P 1 2 P 4
Assertion 2lgslem3a K 0 P = 8 K + 1 N = 2 K

Proof

Step Hyp Ref Expression
1 2lgslem2.n N = P 1 2 P 4
2 oveq1 P = 8 K + 1 P 1 = 8 K + 1 - 1
3 2 oveq1d P = 8 K + 1 P 1 2 = 8 K + 1 - 1 2
4 fvoveq1 P = 8 K + 1 P 4 = 8 K + 1 4
5 3 4 oveq12d P = 8 K + 1 P 1 2 P 4 = 8 K + 1 - 1 2 8 K + 1 4
6 1 5 syl5eq P = 8 K + 1 N = 8 K + 1 - 1 2 8 K + 1 4
7 8nn0 8 0
8 7 a1i K 0 8 0
9 id K 0 K 0
10 8 9 nn0mulcld K 0 8 K 0
11 10 nn0cnd K 0 8 K
12 pncan1 8 K 8 K + 1 - 1 = 8 K
13 11 12 syl K 0 8 K + 1 - 1 = 8 K
14 13 oveq1d K 0 8 K + 1 - 1 2 = 8 K 2
15 4cn 4
16 2cn 2
17 4t2e8 4 2 = 8
18 15 16 17 mulcomli 2 4 = 8
19 18 eqcomi 8 = 2 4
20 19 a1i K 0 8 = 2 4
21 20 oveq1d K 0 8 K = 2 4 K
22 16 a1i K 0 2
23 15 a1i K 0 4
24 nn0cn K 0 K
25 22 23 24 mulassd K 0 2 4 K = 2 4 K
26 21 25 eqtrd K 0 8 K = 2 4 K
27 26 oveq1d K 0 8 K 2 = 2 4 K 2
28 4nn0 4 0
29 28 a1i K 0 4 0
30 29 9 nn0mulcld K 0 4 K 0
31 30 nn0cnd K 0 4 K
32 2ne0 2 0
33 32 a1i K 0 2 0
34 31 22 33 divcan3d K 0 2 4 K 2 = 4 K
35 14 27 34 3eqtrd K 0 8 K + 1 - 1 2 = 4 K
36 1cnd K 0 1
37 4ne0 4 0
38 15 37 pm3.2i 4 4 0
39 38 a1i K 0 4 4 0
40 divdir 8 K 1 4 4 0 8 K + 1 4 = 8 K 4 + 1 4
41 11 36 39 40 syl3anc K 0 8 K + 1 4 = 8 K 4 + 1 4
42 8cn 8
43 42 a1i K 0 8
44 div23 8 K 4 4 0 8 K 4 = 8 4 K
45 43 24 39 44 syl3anc K 0 8 K 4 = 8 4 K
46 17 eqcomi 8 = 4 2
47 46 oveq1i 8 4 = 4 2 4
48 16 15 37 divcan3i 4 2 4 = 2
49 47 48 eqtri 8 4 = 2
50 49 a1i K 0 8 4 = 2
51 50 oveq1d K 0 8 4 K = 2 K
52 45 51 eqtrd K 0 8 K 4 = 2 K
53 52 oveq1d K 0 8 K 4 + 1 4 = 2 K + 1 4
54 41 53 eqtrd K 0 8 K + 1 4 = 2 K + 1 4
55 54 fveq2d K 0 8 K + 1 4 = 2 K + 1 4
56 1lt4 1 < 4
57 2nn0 2 0
58 57 a1i K 0 2 0
59 58 9 nn0mulcld K 0 2 K 0
60 59 nn0zd K 0 2 K
61 1nn0 1 0
62 61 a1i K 0 1 0
63 4nn 4
64 63 a1i K 0 4
65 adddivflid 2 K 1 0 4 1 < 4 2 K + 1 4 = 2 K
66 60 62 64 65 syl3anc K 0 1 < 4 2 K + 1 4 = 2 K
67 56 66 mpbii K 0 2 K + 1 4 = 2 K
68 55 67 eqtrd K 0 8 K + 1 4 = 2 K
69 35 68 oveq12d K 0 8 K + 1 - 1 2 8 K + 1 4 = 4 K 2 K
70 2t2e4 2 2 = 4
71 70 eqcomi 4 = 2 2
72 71 a1i K 0 4 = 2 2
73 72 oveq1d K 0 4 K = 2 2 K
74 22 22 24 mulassd K 0 2 2 K = 2 2 K
75 73 74 eqtrd K 0 4 K = 2 2 K
76 75 oveq1d K 0 4 K 2 K = 2 2 K 2 K
77 59 nn0cnd K 0 2 K
78 2txmxeqx 2 K 2 2 K 2 K = 2 K
79 77 78 syl K 0 2 2 K 2 K = 2 K
80 69 76 79 3eqtrd K 0 8 K + 1 - 1 2 8 K + 1 4 = 2 K
81 6 80 sylan9eqr K 0 P = 8 K + 1 N = 2 K