Step | Hyp | Ref
| Expression |
1 | | ivth.7 |
. . 3
|
2 | | ivth.5 |
. . . 4
|
3 | | ivthinclemlopn.q |
. . . . . 6
|
4 | | fveq2 5496 |
. . . . . . . 8
|
5 | 4 | breq1d 3999 |
. . . . . . 7
|
6 | | ivthinclem.l |
. . . . . . 7
|
7 | 5, 6 | elrab2 2889 |
. . . . . 6
|
8 | 3, 7 | sylib 121 |
. . . . 5
|
9 | 8 | simpld 111 |
. . . 4
|
10 | 2, 9 | sseldd 3148 |
. . 3
|
11 | | ivth.3 |
. . . . 5
|
12 | | fveq2 5496 |
. . . . . . 7
|
13 | 12 | eleq1d 2239 |
. . . . . 6
|
14 | | ivth.8 |
. . . . . . 7
|
15 | 14 | ralrimiva 2543 |
. . . . . 6
|
16 | 13, 15, 9 | rspcdva 2839 |
. . . . 5
|
17 | 11, 16 | resubcld 8300 |
. . . 4
|
18 | 8 | simprd 113 |
. . . . 5
|
19 | 16, 11 | posdifd 8451 |
. . . . 5
|
20 | 18, 19 | mpbid 146 |
. . . 4
|
21 | 17, 20 | elrpd 9650 |
. . 3
|
22 | | cncfi 13359 |
. . 3
|
23 | 1, 10, 21, 22 | syl3anc 1233 |
. 2
|
24 | | ivth.1 |
. . . . . . . . . 10
|
25 | | ivth.2 |
. . . . . . . . . 10
|
26 | | elicc2 9895 |
. . . . . . . . . 10
|
27 | 24, 25, 26 | syl2anc 409 |
. . . . . . . . 9
|
28 | 9, 27 | mpbid 146 |
. . . . . . . 8
|
29 | 28 | simp1d 1004 |
. . . . . . 7
|
30 | 29 | adantr 274 |
. . . . . 6
|
31 | | simprl 526 |
. . . . . . . 8
|
32 | 31 | rphalfcld 9666 |
. . . . . . 7
|
33 | 32 | rpred 9653 |
. . . . . 6
|
34 | 30, 33 | readdcld 7949 |
. . . . 5
|
35 | 24 | adantr 274 |
. . . . . 6
|
36 | 28 | simp2d 1005 |
. . . . . . 7
|
37 | 36 | adantr 274 |
. . . . . 6
|
38 | 30, 32 | ltaddrpd 9687 |
. . . . . . 7
|
39 | 30, 34, 38 | ltled 8038 |
. . . . . 6
|
40 | 35, 30, 34, 37, 39 | letrd 8043 |
. . . . 5
|
41 | 25 | adantr 274 |
. . . . . 6
|
42 | 31 | rpred 9653 |
. . . . . . . 8
|
43 | 30, 42 | readdcld 7949 |
. . . . . . 7
|
44 | | rphalflt 9640 |
. . . . . . . . 9
|
45 | 31, 44 | syl 14 |
. . . . . . . 8
|
46 | 33, 42, 30, 45 | ltadd2dd 8341 |
. . . . . . 7
|
47 | 29 | ad2antrr 485 |
. . . . . . . . . . . . . . . . 17
|
48 | 31 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48 | rpred 9653 |
. . . . . . . . . . . . . . . . 17
|
50 | 47, 49 | resubcld 8300 |
. . . . . . . . . . . . . . . 16
|
51 | 25 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
|
52 | 47, 48 | ltsubrpd 9686 |
. . . . . . . . . . . . . . . 16
|
53 | 28 | simp3d 1006 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
|
55 | 50, 47, 51, 52, 54 | ltletrd 8342 |
. . . . . . . . . . . . . . 15
|
56 | | simpr 109 |
. . . . . . . . . . . . . . 15
|
57 | 51, 47, 49 | absdifltd 11142 |
. . . . . . . . . . . . . . 15
|
58 | 55, 56, 57 | mpbir2and 939 |
. . . . . . . . . . . . . 14
|
59 | | fvoveq1 5876 |
. . . . . . . . . . . . . . . . 17
|
60 | 59 | breq1d 3999 |
. . . . . . . . . . . . . . . 16
|
61 | 60 | imbrov2fvoveq 5878 |
. . . . . . . . . . . . . . 15
|
62 | | simplrr 531 |
. . . . . . . . . . . . . . 15
|
63 | 24 | rexrd 7969 |
. . . . . . . . . . . . . . . . . 18
|
64 | 25 | rexrd 7969 |
. . . . . . . . . . . . . . . . . 18
|
65 | | ivth.4 |
. . . . . . . . . . . . . . . . . . 19
|
66 | 24, 25, 65 | ltled 8038 |
. . . . . . . . . . . . . . . . . 18
|
67 | | ubicc2 9942 |
. . . . . . . . . . . . . . . . . 18
|
68 | 63, 64, 66, 67 | syl3anc 1233 |
. . . . . . . . . . . . . . . . 17
|
69 | 2, 68 | sseldd 3148 |
. . . . . . . . . . . . . . . 16
|
70 | 69 | ad2antrr 485 |
. . . . . . . . . . . . . . 15
|
71 | 61, 62, 70 | rspcdva 2839 |
. . . . . . . . . . . . . 14
|
72 | 58, 71 | mpd 13 |
. . . . . . . . . . . . 13
|
73 | | fveq2 5496 |
. . . . . . . . . . . . . . . . 17
|
74 | 73 | eleq1d 2239 |
. . . . . . . . . . . . . . . 16
|
75 | 15 | adantr 274 |
. . . . . . . . . . . . . . . 16
|
76 | 68 | adantr 274 |
. . . . . . . . . . . . . . . 16
|
77 | 74, 75, 76 | rspcdva 2839 |
. . . . . . . . . . . . . . 15
|
78 | 77 | adantr 274 |
. . . . . . . . . . . . . 14
|
79 | 16 | ad2antrr 485 |
. . . . . . . . . . . . . 14
|
80 | 17 | ad2antrr 485 |
. . . . . . . . . . . . . 14
|
81 | 78, 79, 80 | absdifltd 11142 |
. . . . . . . . . . . . 13
|
82 | 72, 81 | mpbid 146 |
. . . . . . . . . . . 12
|
83 | 82 | simprd 113 |
. . . . . . . . . . 11
|
84 | 79 | recnd 7948 |
. . . . . . . . . . . 12
|
85 | 11 | recnd 7948 |
. . . . . . . . . . . . 13
|
86 | 85 | ad2antrr 485 |
. . . . . . . . . . . 12
|
87 | 84, 86 | pncan3d 8233 |
. . . . . . . . . . 11
|
88 | 83, 87 | breqtrd 4015 |
. . . . . . . . . 10
|
89 | | ivth.9 |
. . . . . . . . . . . 12
|
90 | 89 | simprd 113 |
. . . . . . . . . . 11
|
91 | 90 | ad2antrr 485 |
. . . . . . . . . 10
|
92 | 88, 91 | jca 304 |
. . . . . . . . 9
|
93 | 11 | ad2antrr 485 |
. . . . . . . . . 10
|
94 | | ltnsym2 8010 |
. . . . . . . . . 10
|
95 | 78, 93, 94 | syl2anc 409 |
. . . . . . . . 9
|
96 | 92, 95 | pm2.65da 656 |
. . . . . . . 8
|
97 | 43, 41, 96 | nltled 8040 |
. . . . . . 7
|
98 | 34, 43, 41, 46, 97 | ltletrd 8342 |
. . . . . 6
|
99 | 34, 41, 98 | ltled 8038 |
. . . . 5
|
100 | | elicc2 9895 |
. . . . . 6
|
101 | 35, 41, 100 | syl2anc 409 |
. . . . 5
|
102 | 34, 40, 99, 101 | mpbir3and 1175 |
. . . 4
|
103 | 16 | adantr 274 |
. . . . . . 7
|
104 | | fveq2 5496 |
. . . . . . . . 9
|
105 | 104 | eleq1d 2239 |
. . . . . . . 8
|
106 | 105, 75, 102 | rspcdva 2839 |
. . . . . . 7
|
107 | | breq2 3993 |
. . . . . . . . . . 11
|
108 | | fveq2 5496 |
. . . . . . . . . . . 12
|
109 | 108 | breq2d 4001 |
. . . . . . . . . . 11
|
110 | 107, 109 | imbi12d 233 |
. . . . . . . . . 10
|
111 | | breq1 3992 |
. . . . . . . . . . . . . 14
|
112 | 12 | breq1d 3999 |
. . . . . . . . . . . . . 14
|
113 | 111, 112 | imbi12d 233 |
. . . . . . . . . . . . 13
|
114 | 113 | ralbidv 2470 |
. . . . . . . . . . . 12
|
115 | | ivthinc.i |
. . . . . . . . . . . . . . 15
|
116 | 115 | expr 373 |
. . . . . . . . . . . . . 14
|
117 | 116 | ralrimiva 2543 |
. . . . . . . . . . . . 13
|
118 | 117 | ralrimiva 2543 |
. . . . . . . . . . . 12
|
119 | 114, 118,
9 | rspcdva 2839 |
. . . . . . . . . . 11
|
120 | 119 | adantr 274 |
. . . . . . . . . 10
|
121 | 110, 120,
102 | rspcdva 2839 |
. . . . . . . . 9
|
122 | 38, 121 | mpd 13 |
. . . . . . . 8
|
123 | 103, 106,
122 | ltled 8038 |
. . . . . . 7
|
124 | 103, 106,
123 | abssubge0d 11140 |
. . . . . 6
|
125 | 30 | recnd 7948 |
. . . . . . . . . . 11
|
126 | 33 | recnd 7948 |
. . . . . . . . . . 11
|
127 | 125, 126 | pncan2d 8232 |
. . . . . . . . . 10
|
128 | 127 | fveq2d 5500 |
. . . . . . . . 9
|
129 | 32 | rpge0d 9657 |
. . . . . . . . . 10
|
130 | 33, 129 | absidd 11131 |
. . . . . . . . 9
|
131 | 128, 130 | eqtrd 2203 |
. . . . . . . 8
|
132 | 131, 45 | eqbrtrd 4011 |
. . . . . . 7
|
133 | | fvoveq1 5876 |
. . . . . . . . . 10
|
134 | 133 | breq1d 3999 |
. . . . . . . . 9
|
135 | 134 | imbrov2fvoveq 5878 |
. . . . . . . 8
|
136 | | simprr 527 |
. . . . . . . 8
|
137 | 2 | adantr 274 |
. . . . . . . . 9
|
138 | 137, 102 | sseldd 3148 |
. . . . . . . 8
|
139 | 135, 136,
138 | rspcdva 2839 |
. . . . . . 7
|
140 | 132, 139 | mpd 13 |
. . . . . 6
|
141 | 124, 140 | eqbrtrrd 4013 |
. . . . 5
|
142 | 11 | adantr 274 |
. . . . . 6
|
143 | 106, 142,
103 | ltsub1d 8473 |
. . . . 5
|
144 | 141, 143 | mpbird 166 |
. . . 4
|
145 | | fveq2 5496 |
. . . . . 6
|
146 | 145 | breq1d 3999 |
. . . . 5
|
147 | 146, 6 | elrab2 2889 |
. . . 4
|
148 | 102, 144,
147 | sylanbrc 415 |
. . 3
|
149 | | breq2 3993 |
. . . 4
|
150 | 149 | rspcev 2834 |
. . 3
|
151 | 148, 38, 150 | syl2anc 409 |
. 2
|
152 | 23, 151 | rexlimddv 2592 |
1
|