Metamath Proof Explorer

Theorem 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 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) ∥ ( 𝐴 Yrm 𝑁 ) ) )

Proof

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