Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. . . 4
|
2 | | simpr 477 |
. . . 4
|
3 | | rpre 11839 |
. . . . . 6
|
4 | 3 | ad2antlr 763 |
. . . . 5
|
5 | | rpge0 11845 |
. . . . . 6
|
6 | 5 | ad2antlr 763 |
. . . . 5
|
7 | | elrege0 12278 |
. . . . 5
|
8 | 4, 6, 7 | sylanbrc 698 |
. . . 4
|
9 | | itg2const 23507 |
. . . 4
|
10 | 1, 2, 8, 9 | syl3anc 1326 |
. . 3
|
11 | 4, 2 | remulcld 10070 |
. . 3
|
12 | 10, 11 | eqeltrd 2701 |
. 2
|
13 | | mblvol 23298 |
. . . 4
|
14 | 13 | ad2antrr 762 |
. . 3
|
15 | | mblss 23299 |
. . . . . 6
|
16 | 15 | ad3antrrr 766 |
. . . . 5
|
17 | | peano2re 10209 |
. . . . . . . 8
|
18 | 17 | adantl 482 |
. . . . . . 7
|
19 | | simplr 792 |
. . . . . . 7
|
20 | 18, 19 | rerpdivcld 11903 |
. . . . . 6
|
21 | 20 | adantr 481 |
. . . . 5
|
22 | | simpr 477 |
. . . . 5
|
23 | | ovollecl 23251 |
. . . . 5
|
24 | 16, 21, 22, 23 | syl3anc 1326 |
. . . 4
|
25 | | simplll 798 |
. . . . . . . 8
|
26 | 20 | adantr 481 |
. . . . . . . . . 10
|
27 | 26 | rexrd 10089 |
. . . . . . . . 9
|
28 | | simpr 477 |
. . . . . . . . . . . . 13
|
29 | 3 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 29 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
|
31 | 5 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
32 | | elxrge0 12281 |
. . . . . . . . . . . . . . . . . 18
|
33 | 30, 31, 32 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
|
34 | | 0e0iccpnf 12283 |
. . . . . . . . . . . . . . . . 17
|
35 | | ifcl 4130 |
. . . . . . . . . . . . . . . . 17
|
36 | 33, 34, 35 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
37 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
38 | 36, 37 | fmptd 6385 |
. . . . . . . . . . . . . . 15
|
39 | 38 | adantr 481 |
. . . . . . . . . . . . . 14
|
40 | | itg2ge0 23502 |
. . . . . . . . . . . . . 14
|
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . 13
|
42 | 28, 41 | ge0p1rpd 11902 |
. . . . . . . . . . . 12
|
43 | 42, 19 | rpdivcld 11889 |
. . . . . . . . . . 11
|
44 | 43 | rpge0d 11876 |
. . . . . . . . . 10
|
45 | 44 | adantr 481 |
. . . . . . . . 9
|
46 | 14 | breq2d 4665 |
. . . . . . . . . 10
|
47 | 46 | biimpar 502 |
. . . . . . . . 9
|
48 | | 0xr 10086 |
. . . . . . . . . 10
|
49 | | iccssxr 12256 |
. . . . . . . . . . . 12
|
50 | | volf 23297 |
. . . . . . . . . . . . 13
|
51 | 50 | ffvelrni 6358 |
. . . . . . . . . . . 12
|
52 | 49, 51 | sseldi 3601 |
. . . . . . . . . . 11
|
53 | 25, 52 | syl 17 |
. . . . . . . . . 10
|
54 | | elicc1 12219 |
. . . . . . . . . 10
|
55 | 48, 53, 54 | sylancr 695 |
. . . . . . . . 9
|
56 | 27, 45, 47, 55 | mpbir3and 1245 |
. . . . . . . 8
|
57 | | volivth 23375 |
. . . . . . . 8
|
58 | 25, 56, 57 | syl2anc 693 |
. . . . . . 7
|
59 | 58 | ex 450 |
. . . . . 6
|
60 | | simprl 794 |
. . . . . . . . . . 11
|
61 | | simprrr 805 |
. . . . . . . . . . . 12
|
62 | 20 | adantr 481 |
. . . . . . . . . . . 12
|
63 | 61, 62 | eqeltrd 2701 |
. . . . . . . . . . 11
|
64 | 3 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
65 | 64 | adantr 481 |
. . . . . . . . . . . 12
|
66 | 19 | adantr 481 |
. . . . . . . . . . . . 13
|
67 | 66 | rpge0d 11876 |
. . . . . . . . . . . 12
|
68 | 65, 67, 7 | sylanbrc 698 |
. . . . . . . . . . 11
|
69 | | itg2const 23507 |
. . . . . . . . . . 11
|
70 | 60, 63, 68, 69 | syl3anc 1326 |
. . . . . . . . . 10
|
71 | 61 | oveq2d 6666 |
. . . . . . . . . 10
|
72 | 18 | recnd 10068 |
. . . . . . . . . . . 12
|
73 | 64 | recnd 10068 |
. . . . . . . . . . . 12
|
74 | | rpne0 11848 |
. . . . . . . . . . . . 13
|
75 | 74 | ad2antlr 763 |
. . . . . . . . . . . 12
|
76 | 72, 73, 75 | divcan2d 10803 |
. . . . . . . . . . 11
|
77 | 76 | adantr 481 |
. . . . . . . . . 10
|
78 | 70, 71, 77 | 3eqtrd 2660 |
. . . . . . . . 9
|
79 | 3 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
80 | 79 | rexrd 10089 |
. . . . . . . . . . . . . . 15
|
81 | 5 | adantl 482 |
. . . . . . . . . . . . . . 15
|
82 | 80, 81, 32 | sylanbrc 698 |
. . . . . . . . . . . . . 14
|
83 | | ifcl 4130 |
. . . . . . . . . . . . . 14
|
84 | 82, 34, 83 | sylancl 694 |
. . . . . . . . . . . . 13
|
85 | 84 | adantr 481 |
. . . . . . . . . . . 12
|
86 | | eqid 2622 |
. . . . . . . . . . . 12
|
87 | 85, 86 | fmptd 6385 |
. . . . . . . . . . 11
|
88 | 87 | ad2antrr 762 |
. . . . . . . . . 10
|
89 | 39 | adantr 481 |
. . . . . . . . . 10
|
90 | | simpl 473 |
. . . . . . . . . . 11
|
91 | | simprl 794 |
. . . . . . . . . . 11
|
92 | 79 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
|
93 | 92 | leidd 10594 |
. . . . . . . . . . . . . . 15
|
94 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
|
95 | 94 | adantl 482 |
. . . . . . . . . . . . . . 15
|
96 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
|
97 | 96 | sselda 3603 |
. . . . . . . . . . . . . . . 16
|
98 | 97 | iftrued 4094 |
. . . . . . . . . . . . . . 15
|
99 | 93, 95, 98 | 3brtr4d 4685 |
. . . . . . . . . . . . . 14
|
100 | | iffalse 4095 |
. . . . . . . . . . . . . . . 16
|
101 | 100 | adantl 482 |
. . . . . . . . . . . . . . 15
|
102 | | 0le0 11110 |
. . . . . . . . . . . . . . . . 17
|
103 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
|
104 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
|
105 | 103, 104 | ifboth 4124 |
. . . . . . . . . . . . . . . . 17
|
106 | 81, 102, 105 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
107 | 106 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
108 | 101, 107 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
|
109 | 99, 108 | pm2.61dan 832 |
. . . . . . . . . . . . 13
|
110 | 109 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
111 | | reex 10027 |
. . . . . . . . . . . . . . 15
|
112 | 111 | a1i 11 |
. . . . . . . . . . . . . 14
|
113 | | eqidd 2623 |
. . . . . . . . . . . . . 14
|
114 | | eqidd 2623 |
. . . . . . . . . . . . . 14
|
115 | 112, 85, 36, 113, 114 | ofrfval2 6915 |
. . . . . . . . . . . . 13
|
116 | 115 | biimpar 502 |
. . . . . . . . . . . 12
|
117 | 110, 116 | syldan 487 |
. . . . . . . . . . 11
|
118 | 90, 91, 117 | syl2an 494 |
. . . . . . . . . 10
|
119 | | itg2le 23506 |
. . . . . . . . . 10
|
120 | 88, 89, 118, 119 | syl3anc 1326 |
. . . . . . . . 9
|
121 | 78, 120 | eqbrtrrd 4677 |
. . . . . . . 8
|
122 | | ltp1 10861 |
. . . . . . . . . 10
|
123 | 122 | ad2antlr 763 |
. . . . . . . . 9
|
124 | | simplr 792 |
. . . . . . . . . 10
|
125 | 17 | ad2antlr 763 |
. . . . . . . . . 10
|
126 | 124, 125 | ltnled 10184 |
. . . . . . . . 9
|
127 | 123, 126 | mpbid 222 |
. . . . . . . 8
|
128 | 121, 127 | pm2.21dd 186 |
. . . . . . 7
|
129 | 128 | rexlimdvaa 3032 |
. . . . . 6
|
130 | 59, 129 | syld 47 |
. . . . 5
|
131 | 130 | imp 445 |
. . . 4
|
132 | 52 | ad2antrr 762 |
. . . . . 6
|
133 | 14, 132 | eqeltrrd 2702 |
. . . . 5
|
134 | 20 | rexrd 10089 |
. . . . 5
|
135 | | xrletri 11984 |
. . . . 5
|
136 | 133, 134,
135 | syl2anc 693 |
. . . 4
|
137 | 24, 131, 136 | mpjaodan 827 |
. . 3
|
138 | 14, 137 | eqeltrd 2701 |
. 2
|
139 | 12, 138 | impbida 877 |
1
|