Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic number theory
Quadratic reciprocity
2lgslem3a
Next ⟩
2lgslem3b
Metamath Proof Explorer
Ascii
Unicode
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
eqtrid
⊢
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