Proof of Theorem 2lgsoddprmlem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lgsdir2lem3 27372 | . . 3
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁) → (𝑁 mod 8) ∈ ({1, 7} ∪ {3,
5})) | 
| 2 |  | eleq1 2828 | . . . . 5
⊢ ((𝑁 mod 8) = 𝑅 → ((𝑁 mod 8) ∈ ({1, 7} ∪ {3, 5}) ↔
𝑅 ∈ ({1, 7} ∪ {3,
5}))) | 
| 3 | 2 | eqcoms 2744 | . . . 4
⊢ (𝑅 = (𝑁 mod 8) → ((𝑁 mod 8) ∈ ({1, 7} ∪ {3, 5}) ↔
𝑅 ∈ ({1, 7} ∪ {3,
5}))) | 
| 4 |  | elun 4152 | . . . . . 6
⊢ (𝑅 ∈ ({1, 7} ∪ {3, 5})
↔ (𝑅 ∈ {1, 7}
∨ 𝑅 ∈ {3,
5})) | 
| 5 |  | elpri 4648 | . . . . . . . 8
⊢ (𝑅 ∈ {3, 5} → (𝑅 = 3 ∨ 𝑅 = 5)) | 
| 6 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑅 = 3 → (𝑅↑2) = (3↑2)) | 
| 7 | 6 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑅 = 3 → ((𝑅↑2) − 1) = ((3↑2) −
1)) | 
| 8 | 7 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝑅 = 3 → (((𝑅↑2) − 1) / 8) = (((3↑2)
− 1) / 8)) | 
| 9 |  | 2lgsoddprmlem3b 27456 | . . . . . . . . . . . 12
⊢
(((3↑2) − 1) / 8) = 1 | 
| 10 | 8, 9 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑅 = 3 → (((𝑅↑2) − 1) / 8) =
1) | 
| 11 | 10 | breq2d 5154 | . . . . . . . . . 10
⊢ (𝑅 = 3 → (2 ∥ (((𝑅↑2) − 1) / 8) ↔
2 ∥ 1)) | 
| 12 |  | n2dvds1 16406 | . . . . . . . . . . 11
⊢  ¬ 2
∥ 1 | 
| 13 | 12 | pm2.21i 119 | . . . . . . . . . 10
⊢ (2
∥ 1 → 𝑅 ∈
{1, 7}) | 
| 14 | 11, 13 | biimtrdi 253 | . . . . . . . . 9
⊢ (𝑅 = 3 → (2 ∥ (((𝑅↑2) − 1) / 8) →
𝑅 ∈ {1,
7})) | 
| 15 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑅 = 5 → (𝑅↑2) = (5↑2)) | 
| 16 | 15 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑅 = 5 → ((𝑅↑2) − 1) = ((5↑2) −
1)) | 
| 17 | 16 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝑅 = 5 → (((𝑅↑2) − 1) / 8) = (((5↑2)
− 1) / 8)) | 
| 18 | 17 | breq2d 5154 | . . . . . . . . . . 11
⊢ (𝑅 = 5 → (2 ∥ (((𝑅↑2) − 1) / 8) ↔
2 ∥ (((5↑2) − 1) / 8))) | 
| 19 |  | 2lgsoddprmlem3c 27457 | . . . . . . . . . . . 12
⊢
(((5↑2) − 1) / 8) = 3 | 
| 20 | 19 | breq2i 5150 | . . . . . . . . . . 11
⊢ (2
∥ (((5↑2) − 1) / 8) ↔ 2 ∥ 3) | 
| 21 | 18, 20 | bitrdi 287 | . . . . . . . . . 10
⊢ (𝑅 = 5 → (2 ∥ (((𝑅↑2) − 1) / 8) ↔
2 ∥ 3)) | 
| 22 |  | n2dvds3 16409 | . . . . . . . . . . 11
⊢  ¬ 2
∥ 3 | 
| 23 | 22 | pm2.21i 119 | . . . . . . . . . 10
⊢ (2
∥ 3 → 𝑅 ∈
{1, 7}) | 
| 24 | 21, 23 | biimtrdi 253 | . . . . . . . . 9
⊢ (𝑅 = 5 → (2 ∥ (((𝑅↑2) − 1) / 8) →
𝑅 ∈ {1,
7})) | 
| 25 | 14, 24 | jaoi 857 | . . . . . . . 8
⊢ ((𝑅 = 3 ∨ 𝑅 = 5) → (2 ∥ (((𝑅↑2) − 1) / 8) → 𝑅 ∈ {1,
7})) | 
| 26 | 5, 25 | syl 17 | . . . . . . 7
⊢ (𝑅 ∈ {3, 5} → (2 ∥
(((𝑅↑2) − 1) /
8) → 𝑅 ∈ {1,
7})) | 
| 27 | 26 | jao1i 858 | . . . . . 6
⊢ ((𝑅 ∈ {1, 7} ∨ 𝑅 ∈ {3, 5}) → (2
∥ (((𝑅↑2)
− 1) / 8) → 𝑅
∈ {1, 7})) | 
| 28 | 4, 27 | sylbi 217 | . . . . 5
⊢ (𝑅 ∈ ({1, 7} ∪ {3, 5})
→ (2 ∥ (((𝑅↑2) − 1) / 8) → 𝑅 ∈ {1,
7})) | 
| 29 |  | elpri 4648 | . . . . . 6
⊢ (𝑅 ∈ {1, 7} → (𝑅 = 1 ∨ 𝑅 = 7)) | 
| 30 |  | z0even 16405 | . . . . . . . 8
⊢ 2 ∥
0 | 
| 31 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑅 = 1 → (𝑅↑2) = (1↑2)) | 
| 32 | 31 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑅 = 1 → ((𝑅↑2) − 1) = ((1↑2) −
1)) | 
| 33 | 32 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑅 = 1 → (((𝑅↑2) − 1) / 8) = (((1↑2)
− 1) / 8)) | 
| 34 |  | 2lgsoddprmlem3a 27455 | . . . . . . . . 9
⊢
(((1↑2) − 1) / 8) = 0 | 
| 35 | 33, 34 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑅 = 1 → (((𝑅↑2) − 1) / 8) =
0) | 
| 36 | 30, 35 | breqtrrid 5180 | . . . . . . 7
⊢ (𝑅 = 1 → 2 ∥ (((𝑅↑2) − 1) /
8)) | 
| 37 |  | 2z 12651 | . . . . . . . . 9
⊢ 2 ∈
ℤ | 
| 38 |  | 3z 12652 | . . . . . . . . 9
⊢ 3 ∈
ℤ | 
| 39 |  | dvdsmul1 16316 | . . . . . . . . 9
⊢ ((2
∈ ℤ ∧ 3 ∈ ℤ) → 2 ∥ (2 ·
3)) | 
| 40 | 37, 38, 39 | mp2an 692 | . . . . . . . 8
⊢ 2 ∥
(2 · 3) | 
| 41 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑅 = 7 → (𝑅↑2) = (7↑2)) | 
| 42 | 41 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑅 = 7 → ((𝑅↑2) − 1) = ((7↑2) −
1)) | 
| 43 | 42 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑅 = 7 → (((𝑅↑2) − 1) / 8) = (((7↑2)
− 1) / 8)) | 
| 44 |  | 2lgsoddprmlem3d 27458 | . . . . . . . . 9
⊢
(((7↑2) − 1) / 8) = (2 · 3) | 
| 45 | 43, 44 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑅 = 7 → (((𝑅↑2) − 1) / 8) = (2 ·
3)) | 
| 46 | 40, 45 | breqtrrid 5180 | . . . . . . 7
⊢ (𝑅 = 7 → 2 ∥ (((𝑅↑2) − 1) /
8)) | 
| 47 | 36, 46 | jaoi 857 | . . . . . 6
⊢ ((𝑅 = 1 ∨ 𝑅 = 7) → 2 ∥ (((𝑅↑2) − 1) / 8)) | 
| 48 | 29, 47 | syl 17 | . . . . 5
⊢ (𝑅 ∈ {1, 7} → 2 ∥
(((𝑅↑2) − 1) /
8)) | 
| 49 | 28, 48 | impbid1 225 | . . . 4
⊢ (𝑅 ∈ ({1, 7} ∪ {3, 5})
→ (2 ∥ (((𝑅↑2) − 1) / 8) ↔ 𝑅 ∈ {1,
7})) | 
| 50 | 3, 49 | biimtrdi 253 | . . 3
⊢ (𝑅 = (𝑁 mod 8) → ((𝑁 mod 8) ∈ ({1, 7} ∪ {3, 5}) →
(2 ∥ (((𝑅↑2)
− 1) / 8) ↔ 𝑅
∈ {1, 7}))) | 
| 51 | 1, 50 | syl5com 31 | . 2
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁) → (𝑅 = (𝑁 mod 8) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔
𝑅 ∈ {1,
7}))) | 
| 52 | 51 | 3impia 1117 | 1
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2
∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔
𝑅 ∈ {1,
7})) |