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 
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( A rmY M ) || ( A rmY N ) ) )

Proof

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