Proof of Theorem lgsdir2lem3
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) → 𝐴 ∈
ℤ) |
2 | | 8nn 11068 |
. . . 4
⊢ 8 ∈
ℕ |
3 | | zmodfz 12554 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 8 ∈
ℕ) → (𝐴 mod 8)
∈ (0...(8 − 1))) |
4 | 1, 2, 3 | sylancl 693 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) → (𝐴 mod 8) ∈ (0...(8 −
1))) |
5 | | 8cn 10983 |
. . . . 5
⊢ 8 ∈
ℂ |
6 | | ax-1cn 9873 |
. . . . 5
⊢ 1 ∈
ℂ |
7 | | 7cn 10981 |
. . . . 5
⊢ 7 ∈
ℂ |
8 | 6, 7 | addcomi 10106 |
. . . . . 6
⊢ (1 + 7) =
(7 + 1) |
9 | | df-8 10962 |
. . . . . 6
⊢ 8 = (7 +
1) |
10 | 8, 9 | eqtr4i 2635 |
. . . . 5
⊢ (1 + 7) =
8 |
11 | 5, 6, 7, 10 | subaddrii 10249 |
. . . 4
⊢ (8
− 1) = 7 |
12 | 11 | oveq2i 6560 |
. . 3
⊢ (0...(8
− 1)) = (0...7) |
13 | 4, 12 | syl6eleq 2698 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) → (𝐴 mod 8) ∈
(0...7)) |
14 | | neg1z 11290 |
. . . . . . . 8
⊢ -1 ∈
ℤ |
15 | | 2z 11286 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
16 | | dvds0 14835 |
. . . . . . . . . 10
⊢ (2 ∈
ℤ → 2 ∥ 0) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . 9
⊢ 2 ∥
0 |
18 | | 1pneg1e0 11006 |
. . . . . . . . . 10
⊢ (1 + -1)
= 0 |
19 | | neg1cn 11001 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
20 | 6, 19 | addcomi 10106 |
. . . . . . . . . 10
⊢ (1 + -1)
= (-1 + 1) |
21 | 18, 20 | eqtr3i 2634 |
. . . . . . . . 9
⊢ 0 = (-1 +
1) |
22 | 17, 21 | breqtri 4608 |
. . . . . . . 8
⊢ 2 ∥
(-1 + 1) |
23 | | noel 3878 |
. . . . . . . . . . 11
⊢ ¬
(𝐴 mod 8) ∈
∅ |
24 | 23 | pm2.21i 115 |
. . . . . . . . . 10
⊢ ((𝐴 mod 8) ∈ ∅ →
(𝐴 mod 8) ∈ ({1, 7}
∪ {3, 5})) |
25 | | neg1lt0 11004 |
. . . . . . . . . . 11
⊢ -1 <
0 |
26 | | 0z 11265 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
27 | | fzn 12228 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℤ ∧ -1 ∈ ℤ) → (-1 < 0 ↔ (0...-1) =
∅)) |
28 | 26, 14, 27 | mp2an 704 |
. . . . . . . . . . 11
⊢ (-1 <
0 ↔ (0...-1) = ∅) |
29 | 25, 28 | mpbi 219 |
. . . . . . . . . 10
⊢ (0...-1)
= ∅ |
30 | 24, 29 | eleq2s 2706 |
. . . . . . . . 9
⊢ ((𝐴 mod 8) ∈ (0...-1) →
(𝐴 mod 8) ∈ ({1, 7}
∪ {3, 5})) |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) → ((𝐴 mod 8) ∈ (0...-1) →
(𝐴 mod 8) ∈ ({1, 7}
∪ {3, 5}))) |
32 | 14, 22, 31 | 3pm3.2i 1232 |
. . . . . . 7
⊢ (-1
∈ ℤ ∧ 2 ∥ (-1 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...-1) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3,
5})))) |
33 | | 1e0p1 11428 |
. . . . . . 7
⊢ 1 = (0 +
1) |
34 | | ssun1 3738 |
. . . . . . . 8
⊢ {1, 7}
⊆ ({1, 7} ∪ {3, 5}) |
35 | | 1ex 9914 |
. . . . . . . . 9
⊢ 1 ∈
V |
36 | 35 | prid1 4241 |
. . . . . . . 8
⊢ 1 ∈
{1, 7} |
37 | 34, 36 | sselii 3565 |
. . . . . . 7
⊢ 1 ∈
({1, 7} ∪ {3, 5}) |
38 | 32, 21, 33, 37 | lgsdir2lem2 24851 |
. . . . . 6
⊢ (1 ∈
ℤ ∧ 2 ∥ (1 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...1) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3,
5})))) |
39 | | df-2 10956 |
. . . . . 6
⊢ 2 = (1 +
1) |
40 | | df-3 10957 |
. . . . . 6
⊢ 3 = (2 +
1) |
41 | | ssun2 3739 |
. . . . . . 7
⊢ {3, 5}
⊆ ({1, 7} ∪ {3, 5}) |
42 | | 3ex 10973 |
. . . . . . . 8
⊢ 3 ∈
V |
43 | 42 | prid1 4241 |
. . . . . . 7
⊢ 3 ∈
{3, 5} |
44 | 41, 43 | sselii 3565 |
. . . . . 6
⊢ 3 ∈
({1, 7} ∪ {3, 5}) |
45 | 38, 39, 40, 44 | lgsdir2lem2 24851 |
. . . . 5
⊢ (3 ∈
ℤ ∧ 2 ∥ (3 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...3) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3,
5})))) |
46 | | df-4 10958 |
. . . . 5
⊢ 4 = (3 +
1) |
47 | | df-5 10959 |
. . . . 5
⊢ 5 = (4 +
1) |
48 | | 5nn 11065 |
. . . . . . . 8
⊢ 5 ∈
ℕ |
49 | 48 | elexi 3186 |
. . . . . . 7
⊢ 5 ∈
V |
50 | 49 | prid2 4242 |
. . . . . 6
⊢ 5 ∈
{3, 5} |
51 | 41, 50 | sselii 3565 |
. . . . 5
⊢ 5 ∈
({1, 7} ∪ {3, 5}) |
52 | 45, 46, 47, 51 | lgsdir2lem2 24851 |
. . . 4
⊢ (5 ∈
ℤ ∧ 2 ∥ (5 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...5) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3,
5})))) |
53 | | df-6 10960 |
. . . 4
⊢ 6 = (5 +
1) |
54 | | df-7 10961 |
. . . 4
⊢ 7 = (6 +
1) |
55 | | 7nn 11067 |
. . . . . . 7
⊢ 7 ∈
ℕ |
56 | 55 | elexi 3186 |
. . . . . 6
⊢ 7 ∈
V |
57 | 56 | prid2 4242 |
. . . . 5
⊢ 7 ∈
{1, 7} |
58 | 34, 57 | sselii 3565 |
. . . 4
⊢ 7 ∈
({1, 7} ∪ {3, 5}) |
59 | 52, 53, 54, 58 | lgsdir2lem2 24851 |
. . 3
⊢ (7 ∈
ℤ ∧ 2 ∥ (7 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...7) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3,
5})))) |
60 | 59 | simp3i 1065 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) → ((𝐴 mod 8) ∈ (0...7) →
(𝐴 mod 8) ∈ ({1, 7}
∪ {3, 5}))) |
61 | 13, 60 | mpd 15 |
1
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2
∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3,
5})) |