Metamath Proof Explorer

Theorem lgsdir2lem3

Description: Lemma for lgsdir2 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsdir2lem3 ⊢ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 1 7 ∪ 3 5

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ ℤ ∧ ¬ 2 ∥ A → A ∈ ℤ
2 8nn ⊢ 8 ∈ ℕ
3 zmodfz ⊢ A ∈ ℤ ∧ 8 ∈ ℕ → A mod 8 ∈ 0 … 8 − 1
4 1 2 3 sylancl ⊢ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 0 … 8 − 1
5 8m1e7 ⊢ 8 − 1 = 7
6 5 oveq2i ⊢ 0 … 8 − 1 = 0 … 7
7 4 6 eleqtrdi ⊢ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 0 … 7
8 neg1z ⊢ − 1 ∈ ℤ
9 z0even ⊢ 2 ∥ 0
10 1pneg1e0 ⊢ 1 + -1 = 0
11 ax-1cn ⊢ 1 ∈ ℂ
12 neg1cn ⊢ − 1 ∈ ℂ
13 11 12 addcomi ⊢ 1 + -1 = - 1 + 1
14 10 13 eqtr3i ⊢ 0 = - 1 + 1
15 9 14 breqtri ⊢ 2 ∥ - 1 + 1
16 noel ⊢ ¬ A mod 8 ∈ ∅
17 16 pm2.21i ⊢ A mod 8 ∈ ∅ → A mod 8 ∈ 1 7 ∪ 3 5
18 neg1lt0 ⊢ − 1 < 0
19 0z ⊢ 0 ∈ ℤ
20 fzn ⊢ 0 ∈ ℤ ∧ − 1 ∈ ℤ → − 1 < 0 ↔ 0 … − 1 = ∅
21 19 8 20 mp2an ⊢ − 1 < 0 ↔ 0 … − 1 = ∅
22 18 21 mpbi ⊢ 0 … − 1 = ∅
23 17 22 eleq2s ⊢ A mod 8 ∈ 0 … − 1 → A mod 8 ∈ 1 7 ∪ 3 5
24 23 a1i ⊢ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 0 … − 1 → A mod 8 ∈ 1 7 ∪ 3 5
25 8 15 24 3pm3.2i ⊢ − 1 ∈ ℤ ∧ 2 ∥ - 1 + 1 ∧ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 0 … − 1 → A mod 8 ∈ 1 7 ∪ 3 5
26 1e0p1 ⊢ 1 = 0 + 1
27 ssun1 ⊢ 1 7 ⊆ 1 7 ∪ 3 5
28 1ex ⊢ 1 ∈ V
29 28 prid1 ⊢ 1 ∈ 1 7
30 27 29 sselii ⊢ 1 ∈ 1 7 ∪ 3 5
31 25 14 26 30 lgsdir2lem2 ⊢ 1 ∈ ℤ ∧ 2 ∥ 1 + 1 ∧ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 0 … 1 → A mod 8 ∈ 1 7 ∪ 3 5
32 df-2 ⊢ 2 = 1 + 1
33 df-3 ⊢ 3 = 2 + 1
34 ssun2 ⊢ 3 5 ⊆ 1 7 ∪ 3 5
35 3ex ⊢ 3 ∈ V
36 35 prid1 ⊢ 3 ∈ 3 5
37 34 36 sselii ⊢ 3 ∈ 1 7 ∪ 3 5
38 31 32 33 37 lgsdir2lem2 ⊢ 3 ∈ ℤ ∧ 2 ∥ 3 + 1 ∧ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 0 … 3 → A mod 8 ∈ 1 7 ∪ 3 5
39 df-4 ⊢ 4 = 3 + 1
40 df-5 ⊢ 5 = 4 + 1
41 5nn ⊢ 5 ∈ ℕ
42 41 elexi ⊢ 5 ∈ V
43 42 prid2 ⊢ 5 ∈ 3 5
44 34 43 sselii ⊢ 5 ∈ 1 7 ∪ 3 5
45 38 39 40 44 lgsdir2lem2 ⊢ 5 ∈ ℤ ∧ 2 ∥ 5 + 1 ∧ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 0 … 5 → A mod 8 ∈ 1 7 ∪ 3 5
46 df-6 ⊢ 6 = 5 + 1
47 df-7 ⊢ 7 = 6 + 1
48 7nn ⊢ 7 ∈ ℕ
49 48 elexi ⊢ 7 ∈ V
50 49 prid2 ⊢ 7 ∈ 1 7
51 27 50 sselii ⊢ 7 ∈ 1 7 ∪ 3 5
52 45 46 47 51 lgsdir2lem2 ⊢ 7 ∈ ℤ ∧ 2 ∥ 7 + 1 ∧ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 0 … 7 → A mod 8 ∈ 1 7 ∪ 3 5
53 52 simp3i ⊢ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 0 … 7 → A mod 8 ∈ 1 7 ∪ 3 5
54 7 53 mpd ⊢ A ∈ ℤ ∧ ¬ 2 ∥ A → A mod 8 ∈ 1 7 ∪ 3 5