Metamath Proof Explorer

Theorem lgsdir2lem3

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

Ref Expression
Assertion lgsdir2lem3 ⊢A∈ℤ∧¬2∥A→Amod8∈17∪35

Proof

Step Hyp Ref Expression
1 simpl ⊢A∈ℤ∧¬2∥A→A∈ℤ
2 8nn ⊢8∈ℕ
3 zmodfz ⊢A∈ℤ∧8∈ℕ→Amod8∈0…8−1
4 1 2 3 sylancl ⊢A∈ℤ∧¬2∥A→Amod8∈0…8−1
5 8m1e7 ⊢8−1=7
6 5 oveq2i ⊢0…8−1=0…7
7 4 6 eleqtrdi ⊢A∈ℤ∧¬2∥A→Amod8∈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 ⊢¬Amod8∈∅
17 16 pm2.21i ⊢Amod8∈∅→Amod8∈17∪35
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 ⊢Amod8∈0…−1→Amod8∈17∪35
24 23 a1i ⊢A∈ℤ∧¬2∥A→Amod8∈0…−1→Amod8∈17∪35
25 8 15 24 3pm3.2i ⊢−1∈ℤ∧2∥-1+1∧A∈ℤ∧¬2∥A→Amod8∈0…−1→Amod8∈17∪35
26 1e0p1 ⊢1=0+1
27 ssun1 ⊢17⊆17∪35
28 1ex ⊢1∈V
29 28 prid1 ⊢1∈17
30 27 29 sselii ⊢1∈17∪35
31 25 14 26 30 lgsdir2lem2 ⊢1∈ℤ∧2∥1+1∧A∈ℤ∧¬2∥A→Amod8∈0…1→Amod8∈17∪35
32 df-2 ⊢2=1+1
33 df-3 ⊢3=2+1
34 ssun2 ⊢35⊆17∪35
35 3ex ⊢3∈V
36 35 prid1 ⊢3∈35
37 34 36 sselii ⊢3∈17∪35
38 31 32 33 37 lgsdir2lem2 ⊢3∈ℤ∧2∥3+1∧A∈ℤ∧¬2∥A→Amod8∈0…3→Amod8∈17∪35
39 df-4 ⊢4=3+1
40 df-5 ⊢5=4+1
41 5nn ⊢5∈ℕ
42 41 elexi ⊢5∈V
43 42 prid2 ⊢5∈35
44 34 43 sselii ⊢5∈17∪35
45 38 39 40 44 lgsdir2lem2 ⊢5∈ℤ∧2∥5+1∧A∈ℤ∧¬2∥A→Amod8∈0…5→Amod8∈17∪35
46 df-6 ⊢6=5+1
47 df-7 ⊢7=6+1
48 7nn ⊢7∈ℕ
49 48 elexi ⊢7∈V
50 49 prid2 ⊢7∈17
51 27 50 sselii ⊢7∈17∪35
52 45 46 47 51 lgsdir2lem2 ⊢7∈ℤ∧2∥7+1∧A∈ℤ∧¬2∥A→Amod8∈0…7→Amod8∈17∪35
53 52 simp3i ⊢A∈ℤ∧¬2∥A→Amod8∈0…7→Amod8∈17∪35
54 7 53 mpd ⊢A∈ℤ∧¬2∥A→Amod8∈17∪35