lgsdir2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lgsdir2		GIF version

Theorem lgsdir2 15720

Description: The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)

**Assertion**
Ref	Expression
lgsdir2	⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /_L 2) = ((𝐴 /_L 2) · (𝐵 /_L 2)))

**Proof of Theorem lgsdir2**
Step	Hyp	Ref	Expression
1		0cnd 8147	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → 0 ∈ ℂ)
2		1cnd 8170	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 1 ∈ ℂ)
3		neg1cn 9223	. . . . . . . . . 10 ⊢ -1 ∈ ℂ
4	3	a1i 9	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → -1 ∈ ℂ)
5		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℤ)
6		8nn 9286	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℕ
7	6	a1i 9	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 8 ∈ ℕ)
8	5, 7	zmodcld 10575	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 mod 8) ∈ ℕ₀)
9	8	nn0zd 9575	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 mod 8) ∈ ℤ)
10		1zzd 9481	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 1 ∈ ℤ)
11		zdceq 9530	. . . . . . . . . . . 12 ⊢ (((𝐵 mod 8) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐵 mod 8) = 1)
12	9, 10, 11	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (𝐵 mod 8) = 1)
13		7nn 9285	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℕ
14	13	nnzi 9475	. . . . . . . . . . . . 13 ⊢ 7 ∈ ℤ
15	14	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 7 ∈ ℤ)
16		zdceq 9530	. . . . . . . . . . . 12 ⊢ (((𝐵 mod 8) ∈ ℤ ∧ 7 ∈ ℤ) → DECID (𝐵 mod 8) = 7)
17	9, 15, 16	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (𝐵 mod 8) = 7)
18		dcor 941	. . . . . . . . . . 11 ⊢ (DECID (𝐵 mod 8) = 1 → (DECID (𝐵 mod 8) = 7 → DECID ((𝐵 mod 8) = 1 ∨ (𝐵 mod 8) = 7)))
19	12, 17, 18	sylc 62	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID ((𝐵 mod 8) = 1 ∨ (𝐵 mod 8) = 7))
20		elprg 3686	. . . . . . . . . . . 12 ⊢ ((𝐵 mod 8) ∈ ℕ₀ → ((𝐵 mod 8) ∈ {1, 7} ↔ ((𝐵 mod 8) = 1 ∨ (𝐵 mod 8) = 7)))
21	8, 20	syl 14	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 mod 8) ∈ {1, 7} ↔ ((𝐵 mod 8) = 1 ∨ (𝐵 mod 8) = 7)))
22	21	dcbid 843	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (DECID (𝐵 mod 8) ∈ {1, 7} ↔ DECID ((𝐵 mod 8) = 1 ∨ (𝐵 mod 8) = 7)))
23	19, 22	mpbird 167	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (𝐵 mod 8) ∈ {1, 7})
24	2, 4, 23	ifcldcd 3640	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → if((𝐵 mod 8) ∈ {1, 7}, 1, -1) ∈ ℂ)
25	24	adantr 276	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → if((𝐵 mod 8) ∈ {1, 7}, 1, -1) ∈ ℂ)
26		2nn 9280	. . . . . . . . 9 ⊢ 2 ∈ ℕ
27	26	a1i 9	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → 2 ∈ ℕ)
28		simplr 528	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → 𝐵 ∈ ℤ)
29		dvdsdc 12317	. . . . . . . 8 ⊢ ((2 ∈ ℕ ∧ 𝐵 ∈ ℤ) → DECID 2 ∥ 𝐵)
30	27, 28, 29	syl2anc 411	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → DECID 2 ∥ 𝐵)
31	1, 25, 30	ifcldcd 3640	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) ∈ ℂ)
32	31	mul02d 8546	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → (0 · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = 0)
33		iftrue 3607	. . . . . . 7 ⊢ (2 ∥ 𝐴 → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = 0)
34	33	adantl 277	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = 0)
35	34	oveq1d 6022	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = (0 · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))))
36		2z 9482	. . . . . . . 8 ⊢ 2 ∈ ℤ
37		dvdsmultr1 12350	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2 ∥ 𝐴 → 2 ∥ (𝐴 · 𝐵)))
38	36, 37	mp3an1 1358	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2 ∥ 𝐴 → 2 ∥ (𝐴 · 𝐵)))
39	38	imp 124	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → 2 ∥ (𝐴 · 𝐵))
40	39	iftrued 3609	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)) = 0)
41	32, 35, 40	3eqtr4d 2272	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐴) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)))
42		0cnd 8147	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 0 ∈ ℂ)
43		simpl 109	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈ ℤ)
44	43, 7	zmodcld 10575	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 mod 8) ∈ ℕ₀)
45	44	nn0zd 9575	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 mod 8) ∈ ℤ)
46		zdceq 9530	. . . . . . . . . . . 12 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 mod 8) = 1)
47	45, 10, 46	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (𝐴 mod 8) = 1)
48		zdceq 9530	. . . . . . . . . . . 12 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 7 ∈ ℤ) → DECID (𝐴 mod 8) = 7)
49	45, 15, 48	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (𝐴 mod 8) = 7)
50		dcor 941	. . . . . . . . . . 11 ⊢ (DECID (𝐴 mod 8) = 1 → (DECID (𝐴 mod 8) = 7 → DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
51	47, 49, 50	sylc 62	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7))
52		elprg 3686	. . . . . . . . . . . 12 ⊢ ((𝐴 mod 8) ∈ ℕ₀ → ((𝐴 mod 8) ∈ {1, 7} ↔ ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
53	44, 52	syl 14	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 8) ∈ {1, 7} ↔ ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
54	53	dcbid 843	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (DECID (𝐴 mod 8) ∈ {1, 7} ↔ DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
55	51, 54	mpbird 167	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (𝐴 mod 8) ∈ {1, 7})
56	2, 4, 55	ifcldcd 3640	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ∈ ℂ)
57	26	a1i 9	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 2 ∈ ℕ)
58		dvdsdc 12317	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℤ) → DECID 2 ∥ 𝐴)
59	57, 43, 58	syl2anc 411	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID 2 ∥ 𝐴)
60	42, 56, 59	ifcldcd 3640	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) ∈ ℂ)
61	60	mul01d 8547	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · 0) = 0)
62	61	adantr 276	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐵) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · 0) = 0)
63		iftrue 3607	. . . . . . 7 ⊢ (2 ∥ 𝐵 → if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = 0)
64	63	adantl 277	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐵) → if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = 0)
65	64	oveq2d 6023	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐵) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · 0))
66		dvdsmultr2 12352	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2 ∥ 𝐵 → 2 ∥ (𝐴 · 𝐵)))
67	36, 66	mp3an1 1358	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2 ∥ 𝐵 → 2 ∥ (𝐴 · 𝐵)))
68	67	imp 124	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐵) → 2 ∥ (𝐴 · 𝐵))
69	68	iftrued 3609	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐵) → if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)) = 0)
70	62, 65, 69	3eqtr4d 2272	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥ 𝐵) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)))
71	41, 70	jaodan 802	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵)) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)))
72		ioran 757	. . . 4 ⊢ (¬ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵) ↔ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵))
73	24	ad2antrr 488	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) → if((𝐵 mod 8) ∈ {1, 7}, 1, -1) ∈ ℂ)
74	73	mulid2d 8173	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) → (1 · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = if((𝐵 mod 8) ∈ {1, 7}, 1, -1))
75		iftrue 3607	. . . . . . . . . 10 ⊢ ((𝐴 mod 8) ∈ {1, 7} → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) = 1)
76	75	adantl 277	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) = 1)
77	76	oveq1d 6022	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = (1 · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)))
78		lgsdir2lem4 15718	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐵 mod 8) ∈ {1, 7}))
79	78	adantlr 477	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐵 mod 8) ∈ {1, 7}))
80	79	ifbid 3624	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) → if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1) = if((𝐵 mod 8) ∈ {1, 7}, 1, -1))
81	74, 77, 80	3eqtr4d 2272	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1))
82	56	mulridd 8171	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · 1) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
83	82	ad2antrr 488	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · 1) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
84		iftrue 3607	. . . . . . . . . 10 ⊢ ((𝐵 mod 8) ∈ {1, 7} → if((𝐵 mod 8) ∈ {1, 7}, 1, -1) = 1)
85	84	adantl 277	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → if((𝐵 mod 8) ∈ {1, 7}, 1, -1) = 1)
86	85	oveq2d 6023	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · 1))
87		zcn 9459	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
88		zcn 9459	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℂ)
89		mulcom 8136	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
90	87, 88, 89	syl2an 289	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
91	90	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
92	91	oveq1d 6022	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → ((𝐴 · 𝐵) mod 8) = ((𝐵 · 𝐴) mod 8))
93	92	eleq1d 2298	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ ((𝐵 · 𝐴) mod 8) ∈ {1, 7}))
94		lgsdir2lem4 15718	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (𝐵 mod 8) ∈ {1, 7}) → (((𝐵 · 𝐴) mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
95	94	ancom1s 569	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐵 mod 8) ∈ {1, 7}) → (((𝐵 · 𝐴) mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
96	95	adantlr 477	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → (((𝐵 · 𝐴) mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
97	93, 96	bitrd 188	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
98	97	ifbid 3624	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
99	83, 86, 98	3eqtr4d 2272	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1))
100	81, 99	jaodan 802	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7})) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1))
101		ioran 757	. . . . . . 7 ⊢ (¬ ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7}) ↔ (¬ (𝐴 mod 8) ∈ {1, 7} ∧ ¬ (𝐵 mod 8) ∈ {1, 7}))
102		neg1mulneg1e1 9331	. . . . . . . 8 ⊢ (-1 · -1) = 1
103		iffalse 3610	. . . . . . . . . 10 ⊢ (¬ (𝐴 mod 8) ∈ {1, 7} → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) = -1)
104		iffalse 3610	. . . . . . . . . 10 ⊢ (¬ (𝐵 mod 8) ∈ {1, 7} → if((𝐵 mod 8) ∈ {1, 7}, 1, -1) = -1)
105	103, 104	oveqan12d 6026	. . . . . . . . 9 ⊢ ((¬ (𝐴 mod 8) ∈ {1, 7} ∧ ¬ (𝐵 mod 8) ∈ {1, 7}) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = (-1 · -1))
106	105	adantl 277	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (¬ (𝐴 mod 8) ∈ {1, 7} ∧ ¬ (𝐵 mod 8) ∈ {1, 7})) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = (-1 · -1))
107		lgsdir2lem3 15717	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5}))
108	107	ad2ant2r 509	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5}))
109		elun 3345	. . . . . . . . . . . . 13 ⊢ ((𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5}) ↔ ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐴 mod 8) ∈ {3, 5}))
110	108, 109	sylib 122	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐴 mod 8) ∈ {3, 5}))
111	110	orcanai 933	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ ¬ (𝐴 mod 8) ∈ {1, 7}) → (𝐴 mod 8) ∈ {3, 5})
112		lgsdir2lem3 15717	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵) → (𝐵 mod 8) ∈ ({1, 7} ∪ {3, 5}))
113	112	ad2ant2l 508	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → (𝐵 mod 8) ∈ ({1, 7} ∪ {3, 5}))
114		elun 3345	. . . . . . . . . . . . 13 ⊢ ((𝐵 mod 8) ∈ ({1, 7} ∪ {3, 5}) ↔ ((𝐵 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {3, 5}))
115	113, 114	sylib 122	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → ((𝐵 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {3, 5}))
116	115	orcanai 933	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ ¬ (𝐵 mod 8) ∈ {1, 7}) → (𝐵 mod 8) ∈ {3, 5})
117	111, 116	anim12dan 602	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (¬ (𝐴 mod 8) ∈ {1, 7} ∧ ¬ (𝐵 mod 8) ∈ {1, 7})) → ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5}))
118		lgsdir2lem5 15719	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7})
119	118	adantlr 477	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7})
120	117, 119	syldan 282	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (¬ (𝐴 mod 8) ∈ {1, 7} ∧ ¬ (𝐵 mod 8) ∈ {1, 7})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7})
121	120	iftrued 3609	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (¬ (𝐴 mod 8) ∈ {1, 7} ∧ ¬ (𝐵 mod 8) ∈ {1, 7})) → if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1) = 1)
122	102, 106, 121	3eqtr4a 2288	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ (¬ (𝐴 mod 8) ∈ {1, 7} ∧ ¬ (𝐵 mod 8) ∈ {1, 7})) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1))
123	101, 122	sylan2b 287	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) ∧ ¬ ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7})) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1))
124		dcor 941	. . . . . . . . 9 ⊢ (DECID (𝐴 mod 8) ∈ {1, 7} → (DECID (𝐵 mod 8) ∈ {1, 7} → DECID ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7})))
125	55, 23, 124	sylc 62	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7}))
126	125	adantr 276	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → DECID ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7}))
127		exmiddc 841	. . . . . . 7 ⊢ (DECID ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7}) → (((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7}) ∨ ¬ ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7})))
128	126, 127	syl 14	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → (((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7}) ∨ ¬ ((𝐴 mod 8) ∈ {1, 7} ∨ (𝐵 mod 8) ∈ {1, 7})))
129	100, 123, 128	mpjaodan 803	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1))
130		iffalse 3610	. . . . . . 7 ⊢ (¬ 2 ∥ 𝐴 → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
131		iffalse 3610	. . . . . . 7 ⊢ (¬ 2 ∥ 𝐵 → if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) = if((𝐵 mod 8) ∈ {1, 7}, 1, -1))
132	130, 131	oveqan12d 6026	. . . . . 6 ⊢ ((¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)))
133	132	adantl 277	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) · if((𝐵 mod 8) ∈ {1, 7}, 1, -1)))
134		2prm 12657	. . . . . . . . . 10 ⊢ 2 ∈ ℙ
135		euclemma 12676	. . . . . . . . . 10 ⊢ ((2 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2 ∥ (𝐴 · 𝐵) ↔ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵)))
136	134, 135	mp3an1 1358	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2 ∥ (𝐴 · 𝐵) ↔ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵)))
137	136	notbid 671	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (¬ 2 ∥ (𝐴 · 𝐵) ↔ ¬ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵)))
138	137	biimpar 297	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 · 𝐵))
139	72, 138	sylan2br 288	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 · 𝐵))
140		iffalse 3610	. . . . . 6 ⊢ (¬ 2 ∥ (𝐴 · 𝐵) → if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1))
141	139, 140	syl 14	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1))
142	129, 133, 141	3eqtr4d 2272	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵)) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)))
143	72, 142	sylan2b 287	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵)) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)))
144	57, 5, 29	syl2anc 411	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID 2 ∥ 𝐵)
145		dcor 941	. . . . 5 ⊢ (DECID 2 ∥ 𝐴 → (DECID 2 ∥ 𝐵 → DECID (2 ∥ 𝐴 ∨ 2 ∥ 𝐵)))
146	59, 144, 145	sylc 62	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID (2 ∥ 𝐴 ∨ 2 ∥ 𝐵))
147		exmiddc 841	. . . 4 ⊢ (DECID (2 ∥ 𝐴 ∨ 2 ∥ 𝐵) → ((2 ∥ 𝐴 ∨ 2 ∥ 𝐵) ∨ ¬ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵)))
148	146, 147	syl 14	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((2 ∥ 𝐴 ∨ 2 ∥ 𝐵) ∨ ¬ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵)))
149	71, 143, 148	mpjaodan 803	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))) = if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)))
150		lgs2 15704	. . 3 ⊢ (𝐴 ∈ ℤ → (𝐴 /_L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
151		lgs2 15704	. . 3 ⊢ (𝐵 ∈ ℤ → (𝐵 /_L 2) = if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1)))
152	150, 151	oveqan12d 6026	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 /_L 2) · (𝐵 /_L 2)) = (if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) · if(2 ∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))))
153		zmulcl 9508	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) ∈ ℤ)
154		lgs2 15704	. . 3 ⊢ ((𝐴 · 𝐵) ∈ ℤ → ((𝐴 · 𝐵) /_L 2) = if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)))
155	153, 154	syl 14	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /_L 2) = if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)))
156	149, 152, 155	3eqtr4rd 2273	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /_L 2) = ((𝐴 /_L 2) · (𝐵 /_L 2)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 713 DECID wdc 839 = wceq 1395 ∈ wcel 2200 ∪ cun 3195 ifcif 3602 {cpr 3667 class class class wbr 4083 (class class class)co 6007 ℂcc 8005 0cc0 8007 1c1 8008 · cmul 8012 -cneg 8326 ℕcn 9118 2c2 9169 3c3 9170 5c5 9172 7c7 9174 8c8 9175 ℕ₀cn0 9377 ℤcz 9454 mod cmo 10552 ∥ cdvds 12306 ℙcprime 12637 /_L clgs 15684

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4199 ax-sep 4202 ax-nul 4210 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629 ax-iinf 4680 ax-cnex 8098 ax-resscn 8099 ax-1cn 8100 ax-1re 8101 ax-icn 8102 ax-addcl 8103 ax-addrcl 8104 ax-mulcl 8105 ax-mulrcl 8106 ax-addcom 8107 ax-mulcom 8108 ax-addass 8109 ax-mulass 8110 ax-distr 8111 ax-i2m1 8112 ax-0lt1 8113 ax-1rid 8114 ax-0id 8115 ax-rnegex 8116 ax-precex 8117 ax-cnre 8118 ax-pre-ltirr 8119 ax-pre-ltwlin 8120 ax-pre-lttrn 8121 ax-pre-apti 8122 ax-pre-ltadd 8123 ax-pre-mulgt0 8124 ax-pre-mulext 8125 ax-arch 8126 ax-caucvg 8127

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-xor 1418 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-tr 4183 df-id 4384 df-po 4387 df-iso 4388 df-iord 4457 df-on 4459 df-ilim 4460 df-suc 4462 df-iom 4683 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-isom 5327 df-riota 5960 df-ov 6010 df-oprab 6011 df-mpo 6012 df-1st 6292 df-2nd 6293 df-recs 6457 df-irdg 6522 df-frec 6543 df-1o 6568 df-2o 6569 df-oadd 6572 df-er 6688 df-en 6896 df-dom 6897 df-fin 6898 df-sup 7159 df-inf 7160 df-pnf 8191 df-mnf 8192 df-xr 8193 df-ltxr 8194 df-le 8195 df-sub 8327 df-neg 8328 df-reap 8730 df-ap 8737 df-div 8828 df-inn 9119 df-2 9177 df-3 9178 df-4 9179 df-5 9180 df-6 9181 df-7 9182 df-8 9183 df-9 9184 df-n0 9378 df-z 9455 df-uz 9731 df-q 9823 df-rp 9858 df-fz 10213 df-fzo 10347 df-fl 10498 df-mod 10553 df-seqfrec 10678 df-exp 10769 df-ihash 11006 df-cj 11361 df-re 11362 df-im 11363 df-rsqrt 11517 df-abs 11518 df-clim 11798 df-proddc 12070 df-dvds 12307 df-gcd 12483 df-prm 12638 df-phi 12741 df-pc 12816 df-lgs 15685

This theorem is referenced by: lgsdirprm 15721

W3C validator