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 A2MNMNAYrmMAYrmN

Proof

Step Hyp Ref Expression
1 rmyeq0 A2NN=0AYrmN=0
2 1 3adant2 A2MNN=0AYrmN=0
3 0dvds N0NN=0
4 3 3ad2ant3 A2MN0NN=0
5 frmy Yrm:2×
6 5 fovcl A2NAYrmN
7 6 3adant2 A2MNAYrmN
8 0dvds AYrmN0AYrmNAYrmN=0
9 7 8 syl A2MN0AYrmNAYrmN=0
10 2 4 9 3bitr4d A2MN0N0AYrmN
11 10 adantr A2MNM=00N0AYrmN
12 simpr A2MNM=0M=0
13 12 breq1d A2MNM=0MN0N
14 12 oveq2d A2MNM=0AYrmM=AYrm0
15 simpl1 A2MNM=0A2
16 rmy0 A2AYrm0=0
17 15 16 syl A2MNM=0AYrm0=0
18 14 17 eqtrd A2MNM=0AYrmM=0
19 18 breq1d A2MNM=0AYrmMAYrmN0AYrmN
20 11 13 19 3bitr4d A2MNM=0MNAYrmMAYrmN
21 5 fovcl A2MAYrmM
22 21 3adant3 A2MNAYrmM
23 dvds0 AYrmMAYrmM0
24 22 23 syl A2MNAYrmM0
25 16 3ad2ant1 A2MNAYrm0=0
26 24 25 breqtrrd A2MNAYrmMAYrm0
27 oveq2 NmodM=0AYrmNmodM=AYrm0
28 27 breq2d NmodM=0AYrmMAYrmNmodMAYrmMAYrm0
29 26 28 syl5ibrcom A2MNNmodM=0AYrmMAYrmNmodM
30 29 adantr A2MNM0NmodM=0AYrmMAYrmNmodM
31 zre NN
32 31 3ad2ant3 A2MNN
33 32 ad2antrr A2MNM0NmodM0N
34 zcn MM
35 34 3ad2ant2 A2MNM
36 35 ad2antrr A2MNM0NmodM0M
37 simplr A2MNM0NmodM0M0
38 36 37 absrpcld A2MNM0NmodM0M+
39 modlt NM+NmodM<M
40 33 38 39 syl2anc A2MNM0NmodM0NmodM<M
41 simpll1 A2MNM0NmodM0A2
42 simpll3 A2MNM0NmodM0N
43 simpll2 A2MNM0NmodM0M
44 nnabscl MM0M
45 43 37 44 syl2anc A2MNM0NmodM0M
46 42 45 zmodcld A2MNM0NmodM0NmodM0
47 nn0abscl MM0
48 47 3ad2ant2 A2MNM0
49 48 ad2antrr A2MNM0NmodM0M0
50 ltrmynn0 A2NmodM0M0NmodM<MAYrmNmodM<AYrmM
51 41 46 49 50 syl3anc A2MNM0NmodM0NmodM<MAYrmNmodM<AYrmM
52 40 51 mpbid A2MNM0NmodM0AYrmNmodM<AYrmM
53 46 nn0zd A2MNM0NmodM0NmodM
54 rmyabs A2NmodMAYrmNmodM=AYrmNmodM
55 41 53 54 syl2anc A2MNM0NmodM0AYrmNmodM=AYrmNmodM
56 33 38 modcld A2MNM0NmodM0NmodM
57 modge0 NM+0NmodM
58 33 38 57 syl2anc A2MNM0NmodM00NmodM
59 56 58 absidd A2MNM0NmodM0NmodM=NmodM
60 59 oveq2d A2MNM0NmodM0AYrmNmodM=AYrmNmodM
61 55 60 eqtrd A2MNM0NmodM0AYrmNmodM=AYrmNmodM
62 rmyabs A2MAYrmM=AYrmM
63 41 43 62 syl2anc A2MNM0NmodM0AYrmM=AYrmM
64 52 61 63 3brtr4d A2MNM0NmodM0AYrmNmodM<AYrmM
65 5 fovcl A2NmodMAYrmNmodM
66 41 53 65 syl2anc A2MNM0NmodM0AYrmNmodM
67 nn0abscl AYrmNmodMAYrmNmodM0
68 66 67 syl A2MNM0NmodM0AYrmNmodM0
69 68 nn0red A2MNM0NmodM0AYrmNmodM
70 22 ad2antrr A2MNM0NmodM0AYrmM
71 nn0abscl AYrmMAYrmM0
72 70 71 syl A2MNM0NmodM0AYrmM0
73 72 nn0red A2MNM0NmodM0AYrmM
74 69 73 ltnled A2MNM0NmodM0AYrmNmodM<AYrmM¬AYrmMAYrmNmodM
75 64 74 mpbid A2MNM0NmodM0¬AYrmMAYrmNmodM
76 simpr A2MNM0NmodM0NmodM0
77 rmyeq0 A2NmodMNmodM=0AYrmNmodM=0
78 41 53 77 syl2anc A2MNM0NmodM0NmodM=0AYrmNmodM=0
79 78 necon3bid A2MNM0NmodM0NmodM0AYrmNmodM0
80 76 79 mpbid A2MNM0NmodM0AYrmNmodM0
81 dvdsleabs2 AYrmMAYrmNmodMAYrmNmodM0AYrmMAYrmNmodMAYrmMAYrmNmodM
82 70 66 80 81 syl3anc A2MNM0NmodM0AYrmMAYrmNmodMAYrmMAYrmNmodM
83 75 82 mtod A2MNM0NmodM0¬AYrmMAYrmNmodM
84 83 ex A2MNM0NmodM0¬AYrmMAYrmNmodM
85 84 necon4ad A2MNM0AYrmMAYrmNmodMNmodM=0
86 30 85 impbid A2MNM0NmodM=0AYrmMAYrmNmodM
87 simpl2 A2MNM0M
88 simpl3 A2MNM0N
89 simpr A2MNM0M0
90 dvdsabsmod0 MNM0MNNmodM=0
91 87 88 89 90 syl3anc A2MNM0MNNmodM=0
92 simpl1 A2MNM0A2
93 32 adantr A2MNM0N
94 zre MM
95 94 3ad2ant2 A2MNM
96 95 adantr A2MNM0M
97 modabsdifz NMM0NNmodMM
98 93 96 89 97 syl3anc A2MNM0NNmodMM
99 98 znegcld A2MNM0NNmodMM
100 jm2.19lem4 A2MNNNmodMMAYrmMAYrmNAYrmMAYrmN+NNmodMM M
101 92 87 88 99 100 syl121anc A2MNM0AYrmMAYrmNAYrmMAYrmN+NNmodMM M
102 32 recnd A2MNN
103 102 adantr A2MNM0N
104 35 adantr A2MNM0M
105 104 89 absrpcld A2MNM0M+
106 93 105 modcld A2MNM0NmodM
107 106 recnd A2MNM0NmodM
108 103 107 subcld A2MNM0NNmodM
109 108 104 89 divcld A2MNM0NNmodMM
110 109 104 mulneg1d A2MNM0NNmodMM M=NNmodMM M
111 110 oveq2d A2MNM0N+NNmodMM M=N+NNmodMM M
112 109 104 mulcld A2MNM0NNmodMM M
113 103 112 negsubd A2MNM0N+NNmodMM M=NNNmodMM M
114 108 104 89 divcan1d A2MNM0NNmodMM M=NNmodM
115 114 oveq2d A2MNM0NNNmodMM M=NNNmodM
116 103 107 nncand A2MNM0NNNmodM=NmodM
117 115 116 eqtrd A2MNM0NNNmodMM M=NmodM
118 111 113 117 3eqtrrd A2MNM0NmodM=N+NNmodMM M
119 118 oveq2d A2MNM0AYrmNmodM=AYrmN+NNmodMM M
120 119 breq2d A2MNM0AYrmMAYrmNmodMAYrmMAYrmN+NNmodMM M
121 101 120 bitr4d A2MNM0AYrmMAYrmNAYrmMAYrmNmodM
122 86 91 121 3bitr4d A2MNM0MNAYrmMAYrmN
123 20 122 pm2.61dane A2MNMNAYrmMAYrmN