Theorem lgsdir2lem4

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

	Ref	Expression
Assertion	lgsdir2lem4	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) ∈ { 1 , 7 } ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( 𝐴 mod 8 ) ∈ V
2	1	elpr	⊢ ( ( 𝐴 mod 8 ) ∈ { 1 , 7 } ↔ ( ( 𝐴 mod 8 ) = 1 ∨ ( 𝐴 mod 8 ) = 7 ) )
3		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
4	3	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → 𝐴 ∈ ℝ )
5		1red	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → 1 ∈ ℝ )
6		simplr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → 𝐵 ∈ ℤ )
7		8re	⊢ 8 ∈ ℝ
8		8pos	⊢ 0 < 8
9	7 8	elrpii	⊢ 8 ∈ ℝ+
10	9	a1i	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → 8 ∈ ℝ+ )
11		simpr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → ( 𝐴 mod 8 ) = 1 )
12		lgsdir2lem1	⊢ ( ( ( 1 mod 8 ) = 1 ∧ ( - 1 mod 8 ) = 7 ) ∧ ( ( 3 mod 8 ) = 3 ∧ ( - 3 mod 8 ) = 5 ) )
13	12	simpli	⊢ ( ( 1 mod 8 ) = 1 ∧ ( - 1 mod 8 ) = 7 )
14	13	simpli	⊢ ( 1 mod 8 ) = 1
15	11 14	eqtr4di	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → ( 𝐴 mod 8 ) = ( 1 mod 8 ) )
16		modmul1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 𝐵 ∈ ℤ ∧ 8 ∈ ℝ+ ) ∧ ( 𝐴 mod 8 ) = ( 1 mod 8 ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 1 · 𝐵 ) mod 8 ) )
17	4 5 6 10 15 16	syl221anc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( 1 · 𝐵 ) mod 8 ) )
18		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
19	18	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → 𝐵 ∈ ℂ )
20	19	mullidd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → ( 1 · 𝐵 ) = 𝐵 )
21	20	oveq1d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → ( ( 1 · 𝐵 ) mod 8 ) = ( 𝐵 mod 8 ) )
22	17 21	eqtrd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( 𝐵 mod 8 ) )
23	22	eleq1d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 1 ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
24	3	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → 𝐴 ∈ ℝ )
25		neg1rr	⊢ - 1 ∈ ℝ
26	25	a1i	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → - 1 ∈ ℝ )
27		simplr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → 𝐵 ∈ ℤ )
28	9	a1i	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → 8 ∈ ℝ+ )
29		simpr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → ( 𝐴 mod 8 ) = 7 )
30	13	simpri	⊢ ( - 1 mod 8 ) = 7
31	29 30	eqtr4di	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → ( 𝐴 mod 8 ) = ( - 1 mod 8 ) )
32		modmul1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ - 1 ∈ ℝ ) ∧ ( 𝐵 ∈ ℤ ∧ 8 ∈ ℝ+ ) ∧ ( 𝐴 mod 8 ) = ( - 1 mod 8 ) ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( - 1 · 𝐵 ) mod 8 ) )
33	24 26 27 28 31 32	syl221anc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( ( - 1 · 𝐵 ) mod 8 ) )
34	18	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → 𝐵 ∈ ℂ )
35	34	mulm1d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → ( - 1 · 𝐵 ) = - 𝐵 )
36	35	oveq1d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → ( ( - 1 · 𝐵 ) mod 8 ) = ( - 𝐵 mod 8 ) )
37	33 36	eqtrd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → ( ( 𝐴 · 𝐵 ) mod 8 ) = ( - 𝐵 mod 8 ) )
38	37	eleq1d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { 1 , 7 } ↔ ( - 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
39		znegcl	⊢ ( 𝐵 ∈ ℤ → - 𝐵 ∈ ℤ )
40		oveq1	⊢ ( 𝑥 = - 𝐵 → ( 𝑥 mod 8 ) = ( - 𝐵 mod 8 ) )
41	40	eleq1d	⊢ ( 𝑥 = - 𝐵 → ( ( 𝑥 mod 8 ) ∈ { 1 , 7 } ↔ ( - 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
42		negeq	⊢ ( 𝑥 = - 𝐵 → - 𝑥 = - - 𝐵 )
43	42	oveq1d	⊢ ( 𝑥 = - 𝐵 → ( - 𝑥 mod 8 ) = ( - - 𝐵 mod 8 ) )
44	43	eleq1d	⊢ ( 𝑥 = - 𝐵 → ( ( - 𝑥 mod 8 ) ∈ { 1 , 7 } ↔ ( - - 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
45	41 44	imbi12d	⊢ ( 𝑥 = - 𝐵 → ( ( ( 𝑥 mod 8 ) ∈ { 1 , 7 } → ( - 𝑥 mod 8 ) ∈ { 1 , 7 } ) ↔ ( ( - 𝐵 mod 8 ) ∈ { 1 , 7 } → ( - - 𝐵 mod 8 ) ∈ { 1 , 7 } ) ) )
46		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
47		neg1cn	⊢ - 1 ∈ ℂ
48		mulcom	⊢ ( ( 𝑥 ∈ ℂ ∧ - 1 ∈ ℂ ) → ( 𝑥 · - 1 ) = ( - 1 · 𝑥 ) )
49	47 48	mpan2	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · - 1 ) = ( - 1 · 𝑥 ) )
50		mulm1	⊢ ( 𝑥 ∈ ℂ → ( - 1 · 𝑥 ) = - 𝑥 )
51	49 50	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · - 1 ) = - 𝑥 )
52	46 51	syl	⊢ ( 𝑥 ∈ ℤ → ( 𝑥 · - 1 ) = - 𝑥 )
53	52	adantr	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → ( 𝑥 · - 1 ) = - 𝑥 )
54	53	oveq1d	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → ( ( 𝑥 · - 1 ) mod 8 ) = ( - 𝑥 mod 8 ) )
55		zre	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
56	55	adantr	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → 𝑥 ∈ ℝ )
57		1red	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → 1 ∈ ℝ )
58		neg1z	⊢ - 1 ∈ ℤ
59	58	a1i	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → - 1 ∈ ℤ )
60	9	a1i	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → 8 ∈ ℝ+ )
61		simpr	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → ( 𝑥 mod 8 ) = 1 )
62	61 14	eqtr4di	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → ( 𝑥 mod 8 ) = ( 1 mod 8 ) )
63		modmul1	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( - 1 ∈ ℤ ∧ 8 ∈ ℝ+ ) ∧ ( 𝑥 mod 8 ) = ( 1 mod 8 ) ) → ( ( 𝑥 · - 1 ) mod 8 ) = ( ( 1 · - 1 ) mod 8 ) )
64	56 57 59 60 62 63	syl221anc	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → ( ( 𝑥 · - 1 ) mod 8 ) = ( ( 1 · - 1 ) mod 8 ) )
65	54 64	eqtr3d	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → ( - 𝑥 mod 8 ) = ( ( 1 · - 1 ) mod 8 ) )
66	47	mullidi	⊢ ( 1 · - 1 ) = - 1
67	66	oveq1i	⊢ ( ( 1 · - 1 ) mod 8 ) = ( - 1 mod 8 )
68	67 30	eqtri	⊢ ( ( 1 · - 1 ) mod 8 ) = 7
69	65 68	eqtrdi	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 1 ) → ( - 𝑥 mod 8 ) = 7 )
70	69	ex	⊢ ( 𝑥 ∈ ℤ → ( ( 𝑥 mod 8 ) = 1 → ( - 𝑥 mod 8 ) = 7 ) )
71	52	adantr	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → ( 𝑥 · - 1 ) = - 𝑥 )
72	71	oveq1d	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → ( ( 𝑥 · - 1 ) mod 8 ) = ( - 𝑥 mod 8 ) )
73	55	adantr	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → 𝑥 ∈ ℝ )
74	25	a1i	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → - 1 ∈ ℝ )
75	58	a1i	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → - 1 ∈ ℤ )
76	9	a1i	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → 8 ∈ ℝ+ )
77		simpr	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → ( 𝑥 mod 8 ) = 7 )
78	77 30	eqtr4di	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → ( 𝑥 mod 8 ) = ( - 1 mod 8 ) )
79		modmul1	⊢ ( ( ( 𝑥 ∈ ℝ ∧ - 1 ∈ ℝ ) ∧ ( - 1 ∈ ℤ ∧ 8 ∈ ℝ+ ) ∧ ( 𝑥 mod 8 ) = ( - 1 mod 8 ) ) → ( ( 𝑥 · - 1 ) mod 8 ) = ( ( - 1 · - 1 ) mod 8 ) )
80	73 74 75 76 78 79	syl221anc	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → ( ( 𝑥 · - 1 ) mod 8 ) = ( ( - 1 · - 1 ) mod 8 ) )
81	72 80	eqtr3d	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → ( - 𝑥 mod 8 ) = ( ( - 1 · - 1 ) mod 8 ) )
82		neg1mulneg1e1	⊢ ( - 1 · - 1 ) = 1
83	82	oveq1i	⊢ ( ( - 1 · - 1 ) mod 8 ) = ( 1 mod 8 )
84	83 14	eqtri	⊢ ( ( - 1 · - 1 ) mod 8 ) = 1
85	81 84	eqtrdi	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 mod 8 ) = 7 ) → ( - 𝑥 mod 8 ) = 1 )
86	85	ex	⊢ ( 𝑥 ∈ ℤ → ( ( 𝑥 mod 8 ) = 7 → ( - 𝑥 mod 8 ) = 1 ) )
87	70 86	orim12d	⊢ ( 𝑥 ∈ ℤ → ( ( ( 𝑥 mod 8 ) = 1 ∨ ( 𝑥 mod 8 ) = 7 ) → ( ( - 𝑥 mod 8 ) = 7 ∨ ( - 𝑥 mod 8 ) = 1 ) ) )
88		ovex	⊢ ( 𝑥 mod 8 ) ∈ V
89	88	elpr	⊢ ( ( 𝑥 mod 8 ) ∈ { 1 , 7 } ↔ ( ( 𝑥 mod 8 ) = 1 ∨ ( 𝑥 mod 8 ) = 7 ) )
90		ovex	⊢ ( - 𝑥 mod 8 ) ∈ V
91	90	elpr	⊢ ( ( - 𝑥 mod 8 ) ∈ { 1 , 7 } ↔ ( ( - 𝑥 mod 8 ) = 1 ∨ ( - 𝑥 mod 8 ) = 7 ) )
92		orcom	⊢ ( ( ( - 𝑥 mod 8 ) = 1 ∨ ( - 𝑥 mod 8 ) = 7 ) ↔ ( ( - 𝑥 mod 8 ) = 7 ∨ ( - 𝑥 mod 8 ) = 1 ) )
93	91 92	bitri	⊢ ( ( - 𝑥 mod 8 ) ∈ { 1 , 7 } ↔ ( ( - 𝑥 mod 8 ) = 7 ∨ ( - 𝑥 mod 8 ) = 1 ) )
94	87 89 93	3imtr4g	⊢ ( 𝑥 ∈ ℤ → ( ( 𝑥 mod 8 ) ∈ { 1 , 7 } → ( - 𝑥 mod 8 ) ∈ { 1 , 7 } ) )
95	45 94	vtoclga	⊢ ( - 𝐵 ∈ ℤ → ( ( - 𝐵 mod 8 ) ∈ { 1 , 7 } → ( - - 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
96	39 95	syl	⊢ ( 𝐵 ∈ ℤ → ( ( - 𝐵 mod 8 ) ∈ { 1 , 7 } → ( - - 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
97	18	negnegd	⊢ ( 𝐵 ∈ ℤ → - - 𝐵 = 𝐵 )
98	97	oveq1d	⊢ ( 𝐵 ∈ ℤ → ( - - 𝐵 mod 8 ) = ( 𝐵 mod 8 ) )
99	98	eleq1d	⊢ ( 𝐵 ∈ ℤ → ( ( - - 𝐵 mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
100	96 99	sylibd	⊢ ( 𝐵 ∈ ℤ → ( ( - 𝐵 mod 8 ) ∈ { 1 , 7 } → ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
101		oveq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 mod 8 ) = ( 𝐵 mod 8 ) )
102	101	eleq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
103		negeq	⊢ ( 𝑥 = 𝐵 → - 𝑥 = - 𝐵 )
104	103	oveq1d	⊢ ( 𝑥 = 𝐵 → ( - 𝑥 mod 8 ) = ( - 𝐵 mod 8 ) )
105	104	eleq1d	⊢ ( 𝑥 = 𝐵 → ( ( - 𝑥 mod 8 ) ∈ { 1 , 7 } ↔ ( - 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
106	102 105	imbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ( 𝑥 mod 8 ) ∈ { 1 , 7 } → ( - 𝑥 mod 8 ) ∈ { 1 , 7 } ) ↔ ( ( 𝐵 mod 8 ) ∈ { 1 , 7 } → ( - 𝐵 mod 8 ) ∈ { 1 , 7 } ) ) )
107	106 94	vtoclga	⊢ ( 𝐵 ∈ ℤ → ( ( 𝐵 mod 8 ) ∈ { 1 , 7 } → ( - 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
108	100 107	impbid	⊢ ( 𝐵 ∈ ℤ → ( ( - 𝐵 mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
109	108	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → ( ( - 𝐵 mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
110	38 109	bitrd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) = 7 ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
111	23 110	jaodan	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 mod 8 ) = 1 ∨ ( 𝐴 mod 8 ) = 7 ) ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )
112	2 111	sylan2b	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐴 mod 8 ) ∈ { 1 , 7 } ) → ( ( ( 𝐴 · 𝐵 ) mod 8 ) ∈ { 1 , 7 } ↔ ( 𝐵 mod 8 ) ∈ { 1 , 7 } ) )