lgsdir2lem2

	Ref	Expression
Hypotheses	lgsdir2lem2.1	$⊢ (K \in ℤ \land 2 ∥ (K + 1) \land ((A \in ℤ \land \neg 2 ∥ A) \to (A \mod 8 \in (0 \dots K) \to A \mod 8 \in S)))$
	lgsdir2lem2.2	$⊢ M = K + 1$
	lgsdir2lem2.3	$⊢ N = M + 1$
	lgsdir2lem2.4	$⊢ N \in S$
Assertion	lgsdir2lem2	$⊢ (N \in ℤ \land 2 ∥ (N + 1) \land ((A \in ℤ \land \neg 2 ∥ A) \to (A \mod 8 \in (0 \dots N) \to A \mod 8 \in S)))$

Proof

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

Metamath Proof Explorer

Theorem lgsdir2lem2

Proof