Theorem lgsdir2lem1

Description: Lemma for lgsdir2 . (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Assertion	lgsdir2lem1	⊢ ( ( ( 1 mod 8 ) = 1 ∧ ( - 1 mod 8 ) = 7 ) ∧ ( ( 3 mod 8 ) = 3 ∧ ( - 3 mod 8 ) = 5 ) )

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		8re	⊢ 8 ∈ ℝ
3		8pos	⊢ 0 < 8
4	2 3	elrpii	⊢ 8 ∈ ℝ+
5		0le1	⊢ 0 ≤ 1
6		1lt8	⊢ 1 < 8
7		modid	⊢ ( ( ( 1 ∈ ℝ ∧ 8 ∈ ℝ+ ) ∧ ( 0 ≤ 1 ∧ 1 < 8 ) ) → ( 1 mod 8 ) = 1 )
8	1 4 5 6 7	mp4an	⊢ ( 1 mod 8 ) = 1
9		8cn	⊢ 8 ∈ ℂ
10	9	mulid2i	⊢ ( 1 · 8 ) = 8
11	10	oveq2i	⊢ ( - 1 + ( 1 · 8 ) ) = ( - 1 + 8 )
12		ax-1cn	⊢ 1 ∈ ℂ
13	12	negcli	⊢ - 1 ∈ ℂ
14	9 12	negsubi	⊢ ( 8 + - 1 ) = ( 8 − 1 )
15		8m1e7	⊢ ( 8 − 1 ) = 7
16	14 15	eqtri	⊢ ( 8 + - 1 ) = 7
17	9 13 16	addcomli	⊢ ( - 1 + 8 ) = 7
18	11 17	eqtri	⊢ ( - 1 + ( 1 · 8 ) ) = 7
19	18	oveq1i	⊢ ( ( - 1 + ( 1 · 8 ) ) mod 8 ) = ( 7 mod 8 )
20	1	renegcli	⊢ - 1 ∈ ℝ
21		1z	⊢ 1 ∈ ℤ
22		modcyc	⊢ ( ( - 1 ∈ ℝ ∧ 8 ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( - 1 + ( 1 · 8 ) ) mod 8 ) = ( - 1 mod 8 ) )
23	20 4 21 22	mp3an	⊢ ( ( - 1 + ( 1 · 8 ) ) mod 8 ) = ( - 1 mod 8 )
24		7re	⊢ 7 ∈ ℝ
25		0re	⊢ 0 ∈ ℝ
26		7pos	⊢ 0 < 7
27	25 24 26	ltleii	⊢ 0 ≤ 7
28		7lt8	⊢ 7 < 8
29		modid	⊢ ( ( ( 7 ∈ ℝ ∧ 8 ∈ ℝ+ ) ∧ ( 0 ≤ 7 ∧ 7 < 8 ) ) → ( 7 mod 8 ) = 7 )
30	24 4 27 28 29	mp4an	⊢ ( 7 mod 8 ) = 7
31	19 23 30	3eqtr3i	⊢ ( - 1 mod 8 ) = 7
32	8 31	pm3.2i	⊢ ( ( 1 mod 8 ) = 1 ∧ ( - 1 mod 8 ) = 7 )
33		3re	⊢ 3 ∈ ℝ
34		3pos	⊢ 0 < 3
35	25 33 34	ltleii	⊢ 0 ≤ 3
36		3lt8	⊢ 3 < 8
37		modid	⊢ ( ( ( 3 ∈ ℝ ∧ 8 ∈ ℝ+ ) ∧ ( 0 ≤ 3 ∧ 3 < 8 ) ) → ( 3 mod 8 ) = 3 )
38	33 4 35 36 37	mp4an	⊢ ( 3 mod 8 ) = 3
39	10	oveq2i	⊢ ( - 3 + ( 1 · 8 ) ) = ( - 3 + 8 )
40		3cn	⊢ 3 ∈ ℂ
41	40	negcli	⊢ - 3 ∈ ℂ
42	9 40	negsubi	⊢ ( 8 + - 3 ) = ( 8 − 3 )
43		5cn	⊢ 5 ∈ ℂ
44		5p3e8	⊢ ( 5 + 3 ) = 8
45	43 40 44	addcomli	⊢ ( 3 + 5 ) = 8
46	9 40 43 45	subaddrii	⊢ ( 8 − 3 ) = 5
47	42 46	eqtri	⊢ ( 8 + - 3 ) = 5
48	9 41 47	addcomli	⊢ ( - 3 + 8 ) = 5
49	39 48	eqtri	⊢ ( - 3 + ( 1 · 8 ) ) = 5
50	49	oveq1i	⊢ ( ( - 3 + ( 1 · 8 ) ) mod 8 ) = ( 5 mod 8 )
51	33	renegcli	⊢ - 3 ∈ ℝ
52		modcyc	⊢ ( ( - 3 ∈ ℝ ∧ 8 ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( - 3 + ( 1 · 8 ) ) mod 8 ) = ( - 3 mod 8 ) )
53	51 4 21 52	mp3an	⊢ ( ( - 3 + ( 1 · 8 ) ) mod 8 ) = ( - 3 mod 8 )
54		5re	⊢ 5 ∈ ℝ
55		5pos	⊢ 0 < 5
56	25 54 55	ltleii	⊢ 0 ≤ 5
57		5lt8	⊢ 5 < 8
58		modid	⊢ ( ( ( 5 ∈ ℝ ∧ 8 ∈ ℝ+ ) ∧ ( 0 ≤ 5 ∧ 5 < 8 ) ) → ( 5 mod 8 ) = 5 )
59	54 4 56 57 58	mp4an	⊢ ( 5 mod 8 ) = 5
60	50 53 59	3eqtr3i	⊢ ( - 3 mod 8 ) = 5
61	38 60	pm3.2i	⊢ ( ( 3 mod 8 ) = 3 ∧ ( - 3 mod 8 ) = 5 )
62	32 61	pm3.2i	⊢ ( ( ( 1 mod 8 ) = 1 ∧ ( - 1 mod 8 ) = 7 ) ∧ ( ( 3 mod 8 ) = 3 ∧ ( - 3 mod 8 ) = 5 ) )