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		dvds2add	$⊢ (A X_{rm} N \in ℤ \land (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N))) \in ℤ \land (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot 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)))) \land (A X_{rm} N) ∥ (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N)) \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	107	imp	$⊢ ((A X_{rm} N \in ℤ \land (A Y_{rm} (M + b 2 \cdot N)) (A X_{rm} 2 \cdot N) - (- (A Y_{rm} (M + b 2 \cdot N))) \in ℤ \land (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N) \in ℤ) \land ((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)))) \land (A X_{rm} N) ∥ (A X_{rm} (M + b 2 \cdot N)) (A Y_{rm} 2 \cdot N))) \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))$
109	31 52 58 92 106 108	syl32anc	$⊢ (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))$
110	34	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b \in ℂ$
111	38	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 2 \cdot N \in ℂ$
112	110 70 111	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$
113	112	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$
114	32	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M \in ℂ$
115	43	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b 2 \cdot N \in ℂ$
116		1zzd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 \in ℤ$
117	116 38	zmulcld	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 2 \cdot N \in ℤ$
118	117	zcnd	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 2 \cdot N \in ℂ$
119	114 115 118	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$
120	111	mulid2d	$⊢ (b \in ℤ \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 2 \cdot N = 2 \cdot N$
121	120	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$
122	113 119 121	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$
123	122	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)$
124		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)$
125	29 44 38 124	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)$
126	123 125	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)$
127	126	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)))$
128	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 ℂ$
129	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 ℂ$
130	89 128 129	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)$
131	127 130	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)$
132	109 131	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))))$
133	132	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)))))$
134		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)))))$
135	31 33 42 46 133 134	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)))))$
136	135	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))))))$
137		oveq1	$⊢ a = b \to a 2 \cdot N = b 2 \cdot N$
138	137	oveq2d	$⊢ a = b \to M + a 2 \cdot N = M + b 2 \cdot N$
139	138	oveq2d	$⊢ a = b \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} (M + b 2 \cdot N)$
140	139	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	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))$
143	142	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))))$
144	141 143	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)))))$
145	144	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))))))$
146		oveq1	$⊢ a = b + 1 \to a 2 \cdot N = (b + 1) 2 \cdot N$
147	146	oveq2d	$⊢ a = b + 1 \to M + a 2 \cdot N = M + (b + 1) 2 \cdot N$
148	147	oveq2d	$⊢ a = b + 1 \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} (M + (b + 1) 2 \cdot N)$
149	148	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	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))$
152	151	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))))$
153	150 152	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)))))$
154	153	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))))))$
155		oveq1	$⊢ a = 0 \to a 2 \cdot N = 0 \cdot 2 \cdot N$
156	155	oveq2d	$⊢ a = 0 \to M + a 2 \cdot N = M + 0 \cdot 2 \cdot N$
157	156	oveq2d	$⊢ a = 0 \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} (M + 0 \cdot 2 \cdot N)$
158	157	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	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))$
161	160	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))))$
162	159 161	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)))))$
163	162	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))))))$
164		oveq1	$⊢ a = I \to a 2 \cdot N = I 2 \cdot N$
165	164	oveq2d	$⊢ a = I \to M + a 2 \cdot N = M + I 2 \cdot N$
166	165	oveq2d	$⊢ a = I \to A Y_{rm} (M + a 2 \cdot N) = A Y_{rm} (M + I 2 \cdot N)$
167	166	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	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))$
170	169	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))))$
171	168 170	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)))))$
172	171	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))))))$
173	136 145 154 163 172	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))))))$
174	28 173	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)))))$
175	174	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))))$
176	175	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