Proof of Theorem lgsdir2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0cn 11254 | . . . . . 6
⊢ 0 ∈
ℂ | 
| 2 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 3 |  | neg1cn 12381 | . . . . . . 7
⊢ -1 ∈
ℂ | 
| 4 | 2, 3 | ifcli 4572 | . . . . . 6
⊢ if((𝐵 mod 8) ∈ {1, 7}, 1, -1)
∈ ℂ | 
| 5 | 1, 4 | ifcli 4572 | . . . . 5
⊢ if(2
∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1))
∈ ℂ | 
| 6 | 5 | mul02i 11451 | . . . 4
⊢ (0
· if(2 ∥ 𝐵, 0,
if((𝐵 mod 8) ∈ {1, 7},
1, -1))) = 0 | 
| 7 |  | iftrue 4530 | . . . . . 6
⊢ (2
∥ 𝐴 → if(2
∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) =
0) | 
| 8 | 7 | adantl 481 | . . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥
𝐴) → if(2 ∥
𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) =
0) | 
| 9 | 8 | oveq1d 7447 | . . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 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)))) | 
| 10 |  | 2z 12651 | . . . . . . 7
⊢ 2 ∈
ℤ | 
| 11 |  | dvdsmultr1 16334 | . . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝐴
∈ ℤ ∧ 𝐵
∈ ℤ) → (2 ∥ 𝐴 → 2 ∥ (𝐴 · 𝐵))) | 
| 12 | 10, 11 | mp3an1 1449 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2
∥ 𝐴 → 2 ∥
(𝐴 · 𝐵))) | 
| 13 | 12 | imp 406 | . . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥
𝐴) → 2 ∥ (𝐴 · 𝐵)) | 
| 14 | 13 | iftrued 4532 | . . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥
𝐴) → if(2 ∥
(𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)) =
0) | 
| 15 | 6, 9, 14 | 3eqtr4a 2802 | . . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 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))) | 
| 16 | 2, 3 | ifcli 4572 | . . . . . 6
⊢ if((𝐴 mod 8) ∈ {1, 7}, 1, -1)
∈ ℂ | 
| 17 | 1, 16 | ifcli 4572 | . . . . 5
⊢ if(2
∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
∈ ℂ | 
| 18 | 17 | mul01i 11452 | . . . 4
⊢ (if(2
∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
· 0) = 0 | 
| 19 |  | iftrue 4530 | . . . . . 6
⊢ (2
∥ 𝐵 → if(2
∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) =
0) | 
| 20 | 19 | adantl 481 | . . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥
𝐵) → if(2 ∥
𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) =
0) | 
| 21 | 20 | oveq2d 7448 | . . . 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)) · 0)) | 
| 22 |  | dvdsmultr2 16336 | . . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝐴
∈ ℤ ∧ 𝐵
∈ ℤ) → (2 ∥ 𝐵 → 2 ∥ (𝐴 · 𝐵))) | 
| 23 | 10, 22 | mp3an1 1449 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2
∥ 𝐵 → 2 ∥
(𝐴 · 𝐵))) | 
| 24 | 23 | imp 406 | . . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥
𝐵) → 2 ∥ (𝐴 · 𝐵)) | 
| 25 | 24 | iftrued 4532 | . . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 2 ∥
𝐵) → if(2 ∥
(𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)) =
0) | 
| 26 | 18, 21, 25 | 3eqtr4a 2802 | . . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 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))) | 
| 27 | 4 | mullidi 11267 | . . . . . 6
⊢ (1
· if((𝐵 mod 8)
∈ {1, 7}, 1, -1)) = if((𝐵 mod 8) ∈ {1, 7}, 1,
-1) | 
| 28 |  | iftrue 4530 | . . . . . . . 8
⊢ ((𝐴 mod 8) ∈ {1, 7} →
if((𝐴 mod 8) ∈ {1, 7},
1, -1) = 1) | 
| 29 | 28 | adantl 481 | . . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) →
if((𝐴 mod 8) ∈ {1, 7},
1, -1) = 1) | 
| 30 | 29 | oveq1d 7447 | . . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 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))) | 
| 31 |  | lgsdir2lem4 27373 | . . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 mod 8) ∈ {1, 7}) →
(((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔
(𝐵 mod 8) ∈ {1,
7})) | 
| 32 | 31 | adantlr 715 | . . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) →
(((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔
(𝐵 mod 8) ∈ {1,
7})) | 
| 33 | 32 | ifbid 4548 | . . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐴 mod 8) ∈ {1, 7}) →
if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1) =
if((𝐵 mod 8) ∈ {1, 7},
1, -1)) | 
| 34 | 27, 30, 33 | 3eqtr4a 2802 | . . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 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)) | 
| 35 | 16 | mulridi 11266 | . . . . . 6
⊢
(if((𝐴 mod 8) ∈
{1, 7}, 1, -1) · 1) = if((𝐴 mod 8) ∈ {1, 7}, 1,
-1) | 
| 36 |  | iftrue 4530 | . . . . . . . 8
⊢ ((𝐵 mod 8) ∈ {1, 7} →
if((𝐵 mod 8) ∈ {1, 7},
1, -1) = 1) | 
| 37 | 36 | adantl 481 | . . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) →
if((𝐵 mod 8) ∈ {1, 7},
1, -1) = 1) | 
| 38 | 37 | oveq2d 7448 | . . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 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)) | 
| 39 |  | zcn 12620 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) | 
| 40 |  | zcn 12620 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) | 
| 41 |  | mulcom 11242 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | 
| 42 | 39, 40, 41 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | 
| 43 | 42 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) →
(𝐴 · 𝐵) = (𝐵 · 𝐴)) | 
| 44 | 43 | oveq1d 7447 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) →
((𝐴 · 𝐵) mod 8) = ((𝐵 · 𝐴) mod 8)) | 
| 45 | 44 | eleq1d 2825 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) →
(((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔
((𝐵 · 𝐴) mod 8) ∈ {1,
7})) | 
| 46 |  | lgsdir2lem4 27373 | . . . . . . . . . 10
⊢ (((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (𝐵 mod 8) ∈ {1, 7}) →
(((𝐵 · 𝐴) mod 8) ∈ {1, 7} ↔
(𝐴 mod 8) ∈ {1,
7})) | 
| 47 | 46 | ancom1s 653 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐵 mod 8) ∈ {1, 7}) →
(((𝐵 · 𝐴) mod 8) ∈ {1, 7} ↔
(𝐴 mod 8) ∈ {1,
7})) | 
| 48 | 47 | adantlr 715 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) →
(((𝐵 · 𝐴) mod 8) ∈ {1, 7} ↔
(𝐴 mod 8) ∈ {1,
7})) | 
| 49 | 45, 48 | bitrd 279 | . . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) →
(((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔
(𝐴 mod 8) ∈ {1,
7})) | 
| 50 | 49 | ifbid 4548 | . . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (𝐵 mod 8) ∈ {1, 7}) →
if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1) =
if((𝐴 mod 8) ∈ {1, 7},
1, -1)) | 
| 51 | 35, 38, 50 | 3eqtr4a 2802 | . . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 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)) | 
| 52 |  | neg1mulneg1e1 12480 | . . . . . 6
⊢ (-1
· -1) = 1 | 
| 53 |  | iffalse 4533 | . . . . . . . 8
⊢ (¬
(𝐴 mod 8) ∈ {1, 7}
→ if((𝐴 mod 8) ∈
{1, 7}, 1, -1) = -1) | 
| 54 |  | iffalse 4533 | . . . . . . . 8
⊢ (¬
(𝐵 mod 8) ∈ {1, 7}
→ if((𝐵 mod 8) ∈
{1, 7}, 1, -1) = -1) | 
| 55 | 53, 54 | oveqan12d 7451 | . . . . . . 7
⊢ ((¬
(𝐴 mod 8) ∈ {1, 7}
∧ ¬ (𝐵 mod 8)
∈ {1, 7}) → (if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ·
if((𝐵 mod 8) ∈ {1, 7},
1, -1)) = (-1 · -1)) | 
| 56 | 55 | adantl 481 | . . . . . 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)) = (-1 · -1)) | 
| 57 |  | lgsdir2lem3 27372 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3,
5})) | 
| 58 | 57 | ad2ant2r 747 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3,
5})) | 
| 59 |  | elun 4152 | . . . . . . . . . . 11
⊢ ((𝐴 mod 8) ∈ ({1, 7} ∪ {3,
5}) ↔ ((𝐴 mod 8)
∈ {1, 7} ∨ (𝐴 mod
8) ∈ {3, 5})) | 
| 60 | 58, 59 | sylib 218 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) → ((𝐴 mod 8) ∈ {1, 7} ∨
(𝐴 mod 8) ∈ {3,
5})) | 
| 61 | 60 | orcanai 1004 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ ¬
(𝐴 mod 8) ∈ {1, 7})
→ (𝐴 mod 8) ∈ {3,
5}) | 
| 62 |  | lgsdir2lem3 27372 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℤ ∧ ¬ 2
∥ 𝐵) → (𝐵 mod 8) ∈ ({1, 7} ∪ {3,
5})) | 
| 63 | 62 | ad2ant2l 746 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) → (𝐵 mod 8) ∈ ({1, 7} ∪ {3,
5})) | 
| 64 |  | elun 4152 | . . . . . . . . . . 11
⊢ ((𝐵 mod 8) ∈ ({1, 7} ∪ {3,
5}) ↔ ((𝐵 mod 8)
∈ {1, 7} ∨ (𝐵 mod
8) ∈ {3, 5})) | 
| 65 | 63, 64 | sylib 218 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) → ((𝐵 mod 8) ∈ {1, 7} ∨
(𝐵 mod 8) ∈ {3,
5})) | 
| 66 | 65 | orcanai 1004 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ ¬
(𝐵 mod 8) ∈ {1, 7})
→ (𝐵 mod 8) ∈ {3,
5}) | 
| 67 | 61, 66 | anim12dan 619 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (¬
(𝐴 mod 8) ∈ {1, 7}
∧ ¬ (𝐵 mod 8)
∈ {1, 7})) → ((𝐴
mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) | 
| 68 |  | lgsdir2lem5 27374 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧
(𝐵 mod 8) ∈ {3, 5}))
→ ((𝐴 · 𝐵) mod 8) ∈ {1,
7}) | 
| 69 | 68 | adantlr 715 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧
(𝐵 mod 8) ∈ {3, 5}))
→ ((𝐴 · 𝐵) mod 8) ∈ {1,
7}) | 
| 70 | 67, 69 | syldan 591 | . . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (¬
(𝐴 mod 8) ∈ {1, 7}
∧ ¬ (𝐵 mod 8)
∈ {1, 7})) → ((𝐴
· 𝐵) mod 8) ∈
{1, 7}) | 
| 71 | 70 | iftrued 4532 | . . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) ∧ (¬
(𝐴 mod 8) ∈ {1, 7}
∧ ¬ (𝐵 mod 8)
∈ {1, 7})) → if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1) =
1) | 
| 72 | 52, 56, 71 | 3eqtr4a 2802 | . . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 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)) | 
| 73 | 34, 51, 72 | pm2.61ddan 813 | . . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) →
(if((𝐴 mod 8) ∈ {1,
7}, 1, -1) · if((𝐵
mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1,
-1)) | 
| 74 |  | iffalse 4533 | . . . . . 6
⊢ (¬ 2
∥ 𝐴 → if(2
∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) =
if((𝐴 mod 8) ∈ {1, 7},
1, -1)) | 
| 75 |  | iffalse 4533 | . . . . . 6
⊢ (¬ 2
∥ 𝐵 → if(2
∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1, -1)) =
if((𝐵 mod 8) ∈ {1, 7},
1, -1)) | 
| 76 | 74, 75 | oveqan12d 7451 | . . . . 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))) | 
| 77 | 76 | adantl 481 | . . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 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))) | 
| 78 |  | ioran 985 | . . . . . 6
⊢ (¬ (2
∥ 𝐴 ∨ 2 ∥
𝐵) ↔ (¬ 2 ∥
𝐴 ∧ ¬ 2 ∥
𝐵)) | 
| 79 |  | 2prm 16730 | . . . . . . . . 9
⊢ 2 ∈
ℙ | 
| 80 |  | euclemma 16751 | . . . . . . . . 9
⊢ ((2
∈ ℙ ∧ 𝐴
∈ ℤ ∧ 𝐵
∈ ℤ) → (2 ∥ (𝐴 · 𝐵) ↔ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵))) | 
| 81 | 79, 80 | mp3an1 1449 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2
∥ (𝐴 · 𝐵) ↔ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵))) | 
| 82 | 81 | notbid 318 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (¬ 2
∥ (𝐴 · 𝐵) ↔ ¬ (2 ∥ 𝐴 ∨ 2 ∥ 𝐵))) | 
| 83 | 82 | biimpar 477 | . . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (2
∥ 𝐴 ∨ 2 ∥
𝐵)) → ¬ 2 ∥
(𝐴 · 𝐵)) | 
| 84 | 78, 83 | sylan2br 595 | . . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) → ¬ 2
∥ (𝐴 · 𝐵)) | 
| 85 |  | iffalse 4533 | . . . . 5
⊢ (¬ 2
∥ (𝐴 · 𝐵) → if(2 ∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1,
-1)) | 
| 86 | 84, 85 | syl 17 | . . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (¬ 2
∥ 𝐴 ∧ ¬ 2
∥ 𝐵)) → if(2
∥ (𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1, -1)) = if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1,
-1)) | 
| 87 | 73, 77, 86 | 3eqtr4d 2786 | . . 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))) | 
| 88 | 15, 26, 87 | pm2.61ddan 813 | . 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))) | 
| 89 |  | lgs2 27359 | . . 3
⊢ (𝐴 ∈ ℤ → (𝐴 /L 2) = if(2
∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1,
-1))) | 
| 90 |  | lgs2 27359 | . . 3
⊢ (𝐵 ∈ ℤ → (𝐵 /L 2) = if(2
∥ 𝐵, 0, if((𝐵 mod 8) ∈ {1, 7}, 1,
-1))) | 
| 91 | 89, 90 | oveqan12d 7451 | . 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)))) | 
| 92 |  | zmulcl 12668 | . . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) ∈ ℤ) | 
| 93 |  | lgs2 27359 | . . 3
⊢ ((𝐴 · 𝐵) ∈ ℤ → ((𝐴 · 𝐵) /L 2) = if(2 ∥
(𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1,
-1))) | 
| 94 | 92, 93 | syl 17 | . 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = if(2 ∥
(𝐴 · 𝐵), 0, if(((𝐴 · 𝐵) mod 8) ∈ {1, 7}, 1,
-1))) | 
| 95 | 88, 91, 94 | 3eqtr4rd 2787 | 1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2)
· (𝐵
/L 2))) |