Proof of Theorem jm2.19
Step | Hyp | Ref
| Expression |
1 | | rmyeq0 37520 |
. . . . . 6
Yrm |
2 | 1 | 3adant2 1080 |
. . . . 5
Yrm |
3 | | 0dvds 15002 |
. . . . . 6
|
4 | 3 | 3ad2ant3 1084 |
. . . . 5
|
5 | | frmy 37479 |
. . . . . . . 8
Yrm
|
6 | 5 | fovcl 6765 |
. . . . . . 7
Yrm |
7 | 6 | 3adant2 1080 |
. . . . . 6
Yrm |
8 | | 0dvds 15002 |
. . . . . 6
Yrm Yrm
Yrm |
9 | 7, 8 | syl 17 |
. . . . 5
Yrm Yrm |
10 | 2, 4, 9 | 3bitr4d 300 |
. . . 4
Yrm |
11 | 10 | adantr 481 |
. . 3
Yrm |
12 | | simpr 477 |
. . . 4
|
13 | 12 | breq1d 4663 |
. . 3
|
14 | 12 | oveq2d 6666 |
. . . . 5
Yrm
Yrm |
15 | | simpl1 1064 |
. . . . . 6
|
16 | | rmy0 37494 |
. . . . . 6
Yrm |
17 | 15, 16 | syl 17 |
. . . . 5
Yrm |
18 | 14, 17 | eqtrd 2656 |
. . . 4
Yrm |
19 | 18 | breq1d 4663 |
. . 3
Yrm Yrm Yrm |
20 | 11, 13, 19 | 3bitr4d 300 |
. 2
Yrm Yrm |
21 | 5 | fovcl 6765 |
. . . . . . . . 9
Yrm |
22 | 21 | 3adant3 1081 |
. . . . . . . 8
Yrm |
23 | | dvds0 14997 |
. . . . . . . 8
Yrm
Yrm |
24 | 22, 23 | syl 17 |
. . . . . . 7
Yrm |
25 | 16 | 3ad2ant1 1082 |
. . . . . . 7
Yrm |
26 | 24, 25 | breqtrrd 4681 |
. . . . . 6
Yrm Yrm |
27 | | oveq2 6658 |
. . . . . . 7
Yrm Yrm |
28 | 27 | breq2d 4665 |
. . . . . 6
Yrm Yrm Yrm Yrm |
29 | 26, 28 | syl5ibrcom 237 |
. . . . 5
Yrm Yrm |
30 | 29 | adantr 481 |
. . . 4
Yrm Yrm |
31 | | zre 11381 |
. . . . . . . . . . . . 13
|
32 | 31 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
|
33 | 32 | ad2antrr 762 |
. . . . . . . . . . 11
|
34 | | zcn 11382 |
. . . . . . . . . . . . . 14
|
35 | 34 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
|
36 | 35 | ad2antrr 762 |
. . . . . . . . . . . 12
|
37 | | simplr 792 |
. . . . . . . . . . . 12
|
38 | 36, 37 | absrpcld 14187 |
. . . . . . . . . . 11
|
39 | | modlt 12679 |
. . . . . . . . . . 11
|
40 | 33, 38, 39 | syl2anc 693 |
. . . . . . . . . 10
|
41 | | simpll1 1100 |
. . . . . . . . . . 11
|
42 | | simpll3 1102 |
. . . . . . . . . . . 12
|
43 | | simpll2 1101 |
. . . . . . . . . . . . 13
|
44 | | nnabscl 14065 |
. . . . . . . . . . . . 13
|
45 | 43, 37, 44 | syl2anc 693 |
. . . . . . . . . . . 12
|
46 | 42, 45 | zmodcld 12691 |
. . . . . . . . . . 11
|
47 | | nn0abscl 14052 |
. . . . . . . . . . . . 13
|
48 | 47 | 3ad2ant2 1083 |
. . . . . . . . . . . 12
|
49 | 48 | ad2antrr 762 |
. . . . . . . . . . 11
|
50 | | ltrmynn0 37515 |
. . . . . . . . . . 11
Yrm Yrm |
51 | 41, 46, 49, 50 | syl3anc 1326 |
. . . . . . . . . 10
Yrm Yrm |
52 | 40, 51 | mpbid 222 |
. . . . . . . . 9
Yrm Yrm |
53 | 46 | nn0zd 11480 |
. . . . . . . . . . 11
|
54 | | rmyabs 37525 |
. . . . . . . . . . 11
Yrm Yrm |
55 | 41, 53, 54 | syl2anc 693 |
. . . . . . . . . 10
Yrm
Yrm |
56 | 33, 38 | modcld 12674 |
. . . . . . . . . . . 12
|
57 | | modge0 12678 |
. . . . . . . . . . . . 13
|
58 | 33, 38, 57 | syl2anc 693 |
. . . . . . . . . . . 12
|
59 | 56, 58 | absidd 14161 |
. . . . . . . . . . 11
|
60 | 59 | oveq2d 6666 |
. . . . . . . . . 10
Yrm Yrm |
61 | 55, 60 | eqtrd 2656 |
. . . . . . . . 9
Yrm
Yrm |
62 | | rmyabs 37525 |
. . . . . . . . . 10
Yrm Yrm |
63 | 41, 43, 62 | syl2anc 693 |
. . . . . . . . 9
Yrm Yrm |
64 | 52, 61, 63 | 3brtr4d 4685 |
. . . . . . . 8
Yrm Yrm |
65 | 5 | fovcl 6765 |
. . . . . . . . . . . 12
Yrm |
66 | 41, 53, 65 | syl2anc 693 |
. . . . . . . . . . 11
Yrm |
67 | | nn0abscl 14052 |
. . . . . . . . . . 11
Yrm Yrm |
68 | 66, 67 | syl 17 |
. . . . . . . . . 10
Yrm |
69 | 68 | nn0red 11352 |
. . . . . . . . 9
Yrm |
70 | 22 | ad2antrr 762 |
. . . . . . . . . . 11
Yrm |
71 | | nn0abscl 14052 |
. . . . . . . . . . 11
Yrm Yrm |
72 | 70, 71 | syl 17 |
. . . . . . . . . 10
Yrm |
73 | 72 | nn0red 11352 |
. . . . . . . . 9
Yrm |
74 | 69, 73 | ltnled 10184 |
. . . . . . . 8
Yrm Yrm
Yrm
Yrm |
75 | 64, 74 | mpbid 222 |
. . . . . . 7
Yrm
Yrm |
76 | | simpr 477 |
. . . . . . . . 9
|
77 | | rmyeq0 37520 |
. . . . . . . . . . 11
Yrm |
78 | 41, 53, 77 | syl2anc 693 |
. . . . . . . . . 10
Yrm |
79 | 78 | necon3bid 2838 |
. . . . . . . . 9
Yrm |
80 | 76, 79 | mpbid 222 |
. . . . . . . 8
Yrm |
81 | | dvdsleabs2 15034 |
. . . . . . . 8
Yrm Yrm Yrm Yrm Yrm Yrm Yrm |
82 | 70, 66, 80, 81 | syl3anc 1326 |
. . . . . . 7
Yrm Yrm
Yrm Yrm |
83 | 75, 82 | mtod 189 |
. . . . . 6
Yrm Yrm |
84 | 83 | ex 450 |
. . . . 5
Yrm
Yrm |
85 | 84 | necon4ad 2813 |
. . . 4
Yrm
Yrm |
86 | 30, 85 | impbid 202 |
. . 3
Yrm
Yrm |
87 | | simpl2 1065 |
. . . 4
|
88 | | simpl3 1066 |
. . . 4
|
89 | | simpr 477 |
. . . 4
|
90 | | dvdsabsmod0 37554 |
. . . 4
|
91 | 87, 88, 89, 90 | syl3anc 1326 |
. . 3
|
92 | | simpl1 1064 |
. . . . 5
|
93 | 32 | adantr 481 |
. . . . . . 7
|
94 | | zre 11381 |
. . . . . . . . 9
|
95 | 94 | 3ad2ant2 1083 |
. . . . . . . 8
|
96 | 95 | adantr 481 |
. . . . . . 7
|
97 | | modabsdifz 37553 |
. . . . . . 7
|
98 | 93, 96, 89, 97 | syl3anc 1326 |
. . . . . 6
|
99 | 98 | znegcld 11484 |
. . . . 5
|
100 | | jm2.19lem4 37559 |
. . . . 5
Yrm Yrm Yrm Yrm |
101 | 92, 87, 88, 99, 100 | syl121anc 1331 |
. . . 4
Yrm
Yrm
Yrm
Yrm
|
102 | 32 | recnd 10068 |
. . . . . . . . . . . 12
|
103 | 102 | adantr 481 |
. . . . . . . . . . 11
|
104 | 35 | adantr 481 |
. . . . . . . . . . . . . 14
|
105 | 104, 89 | absrpcld 14187 |
. . . . . . . . . . . . 13
|
106 | 93, 105 | modcld 12674 |
. . . . . . . . . . . 12
|
107 | 106 | recnd 10068 |
. . . . . . . . . . 11
|
108 | 103, 107 | subcld 10392 |
. . . . . . . . . 10
|
109 | 108, 104,
89 | divcld 10801 |
. . . . . . . . 9
|
110 | 109, 104 | mulneg1d 10483 |
. . . . . . . 8
|
111 | 110 | oveq2d 6666 |
. . . . . . 7
|
112 | 109, 104 | mulcld 10060 |
. . . . . . . 8
|
113 | 103, 112 | negsubd 10398 |
. . . . . . 7
|
114 | 108, 104,
89 | divcan1d 10802 |
. . . . . . . . 9
|
115 | 114 | oveq2d 6666 |
. . . . . . . 8
|
116 | 103, 107 | nncand 10397 |
. . . . . . . 8
|
117 | 115, 116 | eqtrd 2656 |
. . . . . . 7
|
118 | 111, 113,
117 | 3eqtrrd 2661 |
. . . . . 6
|
119 | 118 | oveq2d 6666 |
. . . . 5
Yrm Yrm
|
120 | 119 | breq2d 4665 |
. . . 4
Yrm
Yrm
Yrm
Yrm
|
121 | 101, 120 | bitr4d 271 |
. . 3
Yrm
Yrm
Yrm
Yrm |
122 | 86, 91, 121 | 3bitr4d 300 |
. 2
Yrm
Yrm |
123 | 20, 122 | pm2.61dane 2881 |
1
Yrm
Yrm |