Step | Hyp | Ref
| Expression |
1 | | simprl 794 |
. . . . . . . . 9
|
2 | | simprrr 805 |
. . . . . . . . 9
|
3 | | frmx 37478 |
. . . . . . . . . . 11
Xrm
|
4 | 3 | fovcl 6765 |
. . . . . . . . . 10
Xrm |
5 | 4 | nn0zd 11480 |
. . . . . . . . 9
Xrm |
6 | 1, 2, 5 | syl2anc 693 |
. . . . . . . 8
Xrm |
7 | | simprrl 804 |
. . . . . . . . 9
|
8 | | frmy 37479 |
. . . . . . . . . 10
Yrm
|
9 | 8 | fovcl 6765 |
. . . . . . . . 9
Yrm |
10 | 1, 7, 9 | syl2anc 693 |
. . . . . . . 8
Yrm |
11 | | congid 37538 |
. . . . . . . 8
Xrm Yrm Xrm Yrm Yrm |
12 | 6, 10, 11 | syl2anc 693 |
. . . . . . 7
Xrm
Yrm
Yrm |
13 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
|
14 | | zcn 11382 |
. . . . . . . . . . . . . . 15
|
15 | 13, 14 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
16 | 15 | mul02d 10234 |
. . . . . . . . . . . . 13
|
17 | 16 | adantl 482 |
. . . . . . . . . . . 12
|
18 | 17 | oveq2d 6666 |
. . . . . . . . . . 11
|
19 | | zcn 11382 |
. . . . . . . . . . . . 13
|
20 | 19 | addid1d 10236 |
. . . . . . . . . . . 12
|
21 | 20 | adantr 481 |
. . . . . . . . . . 11
|
22 | 18, 21 | eqtrd 2656 |
. . . . . . . . . 10
|
23 | 22 | ad2antll 765 |
. . . . . . . . 9
|
24 | 23 | oveq2d 6666 |
. . . . . . . 8
Yrm Yrm |
25 | 24 | oveq1d 6665 |
. . . . . . 7
Yrm
Yrm Yrm Yrm |
26 | 12, 25 | breqtrrd 4681 |
. . . . . 6
Xrm
Yrm
Yrm |
27 | 26 | orcd 407 |
. . . . 5
Xrm Yrm Yrm Xrm Yrm Yrm |
28 | 27 | ex 450 |
. . . 4
Xrm
Yrm
Yrm Xrm Yrm Yrm |
29 | | simprl 794 |
. . . . . . . 8
|
30 | | simprrr 805 |
. . . . . . . 8
|
31 | 29, 30, 5 | syl2anc 693 |
. . . . . . 7
Xrm |
32 | | simprrl 804 |
. . . . . . . 8
|
33 | 29, 32, 9 | syl2anc 693 |
. . . . . . 7
Yrm |
34 | | simpl 473 |
. . . . . . . . . . 11
|
35 | 34 | peano2zd 11485 |
. . . . . . . . . 10
|
36 | | eluzel2 11692 |
. . . . . . . . . . . 12
|
37 | 36 | ad2antrl 764 |
. . . . . . . . . . 11
|
38 | 37, 30 | zmulcld 11488 |
. . . . . . . . . 10
|
39 | 35, 38 | zmulcld 11488 |
. . . . . . . . 9
|
40 | 32, 39 | zaddcld 11486 |
. . . . . . . 8
|
41 | 8 | fovcl 6765 |
. . . . . . . 8
Yrm |
42 | 29, 40, 41 | syl2anc 693 |
. . . . . . 7
Yrm |
43 | 34, 38 | zmulcld 11488 |
. . . . . . . . 9
|
44 | 32, 43 | zaddcld 11486 |
. . . . . . . 8
|
45 | 8 | fovcl 6765 |
. . . . . . . 8
Yrm |
46 | 29, 44, 45 | syl2anc 693 |
. . . . . . 7
Yrm |
47 | 3 | fovcl 6765 |
. . . . . . . . . . . . . 14
Xrm |
48 | 47 | nn0zd 11480 |
. . . . . . . . . . . . 13
Xrm |
49 | 29, 38, 48 | syl2anc 693 |
. . . . . . . . . . . 12
Xrm |
50 | 46, 49 | zmulcld 11488 |
. . . . . . . . . . 11
Yrm
Xrm |
51 | 46 | znegcld 11484 |
. . . . . . . . . . 11
Yrm |
52 | 50, 51 | zsubcld 11487 |
. . . . . . . . . 10
Yrm Xrm Yrm |
53 | 3 | fovcl 6765 |
. . . . . . . . . . . . 13
Xrm |
54 | 53 | nn0zd 11480 |
. . . . . . . . . . . 12
Xrm |
55 | 29, 44, 54 | syl2anc 693 |
. . . . . . . . . . 11
Xrm |
56 | 8 | fovcl 6765 |
. . . . . . . . . . . 12
Yrm |
57 | 29, 38, 56 | syl2anc 693 |
. . . . . . . . . . 11
Yrm |
58 | 55, 57 | zmulcld 11488 |
. . . . . . . . . 10
Xrm
Yrm |
59 | 37, 31 | zmulcld 11488 |
. . . . . . . . . . . . . 14
Xrm |
60 | | dvdsmul2 15004 |
. . . . . . . . . . . . . 14
Xrm Xrm Xrm Xrm Xrm |
61 | 59, 31, 60 | syl2anc 693 |
. . . . . . . . . . . . 13
Xrm Xrm
Xrm |
62 | | rmxdbl 37504 |
. . . . . . . . . . . . . . . 16
Xrm
Xrm |
63 | 29, 30, 62 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Xrm
Xrm |
64 | 63 | oveq1d 6665 |
. . . . . . . . . . . . . 14
Xrm Xrm |
65 | | 2cnd 11093 |
. . . . . . . . . . . . . . . 16
|
66 | 29, 30, 4 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
Xrm |
67 | 66 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
Xrm |
68 | 67 | sqcld 13006 |
. . . . . . . . . . . . . . . 16
Xrm |
69 | 65, 68 | mulcld 10060 |
. . . . . . . . . . . . . . 15
Xrm |
70 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
|
71 | 69, 70 | npcand 10396 |
. . . . . . . . . . . . . 14
Xrm Xrm |
72 | 67 | sqvald 13005 |
. . . . . . . . . . . . . . . 16
Xrm
Xrm
Xrm |
73 | 72 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
Xrm Xrm Xrm |
74 | | mulass 10024 |
. . . . . . . . . . . . . . . . 17
Xrm Xrm Xrm Xrm Xrm Xrm |
75 | 74 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
Xrm Xrm Xrm Xrm Xrm
Xrm |
76 | 65, 67, 67, 75 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
Xrm Xrm Xrm Xrm |
77 | 73, 76 | eqtrd 2656 |
. . . . . . . . . . . . . 14
Xrm Xrm
Xrm |
78 | 64, 71, 77 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
Xrm Xrm
Xrm |
79 | 61, 78 | breqtrrd 4681 |
. . . . . . . . . . . 12
Xrm
Xrm |
80 | 49 | peano2zd 11485 |
. . . . . . . . . . . . 13
Xrm |
81 | | dvdsmultr2 15021 |
. . . . . . . . . . . . 13
Xrm Yrm Xrm
Xrm Xrm
Xrm Yrm Xrm |
82 | 31, 46, 80, 81 | syl3anc 1326 |
. . . . . . . . . . . 12
Xrm Xrm
Xrm Yrm Xrm |
83 | 79, 82 | mpd 15 |
. . . . . . . . . . 11
Xrm
Yrm Xrm |
84 | 46 | zcnd 11483 |
. . . . . . . . . . . . . 14
Yrm |
85 | 84 | mulid1d 10057 |
. . . . . . . . . . . . 13
Yrm Yrm |
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . 12
Yrm Xrm Yrm Yrm Xrm Yrm |
87 | 49 | zcnd 11483 |
. . . . . . . . . . . . 13
Xrm |
88 | 84, 87, 70 | adddid 10064 |
. . . . . . . . . . . 12
Yrm Xrm Yrm Xrm Yrm |
89 | 50 | zcnd 11483 |
. . . . . . . . . . . . 13
Yrm
Xrm |
90 | 89, 84 | subnegd 10399 |
. . . . . . . . . . . 12
Yrm Xrm Yrm Yrm Xrm Yrm |
91 | 86, 88, 90 | 3eqtr4d 2666 |
. . . . . . . . . . 11
Yrm Xrm Yrm Xrm
Yrm |
92 | 83, 91 | breqtrd 4679 |
. . . . . . . . . 10
Xrm Yrm Xrm Yrm |
93 | 8 | fovcl 6765 |
. . . . . . . . . . . . . . 15
Yrm |
94 | 29, 30, 93 | syl2anc 693 |
. . . . . . . . . . . . . 14
Yrm |
95 | 37, 94 | zmulcld 11488 |
. . . . . . . . . . . . 13
Yrm |
96 | | dvdsmul2 15004 |
. . . . . . . . . . . . 13
Yrm Xrm Xrm Yrm Xrm |
97 | 95, 31, 96 | syl2anc 693 |
. . . . . . . . . . . 12
Xrm Yrm
Xrm |
98 | | rmydbl 37505 |
. . . . . . . . . . . . . 14
Yrm Xrm
Yrm |
99 | 29, 30, 98 | syl2anc 693 |
. . . . . . . . . . . . 13
Yrm Xrm
Yrm |
100 | 94 | zcnd 11483 |
. . . . . . . . . . . . . 14
Yrm |
101 | 65, 67, 100 | mul32d 10246 |
. . . . . . . . . . . . 13
Xrm
Yrm Yrm Xrm |
102 | 99, 101 | eqtrd 2656 |
. . . . . . . . . . . 12
Yrm Yrm
Xrm |
103 | 97, 102 | breqtrrd 4681 |
. . . . . . . . . . 11
Xrm Yrm |
104 | | dvdsmultr2 15021 |
. . . . . . . . . . . 12
Xrm Xrm
Yrm
Xrm
Yrm
Xrm Xrm Yrm |
105 | 31, 55, 57, 104 | syl3anc 1326 |
. . . . . . . . . . 11
Xrm
Yrm
Xrm Xrm Yrm |
106 | 103, 105 | mpd 15 |
. . . . . . . . . 10
Xrm
Xrm
Yrm |
107 | | dvds2add 15015 |
. . . . . . . . . . 11
Xrm
Yrm
Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm |
108 | 107 | imp 445 |
. . . . . . . . . 10
Xrm Yrm Xrm Yrm Xrm Yrm
Xrm Yrm Xrm Yrm
Xrm Xrm Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm |
109 | 31, 52, 58, 92, 106, 108 | syl32anc 1334 |
. . . . . . . . 9
Xrm Yrm Xrm Yrm Xrm Yrm |
110 | 34 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
111 | 38 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
112 | 110, 70, 111 | adddird 10065 |
. . . . . . . . . . . . . . 15
|
113 | 112 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
114 | 32 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
115 | 43 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
116 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . 17
|
117 | 116, 38 | zmulcld 11488 |
. . . . . . . . . . . . . . . 16
|
118 | 117 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
119 | 114, 115,
118 | addassd 10062 |
. . . . . . . . . . . . . 14
|
120 | 111 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
|
121 | 120 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
122 | 113, 119,
121 | 3eqtr2d 2662 |
. . . . . . . . . . . . 13
|
123 | 122 | oveq2d 6666 |
. . . . . . . . . . . 12
Yrm Yrm |
124 | | rmyadd 37496 |
. . . . . . . . . . . . 13
Yrm Yrm Xrm Xrm Yrm |
125 | 29, 44, 38, 124 | syl3anc 1326 |
. . . . . . . . . . . 12
Yrm Yrm Xrm Xrm Yrm |
126 | 123, 125 | eqtrd 2656 |
. . . . . . . . . . 11
Yrm Yrm Xrm Xrm Yrm |
127 | 126 | oveq1d 6665 |
. . . . . . . . . 10
Yrm
Yrm
Yrm
Xrm Xrm Yrm
Yrm |
128 | 58 | zcnd 11483 |
. . . . . . . . . . 11
Xrm
Yrm |
129 | 51 | zcnd 11483 |
. . . . . . . . . . 11
Yrm |
130 | 89, 128, 129 | addsubd 10413 |
. . . . . . . . . 10
Yrm Xrm
Xrm
Yrm Yrm Yrm Xrm
Yrm Xrm Yrm |
131 | 127, 130 | eqtrd 2656 |
. . . . . . . . 9
Yrm
Yrm
Yrm
Xrm Yrm Xrm Yrm |
132 | 109, 131 | breqtrrd 4681 |
. . . . . . . 8
Xrm
Yrm
Yrm |
133 | 132 | olcd 408 |
. . . . . . 7
Xrm Yrm Yrm Xrm Yrm Yrm |
134 | | jm2.25lem1 37565 |
. . . . . . 7
Xrm Yrm Yrm
Yrm
Xrm Yrm Yrm Xrm Yrm Yrm
Xrm Yrm Yrm Xrm Yrm Yrm Xrm Yrm Yrm Xrm
Yrm
Yrm |
135 | 31, 33, 42, 46, 133, 134 | syl221anc 1337 |
. . . . . 6
Xrm Yrm Yrm Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm |
136 | 135 | pm5.74da 723 |
. . . . 5
Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm Xrm
Yrm
Yrm |
137 | | oveq1 6657 |
. . . . . . . . . . 11
|
138 | 137 | oveq2d 6666 |
. . . . . . . . . 10
|
139 | 138 | oveq2d 6666 |
. . . . . . . . 9
Yrm Yrm |
140 | 139 | oveq1d 6665 |
. . . . . . . 8
Yrm
Yrm Yrm Yrm |
141 | 140 | breq2d 4665 |
. . . . . . 7
Xrm Yrm Yrm Xrm Yrm Yrm |
142 | 139 | oveq1d 6665 |
. . . . . . . 8
Yrm
Yrm Yrm Yrm |
143 | 142 | breq2d 4665 |
. . . . . . 7
Xrm Yrm Yrm Xrm Yrm Yrm |
144 | 141, 143 | orbi12d 746 |
. . . . . 6
Xrm Yrm Yrm Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm |
145 | 144 | imbi2d 330 |
. . . . 5
Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm Xrm
Yrm
Yrm |
146 | | oveq1 6657 |
. . . . . . . . . . 11
|
147 | 146 | oveq2d 6666 |
. . . . . . . . . 10
|
148 | 147 | oveq2d 6666 |
. . . . . . . . 9
Yrm Yrm |
149 | 148 | oveq1d 6665 |
. . . . . . . 8
Yrm
Yrm Yrm Yrm |
150 | 149 | breq2d 4665 |
. . . . . . 7
Xrm Yrm Yrm Xrm Yrm Yrm |
151 | 148 | oveq1d 6665 |
. . . . . . . 8
Yrm
Yrm Yrm Yrm |
152 | 151 | breq2d 4665 |
. . . . . . 7
Xrm Yrm Yrm Xrm Yrm Yrm |
153 | 150, 152 | orbi12d 746 |
. . . . . 6
Xrm Yrm Yrm Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm |
154 | 153 | imbi2d 330 |
. . . . 5
Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm Xrm
Yrm
Yrm |
155 | | oveq1 6657 |
. . . . . . . . . . 11
|
156 | 155 | oveq2d 6666 |
. . . . . . . . . 10
|
157 | 156 | oveq2d 6666 |
. . . . . . . . 9
Yrm Yrm |
158 | 157 | oveq1d 6665 |
. . . . . . . 8
Yrm
Yrm Yrm Yrm |
159 | 158 | breq2d 4665 |
. . . . . . 7
Xrm Yrm Yrm Xrm Yrm Yrm |
160 | 157 | oveq1d 6665 |
. . . . . . . 8
Yrm
Yrm Yrm Yrm |
161 | 160 | breq2d 4665 |
. . . . . . 7
Xrm Yrm Yrm Xrm Yrm Yrm |
162 | 159, 161 | orbi12d 746 |
. . . . . 6
Xrm Yrm Yrm Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm |
163 | 162 | imbi2d 330 |
. . . . 5
Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm Xrm
Yrm
Yrm |
164 | | oveq1 6657 |
. . . . . . . . . . 11
|
165 | 164 | oveq2d 6666 |
. . . . . . . . . 10
|
166 | 165 | oveq2d 6666 |
. . . . . . . . 9
Yrm Yrm |
167 | 166 | oveq1d 6665 |
. . . . . . . 8
Yrm
Yrm Yrm Yrm |
168 | 167 | breq2d 4665 |
. . . . . . 7
Xrm Yrm Yrm Xrm Yrm Yrm |
169 | 166 | oveq1d 6665 |
. . . . . . . 8
Yrm
Yrm Yrm Yrm |
170 | 169 | breq2d 4665 |
. . . . . . 7
Xrm Yrm Yrm Xrm Yrm Yrm |
171 | 168, 170 | orbi12d 746 |
. . . . . 6
Xrm Yrm Yrm Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm |
172 | 171 | imbi2d 330 |
. . . . 5
Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm Xrm
Yrm
Yrm |
173 | 136, 145,
154, 163, 172 | zindbi 37511 |
. . . 4
Xrm
Yrm
Yrm Xrm Yrm Yrm
Xrm Yrm Yrm Xrm
Yrm
Yrm |
174 | 28, 173 | mpbid 222 |
. . 3
Xrm
Yrm
Yrm Xrm Yrm Yrm |
175 | 174 | impcom 446 |
. 2
Xrm Yrm Yrm Xrm Yrm Yrm |
176 | 175 | 3impa 1259 |
1
Xrm Yrm Yrm Xrm Yrm Yrm |