Metamath Proof Explorer

Theorem lgsdir2lem3

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

Ref Expression
Assertion lgsdir2lem3 ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( 𝐴 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → 𝐴 ∈ ℤ )
2 8nn ⊢ 8 ∈ ℕ
3 zmodfz ⊢ ( ( 𝐴 ∈ ℤ ∧ 8 ∈ ℕ ) → ( 𝐴 mod 8 ) ∈ ( 0 ... ( 8 − 1 ) ) )
4 1 2 3 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( 𝐴 mod 8 ) ∈ ( 0 ... ( 8 − 1 ) ) )
5 8m1e7 ⊢ ( 8 − 1 ) = 7
6 5 oveq2i ⊢ ( 0 ... ( 8 − 1 ) ) = ( 0 ... 7 )
7 4 6 eleqtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( 𝐴 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 ⊢ ¬ ( 𝐴 mod 8 ) ∈ ∅
17 16 pm2.21i ⊢ ( ( 𝐴 mod 8 ) ∈ ∅ → ( 𝐴 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 ⊢ ( ( 𝐴 mod 8 ) ∈ ( 0 ... - 1 ) → ( 𝐴 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) )
24 23 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... - 1 ) → ( 𝐴 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) ) )
25 8 15 24 3pm3.2i ⊢ ( - 1 ∈ ℤ ∧ 2 ∥ ( - 1 + 1 ) ∧ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... - 1 ) → ( 𝐴 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 ) ∧ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 1 ) → ( 𝐴 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 ) ∧ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 3 ) → ( 𝐴 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 ) ∧ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 5 ) → ( 𝐴 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 ) ∧ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 7 ) → ( 𝐴 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) ) ) )
53 52 simp3i ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 7 ) → ( 𝐴 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) ) )
54 7 53 mpd ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( 𝐴 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) )