jm2.19

Description: Lemma 2.19 of JonesMatijasevic p. 696. Transfer divisibility constraints between Y-values and their indices. (Contributed by Stefan O'Rear, 24-Sep-2014)

		Ref	Expression
	Assertion	jm2.19	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} N))$

Proof

Step	Hyp	Ref	Expression
1		rmyeq0	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (N = 0 \leftrightarrow A Y_{rm} N = 0)$
2	1	3adant2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (N = 0 \leftrightarrow A Y_{rm} N = 0)$
3		0dvds	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow N = 0)$
4	3	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (0 ∥ N \leftrightarrow N = 0)$
5		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
6	5	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
7	6	3adant2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} N \in ℤ$
8		0dvds	$⊢ A Y_{rm} N \in ℤ \to (0 ∥ (A Y_{rm} N) \leftrightarrow A Y_{rm} N = 0)$
9	7 8	syl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (0 ∥ (A Y_{rm} N) \leftrightarrow A Y_{rm} N = 0)$
10	2 4 9	3bitr4d	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (0 ∥ N \leftrightarrow 0 ∥ (A Y_{rm} N))$
11	10	adantr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M = 0) \to (0 ∥ N \leftrightarrow 0 ∥ (A Y_{rm} N))$
12		simpr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M = 0) \to M = 0$
13	12	breq1d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M = 0) \to (M ∥ N \leftrightarrow 0 ∥ N)$
14	12	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A Y_{rm} M = A Y_{rm} 0$
15		simpl1	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A \in ℤ_{\geq 2}$
16		rmy0	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 0 = 0$
17	15 16	syl	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A Y_{rm} 0 = 0$
18	14 17	eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M = 0) \to A Y_{rm} M = 0$
19	18	breq1d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M = 0) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow 0 ∥ (A Y_{rm} N))$
20	11 13 19	3bitr4d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M = 0) \to (M ∥ N \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} N))$
21	5	fovcl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to A Y_{rm} M \in ℤ$
22	21	3adant3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} M \in ℤ$
23		dvds0	$⊢ A Y_{rm} M \in ℤ \to (A Y_{rm} M) ∥ 0$
24	22 23	syl	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} M) ∥ 0$
25	16	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to A Y_{rm} 0 = 0$
26	24 25	breqtrrd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (A Y_{rm} M) ∥ (A Y_{rm} 0)$
27		oveq2	$⊢ N \mod \|M\| = 0 \to A Y_{rm} (N \mod \|M\|) = A Y_{rm} 0$
28	27	breq2d	$⊢ N \mod \|M\| = 0 \to ((A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} 0))$
29	26 28	syl5ibrcom	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (N \mod \|M\| = 0 \to (A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)))$
30	29	adantr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to (N \mod \|M\| = 0 \to (A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)))$
31		zre	$⊢ N \in ℤ \to N \in ℝ$
32	31	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to N \in ℝ$
33	32	ad2antrr	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to N \in ℝ$
34		zcn	$⊢ M \in ℤ \to M \in ℂ$
35	34	3ad2ant2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to M \in ℂ$
36	35	ad2antrr	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to M \in ℂ$
37		simplr	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to M \neq 0$
38	36 37	absrpcld	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|M\| \in ℝ^{+}$
39		modlt	$⊢ (N \in ℝ \land \|M\| \in ℝ^{+}) \to N \mod \|M\| < \|M\|$
40	33 38 39	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to N \mod \|M\| < \|M\|$
41		simpll1	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to A \in ℤ_{\geq 2}$
42		simpll3	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to N \in ℤ$
43		simpll2	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to M \in ℤ$
44		nnabscl	$⊢ (M \in ℤ \land M \neq 0) \to \|M\| \in ℕ$
45	43 37 44	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|M\| \in ℕ$
46	42 45	zmodcld	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to N \mod \|M\| \in ℕ_{0}$
47		nn0abscl	$⊢ M \in ℤ \to \|M\| \in ℕ_{0}$
48	47	3ad2ant2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to \|M\| \in ℕ_{0}$
49	48	ad2antrr	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|M\| \in ℕ_{0}$
50		ltrmynn0	$⊢ (A \in ℤ_{\geq 2} \land N \mod \|M\| \in ℕ_{0} \land \|M\| \in ℕ_{0}) \to (N \mod \|M\| < \|M\| \leftrightarrow A Y_{rm} (N \mod \|M\|) < A Y_{rm} \|M\|)$
51	41 46 49 50	syl3anc	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to (N \mod \|M\| < \|M\| \leftrightarrow A Y_{rm} (N \mod \|M\|) < A Y_{rm} \|M\|)$
52	40 51	mpbid	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to A Y_{rm} (N \mod \|M\|) < A Y_{rm} \|M\|$
53	46	nn0zd	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to N \mod \|M\| \in ℤ$
54		rmyabs	$⊢ (A \in ℤ_{\geq 2} \land N \mod \|M\| \in ℤ) \to \|A Y_{rm} (N \mod \|M\|)\| = A Y_{rm} \|N \mod \|M\|\|$
55	41 53 54	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|A Y_{rm} (N \mod \|M\|)\| = A Y_{rm} \|N \mod \|M\|\|$
56	33 38	modcld	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to N \mod \|M\| \in ℝ$
57		modge0	$⊢ (N \in ℝ \land \|M\| \in ℝ^{+}) \to 0 \leq N \mod \|M\|$
58	33 38 57	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to 0 \leq N \mod \|M\|$
59	56 58	absidd	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|N \mod \|M\|\| = N \mod \|M\|$
60	59	oveq2d	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to A Y_{rm} \|N \mod \|M\|\| = A Y_{rm} (N \mod \|M\|)$
61	55 60	eqtrd	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|A Y_{rm} (N \mod \|M\|)\| = A Y_{rm} (N \mod \|M\|)$
62		rmyabs	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ) \to \|A Y_{rm} M\| = A Y_{rm} \|M\|$
63	41 43 62	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|A Y_{rm} M\| = A Y_{rm} \|M\|$
64	52 61 63	3brtr4d	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|A Y_{rm} (N \mod \|M\|)\| < \|A Y_{rm} M\|$
65	5	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \mod \|M\| \in ℤ) \to A Y_{rm} (N \mod \|M\|) \in ℤ$
66	41 53 65	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to A Y_{rm} (N \mod \|M\|) \in ℤ$
67		nn0abscl	$⊢ A Y_{rm} (N \mod \|M\|) \in ℤ \to \|A Y_{rm} (N \mod \|M\|)\| \in ℕ_{0}$
68	66 67	syl	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|A Y_{rm} (N \mod \|M\|)\| \in ℕ_{0}$
69	68	nn0red	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|A Y_{rm} (N \mod \|M\|)\| \in ℝ$
70	22	ad2antrr	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to A Y_{rm} M \in ℤ$
71		nn0abscl	$⊢ A Y_{rm} M \in ℤ \to \|A Y_{rm} M\| \in ℕ_{0}$
72	70 71	syl	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|A Y_{rm} M\| \in ℕ_{0}$
73	72	nn0red	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \|A Y_{rm} M\| \in ℝ$
74	69 73	ltnled	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to (\|A Y_{rm} (N \mod \|M\|)\| < \|A Y_{rm} M\| \leftrightarrow \neg \|A Y_{rm} M\| \leq \|A Y_{rm} (N \mod \|M\|)\|)$
75	64 74	mpbid	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \neg \|A Y_{rm} M\| \leq \|A Y_{rm} (N \mod \|M\|)\|$
76		simpr	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to N \mod \|M\| \neq 0$
77		rmyeq0	$⊢ (A \in ℤ_{\geq 2} \land N \mod \|M\| \in ℤ) \to (N \mod \|M\| = 0 \leftrightarrow A Y_{rm} (N \mod \|M\|) = 0)$
78	41 53 77	syl2anc	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to (N \mod \|M\| = 0 \leftrightarrow A Y_{rm} (N \mod \|M\|) = 0)$
79	78	necon3bid	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to (N \mod \|M\| \neq 0 \leftrightarrow A Y_{rm} (N \mod \|M\|) \neq 0)$
80	76 79	mpbid	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to A Y_{rm} (N \mod \|M\|) \neq 0$
81		dvdsleabs2	$⊢ (A Y_{rm} M \in ℤ \land A Y_{rm} (N \mod \|M\|) \in ℤ \land A Y_{rm} (N \mod \|M\|) \neq 0) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)) \to \|A Y_{rm} M\| \leq \|A Y_{rm} (N \mod \|M\|)\|)$
82	70 66 80 81	syl3anc	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)) \to \|A Y_{rm} M\| \leq \|A Y_{rm} (N \mod \|M\|)\|)$
83	75 82	mtod	$⊢ (((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \land N \mod \|M\| \neq 0) \to \neg (A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|))$
84	83	ex	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to (N \mod \|M\| \neq 0 \to \neg (A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)))$
85	84	necon4ad	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)) \to N \mod \|M\| = 0)$
86	30 85	impbid	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to (N \mod \|M\| = 0 \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)))$
87		simpl2	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to M \in ℤ$
88		simpl3	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N \in ℤ$
89		simpr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to M \neq 0$
90		dvdsabsmod0	$⊢ (M \in ℤ \land N \in ℤ \land M \neq 0) \to (M ∥ N \leftrightarrow N \mod \|M\| = 0)$
91	87 88 89 90	syl3anc	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to (M ∥ N \leftrightarrow N \mod \|M\| = 0)$
92		simpl1	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to A \in ℤ_{\geq 2}$
93	32	adantr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N \in ℝ$
94		zre	$⊢ M \in ℤ \to M \in ℝ$
95	94	3ad2ant2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to M \in ℝ$
96	95	adantr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to M \in ℝ$
97		modabsdifz	$⊢ (N \in ℝ \land M \in ℝ \land M \neq 0) \to \frac{N - (N \mod \|M\|)}{M} \in ℤ$
98	93 96 89 97	syl3anc	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to \frac{N - (N \mod \|M\|)}{M} \in ℤ$
99	98	znegcld	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to - \frac{N - (N \mod \|M\|)}{M} \in ℤ$
100		jm2.19lem4	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ) \land - \frac{N - (N \mod \|M\|)}{M} \in ℤ) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (- \frac{N - (N \mod \|M\|)}{M}) \cdot M)))$
101	92 87 88 99 100	syl121anc	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (- \frac{N - (N \mod \|M\|)}{M}) \cdot M)))$
102	32	recnd	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to N \in ℂ$
103	102	adantr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N \in ℂ$
104	35	adantr	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to M \in ℂ$
105	104 89	absrpcld	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to \|M\| \in ℝ^{+}$
106	93 105	modcld	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N \mod \|M\| \in ℝ$
107	106	recnd	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N \mod \|M\| \in ℂ$
108	103 107	subcld	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N - (N \mod \|M\|) \in ℂ$
109	108 104 89	divcld	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to \frac{N - (N \mod \|M\|)}{M} \in ℂ$
110	109 104	mulneg1d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to (- \frac{N - (N \mod \|M\|)}{M}) \cdot M = - (\frac{N - (N \mod \|M\|)}{M}) \cdot M$
111	110	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N + (- \frac{N - (N \mod \|M\|)}{M}) \cdot M = N + (- (\frac{N - (N \mod \|M\|)}{M}) \cdot M)$
112	109 104	mulcld	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to (\frac{N - (N \mod \|M\|)}{M}) \cdot M \in ℂ$
113	103 112	negsubd	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N + (- (\frac{N - (N \mod \|M\|)}{M}) \cdot M) = N - (\frac{N - (N \mod \|M\|)}{M}) \cdot M$
114	108 104 89	divcan1d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to (\frac{N - (N \mod \|M\|)}{M}) \cdot M = N - (N \mod \|M\|)$
115	114	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N - (\frac{N - (N \mod \|M\|)}{M}) \cdot M = N - (N - (N \mod \|M\|))$
116	103 107	nncand	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N - (N - (N \mod \|M\|)) = N \mod \|M\|$
117	115 116	eqtrd	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N - (\frac{N - (N \mod \|M\|)}{M}) \cdot M = N \mod \|M\|$
118	111 113 117	3eqtrrd	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to N \mod \|M\| = N + (- \frac{N - (N \mod \|M\|)}{M}) \cdot M$
119	118	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to A Y_{rm} (N \mod \|M\|) = A Y_{rm} (N + (- \frac{N - (N \mod \|M\|)}{M}) \cdot M)$
120	119	breq2d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (- \frac{N - (N \mod \|M\|)}{M}) \cdot M)))$
121	101 120	bitr4d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N \mod \|M\|)))$
122	86 91 121	3bitr4d	$⊢ ((A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \land M \neq 0) \to (M ∥ N \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} N))$
123	20 122	pm2.61dane	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} N))$

Metamath Proof Explorer

Theorem jm2.19

Proof