lgsdir2lem5

		Ref	Expression
	Assertion	lgsdir2lem5	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 \in \{3, 5\} \land B \mod 8 \in \{3, 5\})) \to A B \mod 8 \in \{1, 7\}$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ A \mod 8 \in V$
2	1	elpr	$⊢ A \mod 8 \in \{3, 5\} \leftrightarrow (A \mod 8 = 3 \lor A \mod 8 = 5)$
3		ovex	$⊢ B \mod 8 \in V$
4	3	elpr	$⊢ B \mod 8 \in \{3, 5\} \leftrightarrow (B \mod 8 = 3 \lor B \mod 8 = 5)$
5	2 4	anbi12i	$⊢ (A \mod 8 \in \{3, 5\} \land B \mod 8 \in \{3, 5\}) \leftrightarrow ((A \mod 8 = 3 \lor A \mod 8 = 5) \land (B \mod 8 = 3 \lor B \mod 8 = 5))$
6		simpll	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to A \in ℤ$
7		3z	$⊢ 3 \in ℤ$
8	7	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to 3 \in ℤ$
9		simplr	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to B \in ℤ$
10		8re	$⊢ 8 \in ℝ$
11		8pos	$⊢ 0 < 8$
12	10 11	elrpii	$⊢ 8 \in ℝ^{+}$
13	12	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to 8 \in ℝ^{+}$
14		simprl	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to A \mod 8 = 3$
15		lgsdir2lem1	$⊢ ((1 \mod 8 = 1 \land -1 \mod 8 = 7) \land (3 \mod 8 = 3 \land -3 \mod 8 = 5))$
16	15	simpri	$⊢ (3 \mod 8 = 3 \land -3 \mod 8 = 5)$
17	16	simpli	$⊢ 3 \mod 8 = 3$
18	14 17	eqtr4di	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to A \mod 8 = 3 \mod 8$
19		simprr	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to B \mod 8 = 3$
20	19 17	eqtr4di	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to B \mod 8 = 3 \mod 8$
21	6 8 9 8 13 18 20	modmul12d	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to A B \mod 8 = 3 \cdot 3 \mod 8$
22	21	orcd	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 3)) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8)$
23	22	ex	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \mod 8 = 3 \land B \mod 8 = 3) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8))$
24		simpll	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to A \in ℤ$
25		znegcl	$⊢ 3 \in ℤ \to - 3 \in ℤ$
26	7 25	mp1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to - 3 \in ℤ$
27		simplr	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to B \in ℤ$
28	7	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to 3 \in ℤ$
29	12	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to 8 \in ℝ^{+}$
30		simprl	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to A \mod 8 = 5$
31	16	simpri	$⊢ -3 \mod 8 = 5$
32	30 31	eqtr4di	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to A \mod 8 = -3 \mod 8$
33		simprr	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to B \mod 8 = 3$
34	33 17	eqtr4di	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to B \mod 8 = 3 \mod 8$
35	24 26 27 28 29 32 34	modmul12d	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to A B \mod 8 = -3 \cdot 3 \mod 8$
36		3cn	$⊢ 3 \in ℂ$
37	36 36	mulneg1i	$⊢ -3 \cdot 3 = - 3 \cdot 3$
38	37	oveq1i	$⊢ -3 \cdot 3 \mod 8 = (- 3 \cdot 3) \mod 8$
39	35 38	eqtrdi	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to A B \mod 8 = (- 3 \cdot 3) \mod 8$
40	39	olcd	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 3)) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8)$
41	40	ex	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \mod 8 = 5 \land B \mod 8 = 3) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8))$
42		simpll	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to A \in ℤ$
43	7	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to 3 \in ℤ$
44		simplr	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to B \in ℤ$
45	7 25	mp1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to - 3 \in ℤ$
46	12	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to 8 \in ℝ^{+}$
47		simprl	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to A \mod 8 = 3$
48	47 17	eqtr4di	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to A \mod 8 = 3 \mod 8$
49		simprr	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to B \mod 8 = 5$
50	49 31	eqtr4di	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to B \mod 8 = -3 \mod 8$
51	42 43 44 45 46 48 50	modmul12d	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to A B \mod 8 = 3 -3 \mod 8$
52	36 36	mulneg2i	$⊢ 3 -3 = - 3 \cdot 3$
53	52	oveq1i	$⊢ 3 -3 \mod 8 = (- 3 \cdot 3) \mod 8$
54	51 53	eqtrdi	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to A B \mod 8 = (- 3 \cdot 3) \mod 8$
55	54	olcd	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 3 \land B \mod 8 = 5)) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8)$
56	55	ex	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \mod 8 = 3 \land B \mod 8 = 5) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8))$
57		simpll	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to A \in ℤ$
58	7 25	mp1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to - 3 \in ℤ$
59		simplr	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to B \in ℤ$
60	12	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to 8 \in ℝ^{+}$
61		simprl	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to A \mod 8 = 5$
62	61 31	eqtr4di	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to A \mod 8 = -3 \mod 8$
63		simprr	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to B \mod 8 = 5$
64	63 31	eqtr4di	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to B \mod 8 = -3 \mod 8$
65	57 58 59 58 60 62 64	modmul12d	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to A B \mod 8 = -3 -3 \mod 8$
66	36 36	mul2negi	$⊢ -3 -3 = 3 \cdot 3$
67	66	oveq1i	$⊢ -3 -3 \mod 8 = 3 \cdot 3 \mod 8$
68	65 67	eqtrdi	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to A B \mod 8 = 3 \cdot 3 \mod 8$
69	68	orcd	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 = 5 \land B \mod 8 = 5)) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8)$
70	69	ex	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \mod 8 = 5 \land B \mod 8 = 5) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8))$
71	23 41 56 70	ccased	$⊢ (A \in ℤ \land B \in ℤ) \to (((A \mod 8 = 3 \lor A \mod 8 = 5) \land (B \mod 8 = 3 \lor B \mod 8 = 5)) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8))$
72	5 71	syl5bi	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \mod 8 \in \{3, 5\} \land B \mod 8 \in \{3, 5\}) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8))$
73	72	imp	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 \in \{3, 5\} \land B \mod 8 \in \{3, 5\})) \to (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8)$
74		ovex	$⊢ A B \mod 8 \in V$
75	74	elpr	$⊢ A B \mod 8 \in \{3 \cdot 3 \mod 8, (- 3 \cdot 3) \mod 8\} \leftrightarrow (A B \mod 8 = 3 \cdot 3 \mod 8 \lor A B \mod 8 = (- 3 \cdot 3) \mod 8)$
76	73 75	sylibr	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 \in \{3, 5\} \land B \mod 8 \in \{3, 5\})) \to A B \mod 8 \in \{3 \cdot 3 \mod 8, (- 3 \cdot 3) \mod 8\}$
77		df-9	$⊢ 9 = 8 + 1$
78		8cn	$⊢ 8 \in ℂ$
79		ax-1cn	$⊢ 1 \in ℂ$
80	78 79	addcomi	$⊢ 8 + 1 = 1 + 8$
81	77 80	eqtri	$⊢ 9 = 1 + 8$
82		3t3e9	$⊢ 3 \cdot 3 = 9$
83	78	mulid2i	$⊢ 1 \cdot 8 = 8$
84	83	oveq2i	$⊢ 1 + 1 \cdot 8 = 1 + 8$
85	81 82 84	3eqtr4i	$⊢ 3 \cdot 3 = 1 + 1 \cdot 8$
86	85	oveq1i	$⊢ 3 \cdot 3 \mod 8 = (1 + 1 \cdot 8) \mod 8$
87		1re	$⊢ 1 \in ℝ$
88		1z	$⊢ 1 \in ℤ$
89		modcyc	$⊢ (1 \in ℝ \land 8 \in ℝ^{+} \land 1 \in ℤ) \to (1 + 1 \cdot 8) \mod 8 = 1 \mod 8$
90	87 12 88 89	mp3an	$⊢ (1 + 1 \cdot 8) \mod 8 = 1 \mod 8$
91	86 90	eqtri	$⊢ 3 \cdot 3 \mod 8 = 1 \mod 8$
92	15	simpli	$⊢ (1 \mod 8 = 1 \land -1 \mod 8 = 7)$
93	92	simpli	$⊢ 1 \mod 8 = 1$
94	91 93	eqtri	$⊢ 3 \cdot 3 \mod 8 = 1$
95		znegcl	$⊢ 1 \in ℤ \to - 1 \in ℤ$
96	88 95	mp1i	$⊢ ⊤ \to - 1 \in ℤ$
97		3nn	$⊢ 3 \in ℕ$
98	97 97	nnmulcli	$⊢ 3 \cdot 3 \in ℕ$
99	98	nnzi	$⊢ 3 \cdot 3 \in ℤ$
100	99	a1i	$⊢ ⊤ \to 3 \cdot 3 \in ℤ$
101	88	a1i	$⊢ ⊤ \to 1 \in ℤ$
102	12	a1i	$⊢ ⊤ \to 8 \in ℝ^{+}$
103		eqidd	$⊢ ⊤ \to -1 \mod 8 = -1 \mod 8$
104	91	a1i	$⊢ ⊤ \to 3 \cdot 3 \mod 8 = 1 \mod 8$
105	96 96 100 101 102 103 104	modmul12d	$⊢ ⊤ \to -1 3 \cdot 3 \mod 8 = -1 \cdot 1 \mod 8$
106	105	mptru	$⊢ -1 3 \cdot 3 \mod 8 = -1 \cdot 1 \mod 8$
107	36 36	mulcli	$⊢ 3 \cdot 3 \in ℂ$
108	107	mulm1i	$⊢ -1 3 \cdot 3 = - 3 \cdot 3$
109	108	oveq1i	$⊢ -1 3 \cdot 3 \mod 8 = (- 3 \cdot 3) \mod 8$
110	79	mulm1i	$⊢ -1 \cdot 1 = - 1$
111	110	oveq1i	$⊢ -1 \cdot 1 \mod 8 = -1 \mod 8$
112	106 109 111	3eqtr3i	$⊢ (- 3 \cdot 3) \mod 8 = -1 \mod 8$
113	92	simpri	$⊢ -1 \mod 8 = 7$
114	112 113	eqtri	$⊢ (- 3 \cdot 3) \mod 8 = 7$
115	94 114	preq12i	$⊢ \{3 \cdot 3 \mod 8, (- 3 \cdot 3) \mod 8\} = \{1, 7\}$
116	76 115	eleqtrdi	$⊢ ((A \in ℤ \land B \in ℤ) \land (A \mod 8 \in \{3, 5\} \land B \mod 8 \in \{3, 5\})) \to A B \mod 8 \in \{1, 7\}$

Metamath Proof Explorer

Theorem lgsdir2lem5

Proof