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	14	elfzelzd	$⊢ ((((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 ℤ$
16		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 ℤ$
17	16	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 ℤ$
18		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)))$
19		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)$
20		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}$
21	20	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}$
22		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
23	22	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
24	23	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℤ$
25	21 9 24	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 ℤ$
26	19	elfzelzd	$⊢ ((((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 ℤ$
27		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
28	27	fovcl	$⊢ (A \in ℤ_{\geq 2} \land k \in ℤ) \to A Y_{rm} k \in ℤ$
29	21 26 28	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 ℤ$
30	27	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A Y_{rm} M \in ℤ$
31	21 17 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} M \in ℤ$
32	27	fovcl	$⊢ (A \in ℤ_{\geq 2} \land m \in ℤ) \to A Y_{rm} m \in ℤ$
33	21 15 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	27	fovcl	$⊢ (A \in ℤ_{\geq 2} \land K \in ℤ) \to A Y_{rm} K \in ℤ$
35	21 13 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} K \in ℤ$
36		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)))))$
37	21 9 26 13 36	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)))))$
38	18 37	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))))$
39		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))))$
40		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))))$
41	25 29 35 31 38 39 40	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))))$
42		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))$
43		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)))$
44	11 15 17 42 43	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)))$
45		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)))))$
46	21 9 17 15 45	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)))))$
47	44 46	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))))$
48		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))))$
49	25 29 31 33 41 47 48	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))))$
50		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$
51	6 19 14 49 50	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$
52		id	$⊢ k = m \to k = m$
53		eqidd	$⊢ k = m \to K = K$
54	52 53	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))))$
55	51 54	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))))$
56	18 55	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)))$
57		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)))$
58	11 15 13 56 57	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)))$
59		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))$
60	11 13 15 17 58 42 59	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))$
61	60	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)))))$
62	61	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))))))$
63	62	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)))))$
64	4 63	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))))$
65	64	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)))))$
66	65	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))))$
67	2 66	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)))$
68		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)))))$
69	7 68	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)))))$
70	67 69	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