jm2.26

Description: Lemma 2.26 of JonesMatijasevic p. 697, the "second step down lemma". (Contributed by Stefan O'Rear, 2-Oct-2014)

		Ref	Expression
	Assertion	jm2.26	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to (((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))) \leftrightarrow (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M)))$

Proof

Step	Hyp	Ref	Expression
1		acongrep	$⊢ (N \in ℕ \land M \in ℤ) \to \exists m \in (0 \dots N) (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M))$
2	1	ad2ant2l	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to \exists m \in (0 \dots N) (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M))$
3		acongrep	$⊢ (N \in ℕ \land K \in ℤ) \to \exists k \in (0 \dots N) (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))$
4	3	ad2ant2lr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to \exists k \in (0 \dots N) (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))$
5		2z	$⊢ 2 \in ℤ$
6		simpl1l	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to (A \in ℤ_{\geq 2} \land N \in ℕ)$
7		nnz	$⊢ N \in ℕ \to N \in ℤ$
8	7	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N \in ℤ$
9	6 8	syl	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to N \in ℤ$
10		zmulcl	$⊢ (2 \in ℤ \land N \in ℤ) \to 2 \cdot N \in ℤ$
11	5 9 10	sylancr	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to 2 \cdot N \in ℤ$
12		simplrl	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to K \in ℤ$
13	12	3ad2antl1	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to K \in ℤ$
14		simpl3l	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to m \in (0 \dots N)$
15		elfzelz	$⊢ m \in (0 \dots N) \to m \in ℤ$
16	14 15	syl	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to m \in ℤ$
17		simplrr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to M \in ℤ$
18	17	3ad2antl1	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to M \in ℤ$
19		simpl2r	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))$
20		simpl2l	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to k \in (0 \dots N)$
21		simplll	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to A \in ℤ_{\geq 2}$
22	21	3ad2antl1	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to A \in ℤ_{\geq 2}$
23		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
24	23	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
25	24	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℤ$
26	22 9 25	syl2anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to A X_{rm} N \in ℤ$
27		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
28	20 27	syl	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to k \in ℤ$
29		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
30	29	fovcl	$⊢ (A \in ℤ_{\geq 2} \land k \in ℤ) \to A Y_{rm} k \in ℤ$
31	22 28 30	syl2anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to A Y_{rm} k \in ℤ$
32	29	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A Y_{rm} M \in ℤ$
33	22 18 32	syl2anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to A Y_{rm} M \in ℤ$
34	29	fovcl	$⊢ (A \in ℤ_{\geq 2} \land m \in ℤ) \to A Y_{rm} m \in ℤ$
35	22 16 34	syl2anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to A Y_{rm} m \in ℤ$
36	29	fovcl	$⊢ (A \in ℤ_{\geq 2} \land K \in ℤ) \to A Y_{rm} K \in ℤ$
37	22 13 36	syl2anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to A Y_{rm} K \in ℤ$
38		jm2.26a	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (k \in ℤ \land K \in ℤ)) \to ((2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K))) \to ((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} K)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} K)))))$
39	22 9 28 13 38	syl22anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to ((2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K))) \to ((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} K)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} K)))))$
40	19 39	mpd	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to ((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} K)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} K))))$
41		simpr	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))$
42		acongtr	$⊢ ((A X_{rm} N \in ℤ \land A Y_{rm} k \in ℤ) \land (A Y_{rm} K \in ℤ \land A Y_{rm} M \in ℤ) \land (((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} K)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} K)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))))) \to ((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} M))))$
43	26 31 37 33 40 41 42	syl222anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to ((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} M))))$
44		simpl3r	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M))$
45		acongsym	$⊢ ((2 \cdot N \in ℤ \land m \in ℤ \land M \in ℤ) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M))) \to (2 \cdot N ∥ (M - m) \lor 2 \cdot N ∥ (M - (- m)))$
46	11 16 18 44 45	syl31anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to (2 \cdot N ∥ (M - m) \lor 2 \cdot N ∥ (M - (- m)))$
47		jm2.26a	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (M \in ℤ \land m \in ℤ)) \to ((2 \cdot N ∥ (M - m) \lor 2 \cdot N ∥ (M - (- m))) \to ((A X_{rm} N) ∥ ((A Y_{rm} M) - (A Y_{rm} m)) \lor (A X_{rm} N) ∥ ((A Y_{rm} M) - (- (A Y_{rm} m)))))$
48	22 9 18 16 47	syl22anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to ((2 \cdot N ∥ (M - m) \lor 2 \cdot N ∥ (M - (- m))) \to ((A X_{rm} N) ∥ ((A Y_{rm} M) - (A Y_{rm} m)) \lor (A X_{rm} N) ∥ ((A Y_{rm} M) - (- (A Y_{rm} m)))))$
49	46 48	mpd	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to ((A X_{rm} N) ∥ ((A Y_{rm} M) - (A Y_{rm} m)) \lor (A X_{rm} N) ∥ ((A Y_{rm} M) - (- (A Y_{rm} m))))$
50		acongtr	$⊢ ((A X_{rm} N \in ℤ \land A Y_{rm} k \in ℤ) \land (A Y_{rm} M \in ℤ \land A Y_{rm} m \in ℤ) \land (((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} M) - (A Y_{rm} m)) \lor (A X_{rm} N) ∥ ((A Y_{rm} M) - (- (A Y_{rm} m)))))) \to ((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} m)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} m))))$
51	26 31 33 35 43 49 50	syl222anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to ((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} m)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} m))))$
52		jm2.26lem3	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (k \in (0 \dots N) \land m \in (0 \dots N)) \land ((A X_{rm} N) ∥ ((A Y_{rm} k) - (A Y_{rm} m)) \lor (A X_{rm} N) ∥ ((A Y_{rm} k) - (- (A Y_{rm} m))))) \to k = m$
53	6 20 14 51 52	syl121anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to k = m$
54		id	$⊢ k = m \to k = m$
55		eqidd	$⊢ k = m \to K = K$
56	54 55	acongeq12d	$⊢ k = m \to ((2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K))) \leftrightarrow (2 \cdot N ∥ (m - K) \lor 2 \cdot N ∥ (m - (- K))))$
57	53 56	syl	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to ((2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K))) \leftrightarrow (2 \cdot N ∥ (m - K) \lor 2 \cdot N ∥ (m - (- K))))$
58	19 57	mpbid	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to (2 \cdot N ∥ (m - K) \lor 2 \cdot N ∥ (m - (- K)))$
59		acongsym	$⊢ ((2 \cdot N \in ℤ \land m \in ℤ \land K \in ℤ) \land (2 \cdot N ∥ (m - K) \lor 2 \cdot N ∥ (m - (- K)))) \to (2 \cdot N ∥ (K - m) \lor 2 \cdot N ∥ (K - (- m)))$
60	11 16 13 58 59	syl31anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to (2 \cdot N ∥ (K - m) \lor 2 \cdot N ∥ (K - (- m)))$
61		acongtr	$⊢ ((2 \cdot N \in ℤ \land K \in ℤ) \land (m \in ℤ \land M \in ℤ) \land ((2 \cdot N ∥ (K - m) \lor 2 \cdot N ∥ (K - (- m))) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \to (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M))$
62	11 13 16 18 60 44 61	syl222anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \land (k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \land (m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)))) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M))$
63	62	3exp1	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to ((k \in (0 \dots N) \land (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K)))) \to ((m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M))) \to (((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))) \to (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M)))))$
64	63	expd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to (k \in (0 \dots N) \to ((2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K))) \to ((m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M))) \to (((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))) \to (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M))))))$
65	64	rexlimdv	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to (\exists k \in (0 \dots N) (2 \cdot N ∥ (k - K) \lor 2 \cdot N ∥ (k - (- K))) \to ((m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M))) \to (((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))) \to (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M)))))$
66	4 65	mpd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to ((m \in (0 \dots N) \land (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M))) \to (((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))) \to (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M))))$
67	66	expd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to (m \in (0 \dots N) \to ((2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)) \to (((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))) \to (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M)))))$
68	67	rexlimdv	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to (\exists m \in (0 \dots N) (2 \cdot N ∥ (m - M) \lor 2 \cdot N ∥ (m - -M)) \to (((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))) \to (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M))))$
69	2 68	mpd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to (((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))) \to (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M)))$
70		jm2.26a	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to ((2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M)) \to ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))))$
71	7 70	sylanl2	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to ((2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M)) \to ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))))$
72	69 71	impbid	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in ℤ \land M \in ℤ)) \to (((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M)))) \leftrightarrow (2 \cdot N ∥ (K - M) \lor 2 \cdot N ∥ (K - -M)))$

Metamath Proof Explorer

Theorem jm2.26

Proof