Metamath Proof Explorer

Theorem lgsdir2lem2

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

Ref Expression
Hypotheses lgsdir2lem2.1 ⊢ ( 𝐾 ∈ ℤ ∧ 2 ∥ ( 𝐾 + 1 ) ∧ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝐾 ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) ) )
lgsdir2lem2.2 ⊢ 𝑀 = ( 𝐾 + 1 )
lgsdir2lem2.3 ⊢ 𝑁 = ( 𝑀 + 1 )
lgsdir2lem2.4 ⊢ 𝑁 ∈ 𝑆
Assertion lgsdir2lem2 ( 𝑁 ∈ ℤ ∧ 2 ∥ ( 𝑁 + 1 ) ∧ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑁 ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 lgsdir2lem2.1 ⊢ ( 𝐾 ∈ ℤ ∧ 2 ∥ ( 𝐾 + 1 ) ∧ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝐾 ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) ) )
2 lgsdir2lem2.2 ⊢ 𝑀 = ( 𝐾 + 1 )
3 lgsdir2lem2.3 ⊢ 𝑁 = ( 𝑀 + 1 )
4 lgsdir2lem2.4 ⊢ 𝑁 ∈ 𝑆
5 1 simp1i ⊢ 𝐾 ∈ ℤ
6 peano2z ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 + 1 ) ∈ ℤ )
7 5 6 ax-mp ⊢ ( 𝐾 + 1 ) ∈ ℤ
8 2 7 eqeltri ⊢ 𝑀 ∈ ℤ
9 peano2z ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ )
10 8 9 ax-mp ⊢ ( 𝑀 + 1 ) ∈ ℤ
11 3 10 eqeltri ⊢ 𝑁 ∈ ℤ
12 1 simp2i ⊢ 2 ∥ ( 𝐾 + 1 )
13 2z ⊢ 2 ∈ ℤ
14 dvdsadd ⊢ ( ( 2 ∈ ℤ ∧ ( 𝐾 + 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝐾 + 1 ) ↔ 2 ∥ ( 2 + ( 𝐾 + 1 ) ) ) )
15 13 7 14 mp2an ⊢ ( 2 ∥ ( 𝐾 + 1 ) ↔ 2 ∥ ( 2 + ( 𝐾 + 1 ) ) )
16 12 15 mpbi ⊢ 2 ∥ ( 2 + ( 𝐾 + 1 ) )
17 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
18 5 17 ax-mp ⊢ 𝐾 ∈ ℂ
19 ax-1cn ⊢ 1 ∈ ℂ
20 18 19 addcomi ⊢ ( 𝐾 + 1 ) = ( 1 + 𝐾 )
21 2 20 eqtri ⊢ 𝑀 = ( 1 + 𝐾 )
22 21 oveq1i ⊢ ( 𝑀 + 1 ) = ( ( 1 + 𝐾 ) + 1 )
23 3 22 eqtri ⊢ 𝑁 = ( ( 1 + 𝐾 ) + 1 )
24 df-2 ⊢ 2 = ( 1 + 1 )
25 24 oveq1i ⊢ ( 2 + 𝐾 ) = ( ( 1 + 1 ) + 𝐾 )
26 19 18 19 add32i ⊢ ( ( 1 + 𝐾 ) + 1 ) = ( ( 1 + 1 ) + 𝐾 )
27 25 26 eqtr4i ⊢ ( 2 + 𝐾 ) = ( ( 1 + 𝐾 ) + 1 )
28 23 27 eqtr4i ⊢ 𝑁 = ( 2 + 𝐾 )
29 28 oveq1i ⊢ ( 𝑁 + 1 ) = ( ( 2 + 𝐾 ) + 1 )
30 2cn ⊢ 2 ∈ ℂ
31 30 18 19 addassi ⊢ ( ( 2 + 𝐾 ) + 1 ) = ( 2 + ( 𝐾 + 1 ) )
32 29 31 eqtri ⊢ ( 𝑁 + 1 ) = ( 2 + ( 𝐾 + 1 ) )
33 16 32 breqtrri ⊢ 2 ∥ ( 𝑁 + 1 )
34 elfzuz2 ⊢ ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
35 fzm1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ( 𝐴 mod 8 ) = 𝑁 ) ) )
36 34 35 syl ⊢ ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑁 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ( 𝐴 mod 8 ) = 𝑁 ) ) )
37 36 ibi ⊢ ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑁 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ( 𝐴 mod 8 ) = 𝑁 ) )
38 elfzuz2 ⊢ ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
39 fzm1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑀 ) ↔ ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) ∨ ( 𝐴 mod 8 ) = 𝑀 ) ) )
40 38 39 syl ⊢ ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑀 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑀 ) ↔ ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) ∨ ( 𝐴 mod 8 ) = 𝑀 ) ) )
41 40 ibi ⊢ ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑀 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) ∨ ( 𝐴 mod 8 ) = 𝑀 ) )
42 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
43 8 42 ax-mp ⊢ 𝑀 ∈ ℂ
44 43 19 3 mvrraddi ⊢ ( 𝑁 − 1 ) = 𝑀
45 44 oveq2i ⊢ ( 0 ... ( 𝑁 − 1 ) ) = ( 0 ... 𝑀 )
46 41 45 eleq2s ⊢ ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) ∨ ( 𝐴 mod 8 ) = 𝑀 ) )
47 18 19 2 mvrraddi ⊢ ( 𝑀 − 1 ) = 𝐾
48 47 oveq2i ⊢ ( 0 ... ( 𝑀 − 1 ) ) = ( 0 ... 𝐾 )
49 48 eleq2i ⊢ ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) ↔ ( 𝐴 mod 8 ) ∈ ( 0 ... 𝐾 ) )
50 1 simp3i ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝐾 ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) )
51 49 50 syl5bi ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) )
52 2nn ⊢ 2 ∈ ℕ
53 8nn ⊢ 8 ∈ ℕ
54 4z ⊢ 4 ∈ ℤ
55 dvdsmul2 ⊢ ( ( 4 ∈ ℤ ∧ 2 ∈ ℤ ) → 2 ∥ ( 4 · 2 ) )
56 54 13 55 mp2an ⊢ 2 ∥ ( 4 · 2 )
57 4t2e8 ⊢ ( 4 · 2 ) = 8
58 56 57 breqtri ⊢ 2 ∥ 8
59 dvdsmod ⊢ ( ( ( 2 ∈ ℕ ∧ 8 ∈ ℕ ∧ 𝐴 ∈ ℤ ) ∧ 2 ∥ 8 ) → ( 2 ∥ ( 𝐴 mod 8 ) ↔ 2 ∥ 𝐴 ) )
60 58 59 mpan2 ⊢ ( ( 2 ∈ ℕ ∧ 8 ∈ ℕ ∧ 𝐴 ∈ ℤ ) → ( 2 ∥ ( 𝐴 mod 8 ) ↔ 2 ∥ 𝐴 ) )
61 52 53 60 mp3an12 ⊢ ( 𝐴 ∈ ℤ → ( 2 ∥ ( 𝐴 mod 8 ) ↔ 2 ∥ 𝐴 ) )
62 61 notbid ⊢ ( 𝐴 ∈ ℤ → ( ¬ 2 ∥ ( 𝐴 mod 8 ) ↔ ¬ 2 ∥ 𝐴 ) )
63 62 biimpar ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ¬ 2 ∥ ( 𝐴 mod 8 ) )
64 12 2 breqtrri ⊢ 2 ∥ 𝑀
65 id ⊢ ( ( 𝐴 mod 8 ) = 𝑀 → ( 𝐴 mod 8 ) = 𝑀 )
66 64 65 breqtrrid ⊢ ( ( 𝐴 mod 8 ) = 𝑀 → 2 ∥ ( 𝐴 mod 8 ) )
67 63 66 nsyl ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ¬ ( 𝐴 mod 8 ) = 𝑀 )
68 67 pm2.21d ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) = 𝑀 → ( 𝐴 mod 8 ) ∈ 𝑆 ) )
69 51 68 jaod ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) ∨ ( 𝐴 mod 8 ) = 𝑀 ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) )
70 46 69 syl5 ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) )
71 eleq1 ⊢ ( ( 𝐴 mod 8 ) = 𝑁 → ( ( 𝐴 mod 8 ) ∈ 𝑆 ↔ 𝑁 ∈ 𝑆 ) )
72 4 71 mpbiri ⊢ ( ( 𝐴 mod 8 ) = 𝑁 → ( 𝐴 mod 8 ) ∈ 𝑆 )
73 72 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) = 𝑁 → ( 𝐴 mod 8 ) ∈ 𝑆 ) )
74 70 73 jaod ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( ( 𝐴 mod 8 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ ( 𝐴 mod 8 ) = 𝑁 ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) )
75 37 74 syl5 ⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑁 ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) )
76 11 33 75 3pm3.2i ⊢ ( 𝑁 ∈ ℤ ∧ 2 ∥ ( 𝑁 + 1 ) ∧ ( ( 𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴 ) → ( ( 𝐴 mod 8 ) ∈ ( 0 ... 𝑁 ) → ( 𝐴 mod 8 ) ∈ 𝑆 ) ) )