Step | Hyp | Ref
| Expression |
1 | | 2z 11409 |
. . . . . . . . . 10
|
2 | | eluzelz 11697 |
. . . . . . . . . . 11
|
3 | 2 | adantr 481 |
. . . . . . . . . 10
|
4 | | zmulcl 11426 |
. . . . . . . . . 10
|
5 | 1, 3, 4 | sylancr 695 |
. . . . . . . . 9
|
6 | | nn0z 11400 |
. . . . . . . . . 10
|
7 | 6 | adantl 482 |
. . . . . . . . 9
|
8 | 5, 7 | zmulcld 11488 |
. . . . . . . 8
|
9 | | zsqcl 12934 |
. . . . . . . . 9
|
10 | 7, 9 | syl 17 |
. . . . . . . 8
|
11 | 8, 10 | zsubcld 11487 |
. . . . . . 7
|
12 | | peano2zm 11420 |
. . . . . . 7
|
13 | 11, 12 | syl 17 |
. . . . . 6
|
14 | | dvds0 14997 |
. . . . . 6
|
15 | 13, 14 | syl 17 |
. . . . 5
|
16 | | rmx0 37490 |
. . . . . . . . . 10
Xrm |
17 | 16 | adantr 481 |
. . . . . . . . 9
Xrm |
18 | | rmy0 37494 |
. . . . . . . . . . . 12
Yrm |
19 | 18 | adantr 481 |
. . . . . . . . . . 11
Yrm |
20 | 19 | oveq2d 6666 |
. . . . . . . . . 10
Yrm |
21 | 3, 7 | zsubcld 11487 |
. . . . . . . . . . . 12
|
22 | 21 | zcnd 11483 |
. . . . . . . . . . 11
|
23 | 22 | mul01d 10235 |
. . . . . . . . . 10
|
24 | 20, 23 | eqtrd 2656 |
. . . . . . . . 9
Yrm |
25 | 17, 24 | oveq12d 6668 |
. . . . . . . 8
Xrm Yrm |
26 | | 1m0e1 11131 |
. . . . . . . 8
|
27 | 25, 26 | syl6eq 2672 |
. . . . . . 7
Xrm Yrm |
28 | | nn0cn 11302 |
. . . . . . . . 9
|
29 | 28 | adantl 482 |
. . . . . . . 8
|
30 | 29 | exp0d 13002 |
. . . . . . 7
|
31 | 27, 30 | oveq12d 6668 |
. . . . . 6
Xrm
Yrm |
32 | | 1m1e0 11089 |
. . . . . 6
|
33 | 31, 32 | syl6eq 2672 |
. . . . 5
Xrm
Yrm |
34 | 15, 33 | breqtrrd 4681 |
. . . 4
Xrm Yrm |
35 | | rmx1 37491 |
. . . . . . . . . 10
Xrm |
36 | 35 | adantr 481 |
. . . . . . . . 9
Xrm |
37 | | rmy1 37495 |
. . . . . . . . . . . 12
Yrm |
38 | 37 | adantr 481 |
. . . . . . . . . . 11
Yrm |
39 | 38 | oveq2d 6666 |
. . . . . . . . . 10
Yrm |
40 | 22 | mulid1d 10057 |
. . . . . . . . . 10
|
41 | 39, 40 | eqtrd 2656 |
. . . . . . . . 9
Yrm |
42 | 36, 41 | oveq12d 6668 |
. . . . . . . 8
Xrm Yrm
|
43 | 3 | zcnd 11483 |
. . . . . . . . 9
|
44 | 43, 29 | nncand 10397 |
. . . . . . . 8
|
45 | 42, 44 | eqtrd 2656 |
. . . . . . 7
Xrm Yrm |
46 | 29 | exp1d 13003 |
. . . . . . 7
|
47 | 45, 46 | oveq12d 6668 |
. . . . . 6
Xrm
Yrm |
48 | 29 | subidd 10380 |
. . . . . 6
|
49 | 47, 48 | eqtrd 2656 |
. . . . 5
Xrm
Yrm |
50 | 15, 49 | breqtrrd 4681 |
. . . 4
Xrm Yrm |
51 | | pm3.43 906 |
. . . . 5
Xrm
Yrm Xrm Yrm
Xrm
Yrm Xrm
Yrm |
52 | 13 | adantr 481 |
. . . . . . . . . . . 12
|
53 | 5 | adantr 481 |
. . . . . . . . . . . . . 14
|
54 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
|
55 | | nnz 11399 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
57 | | frmx 37478 |
. . . . . . . . . . . . . . . . . 18
Xrm
|
58 | 57 | fovcl 6765 |
. . . . . . . . . . . . . . . . 17
Xrm |
59 | 54, 56, 58 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
Xrm |
60 | 59 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
Xrm |
61 | 21 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
62 | | frmy 37479 |
. . . . . . . . . . . . . . . . . 18
Yrm
|
63 | 62 | fovcl 6765 |
. . . . . . . . . . . . . . . . 17
Yrm |
64 | 54, 56, 63 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
Yrm |
65 | 61, 64 | zmulcld 11488 |
. . . . . . . . . . . . . . 15
Yrm |
66 | 60, 65 | zsubcld 11487 |
. . . . . . . . . . . . . 14
Xrm
Yrm |
67 | 53, 66 | zmulcld 11488 |
. . . . . . . . . . . . 13
Xrm Yrm |
68 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . 17
|
69 | 56, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
|
70 | 57 | fovcl 6765 |
. . . . . . . . . . . . . . . 16
Xrm |
71 | 54, 69, 70 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Xrm |
72 | 71 | nn0zd 11480 |
. . . . . . . . . . . . . 14
Xrm |
73 | 62 | fovcl 6765 |
. . . . . . . . . . . . . . . 16
Yrm |
74 | 54, 69, 73 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Yrm |
75 | 61, 74 | zmulcld 11488 |
. . . . . . . . . . . . . 14
Yrm |
76 | 72, 75 | zsubcld 11487 |
. . . . . . . . . . . . 13
Xrm
Yrm |
77 | 67, 76 | zsubcld 11487 |
. . . . . . . . . . . 12
Xrm
Yrm
Xrm Yrm |
78 | 52, 77 | jca 554 |
. . . . . . . . . . 11
Xrm
Yrm
Xrm Yrm |
79 | 78 | adantr 481 |
. . . . . . . . . 10
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Yrm |
80 | 7 | adantr 481 |
. . . . . . . . . . . . . . 15
|
81 | | nnnn0 11299 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | adantl 482 |
. . . . . . . . . . . . . . 15
|
83 | | zexpcl 12875 |
. . . . . . . . . . . . . . 15
|
84 | 80, 82, 83 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
85 | 53, 84 | zmulcld 11488 |
. . . . . . . . . . . . 13
|
86 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . 15
|
87 | 86 | adantl 482 |
. . . . . . . . . . . . . 14
|
88 | | zexpcl 12875 |
. . . . . . . . . . . . . 14
|
89 | 80, 87, 88 | syl2anc 693 |
. . . . . . . . . . . . 13
|
90 | 85, 89 | zsubcld 11487 |
. . . . . . . . . . . 12
|
91 | | 0z 11388 |
. . . . . . . . . . . . . . 15
|
92 | | zaddcl 11417 |
. . . . . . . . . . . . . . 15
|
93 | 91, 10, 92 | sylancr 695 |
. . . . . . . . . . . . . 14
|
94 | 93 | adantr 481 |
. . . . . . . . . . . . 13
|
95 | 89, 94 | zmulcld 11488 |
. . . . . . . . . . . 12
|
96 | 90, 95 | jca 554 |
. . . . . . . . . . 11
|
97 | 96 | adantr 481 |
. . . . . . . . . 10
Xrm Yrm Xrm
Yrm |
98 | 52, 67, 85 | 3jca 1242 |
. . . . . . . . . . . 12
Xrm Yrm |
99 | 98 | adantr 481 |
. . . . . . . . . . 11
Xrm Yrm Xrm
Yrm Xrm Yrm |
100 | 76, 89 | jca 554 |
. . . . . . . . . . . 12
Xrm Yrm |
101 | 100 | adantr 481 |
. . . . . . . . . . 11
Xrm Yrm Xrm
Yrm Xrm
Yrm |
102 | 13, 5, 5 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
103 | 102 | ad2antrr 762 |
. . . . . . . . . . . . 13
Xrm
Yrm
|
104 | 66, 84 | jca 554 |
. . . . . . . . . . . . . 14
Xrm Yrm |
105 | 104 | adantr 481 |
. . . . . . . . . . . . 13
Xrm
Yrm
Xrm Yrm |
106 | | congid 37538 |
. . . . . . . . . . . . . . 15
|
107 | 13, 5, 106 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
108 | 107 | ad2antrr 762 |
. . . . . . . . . . . . 13
Xrm
Yrm
|
109 | | simpr 477 |
. . . . . . . . . . . . 13
Xrm
Yrm
Xrm Yrm |
110 | | congmul 37534 |
. . . . . . . . . . . . 13
Xrm Yrm Xrm Yrm Xrm
Yrm |
111 | 103, 105,
108, 109, 110 | syl112anc 1330 |
. . . . . . . . . . . 12
Xrm
Yrm
Xrm
Yrm |
112 | 111 | adantrl 752 |
. . . . . . . . . . 11
Xrm Yrm Xrm
Yrm Xrm
Yrm |
113 | | simprl 794 |
. . . . . . . . . . 11
Xrm Yrm Xrm
Yrm Xrm Yrm |
114 | | congsub 37537 |
. . . . . . . . . . 11
Xrm Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm |
115 | 99, 101, 112, 113, 114 | syl112anc 1330 |
. . . . . . . . . 10
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm |
116 | 13, 10 | zaddcld 11486 |
. . . . . . . . . . . . . 14
|
117 | 116 | adantr 481 |
. . . . . . . . . . . . 13
|
118 | | congid 37538 |
. . . . . . . . . . . . . 14
|
119 | 52, 89, 118 | syl2anc 693 |
. . . . . . . . . . . . 13
|
120 | | 0zd 11389 |
. . . . . . . . . . . . . . 15
|
121 | | iddvds 14995 |
. . . . . . . . . . . . . . . . 17
|
122 | 13, 121 | syl 17 |
. . . . . . . . . . . . . . . 16
|
123 | 13 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
|
124 | 123 | subid1d 10381 |
. . . . . . . . . . . . . . . 16
|
125 | 122, 124 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
|
126 | | congid 37538 |
. . . . . . . . . . . . . . . 16
|
127 | 13, 10, 126 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
128 | | congadd 37533 |
. . . . . . . . . . . . . . 15
|
129 | 13, 13, 120, 10, 10, 125, 127, 128 | syl322anc 1354 |
. . . . . . . . . . . . . 14
|
130 | 129 | adantr 481 |
. . . . . . . . . . . . 13
|
131 | | congmul 37534 |
. . . . . . . . . . . . 13
|
132 | 52, 89, 89, 117, 94, 119, 130, 131 | syl322anc 1354 |
. . . . . . . . . . . 12
|
133 | 11 | zcnd 11483 |
. . . . . . . . . . . . . . . . . 18
|
134 | 29 | sqcld 13006 |
. . . . . . . . . . . . . . . . . 18
|
135 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . 18
|
136 | 133, 134,
135 | addsubd 10413 |
. . . . . . . . . . . . . . . . 17
|
137 | 8 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
|
138 | 137, 134 | npcand 10396 |
. . . . . . . . . . . . . . . . . 18
|
139 | 138 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
140 | 136, 139 | eqtr3d 2658 |
. . . . . . . . . . . . . . . 16
|
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . 15
|
142 | 141 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
143 | 28 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
|
144 | 143, 87 | expcld 13008 |
. . . . . . . . . . . . . . 15
|
145 | 137 | adantr 481 |
. . . . . . . . . . . . . . 15
|
146 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
|
147 | 144, 145,
146 | subdid 10486 |
. . . . . . . . . . . . . 14
|
148 | 5 | zcnd 11483 |
. . . . . . . . . . . . . . . . . 18
|
149 | 148 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
150 | 144, 149,
143 | mul12d 10245 |
. . . . . . . . . . . . . . . 16
|
151 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
152 | | expm1t 12888 |
. . . . . . . . . . . . . . . . . 18
|
153 | 143, 151,
152 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
154 | 153 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
155 | 150, 154 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
|
156 | 144 | mulid1d 10057 |
. . . . . . . . . . . . . . 15
|
157 | 155, 156 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
158 | 142, 147,
157 | 3eqtrrd 2661 |
. . . . . . . . . . . . 13
|
159 | 158 | oveq1d 6665 |
. . . . . . . . . . . 12
|
160 | 132, 159 | breqtrrd 4681 |
. . . . . . . . . . 11
|
161 | 160 | adantr 481 |
. . . . . . . . . 10
Xrm Yrm Xrm
Yrm |
162 | | congtr 37532 |
. . . . . . . . . 10
Xrm
Yrm
Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm
Yrm |
163 | 79, 97, 115, 161, 162 | syl112anc 1330 |
. . . . . . . . 9
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm |
164 | | rmxluc 37501 |
. . . . . . . . . . . . . 14
Xrm Xrm
Xrm |
165 | 54, 56, 164 | syl2anc 693 |
. . . . . . . . . . . . 13
Xrm
Xrm Xrm |
166 | | rmyluc 37502 |
. . . . . . . . . . . . . . . 16
Yrm
Yrm
Yrm |
167 | 54, 56, 166 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Yrm Yrm Yrm |
168 | 167 | oveq2d 6666 |
. . . . . . . . . . . . . 14
Yrm
Yrm
Yrm |
169 | 2 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
|
170 | 169 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
171 | 170, 143 | subcld 10392 |
. . . . . . . . . . . . . . 15
|
172 | | 2cn 11091 |
. . . . . . . . . . . . . . . 16
|
173 | 63 | zcnd 11483 |
. . . . . . . . . . . . . . . . . 18
Yrm |
174 | 54, 56, 173 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
Yrm |
175 | 174, 170 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
Yrm |
176 | | mulcl 10020 |
. . . . . . . . . . . . . . . 16
Yrm Yrm |
177 | 172, 175,
176 | sylancr 695 |
. . . . . . . . . . . . . . 15
Yrm |
178 | 73 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
Yrm |
179 | 54, 69, 178 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Yrm |
180 | 171, 177,
179 | subdid 10486 |
. . . . . . . . . . . . . 14
Yrm
Yrm Yrm Yrm |
181 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . 19
|
182 | 181, 174,
170 | mul12d 10245 |
. . . . . . . . . . . . . . . . . 18
Yrm Yrm |
183 | 174, 149 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . 18
Yrm Yrm |
184 | 182, 183 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
Yrm Yrm |
185 | 184 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
Yrm Yrm |
186 | 171, 149,
174 | mul12d 10245 |
. . . . . . . . . . . . . . . 16
Yrm Yrm |
187 | 185, 186 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
Yrm Yrm |
188 | 187 | oveq1d 6665 |
. . . . . . . . . . . . . 14
Yrm
Yrm Yrm Yrm |
189 | 168, 180,
188 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
Yrm Yrm
Yrm |
190 | 165, 189 | oveq12d 6668 |
. . . . . . . . . . . 12
Xrm
Yrm Xrm
Xrm
Yrm Yrm |
191 | 58 | nn0cnd 11353 |
. . . . . . . . . . . . . . 15
Xrm |
192 | 54, 56, 191 | syl2anc 693 |
. . . . . . . . . . . . . 14
Xrm |
193 | 149, 192 | mulcld 10060 |
. . . . . . . . . . . . 13
Xrm |
194 | 70 | nn0cnd 11353 |
. . . . . . . . . . . . . 14
Xrm |
195 | 54, 69, 194 | syl2anc 693 |
. . . . . . . . . . . . 13
Xrm |
196 | 171, 174 | mulcld 10060 |
. . . . . . . . . . . . . 14
Yrm |
197 | 149, 196 | mulcld 10060 |
. . . . . . . . . . . . 13
Yrm |
198 | 171, 179 | mulcld 10060 |
. . . . . . . . . . . . 13
Yrm |
199 | 193, 195,
197, 198 | sub4d 10441 |
. . . . . . . . . . . 12
Xrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm |
200 | 149, 192,
196 | subdid 10486 |
. . . . . . . . . . . . . 14
Xrm Yrm Xrm Yrm |
201 | 200 | eqcomd 2628 |
. . . . . . . . . . . . 13
Xrm Yrm Xrm Yrm |
202 | 201 | oveq1d 6665 |
. . . . . . . . . . . 12
Xrm
Yrm
Xrm Yrm Xrm Yrm Xrm Yrm |
203 | 190, 199,
202 | 3eqtrd 2660 |
. . . . . . . . . . 11
Xrm
Yrm Xrm Yrm Xrm Yrm |
204 | 143, 82 | expp1d 13009 |
. . . . . . . . . . . 12
|
205 | | nncn 11028 |
. . . . . . . . . . . . . . . . 17
|
206 | 205 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
207 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . 16
|
208 | | npcan 10290 |
. . . . . . . . . . . . . . . 16
|
209 | 206, 207,
208 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
210 | 209 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
211 | 143, 87 | expp1d 13009 |
. . . . . . . . . . . . . 14
|
212 | 210, 211 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
213 | 212 | oveq1d 6665 |
. . . . . . . . . . . 12
|
214 | 144, 143,
143 | mulassd 10063 |
. . . . . . . . . . . . 13
|
215 | 134 | addid2d 10237 |
. . . . . . . . . . . . . . . 16
|
216 | 29 | sqvald 13005 |
. . . . . . . . . . . . . . . 16
|
217 | 215, 216 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
|
218 | 217 | adantr 481 |
. . . . . . . . . . . . . 14
|
219 | 218 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
220 | 214, 219 | eqtrd 2656 |
. . . . . . . . . . . 12
|
221 | 204, 213,
220 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
222 | 203, 221 | oveq12d 6668 |
. . . . . . . . . 10
Xrm Yrm Xrm Yrm Xrm Yrm |
223 | 222 | adantr 481 |
. . . . . . . . 9
Xrm Yrm Xrm
Yrm Xrm
Yrm Xrm Yrm Xrm Yrm |
224 | 163, 223 | breqtrrd 4681 |
. . . . . . . 8
Xrm Yrm Xrm
Yrm Xrm Yrm |
225 | 224 | ex 450 |
. . . . . . 7
Xrm Yrm Xrm
Yrm
Xrm Yrm |
226 | 225 | expcom 451 |
. . . . . 6
Xrm Yrm Xrm
Yrm
Xrm Yrm |
227 | 226 | a2d 29 |
. . . . 5
Xrm Yrm Xrm
Yrm
Xrm Yrm |
228 | 51, 227 | syl5 34 |
. . . 4
Xrm Yrm Xrm Yrm
Xrm Yrm |
229 | | oveq2 6658 |
. . . . . . . 8
Xrm Xrm |
230 | | oveq2 6658 |
. . . . . . . . 9
Yrm Yrm |
231 | 230 | oveq2d 6666 |
. . . . . . . 8
Yrm Yrm |
232 | 229, 231 | oveq12d 6668 |
. . . . . . 7
Xrm Yrm Xrm Yrm |
233 | | oveq2 6658 |
. . . . . . 7
|
234 | 232, 233 | oveq12d 6668 |
. . . . . 6
Xrm
Yrm Xrm Yrm |
235 | 234 | breq2d 4665 |
. . . . 5
Xrm Yrm Xrm
Yrm |
236 | 235 | imbi2d 330 |
. . . 4
Xrm
Yrm
Xrm Yrm |
237 | | oveq2 6658 |
. . . . . . . 8
Xrm Xrm |
238 | | oveq2 6658 |
. . . . . . . . 9
Yrm Yrm |
239 | 238 | oveq2d 6666 |
. . . . . . . 8
Yrm Yrm |
240 | 237, 239 | oveq12d 6668 |
. . . . . . 7
Xrm Yrm Xrm Yrm |
241 | | oveq2 6658 |
. . . . . . 7
|
242 | 240, 241 | oveq12d 6668 |
. . . . . 6
Xrm
Yrm Xrm Yrm |
243 | 242 | breq2d 4665 |
. . . . 5
Xrm Yrm Xrm
Yrm |
244 | 243 | imbi2d 330 |
. . . 4
Xrm
Yrm
Xrm Yrm |
245 | | oveq2 6658 |
. . . . . . . 8
Xrm Xrm |
246 | | oveq2 6658 |
. . . . . . . . 9
Yrm Yrm |
247 | 246 | oveq2d 6666 |
. . . . . . . 8
Yrm Yrm |
248 | 245, 247 | oveq12d 6668 |
. . . . . . 7
Xrm Yrm Xrm Yrm |
249 | | oveq2 6658 |
. . . . . . 7
|
250 | 248, 249 | oveq12d 6668 |
. . . . . 6
Xrm
Yrm Xrm Yrm |
251 | 250 | breq2d 4665 |
. . . . 5
Xrm Yrm Xrm
Yrm |
252 | 251 | imbi2d 330 |
. . . 4
Xrm
Yrm
Xrm Yrm |
253 | | oveq2 6658 |
. . . . . . . 8
Xrm Xrm |
254 | | oveq2 6658 |
. . . . . . . . 9
Yrm Yrm |
255 | 254 | oveq2d 6666 |
. . . . . . . 8
Yrm Yrm |
256 | 253, 255 | oveq12d 6668 |
. . . . . . 7
Xrm Yrm Xrm Yrm |
257 | | oveq2 6658 |
. . . . . . 7
|
258 | 256, 257 | oveq12d 6668 |
. . . . . 6
Xrm
Yrm Xrm Yrm |
259 | 258 | breq2d 4665 |
. . . . 5
Xrm Yrm Xrm
Yrm |
260 | 259 | imbi2d 330 |
. . . 4
Xrm
Yrm
Xrm Yrm |
261 | | oveq2 6658 |
. . . . . . . 8
Xrm Xrm |
262 | | oveq2 6658 |
. . . . . . . . 9
Yrm Yrm |
263 | 262 | oveq2d 6666 |
. . . . . . . 8
Yrm Yrm |
264 | 261, 263 | oveq12d 6668 |
. . . . . . 7
Xrm Yrm Xrm Yrm |
265 | | oveq2 6658 |
. . . . . . 7
|
266 | 264, 265 | oveq12d 6668 |
. . . . . 6
Xrm
Yrm Xrm Yrm |
267 | 266 | breq2d 4665 |
. . . . 5
Xrm Yrm Xrm
Yrm |
268 | 267 | imbi2d 330 |
. . . 4
Xrm
Yrm
Xrm Yrm |
269 | | oveq2 6658 |
. . . . . . . 8
Xrm Xrm |
270 | | oveq2 6658 |
. . . . . . . . 9
Yrm Yrm |
271 | 270 | oveq2d 6666 |
. . . . . . . 8
Yrm Yrm |
272 | 269, 271 | oveq12d 6668 |
. . . . . . 7
Xrm Yrm Xrm Yrm |
273 | | oveq2 6658 |
. . . . . . 7
|
274 | 272, 273 | oveq12d 6668 |
. . . . . 6
Xrm
Yrm Xrm Yrm |
275 | 274 | breq2d 4665 |
. . . . 5
Xrm Yrm Xrm
Yrm |
276 | 275 | imbi2d 330 |
. . . 4
Xrm
Yrm
Xrm Yrm |
277 | 34, 50, 228, 236, 244, 252, 260, 268, 276 | 2nn0ind 37510 |
. . 3
Xrm Yrm |
278 | 277 | impcom 446 |
. 2
Xrm Yrm |
279 | 278 | 3impa 1259 |
1
Xrm Yrm |