jm2.26a

Description: Lemma for jm2.26 . Reverse direction is required to prove forward direction, so do it separately. Induction on difference between K and M, together with the addition formula fact that adding 2N only inverts sign. (Contributed by Stefan O'Rear, 2-Oct-2014)

		Ref	Expression
	Assertion	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)))))$

Proof

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		simplr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to N \in ℤ$
3		zmulcl	$⊢ (2 \in ℤ \land N \in ℤ) \to 2 \cdot N \in ℤ$
4	1 2 3	sylancr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to 2 \cdot N \in ℤ$
5		zsubcl	$⊢ (K \in ℤ \land M \in ℤ) \to K - M \in ℤ$
6	5	adantl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to K - M \in ℤ$
7		divides	$⊢ (2 \cdot N \in ℤ \land K - M \in ℤ) \to (2 \cdot N ∥ (K - M) \leftrightarrow \exists a \in ℤ a 2 \cdot N = K - M)$
8	4 6 7	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to (2 \cdot N ∥ (K - M) \leftrightarrow \exists a \in ℤ a 2 \cdot N = K - M)$
9		simplll	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to A \in ℤ_{\geq 2}$
10		simplrr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to M \in ℤ$
11		simpllr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to N \in ℤ$
12		simpr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to a \in ℤ$
13		jm2.25	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ) \land a \in ℤ) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M))))$
14	9 10 11 12 13	syl121anc	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M))))$
15	14	adantr	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 2 \cdot N = K - M) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M))))$
16		oveq2	$⊢ a 2 \cdot N = K - M \to M + a 2 \cdot N = M + K - M$
17	16	oveq2d	$⊢ a 2 \cdot N = K - M \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} (M + K - M)$
18		zcn	$⊢ M \in ℤ \to M \in ℂ$
19		zcn	$⊢ K \in ℤ \to K \in ℂ$
20		pncan3	$⊢ (M \in ℂ \land K \in ℂ) \to M + K - M = K$
21	18 19 20	syl2anr	$⊢ (K \in ℤ \land M \in ℤ) \to M + K - M = K$
22	21	ad2antlr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to M + K - M = K$
23	22	oveq2d	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to A Y_{rm} (M + K - M) = A Y_{rm} K$
24	17 23	sylan9eqr	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 2 \cdot N = K - M) \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} K$
25		eqidd	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 2 \cdot N = K - M) \to A Y_{rm} M = A Y_{rm} M$
26	24 25	acongeq12d	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 2 \cdot N = K - M) \to (((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M)))) \leftrightarrow ((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)))))$
27	15 26	mpbid	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 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))))$
28	27	rexlimdva2	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to (\exists a \in ℤ a 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)))))$
29	8 28	sylbid	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to (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)))))$
30		simprl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to K \in ℤ$
31		znegcl	$⊢ M \in ℤ \to - M \in ℤ$
32	31	ad2antll	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to - M \in ℤ$
33	30 32	zsubcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to K - -M \in ℤ$
34		divides	$⊢ (2 \cdot N \in ℤ \land K - -M \in ℤ) \to (2 \cdot N ∥ (K - -M) \leftrightarrow \exists a \in ℤ a 2 \cdot N = K - -M)$
35	4 33 34	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to (2 \cdot N ∥ (K - -M) \leftrightarrow \exists a \in ℤ a 2 \cdot N = K - -M)$
36		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
37	36	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
38	37	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℤ$
39	9 11 38	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to A X_{rm} N \in ℤ$
40		simplrl	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to K \in ℤ$
41		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
42	41	fovcl	$⊢ (A \in ℤ_{\geq 2} \land K \in ℤ) \to A Y_{rm} K \in ℤ$
43	9 40 42	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to A Y_{rm} K \in ℤ$
44	41	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A Y_{rm} M \in ℤ$
45	9 10 44	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to A Y_{rm} M \in ℤ$
46	39 43 45	3jca	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to (A X_{rm} N \in ℤ \land A Y_{rm} K \in ℤ \land A Y_{rm} M \in ℤ)$
47	46	adantr	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 2 \cdot N = K - -M) \to (A X_{rm} N \in ℤ \land A Y_{rm} K \in ℤ \land A Y_{rm} M \in ℤ)$
48	32	adantr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to - M \in ℤ$
49		jm2.25	$⊢ (A \in ℤ_{\geq 2} \land (- M \in ℤ \land N \in ℤ) \land a \in ℤ) \to ((A X_{rm} N) ∥ ((A Y_{rm} (- M + a 2 \cdot N)) - (A Y_{rm} -M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (- M + a 2 \cdot N)) - (- (A Y_{rm} -M))))$
50	9 48 11 12 49	syl121anc	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to ((A X_{rm} N) ∥ ((A Y_{rm} (- M + a 2 \cdot N)) - (A Y_{rm} -M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (- M + a 2 \cdot N)) - (- (A Y_{rm} -M))))$
51	50	adantr	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 2 \cdot N = K - -M) \to ((A X_{rm} N) ∥ ((A Y_{rm} (- M + a 2 \cdot N)) - (A Y_{rm} -M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (- M + a 2 \cdot N)) - (- (A Y_{rm} -M))))$
52		oveq2	$⊢ a 2 \cdot N = K - -M \to - M + a 2 \cdot N = -M + K - -M$
53	52	oveq2d	$⊢ a 2 \cdot N = K - -M \to A Y_{rm} (- M + a 2 \cdot N) = A Y_{rm} (-M + K - -M)$
54	18	negcld	$⊢ M \in ℤ \to - M \in ℂ$
55		pncan3	$⊢ (- M \in ℂ \land K \in ℂ) \to -M + K - -M = K$
56	54 19 55	syl2anr	$⊢ (K \in ℤ \land M \in ℤ) \to -M + K - -M = K$
57	56	ad2antlr	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to -M + K - -M = K$
58	57	oveq2d	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to A Y_{rm} (-M + K - -M) = A Y_{rm} K$
59	53 58	sylan9eqr	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 2 \cdot N = K - -M) \to A Y_{rm} (- M + a 2 \cdot N) = A Y_{rm} K$
60		rmyneg	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A Y_{rm} -M = - (A Y_{rm} M)$
61	9 10 60	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \to A Y_{rm} -M = - (A Y_{rm} M)$
62	61	adantr	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 2 \cdot N = K - -M) \to A Y_{rm} -M = - (A Y_{rm} M)$
63	59 62	acongeq12d	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 2 \cdot N = K - -M) \to (((A X_{rm} N) ∥ ((A Y_{rm} (- M + a 2 \cdot N)) - (A Y_{rm} -M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (- M + a 2 \cdot N)) - (- (A Y_{rm} -M)))) \leftrightarrow ((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))))))$
64	51 63	mpbid	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 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)))))$
65		acongneg2	$⊢ ((A X_{rm} N \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} 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))))$
66	47 64 65	syl2anc	$⊢ ((((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \land a \in ℤ) \land a 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))))$
67	66	rexlimdva2	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to (\exists a \in ℤ a 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)))))$
68	35 67	sylbid	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land (K \in ℤ \land M \in ℤ)) \to (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	29 68	jaod	$⊢ ((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)))))$

Metamath Proof Explorer

Theorem jm2.26a

Proof