Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . 5
|
2 | 1 | breq1d 4663 |
. . . 4
|
3 | 2 | rexbidv 3052 |
. . 3
|
4 | | nnssnn0 11295 |
. . . . 5
|
5 | | ply1divalg.r1 |
. . . . . . . . . 10
|
6 | 5 | adantr 481 |
. . . . . . . . 9
|
7 | | ply1divalg.f |
. . . . . . . . . 10
|
8 | 7 | adantr 481 |
. . . . . . . . 9
|
9 | | simpr 477 |
. . . . . . . . 9
|
10 | | ply1divalg.d |
. . . . . . . . . 10
deg1 |
11 | | ply1divalg.p |
. . . . . . . . . 10
Poly1 |
12 | | ply1divalg.z |
. . . . . . . . . 10
|
13 | | ply1divalg.b |
. . . . . . . . . 10
|
14 | 10, 11, 12, 13 | deg1nn0cl 23848 |
. . . . . . . . 9
|
15 | 6, 8, 9, 14 | syl3anc 1326 |
. . . . . . . 8
|
16 | 15 | nn0red 11352 |
. . . . . . 7
|
17 | | ply1divalg.g1 |
. . . . . . . . . 10
|
18 | | ply1divalg.g2 |
. . . . . . . . . 10
|
19 | 10, 11, 12, 13 | deg1nn0cl 23848 |
. . . . . . . . . 10
|
20 | 5, 17, 18, 19 | syl3anc 1326 |
. . . . . . . . 9
|
21 | 20 | nn0red 11352 |
. . . . . . . 8
|
22 | 21 | adantr 481 |
. . . . . . 7
|
23 | 16, 22 | resubcld 10458 |
. . . . . 6
|
24 | | arch 11289 |
. . . . . 6
|
25 | 23, 24 | syl 17 |
. . . . 5
|
26 | | ssrexv 3667 |
. . . . 5
|
27 | 4, 25, 26 | mpsyl 68 |
. . . 4
|
28 | 16 | adantr 481 |
. . . . . . 7
|
29 | 21 | ad2antrr 762 |
. . . . . . 7
|
30 | | nn0re 11301 |
. . . . . . . 8
|
31 | 30 | adantl 482 |
. . . . . . 7
|
32 | 28, 29, 31 | ltsubadd2d 10625 |
. . . . . 6
|
33 | 32 | biimpd 219 |
. . . . 5
|
34 | 33 | reximdva 3017 |
. . . 4
|
35 | 27, 34 | mpd 15 |
. . 3
|
36 | | 0nn0 11307 |
. . . 4
|
37 | 10, 11, 12 | deg1z 23847 |
. . . . . 6
|
38 | 5, 37 | syl 17 |
. . . . 5
|
39 | | 0re 10040 |
. . . . . . 7
|
40 | | readdcl 10019 |
. . . . . . 7
|
41 | 21, 39, 40 | sylancl 694 |
. . . . . 6
|
42 | | mnflt 11957 |
. . . . . 6
|
43 | 41, 42 | syl 17 |
. . . . 5
|
44 | 38, 43 | eqbrtrd 4675 |
. . . 4
|
45 | | oveq2 6658 |
. . . . . 6
|
46 | 45 | breq2d 4665 |
. . . . 5
|
47 | 46 | rspcev 3309 |
. . . 4
|
48 | 36, 44, 47 | sylancr 695 |
. . 3
|
49 | 3, 35, 48 | pm2.61ne 2879 |
. 2
|
50 | 7 | adantr 481 |
. . . 4
|
51 | | oveq2 6658 |
. . . . . . . . . 10
|
52 | 51 | breq2d 4665 |
. . . . . . . . 9
|
53 | 52 | imbi1d 331 |
. . . . . . . 8
|
54 | 53 | ralbidv 2986 |
. . . . . . 7
|
55 | 54 | imbi2d 330 |
. . . . . 6
|
56 | | oveq2 6658 |
. . . . . . . . . 10
|
57 | 56 | breq2d 4665 |
. . . . . . . . 9
|
58 | 57 | imbi1d 331 |
. . . . . . . 8
|
59 | 58 | ralbidv 2986 |
. . . . . . 7
|
60 | 59 | imbi2d 330 |
. . . . . 6
|
61 | | oveq2 6658 |
. . . . . . . . . 10
|
62 | 61 | breq2d 4665 |
. . . . . . . . 9
|
63 | 62 | imbi1d 331 |
. . . . . . . 8
|
64 | 63 | ralbidv 2986 |
. . . . . . 7
|
65 | 64 | imbi2d 330 |
. . . . . 6
|
66 | 11 | ply1ring 19618 |
. . . . . . . . . . . 12
|
67 | 5, 66 | syl 17 |
. . . . . . . . . . 11
|
68 | 13, 12 | ring0cl 18569 |
. . . . . . . . . . 11
|
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
|
70 | 69 | ad2antrr 762 |
. . . . . . . . 9
|
71 | | ply1divalg.t |
. . . . . . . . . . . . . . . . 17
|
72 | 13, 71, 12 | ringrz 18588 |
. . . . . . . . . . . . . . . 16
|
73 | 67, 17, 72 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
74 | 73 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
75 | 74 | adantr 481 |
. . . . . . . . . . . . 13
|
76 | | ringgrp 18552 |
. . . . . . . . . . . . . . 15
|
77 | 67, 76 | syl 17 |
. . . . . . . . . . . . . 14
|
78 | | ply1divalg.m |
. . . . . . . . . . . . . . 15
|
79 | 13, 12, 78 | grpsubid1 17500 |
. . . . . . . . . . . . . 14
|
80 | 77, 79 | sylan 488 |
. . . . . . . . . . . . 13
|
81 | 75, 80 | eqtr2d 2657 |
. . . . . . . . . . . 12
|
82 | 81 | fveq2d 6195 |
. . . . . . . . . . 11
|
83 | 20 | nn0cnd 11353 |
. . . . . . . . . . . . 13
|
84 | 83 | addid1d 10236 |
. . . . . . . . . . . 12
|
85 | 84 | adantr 481 |
. . . . . . . . . . 11
|
86 | 82, 85 | breq12d 4666 |
. . . . . . . . . 10
|
87 | 86 | biimpa 501 |
. . . . . . . . 9
|
88 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
89 | 88 | oveq2d 6666 |
. . . . . . . . . . . 12
|
90 | 89 | fveq2d 6195 |
. . . . . . . . . . 11
|
91 | 90 | breq1d 4663 |
. . . . . . . . . 10
|
92 | 91 | rspcev 3309 |
. . . . . . . . 9
|
93 | 70, 87, 92 | syl2anc 693 |
. . . . . . . 8
|
94 | 93 | ex 450 |
. . . . . . 7
|
95 | 94 | ralrimiva 2966 |
. . . . . 6
|
96 | | nn0addcl 11328 |
. . . . . . . . . . . . . . . . . 18
|
97 | 20, 96 | sylan 488 |
. . . . . . . . . . . . . . . . 17
|
98 | 97 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
99 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
100 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
101 | 10, 11, 13 | deg1cl 23843 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
103 | 20 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
104 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
105 | 104 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
|
106 | 103, 105 | nn0addcld 11355 |
. . . . . . . . . . . . . . . . . . . . 21
|
107 | 106 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | | degltlem1 23832 |
. . . . . . . . . . . . . . . . . . . 20
|
109 | 102, 107,
108 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
110 | 109 | biimpd 219 |
. . . . . . . . . . . . . . . . . 18
|
111 | 110 | impr 649 |
. . . . . . . . . . . . . . . . 17
|
112 | 20 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
113 | 112 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . 20
|
114 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . 22
|
115 | 114 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
116 | | peano2cn 10208 |
. . . . . . . . . . . . . . . . . . . . 21
|
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
118 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . 20
|
119 | 113, 117,
118 | addsubassd 10412 |
. . . . . . . . . . . . . . . . . . 19
|
120 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . 21
|
121 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . . 21
|
122 | 115, 120,
121 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
|
123 | 122 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
124 | 119, 123 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
125 | 124 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
126 | 111, 125 | breqtrd 4679 |
. . . . . . . . . . . . . . . 16
|
127 | 67 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
128 | 17 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
129 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
130 | | ply1divex.i |
. . . . . . . . . . . . . . . . . . . . 21
|
131 | 130 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
132 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 coe1 |
133 | | ply1divex.k |
. . . . . . . . . . . . . . . . . . . . . . 23
|
134 | 132, 13, 11, 133 | coe1f 19581 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 |
135 | 134 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 |
136 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
|
137 | 103, 136 | nn0addcld 11355 |
. . . . . . . . . . . . . . . . . . . . 21
|
138 | 135, 137 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
coe1 |
139 | | ply1divex.u |
. . . . . . . . . . . . . . . . . . . . 21
|
140 | 133, 139 | ringcl 18561 |
. . . . . . . . . . . . . . . . . . . 20
coe1
coe1 |
141 | 129, 131,
138, 140 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
coe1 |
142 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
var1 var1 |
143 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
|
144 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
mulGrp mulGrp |
145 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
.gmulGrp .gmulGrp |
146 | 133, 11, 142, 143, 144, 145, 13 | ply1tmcl 19642 |
. . . . . . . . . . . . . . . . . . 19
coe1
coe1 .gmulGrpvar1 |
147 | 129, 141,
136, 146 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1 |
148 | 13, 71 | ringcl 18561 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 |
149 | 127, 128,
147, 148 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
coe1 .gmulGrpvar1 |
150 | 149 | adantrr 753 |
. . . . . . . . . . . . . . . 16
coe1 .gmulGrpvar1 |
151 | 103 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . 19
|
152 | 151 | leidd 10594 |
. . . . . . . . . . . . . . . . . 18
|
153 | 10, 133, 11, 142, 143, 144, 145 | deg1tmle 23877 |
. . . . . . . . . . . . . . . . . . 19
coe1
coe1 .gmulGrpvar1
|
154 | 129, 141,
136, 153 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1 |
155 | 11, 10, 129, 13, 71, 128, 147, 103, 136, 152, 154 | deg1mulle2 23869 |
. . . . . . . . . . . . . . . . 17
coe1 .gmulGrpvar1 |
156 | 155 | adantrr 753 |
. . . . . . . . . . . . . . . 16
coe1 .gmulGrpvar1
|
157 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
coe1 coe1 .gmulGrpvar1 coe1 coe1 .gmulGrpvar1 |
158 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
159 | 158, 133,
11, 142, 143, 144, 145, 13, 71, 139, 128, 129, 141, 136, 103 | coe1tmmul2fv 19648 |
. . . . . . . . . . . . . . . . . 18
coe1 coe1 .gmulGrpvar1 coe1 coe1 |
160 | 103 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . 20
|
161 | 114 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
162 | 160, 161 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . 19
|
163 | 162 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
coe1 coe1 .gmulGrpvar1 coe1 coe1 .gmulGrpvar1 |
164 | | ply1divex.g3 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 |
165 | 164 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
coe1
coe1 coe1 |
166 | 165 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
coe1 coe1 coe1 |
167 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1 coe1 |
168 | 167, 13, 11, 133 | coe1f 19581 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 |
169 | 17, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 |
170 | 169 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 |
171 | 170, 103 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
coe1 |
172 | 133, 139 | ringass 18564 |
. . . . . . . . . . . . . . . . . . . 20
coe1
coe1 coe1 coe1 coe1
coe1 |
173 | 129, 171,
131, 138, 172 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . 19
coe1 coe1 coe1
coe1 |
174 | | ply1divex.o |
. . . . . . . . . . . . . . . . . . . . 21
|
175 | 133, 139,
174 | ringlidm 18571 |
. . . . . . . . . . . . . . . . . . . 20
coe1
coe1 coe1 |
176 | 129, 138,
175 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
coe1 coe1 |
177 | 166, 173,
176 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . . . . . 18
coe1 coe1 coe1 |
178 | 159, 163,
177 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . . . 17
coe1 coe1 coe1 .gmulGrpvar1 |
179 | 178 | adantrr 753 |
. . . . . . . . . . . . . . . 16
coe1 coe1 coe1 .gmulGrpvar1 |
180 | 10, 11, 13, 78, 98, 99, 100, 126, 150, 156, 132, 157, 179 | deg1sublt 23870 |
. . . . . . . . . . . . . . 15
coe1 .gmulGrpvar1 |
181 | 180 | adantlrr 757 |
. . . . . . . . . . . . . 14
coe1 .gmulGrpvar1 |
182 | 77 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
183 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
184 | 13, 78 | grpsubcl 17495 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 |
185 | 182, 183,
149, 184 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
coe1 .gmulGrpvar1 |
186 | 185 | adantrr 753 |
. . . . . . . . . . . . . . . 16
coe1 .gmulGrpvar1 |
187 | 186 | adantlrr 757 |
. . . . . . . . . . . . . . 15
coe1 .gmulGrpvar1 |
188 | | simplrr 801 |
. . . . . . . . . . . . . . 15
|
189 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
190 | 189 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
191 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
192 | 191 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
193 | 192 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
194 | 193 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
195 | 190, 194 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
196 | 195 | rspcva 3307 |
. . . . . . . . . . . . . . 15
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 |
197 | 187, 188,
196 | syl2anc 693 |
. . . . . . . . . . . . . 14
coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 |
198 | 181, 197 | mpd 15 |
. . . . . . . . . . . . 13
coe1 .gmulGrpvar1 |
199 | 67 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
|
200 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
201 | 147 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1 |
202 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
203 | 13, 202 | ringacl 18578 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 |
204 | 199, 200,
201, 203 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
coe1 .gmulGrpvar1 |
205 | 77 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
|
206 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
|
207 | 149 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 .gmulGrpvar1 |
208 | 17 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
209 | 13, 71 | ringcl 18561 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
210 | 199, 208,
200, 209 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
|
211 | 13, 202, 78 | grpsubsub4 17508 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 |
212 | 205, 206,
207, 210, 211 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 |
213 | 13, 202, 71 | ringdi 18566 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
214 | 199, 208,
200, 201, 213 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
215 | 214 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
216 | 212, 215 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . 20
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
217 | 216 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
218 | 217 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
219 | 218 | biimpd 219 |
. . . . . . . . . . . . . . . . 17
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
220 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
221 | 220 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
222 | 221 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
223 | 222 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
coe1 .gmulGrpvar1
coe1 .gmulGrpvar1 |
224 | 223 | rspcev 3309 |
. . . . . . . . . . . . . . . . 17
coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
|
225 | 204, 219,
224 | syl6an 568 |
. . . . . . . . . . . . . . . 16
coe1 .gmulGrpvar1
|
226 | 225 | rexlimdva 3031 |
. . . . . . . . . . . . . . 15
coe1 .gmulGrpvar1
|
227 | 226 | adantrr 753 |
. . . . . . . . . . . . . 14
coe1 .gmulGrpvar1
|
228 | 227 | adantlrr 757 |
. . . . . . . . . . . . 13
coe1 .gmulGrpvar1
|
229 | 198, 228 | mpd 15 |
. . . . . . . . . . . 12
|
230 | 229 | expr 643 |
. . . . . . . . . . 11
|
231 | 230 | ralrimiva 2966 |
. . . . . . . . . 10
|
232 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
233 | 232 | breq1d 4663 |
. . . . . . . . . . . 12
|
234 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
235 | 234 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
236 | 235 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
237 | 236 | rexbidv 3052 |
. . . . . . . . . . . . 13
|
238 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
239 | 238 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
240 | 239 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
241 | 240 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
242 | 241 | cbvrexv 3172 |
. . . . . . . . . . . . 13
|
243 | 237, 242 | syl6bb 276 |
. . . . . . . . . . . 12
|
244 | 233, 243 | imbi12d 334 |
. . . . . . . . . . 11
|
245 | 244 | cbvralv 3171 |
. . . . . . . . . 10
|
246 | 231, 245 | sylib 208 |
. . . . . . . . 9
|
247 | 246 | exp32 631 |
. . . . . . . 8
|
248 | 247 | com12 32 |
. . . . . . 7
|
249 | 248 | a2d 29 |
. . . . . 6
|
250 | 55, 60, 65, 60, 95, 249 | nn0ind 11472 |
. . . . 5
|
251 | 250 | impcom 446 |
. . . 4
|
252 | | fveq2 6191 |
. . . . . . 7
|
253 | 252 | breq1d 4663 |
. . . . . 6
|
254 | | oveq1 6657 |
. . . . . . . . 9
|
255 | 254 | fveq2d 6195 |
. . . . . . . 8
|
256 | 255 | breq1d 4663 |
. . . . . . 7
|
257 | 256 | rexbidv 3052 |
. . . . . 6
|
258 | 253, 257 | imbi12d 334 |
. . . . 5
|
259 | 258 | rspcva 3307 |
. . . 4
|
260 | 50, 251, 259 | syl2anc 693 |
. . 3
|
261 | 260 | rexlimdva 3031 |
. 2
|
262 | 49, 261 | mpd 15 |
1
|