# Metamath Proof Explorer

## Theorem 2lgslem3b

Description: Lemma for 2lgslem3b1 . (Contributed by AV, 16-Jul-2021)

Ref Expression
Hypothesis 2lgslem2.n $⊢ N = P − 1 2 − P 4$
Assertion 2lgslem3b $⊢ K ∈ ℕ 0 ∧ P = 8 ⁢ K + 3 → N = 2 ⁢ K + 1$

### Proof

Step Hyp Ref Expression
1 2lgslem2.n $⊢ N = P − 1 2 − P 4$
2 oveq1 $⊢ P = 8 ⁢ K + 3 → P − 1 = 8 ⁢ K + 3 - 1$
3 2 oveq1d $⊢ P = 8 ⁢ K + 3 → P − 1 2 = 8 ⁢ K + 3 - 1 2$
4 fvoveq1 $⊢ P = 8 ⁢ K + 3 → P 4 = 8 ⁢ K + 3 4$
5 3 4 oveq12d $⊢ P = 8 ⁢ K + 3 → P − 1 2 − P 4 = 8 ⁢ K + 3 - 1 2 − 8 ⁢ K + 3 4$
6 1 5 syl5eq $⊢ P = 8 ⁢ K + 3 → N = 8 ⁢ K + 3 - 1 2 − 8 ⁢ K + 3 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 3cn $⊢ 3 ∈ ℂ$
13 12 a1i $⊢ K ∈ ℕ 0 → 3 ∈ ℂ$
14 1cnd $⊢ K ∈ ℕ 0 → 1 ∈ ℂ$
15 11 13 14 addsubassd $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 - 1 = 8 ⁢ K + 3 - 1$
16 4t2e8 $⊢ 4 ⋅ 2 = 8$
17 16 eqcomi $⊢ 8 = 4 ⋅ 2$
18 17 a1i $⊢ K ∈ ℕ 0 → 8 = 4 ⋅ 2$
19 18 oveq1d $⊢ K ∈ ℕ 0 → 8 ⁢ K = 4 ⋅ 2 ⁢ K$
20 4cn $⊢ 4 ∈ ℂ$
21 20 a1i $⊢ K ∈ ℕ 0 → 4 ∈ ℂ$
22 2cn $⊢ 2 ∈ ℂ$
23 22 a1i $⊢ K ∈ ℕ 0 → 2 ∈ ℂ$
24 nn0cn $⊢ K ∈ ℕ 0 → K ∈ ℂ$
25 21 23 24 mul32d $⊢ K ∈ ℕ 0 → 4 ⋅ 2 ⁢ K = 4 ⁢ K ⋅ 2$
26 19 25 eqtrd $⊢ K ∈ ℕ 0 → 8 ⁢ K = 4 ⁢ K ⋅ 2$
27 3m1e2 $⊢ 3 − 1 = 2$
28 27 a1i $⊢ K ∈ ℕ 0 → 3 − 1 = 2$
29 26 28 oveq12d $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 - 1 = 4 ⁢ K ⋅ 2 + 2$
30 15 29 eqtrd $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 - 1 = 4 ⁢ K ⋅ 2 + 2$
31 30 oveq1d $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 - 1 2 = 4 ⁢ K ⋅ 2 + 2 2$
32 4nn0 $⊢ 4 ∈ ℕ 0$
33 32 a1i $⊢ K ∈ ℕ 0 → 4 ∈ ℕ 0$
34 33 9 nn0mulcld $⊢ K ∈ ℕ 0 → 4 ⁢ K ∈ ℕ 0$
35 34 nn0cnd $⊢ K ∈ ℕ 0 → 4 ⁢ K ∈ ℂ$
36 35 23 mulcld $⊢ K ∈ ℕ 0 → 4 ⁢ K ⋅ 2 ∈ ℂ$
37 2rp $⊢ 2 ∈ ℝ +$
38 37 a1i $⊢ K ∈ ℕ 0 → 2 ∈ ℝ +$
39 38 rpcnne0d $⊢ K ∈ ℕ 0 → 2 ∈ ℂ ∧ 2 ≠ 0$
40 divdir $⊢ 4 ⁢ K ⋅ 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → 4 ⁢ K ⋅ 2 + 2 2 = 4 ⁢ K ⋅ 2 2 + 2 2$
41 36 23 39 40 syl3anc $⊢ K ∈ ℕ 0 → 4 ⁢ K ⋅ 2 + 2 2 = 4 ⁢ K ⋅ 2 2 + 2 2$
42 2ne0 $⊢ 2 ≠ 0$
43 42 a1i $⊢ K ∈ ℕ 0 → 2 ≠ 0$
44 35 23 43 divcan4d $⊢ K ∈ ℕ 0 → 4 ⁢ K ⋅ 2 2 = 4 ⁢ K$
45 2div2e1 $⊢ 2 2 = 1$
46 45 a1i $⊢ K ∈ ℕ 0 → 2 2 = 1$
47 44 46 oveq12d $⊢ K ∈ ℕ 0 → 4 ⁢ K ⋅ 2 2 + 2 2 = 4 ⁢ K + 1$
48 31 41 47 3eqtrd $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 - 1 2 = 4 ⁢ K + 1$
49 4ne0 $⊢ 4 ≠ 0$
50 20 49 pm3.2i $⊢ 4 ∈ ℂ ∧ 4 ≠ 0$
51 50 a1i $⊢ K ∈ ℕ 0 → 4 ∈ ℂ ∧ 4 ≠ 0$
52 divdir $⊢ 8 ⁢ K ∈ ℂ ∧ 3 ∈ ℂ ∧ 4 ∈ ℂ ∧ 4 ≠ 0 → 8 ⁢ K + 3 4 = 8 ⁢ K 4 + 3 4$
53 11 13 51 52 syl3anc $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 4 = 8 ⁢ K 4 + 3 4$
54 8cn $⊢ 8 ∈ ℂ$
55 54 a1i $⊢ K ∈ ℕ 0 → 8 ∈ ℂ$
56 div23 $⊢ 8 ∈ ℂ ∧ K ∈ ℂ ∧ 4 ∈ ℂ ∧ 4 ≠ 0 → 8 ⁢ K 4 = 8 4 ⁢ K$
57 55 24 51 56 syl3anc $⊢ K ∈ ℕ 0 → 8 ⁢ K 4 = 8 4 ⁢ K$
58 17 oveq1i $⊢ 8 4 = 4 ⋅ 2 4$
59 22 20 49 divcan3i $⊢ 4 ⋅ 2 4 = 2$
60 58 59 eqtri $⊢ 8 4 = 2$
61 60 a1i $⊢ K ∈ ℕ 0 → 8 4 = 2$
62 61 oveq1d $⊢ K ∈ ℕ 0 → 8 4 ⁢ K = 2 ⁢ K$
63 57 62 eqtrd $⊢ K ∈ ℕ 0 → 8 ⁢ K 4 = 2 ⁢ K$
64 63 oveq1d $⊢ K ∈ ℕ 0 → 8 ⁢ K 4 + 3 4 = 2 ⁢ K + 3 4$
65 53 64 eqtrd $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 4 = 2 ⁢ K + 3 4$
66 65 fveq2d $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 4 = 2 ⁢ K + 3 4$
67 3lt4 $⊢ 3 < 4$
68 2nn0 $⊢ 2 ∈ ℕ 0$
69 68 a1i $⊢ K ∈ ℕ 0 → 2 ∈ ℕ 0$
70 69 9 nn0mulcld $⊢ K ∈ ℕ 0 → 2 ⁢ K ∈ ℕ 0$
71 70 nn0zd $⊢ K ∈ ℕ 0 → 2 ⁢ K ∈ ℤ$
72 3nn0 $⊢ 3 ∈ ℕ 0$
73 72 a1i $⊢ K ∈ ℕ 0 → 3 ∈ ℕ 0$
74 4nn $⊢ 4 ∈ ℕ$
75 74 a1i $⊢ K ∈ ℕ 0 → 4 ∈ ℕ$
76 adddivflid $⊢ 2 ⁢ K ∈ ℤ ∧ 3 ∈ ℕ 0 ∧ 4 ∈ ℕ → 3 < 4 ↔ 2 ⁢ K + 3 4 = 2 ⁢ K$
77 71 73 75 76 syl3anc $⊢ K ∈ ℕ 0 → 3 < 4 ↔ 2 ⁢ K + 3 4 = 2 ⁢ K$
78 67 77 mpbii $⊢ K ∈ ℕ 0 → 2 ⁢ K + 3 4 = 2 ⁢ K$
79 66 78 eqtrd $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 4 = 2 ⁢ K$
80 48 79 oveq12d $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 - 1 2 − 8 ⁢ K + 3 4 = 4 ⁢ K + 1 - 2 ⁢ K$
81 70 nn0cnd $⊢ K ∈ ℕ 0 → 2 ⁢ K ∈ ℂ$
82 35 14 81 addsubd $⊢ K ∈ ℕ 0 → 4 ⁢ K + 1 - 2 ⁢ K = 4 ⁢ K - 2 ⁢ K + 1$
83 2t2e4 $⊢ 2 ⋅ 2 = 4$
84 83 eqcomi $⊢ 4 = 2 ⋅ 2$
85 84 a1i $⊢ K ∈ ℕ 0 → 4 = 2 ⋅ 2$
86 85 oveq1d $⊢ K ∈ ℕ 0 → 4 ⁢ K = 2 ⋅ 2 ⁢ K$
87 23 23 24 mulassd $⊢ K ∈ ℕ 0 → 2 ⋅ 2 ⁢ K = 2 ⁢ 2 ⁢ K$
88 86 87 eqtrd $⊢ K ∈ ℕ 0 → 4 ⁢ K = 2 ⁢ 2 ⁢ K$
89 88 oveq1d $⊢ K ∈ ℕ 0 → 4 ⁢ K − 2 ⁢ K = 2 ⁢ 2 ⁢ K − 2 ⁢ K$
90 2txmxeqx $⊢ 2 ⁢ K ∈ ℂ → 2 ⁢ 2 ⁢ K − 2 ⁢ K = 2 ⁢ K$
91 81 90 syl $⊢ K ∈ ℕ 0 → 2 ⁢ 2 ⁢ K − 2 ⁢ K = 2 ⁢ K$
92 89 91 eqtrd $⊢ K ∈ ℕ 0 → 4 ⁢ K − 2 ⁢ K = 2 ⁢ K$
93 92 oveq1d $⊢ K ∈ ℕ 0 → 4 ⁢ K - 2 ⁢ K + 1 = 2 ⁢ K + 1$
94 80 82 93 3eqtrd $⊢ K ∈ ℕ 0 → 8 ⁢ K + 3 - 1 2 − 8 ⁢ K + 3 4 = 2 ⁢ K + 1$
95 6 94 sylan9eqr $⊢ K ∈ ℕ 0 ∧ P = 8 ⁢ K + 3 → N = 2 ⁢ K + 1$