Step | Hyp | Ref
| Expression |
1 | | ovolval5lem2.z |
. . . . . 6
Σ^
|
2 | 1 | a1i 11 |
. . . . 5
Σ^
|
3 | | nnex 11026 |
. . . . . . 7
|
4 | 3 | a1i 11 |
. . . . . 6
|
5 | | volioof 40204 |
. . . . . . . 8
|
6 | 5 | a1i 11 |
. . . . . . 7
|
7 | | rexpssxrxp 10084 |
. . . . . . . 8
|
8 | 7 | a1i 11 |
. . . . . . 7
|
9 | | ovolval5lem2.f |
. . . . . . . . . . . 12
|
10 | 9 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
11 | | xp1st 7198 |
. . . . . . . . . . 11
|
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
|
13 | | ovolval5lem2.w |
. . . . . . . . . . . . 13
|
14 | 13 | rpred 11872 |
. . . . . . . . . . . 12
|
15 | 14 | adantr 481 |
. . . . . . . . . . 11
|
16 | | 2nn 11185 |
. . . . . . . . . . . . . . 15
|
17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
|
18 | | nnnn0 11299 |
. . . . . . . . . . . . . 14
|
19 | 17, 18 | nnexpcld 13030 |
. . . . . . . . . . . . 13
|
20 | 19 | nnred 11035 |
. . . . . . . . . . . 12
|
21 | 20 | adantl 482 |
. . . . . . . . . . 11
|
22 | 19 | nnne0d 11065 |
. . . . . . . . . . . 12
|
23 | 22 | adantl 482 |
. . . . . . . . . . 11
|
24 | 15, 21, 23 | redivcld 10853 |
. . . . . . . . . 10
|
25 | 12, 24 | resubcld 10458 |
. . . . . . . . 9
|
26 | | xp2nd 7199 |
. . . . . . . . . 10
|
27 | 10, 26 | syl 17 |
. . . . . . . . 9
|
28 | 25, 27 | opelxpd 5149 |
. . . . . . . 8
|
29 | | ovolval5lem2.g |
. . . . . . . 8
|
30 | 28, 29 | fmptd 6385 |
. . . . . . 7
|
31 | 6, 8, 30 | fcoss 39402 |
. . . . . 6
|
32 | 4, 31 | sge0xrcl 40602 |
. . . . 5
Σ^
|
33 | 2, 32 | eqeltrd 2701 |
. . . 4
|
34 | | reex 10027 |
. . . . . . . . 9
|
35 | 34, 34 | xpex 6962 |
. . . . . . . 8
|
36 | 35 | a1i 11 |
. . . . . . 7
|
37 | 36, 4 | elmapd 7871 |
. . . . . 6
|
38 | 30, 37 | mpbird 247 |
. . . . 5
|
39 | | ovolval5lem2.s |
. . . . . . 7
|
40 | 30 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
|
41 | | xp1st 7198 |
. . . . . . . . . . . . . 14
|
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . 13
|
43 | 42 | rexrd 10089 |
. . . . . . . . . . . 12
|
44 | | xp2nd 7199 |
. . . . . . . . . . . . . 14
|
45 | 40, 44 | syl 17 |
. . . . . . . . . . . . 13
|
46 | 45 | rexrd 10089 |
. . . . . . . . . . . 12
|
47 | 13 | adantr 481 |
. . . . . . . . . . . . . . 15
|
48 | 19 | nnrpd 11870 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . 15
|
50 | 47, 49 | rpdivcld 11889 |
. . . . . . . . . . . . . 14
|
51 | 12, 50 | ltsubrpd 11904 |
. . . . . . . . . . . . 13
|
52 | | id 22 |
. . . . . . . . . . . . . . . . . 18
|
53 | | opex 4932 |
. . . . . . . . . . . . . . . . . . 19
|
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
55 | 29 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . 18
|
56 | 52, 54, 55 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
58 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
|
59 | | fvex 6201 |
. . . . . . . . . . . . . . . . . 18
|
60 | | op1stg 7180 |
. . . . . . . . . . . . . . . . . 18
|
61 | 58, 59, 60 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
|
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
63 | 57, 62 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
64 | 63 | adantl 482 |
. . . . . . . . . . . . . 14
|
65 | 64 | breq1d 4663 |
. . . . . . . . . . . . 13
|
66 | 51, 65 | mpbird 247 |
. . . . . . . . . . . 12
|
67 | 56 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
68 | 58, 59 | op2nd 7177 |
. . . . . . . . . . . . . . . . 17
|
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
70 | 67, 69 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
71 | 70 | adantl 482 |
. . . . . . . . . . . . . 14
|
72 | 71 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
73 | 27, 72 | eqled 10140 |
. . . . . . . . . . . 12
|
74 | | icossioo 12264 |
. . . . . . . . . . . 12
|
75 | 43, 46, 66, 73, 74 | syl22anc 1327 |
. . . . . . . . . . 11
|
76 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . 15
|
77 | 10, 76 | syl 17 |
. . . . . . . . . . . . . 14
|
78 | 77 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
79 | | df-ov 6653 |
. . . . . . . . . . . . . 14
|
80 | 79 | a1i 11 |
. . . . . . . . . . . . 13
|
81 | 78, 80 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
82 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . 15
|
83 | 40, 82 | syl 17 |
. . . . . . . . . . . . . 14
|
84 | 83 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
85 | | df-ov 6653 |
. . . . . . . . . . . . . 14
|
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
|
87 | 84, 86 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
88 | 81, 87 | sseq12d 3634 |
. . . . . . . . . . 11
|
89 | 75, 88 | mpbird 247 |
. . . . . . . . . 10
|
90 | 89 | ralrimiva 2966 |
. . . . . . . . 9
|
91 | | ss2iun 4536 |
. . . . . . . . 9
|
92 | 90, 91 | syl 17 |
. . . . . . . 8
|
93 | | fvex 6201 |
. . . . . . . . . . . . 13
|
94 | 93 | rgenw 2924 |
. . . . . . . . . . . 12
|
95 | 94 | a1i 11 |
. . . . . . . . . . 11
|
96 | | dfiun3g 5378 |
. . . . . . . . . . 11
|
97 | 95, 96 | syl 17 |
. . . . . . . . . 10
|
98 | | icof 39411 |
. . . . . . . . . . . . . . 15
|
99 | 98 | a1i 11 |
. . . . . . . . . . . . . 14
|
100 | 9, 8, 99 | fcomptss 39395 |
. . . . . . . . . . . . 13
|
101 | 100 | eqcomd 2628 |
. . . . . . . . . . . 12
|
102 | 101 | rneqd 5353 |
. . . . . . . . . . 11
|
103 | 102 | unieqd 4446 |
. . . . . . . . . 10
|
104 | 97, 103 | eqtr2d 2657 |
. . . . . . . . 9
|
105 | | fvex 6201 |
. . . . . . . . . . . . 13
|
106 | 105 | rgenw 2924 |
. . . . . . . . . . . 12
|
107 | 106 | a1i 11 |
. . . . . . . . . . 11
|
108 | | dfiun3g 5378 |
. . . . . . . . . . 11
|
109 | 107, 108 | syl 17 |
. . . . . . . . . 10
|
110 | | ioof 12271 |
. . . . . . . . . . . . . . 15
|
111 | 110 | a1i 11 |
. . . . . . . . . . . . . 14
|
112 | 30, 8, 111 | fcomptss 39395 |
. . . . . . . . . . . . 13
|
113 | 112 | eqcomd 2628 |
. . . . . . . . . . . 12
|
114 | 113 | rneqd 5353 |
. . . . . . . . . . 11
|
115 | 114 | unieqd 4446 |
. . . . . . . . . 10
|
116 | 109, 115 | eqtr2d 2657 |
. . . . . . . . 9
|
117 | 104, 116 | sseq12d 3634 |
. . . . . . . 8
|
118 | 92, 117 | mpbird 247 |
. . . . . . 7
|
119 | 39, 118 | sstrd 3613 |
. . . . . 6
|
120 | 119, 2 | jca 554 |
. . . . 5
Σ^
|
121 | | coeq2 5280 |
. . . . . . . . . 10
|
122 | 121 | rneqd 5353 |
. . . . . . . . 9
|
123 | 122 | unieqd 4446 |
. . . . . . . 8
|
124 | 123 | sseq2d 3633 |
. . . . . . 7
|
125 | | coeq2 5280 |
. . . . . . . . 9
|
126 | 125 | fveq2d 6195 |
. . . . . . . 8
Σ^
Σ^
|
127 | 126 | eqeq2d 2632 |
. . . . . . 7
Σ^
Σ^
|
128 | 124, 127 | anbi12d 747 |
. . . . . 6
Σ^
Σ^
|
129 | 128 | rspcev 3309 |
. . . . 5
Σ^
Σ^
|
130 | 38, 120, 129 | syl2anc 693 |
. . . 4
Σ^
|
131 | 33, 130 | jca 554 |
. . 3
Σ^
|
132 | | eqeq1 2626 |
. . . . . 6
Σ^
Σ^
|
133 | 132 | anbi2d 740 |
. . . . 5
Σ^
Σ^
|
134 | 133 | rexbidv 3052 |
. . . 4
Σ^
Σ^
|
135 | | ovolval5lem2.q |
. . . 4
Σ^
|
136 | 134, 135 | elrab2 3366 |
. . 3
Σ^
|
137 | 131, 136 | sylibr 224 |
. 2
|
138 | | fveq2 6191 |
. . . . . . 7
|
139 | 138 | fveq2d 6195 |
. . . . . 6
|
140 | 138 | fveq2d 6195 |
. . . . . 6
|
141 | 139, 140 | breq12d 4666 |
. . . . 5
|
142 | 141 | cbvrabv 3199 |
. . . 4
|
143 | 12, 27, 13, 142 | ovolval5lem1 40866 |
. . 3
Σ^
Σ^ |
144 | | nfcv 2764 |
. . . . . . . 8
|
145 | 30, 8 | fssd 6057 |
. . . . . . . 8
|
146 | 144, 145 | volioofmpt 40211 |
. . . . . . 7
|
147 | 64, 71 | oveq12d 6668 |
. . . . . . . . 9
|
148 | 147 | fveq2d 6195 |
. . . . . . . 8
|
149 | 148 | mpteq2dva 4744 |
. . . . . . 7
|
150 | 146, 149 | eqtrd 2656 |
. . . . . 6
|
151 | 150 | fveq2d 6195 |
. . . . 5
Σ^
Σ^ |
152 | 2, 151 | eqtrd 2656 |
. . . 4
Σ^ |
153 | | ovolval5lem2.y |
. . . . . 6
Σ^
|
154 | | nfcv 2764 |
. . . . . . . 8
|
155 | | ressxr 10083 |
. . . . . . . . . . 11
|
156 | | xpss2 5229 |
. . . . . . . . . . 11
|
157 | 155, 156 | ax-mp 5 |
. . . . . . . . . 10
|
158 | 157 | a1i 11 |
. . . . . . . . 9
|
159 | 9, 158 | fssd 6057 |
. . . . . . . 8
|
160 | 154, 159 | volicofmpt 40214 |
. . . . . . 7
|
161 | 160 | fveq2d 6195 |
. . . . . 6
Σ^
Σ^ |
162 | 153, 161 | eqtrd 2656 |
. . . . 5
Σ^ |
163 | 162 | oveq1d 6665 |
. . . 4
Σ^ |
164 | 152, 163 | breq12d 4666 |
. . 3
Σ^
Σ^ |
165 | 143, 164 | mpbird 247 |
. 2
|
166 | | breq1 4656 |
. . 3
|
167 | 166 | rspcev 3309 |
. 2
|
168 | 137, 165,
167 | syl2anc 693 |
1
|