jm2.25

Description: Lemma for jm2.26 . Remainders mod X(2n) are negaperiodic mod 2n. (Contributed by Stefan O'Rear, 2-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A \in ℤ_{\geq 2}$
2		simprrr	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to N \in ℤ$
3		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
4	3	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
5	4	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℤ$
6	1 2 5	syl2anc	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A X_{rm} N \in ℤ$
7		simprrl	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M \in ℤ$
8		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
9	8	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A Y_{rm} M \in ℤ$
10	1 7 9	syl2anc	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} M \in ℤ$
11		congid	$⊢ (A X_{rm} N \in ℤ \land A Y_{rm} M \in ℤ) \to (A X_{rm} N) ∥ ((A Y_{rm} M) - (A Y_{rm} M))$
12	6 10 11	syl2anc	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ ((A Y_{rm} M) - (A Y_{rm} M))$
13		2cnd	$⊢ N \in ℤ \to 2 \in ℂ$
14		zcn	$⊢ N \in ℤ \to N \in ℂ$
15	13 14	mulcld	$⊢ N \in ℤ \to 2 \cdot N \in ℂ$
16	15	mul02d	$⊢ N \in ℤ \to 0 \cdot 2 \cdot N = 0$
17	16	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to 0 \cdot 2 \cdot N = 0$
18	17	oveq2d	$⊢ (M \in ℤ \land N \in ℤ) \to M + 0 \cdot 2 \cdot N = M + 0$
19		zcn	$⊢ M \in ℤ \to M \in ℂ$
20	19	addid1d	$⊢ M \in ℤ \to M + 0 = M$
21	20	adantr	$⊢ (M \in ℤ \land N \in ℤ) \to M + 0 = M$
22	18 21	eqtrd	$⊢ (M \in ℤ \land N \in ℤ) \to M + 0 \cdot 2 \cdot N = M$
23	22	ad2antll	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M + 0 \cdot 2 \cdot N = M$
24	23	oveq2d	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} (M + 0 \cdot 2 \cdot N) = A Y_{rm} M$
25	24	oveq1d	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (A Y_{rm} M) = (A Y_{rm} M) - (A Y_{rm} M)$
26	12 25	breqtrrd	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (A Y_{rm} M))$
27	26	orcd	$⊢ (I \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (- (A Y_{rm} M))))$
28	27	ex	$⊢ I \in ℤ \to ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (- (A Y_{rm} M)))))$
29		simprl	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A \in ℤ_{\geq 2}$
30		simprrr	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to N \in ℤ$
31	29 30 5	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A X_{rm} N \in ℤ$
32		simprrl	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M \in ℤ$
33	29 32 9	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} M \in ℤ$
34		simpl	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b \in ℤ$
35	34	peano2zd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b + 1 \in ℤ$
36		eluzel2	$⊢ A \in ℤ_{\geq 2} \to 2 \in ℤ$
37	36	ad2antrl	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 \in ℤ$
38	37 30	zmulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 \cdot N \in ℤ$
39	35 38	zmulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (b + 1) 2 \cdot N \in ℤ$
40	32 39	zaddcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M + (b + 1) 2 \cdot N \in ℤ$
41	8	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M + (b + 1) 2 \cdot N \in ℤ) \to A Y_{rm} (M + (b + 1) 2 \cdot N) \in ℤ$
42	29 40 41	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} (M + (b + 1) 2 \cdot N) \in ℤ$
43	34 38	zmulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b 2 \cdot N \in ℤ$
44	32 43	zaddcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M + b 2 \cdot N \in ℤ$
45	8	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M + b 2 \cdot N \in ℤ) \to A Y_{rm} (M + b 2 \cdot N) \in ℤ$
46	29 44 45	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} (M + b 2 \cdot N) \in ℤ$
47	3	fovcl	$⊢ (A \in ℤ_{\geq 2} \land 2 \cdot N \in ℤ) \to A X_{rm} 2 \cdot N \in ℕ_{0}$
48	47	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land 2 \cdot N \in ℤ) \to A X_{rm} 2 \cdot N \in ℤ$
49	29 38 48	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A X_{rm} 2 \cdot N \in ℤ$
50	46 49	zmulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) \in ℤ$
51	46	znegcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to - (A Y_{rm} (M + b 2 \cdot N)) \in ℤ$
52	50 51	zsubcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N))) \in ℤ$
53	3	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M + b 2 \cdot N \in ℤ) \to A X_{rm} (M + b 2 \cdot N) \in ℕ_{0}$
54	53	nn0zd	$⊢ (A \in ℤ_{\geq 2} \land M + b 2 \cdot N \in ℤ) \to A X_{rm} (M + b 2 \cdot N) \in ℤ$
55	29 44 54	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A X_{rm} (M + b 2 \cdot N) \in ℤ$
56	8	fovcl	$⊢ (A \in ℤ_{\geq 2} \land 2 \cdot N \in ℤ) \to A Y_{rm} 2 \cdot N \in ℤ$
57	29 38 56	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} 2 \cdot N \in ℤ$
58	55 57	zmulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N) \in ℤ$
59	37 31	zmulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 (A X_{rm} N) \in ℤ$
60		dvdsmul2	$⊢ (2 (A X_{rm} N) \in ℤ \land A X_{rm} N \in ℤ) \to (A X_{rm} N) ∥ 2 (A X_{rm} N) (A X_{rm} N)$
61	59 31 60	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ 2 (A X_{rm} N) (A X_{rm} N)$
62		rmxdbl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} 2 \cdot N = 2 {(A X_{rm} N)}^{2} - 1$
63	29 30 62	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A X_{rm} 2 \cdot N = 2 {(A X_{rm} N)}^{2} - 1$
64	63	oveq1d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} 2 \cdot N) + 1 = 2 {(A X_{rm} N)}^{2} - 1 + 1$
65		2cnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 \in ℂ$
66	29 30 4	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A X_{rm} N \in ℕ_{0}$
67	66	nn0cnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A X_{rm} N \in ℂ$
68	67	sqcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to {(A X_{rm} N)}^{2} \in ℂ$
69	65 68	mulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 {(A X_{rm} N)}^{2} \in ℂ$
70		1cnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 \in ℂ$
71	69 70	npcand	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 {(A X_{rm} N)}^{2} - 1 + 1 = 2 {(A X_{rm} N)}^{2}$
72	67	sqvald	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to {(A X_{rm} N)}^{2} = (A X_{rm} N) (A X_{rm} N)$
73	72	oveq2d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 {(A X_{rm} N)}^{2} = 2 (A X_{rm} N) (A X_{rm} N)$
74		mulass	$⊢ (2 \in ℂ \land A X_{rm} N \in ℂ \land A X_{rm} N \in ℂ) \to 2 (A X_{rm} N) (A X_{rm} N) = 2 (A X_{rm} N) (A X_{rm} N)$
75	74	eqcomd	$⊢ (2 \in ℂ \land A X_{rm} N \in ℂ \land A X_{rm} N \in ℂ) \to 2 (A X_{rm} N) (A X_{rm} N) = 2 (A X_{rm} N) (A X_{rm} N)$
76	65 67 67 75	syl3anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 (A X_{rm} N) (A X_{rm} N) = 2 (A X_{rm} N) (A X_{rm} N)$
77	73 76	eqtrd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 {(A X_{rm} N)}^{2} = 2 (A X_{rm} N) (A X_{rm} N)$
78	64 71 77	3eqtrd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} 2 \cdot N) + 1 = 2 (A X_{rm} N) (A X_{rm} N)$
79	61 78	breqtrrd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ ((A X_{rm} 2 \cdot N) + 1)$
80	49	peano2zd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} 2 \cdot N) + 1 \in ℤ$
81		dvdsmultr2	$⊢ (A X_{rm} N \in ℤ \land A Y_{rm} (M + b 2 \cdot N) \in ℤ \land (A X_{rm} 2 \cdot N) + 1 \in ℤ) \to ((A X_{rm} N) ∥ ((A X_{rm} 2 \cdot N) + 1) \to (A X_{rm} N) ∥ (A Y_{rm} (M + b 2 \cdot N)) ((A X_{rm} 2 \cdot N) + 1))$
82	31 46 80 81	syl3anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to ((A X_{rm} N) ∥ ((A X_{rm} 2 \cdot N) + 1) \to (A X_{rm} N) ∥ (A Y_{rm} (M + b 2 \cdot N)) ((A X_{rm} 2 \cdot N) + 1))$
83	79 82	mpd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ (A Y_{rm} (M + b 2 \cdot N)) ((A X_{rm} 2 \cdot N) + 1)$
84	46	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} (M + b 2 \cdot N) \in ℂ$
85	84	mulid1d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + b 2 \cdot N)) \cdot 1 = A Y_{rm} (M + b 2 \cdot N)$
86	85	oveq2d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) + (A Y_{rm} (M + b 2 \cdot N)) \cdot 1 = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) + (A Y_{rm} (M + b 2 \cdot N))$
87	49	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A X_{rm} 2 \cdot N \in ℂ$
88	84 87 70	adddid	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + b 2 \cdot N)) ((A X_{rm} 2 \cdot N) + 1) = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) + (A Y_{rm} (M + b 2 \cdot N)) \cdot 1$
89	50	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) \in ℂ$
90	89 84	subnegd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N))) = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) + (A Y_{rm} (M + b 2 \cdot N))$
91	86 88 90	3eqtr4d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + b 2 \cdot N)) ((A X_{rm} 2 \cdot N) + 1) = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N)))$
92	83 91	breqtrd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N))))$
93	8	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
94	29 30 93	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} N \in ℤ$
95	37 94	zmulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 (A Y_{rm} N) \in ℤ$
96		dvdsmul2	$⊢ (2 (A Y_{rm} N) \in ℤ \land A X_{rm} N \in ℤ) \to (A X_{rm} N) ∥ 2 (A Y_{rm} N) (A X_{rm} N)$
97	95 31 96	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ 2 (A Y_{rm} N) (A X_{rm} N)$
98		rmydbl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} 2 \cdot N = 2 (A X_{rm} N) (A Y_{rm} N)$
99	29 30 98	syl2anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} 2 \cdot N = 2 (A X_{rm} N) (A Y_{rm} N)$
100	94	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} N \in ℂ$
101	65 67 100	mul32d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 (A X_{rm} N) (A Y_{rm} N) = 2 (A Y_{rm} N) (A X_{rm} N)$
102	99 101	eqtrd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} 2 \cdot N = 2 (A Y_{rm} N) (A X_{rm} N)$
103	97 102	breqtrrd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ (A Y_{rm} 2 \cdot N)$
104		dvdsmultr2	$⊢ (A X_{rm} N \in ℤ \land A X_{rm} (M + b 2 \cdot N) \in ℤ \land A Y_{rm} 2 \cdot N \in ℤ) \to ((A X_{rm} N) ∥ (A Y_{rm} 2 \cdot N) \to (A X_{rm} N) ∥ (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N))$
105	31 55 57 104	syl3anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to ((A X_{rm} N) ∥ (A Y_{rm} 2 \cdot N) \to (A X_{rm} N) ∥ (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N))$
106	103 105	mpd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N)$
107	31 52 58 92 106	dvds2addd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N))) + (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N))$
108	34	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b \in ℂ$
109	38	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 \cdot N \in ℂ$
110	108 70 109	adddird	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (b + 1) 2 \cdot N = b 2 \cdot N + 1 2 \cdot N$
111	110	oveq2d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M + (b + 1) 2 \cdot N = M + b 2 \cdot N + 1 2 \cdot N$
112	32	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M \in ℂ$
113	43	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b 2 \cdot N \in ℂ$
114		1zzd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 \in ℤ$
115	114 38	zmulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 2 \cdot N \in ℤ$
116	115	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 2 \cdot N \in ℂ$
117	112 113 116	addassd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M + b 2 \cdot N + 1 2 \cdot N = M + b 2 \cdot N + 1 2 \cdot N$
118	109	mulid2d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 2 \cdot N = 2 \cdot N$
119	118	oveq2d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M + b 2 \cdot N + 1 2 \cdot N = M + b 2 \cdot N + 2 \cdot N$
120	111 117 119	3eqtr2d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M + (b + 1) 2 \cdot N = M + b 2 \cdot N + 2 \cdot N$
121	120	oveq2d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} (M + (b + 1) 2 \cdot N) = A Y_{rm} (M + b 2 \cdot N + 2 \cdot N)$
122		rmyadd	$⊢ (A \in ℤ_{\geq 2} \land M + b 2 \cdot N \in ℤ \land 2 \cdot N \in ℤ) \to A Y_{rm} (M + b 2 \cdot N + 2 \cdot N) = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) + (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N)$
123	29 44 38 122	syl3anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} (M + b 2 \cdot N + 2 \cdot N) = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) + (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N)$
124	121 123	eqtrd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} (M + (b + 1) 2 \cdot N) = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) + (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N)$
125	124	oveq1d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} (M + b 2 \cdot N))) = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) + (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N)))$
126	58	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N) \in ℂ$
127	51	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to - (A Y_{rm} (M + b 2 \cdot N)) \in ℂ$
128	89 126 127	addsubd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) + (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N))) = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N))) + (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N)$
129	125 128	eqtrd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} (M + b 2 \cdot N))) = (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N))) + (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N)$
130	107 129	breqtrrd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} (M + b 2 \cdot N))))$
131	130	olcd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (A Y_{rm} (M + b 2 \cdot N))) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} (M + b 2 \cdot N)))))$
132		jm2.25lem1	$⊢ ((A X_{rm} N \in ℤ \land A Y_{rm} M \in ℤ) \land (A Y_{rm} (M + (b + 1) 2 \cdot N) \in ℤ \land A Y_{rm} (M + b 2 \cdot N) \in ℤ) \land ((A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (A Y_{rm} (M + b 2 \cdot N))) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} (M + b 2 \cdot N)))))) \to (((A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (- (A Y_{rm} M)))) \leftrightarrow ((A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} M)))))$
133	31 33 42 46 131 132	syl221anc	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (((A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (- (A Y_{rm} M)))) \leftrightarrow ((A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} M)))))$
134	133	pm5.74da	$⊢ b \in ℤ \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (- (A Y_{rm} M))))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} M))))))$
135		oveq1	$⊢ a = b \to a 2 \cdot N = b 2 \cdot N$
136	135	oveq2d	$⊢ a = b \to M + a 2 \cdot N = M + b 2 \cdot N$
137	136	oveq2d	$⊢ a = b \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} (M + b 2 \cdot N)$
138	137	oveq1d	$⊢ a = b \to (A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M) = (A Y_{rm} (M + b 2 \cdot N)) - (A Y_{rm} M)$
139	138	breq2d	$⊢ a = b \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M)) \leftrightarrow (A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (A Y_{rm} M)))$
140	137	oveq1d	$⊢ a = b \to (A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M)) = (A Y_{rm} (M + b 2 \cdot N)) - (- (A Y_{rm} M))$
141	140	breq2d	$⊢ a = b \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M))) \leftrightarrow (A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (- (A Y_{rm} M))))$
142	139 141	orbi12d	$⊢ a = b \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} (M + b 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (- (A Y_{rm} M)))))$
143	142	imbi2d	$⊢ a = b \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \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))))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + b 2 \cdot N)) - (- (A Y_{rm} M))))))$
144		oveq1	$⊢ a = b + 1 \to a 2 \cdot N = (b + 1) 2 \cdot N$
145	144	oveq2d	$⊢ a = b + 1 \to M + a 2 \cdot N = M + (b + 1) 2 \cdot N$
146	145	oveq2d	$⊢ a = b + 1 \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} (M + (b + 1) 2 \cdot N)$
147	146	oveq1d	$⊢ a = b + 1 \to (A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M) = (A Y_{rm} (M + (b + 1) 2 \cdot N)) - (A Y_{rm} M)$
148	147	breq2d	$⊢ a = b + 1 \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M)) \leftrightarrow (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (A Y_{rm} M)))$
149	146	oveq1d	$⊢ a = b + 1 \to (A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M)) = (A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} M))$
150	149	breq2d	$⊢ a = b + 1 \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M))) \leftrightarrow (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} M))))$
151	148 150	orbi12d	$⊢ a = b + 1 \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} (M + (b + 1) 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} M)))))$
152	151	imbi2d	$⊢ a = b + 1 \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \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))))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + (b + 1) 2 \cdot N)) - (- (A Y_{rm} M))))))$
153		oveq1	$⊢ a = 0 \to a 2 \cdot N = 0 \cdot 2 \cdot N$
154	153	oveq2d	$⊢ a = 0 \to M + a 2 \cdot N = M + 0 \cdot 2 \cdot N$
155	154	oveq2d	$⊢ a = 0 \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} (M + 0 \cdot 2 \cdot N)$
156	155	oveq1d	$⊢ a = 0 \to (A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M) = (A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (A Y_{rm} M)$
157	156	breq2d	$⊢ a = 0 \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M)) \leftrightarrow (A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (A Y_{rm} M)))$
158	155	oveq1d	$⊢ a = 0 \to (A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M)) = (A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (- (A Y_{rm} M))$
159	158	breq2d	$⊢ a = 0 \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M))) \leftrightarrow (A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (- (A Y_{rm} M))))$
160	157 159	orbi12d	$⊢ a = 0 \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} (M + 0 \cdot 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (- (A Y_{rm} M)))))$
161	160	imbi2d	$⊢ a = 0 \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \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))))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (- (A Y_{rm} M))))))$
162		oveq1	$⊢ a = I \to a 2 \cdot N = I 2 \cdot N$
163	162	oveq2d	$⊢ a = I \to M + a 2 \cdot N = M + I 2 \cdot N$
164	163	oveq2d	$⊢ a = I \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} (M + I 2 \cdot N)$
165	164	oveq1d	$⊢ a = I \to (A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M) = (A Y_{rm} (M + I 2 \cdot N)) - (A Y_{rm} M)$
166	165	breq2d	$⊢ a = I \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (A Y_{rm} M)) \leftrightarrow (A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (A Y_{rm} M)))$
167	164	oveq1d	$⊢ a = I \to (A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M)) = (A Y_{rm} (M + I 2 \cdot N)) - (- (A Y_{rm} M))$
168	167	breq2d	$⊢ a = I \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + a 2 \cdot N)) - (- (A Y_{rm} M))) \leftrightarrow (A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (- (A Y_{rm} M))))$
169	166 168	orbi12d	$⊢ a = I \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} (M + I 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (- (A Y_{rm} M)))))$
170	169	imbi2d	$⊢ a = I \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \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))))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (- (A Y_{rm} M))))))$
171	134 143 152 161 170	zindbi	$⊢ I \in ℤ \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + 0 \cdot 2 \cdot N)) - (- (A Y_{rm} M))))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (- (A Y_{rm} M))))))$
172	28 171	mpbid	$⊢ I \in ℤ \to ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (- (A Y_{rm} M)))))$
173	172	impcom	$⊢ ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℤ) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (- (A Y_{rm} M))))$
174	173	3impa	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ) \land I \in ℤ) \to ((A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} (M + I 2 \cdot N)) - (- (A Y_{rm} M))))$

Metamath Proof Explorer

Theorem jm2.25

Proof