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	biimtrid	⊢ ( ( 𝐴 ∈ ℤ ∧ ¬ 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 ) ∈ 𝑆 ) ) )