Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . . 5
|
2 | 1 | rpred 11872 |
. . . 4
|
3 | | simpl2 1065 |
. . . . 5
|
4 | 3 | rpred 11872 |
. . . 4
|
5 | | simpl3 1066 |
. . . 4
|
6 | 1 | rpgt0d 11875 |
. . . . . . . . . . 11
|
7 | | ltpnf 11954 |
. . . . . . . . . . . 12
|
8 | 4, 7 | syl 17 |
. . . . . . . . . . 11
|
9 | | 0xr 10086 |
. . . . . . . . . . . 12
|
10 | | pnfxr 10092 |
. . . . . . . . . . . 12
|
11 | | iccssioo 12242 |
. . . . . . . . . . . 12
|
12 | 9, 10, 11 | mpanl12 718 |
. . . . . . . . . . 11
|
13 | 6, 8, 12 | syl2anc 693 |
. . . . . . . . . 10
|
14 | | ioorp 12251 |
. . . . . . . . . 10
|
15 | 13, 14 | syl6sseq 3651 |
. . . . . . . . 9
|
16 | 15 | sselda 3603 |
. . . . . . . 8
|
17 | 16 | relogcld 24369 |
. . . . . . 7
|
18 | 17 | renegcld 10457 |
. . . . . 6
|
19 | | eqid 2622 |
. . . . . 6
|
20 | 18, 19 | fmptd 6385 |
. . . . 5
|
21 | | ax-resscn 9993 |
. . . . . 6
|
22 | 15 | resabs1d 5428 |
. . . . . . . 8
|
23 | | ssid 3624 |
. . . . . . . . . . 11
|
24 | | cncfss 22702 |
. . . . . . . . . . 11
|
25 | 21, 23, 24 | mp2an 708 |
. . . . . . . . . 10
|
26 | | relogcn 24384 |
. . . . . . . . . 10
|
27 | 25, 26 | sselii 3600 |
. . . . . . . . 9
|
28 | | rescncf 22700 |
. . . . . . . . 9
|
29 | 15, 27, 28 | mpisyl 21 |
. . . . . . . 8
|
30 | 22, 29 | eqeltrrd 2702 |
. . . . . . 7
|
31 | | fvres 6207 |
. . . . . . . . . . 11
|
32 | 31 | negeqd 10275 |
. . . . . . . . . 10
|
33 | 32 | mpteq2ia 4740 |
. . . . . . . . 9
|
34 | 33 | eqcomi 2631 |
. . . . . . . 8
|
35 | 34 | negfcncf 22722 |
. . . . . . 7
|
36 | 30, 35 | syl 17 |
. . . . . 6
|
37 | | cncffvrn 22701 |
. . . . . 6
|
38 | 21, 36, 37 | sylancr 695 |
. . . . 5
|
39 | 20, 38 | mpbird 247 |
. . . 4
|
40 | | ioossre 12235 |
. . . . . . . 8
|
41 | | ltso 10118 |
. . . . . . . 8
|
42 | | soss 5053 |
. . . . . . . 8
|
43 | 40, 41, 42 | mp2 9 |
. . . . . . 7
|
44 | 43 | a1i 11 |
. . . . . 6
|
45 | | ioossicc 12259 |
. . . . . . . . . . . . . 14
|
46 | 45, 15 | syl5ss 3614 |
. . . . . . . . . . . . 13
|
47 | 46 | sselda 3603 |
. . . . . . . . . . . 12
|
48 | 47 | rprecred 11883 |
. . . . . . . . . . 11
|
49 | 48 | renegcld 10457 |
. . . . . . . . . 10
|
50 | | eqid 2622 |
. . . . . . . . . 10
|
51 | 49, 50 | fmptd 6385 |
. . . . . . . . 9
|
52 | | frn 6053 |
. . . . . . . . 9
|
53 | 51, 52 | syl 17 |
. . . . . . . 8
|
54 | | soss 5053 |
. . . . . . . 8
|
55 | 53, 41, 54 | mpisyl 21 |
. . . . . . 7
|
56 | | sopo 5052 |
. . . . . . 7
|
57 | 55, 56 | syl 17 |
. . . . . 6
|
58 | | negex 10279 |
. . . . . . . . 9
|
59 | 58, 50 | fnmpti 6022 |
. . . . . . . 8
|
60 | | dffn4 6121 |
. . . . . . . 8
|
61 | 59, 60 | mpbi 220 |
. . . . . . 7
|
62 | 61 | a1i 11 |
. . . . . 6
|
63 | 46 | sselda 3603 |
. . . . . . . . . . . 12
|
64 | 63 | adantrl 752 |
. . . . . . . . . . 11
|
65 | 64 | rprecred 11883 |
. . . . . . . . . 10
|
66 | 46 | sselda 3603 |
. . . . . . . . . . . 12
|
67 | 66 | adantrr 753 |
. . . . . . . . . . 11
|
68 | 67 | rprecred 11883 |
. . . . . . . . . 10
|
69 | 65, 68 | ltnegd 10605 |
. . . . . . . . 9
|
70 | 67, 64 | ltrecd 11890 |
. . . . . . . . 9
|
71 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
72 | 71 | negeqd 10275 |
. . . . . . . . . . . 12
|
73 | | negex 10279 |
. . . . . . . . . . . 12
|
74 | 72, 50, 73 | fvmpt 6282 |
. . . . . . . . . . 11
|
75 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
76 | 75 | negeqd 10275 |
. . . . . . . . . . . 12
|
77 | | negex 10279 |
. . . . . . . . . . . 12
|
78 | 76, 50, 77 | fvmpt 6282 |
. . . . . . . . . . 11
|
79 | 74, 78 | breqan12d 4669 |
. . . . . . . . . 10
|
80 | 79 | adantl 482 |
. . . . . . . . 9
|
81 | 69, 70, 80 | 3bitr4d 300 |
. . . . . . . 8
|
82 | 81 | biimpd 219 |
. . . . . . 7
|
83 | 82 | ralrimivva 2971 |
. . . . . 6
|
84 | | soisoi 6578 |
. . . . . 6
|
85 | 44, 57, 62, 83, 84 | syl22anc 1327 |
. . . . 5
|
86 | | reelprrecn 10028 |
. . . . . . . 8
|
87 | 86 | a1i 11 |
. . . . . . 7
|
88 | | relogcl 24322 |
. . . . . . . . . 10
|
89 | 88 | adantl 482 |
. . . . . . . . 9
|
90 | 89 | recnd 10068 |
. . . . . . . 8
|
91 | 90 | negcld 10379 |
. . . . . . 7
|
92 | 58 | a1i 11 |
. . . . . . 7
|
93 | | ovexd 6680 |
. . . . . . . 8
|
94 | | dvrelog 24383 |
. . . . . . . . 9
|
95 | | relogf1o 24313 |
. . . . . . . . . . . . 13
|
96 | | f1of 6137 |
. . . . . . . . . . . . 13
|
97 | 95, 96 | mp1i 13 |
. . . . . . . . . . . 12
|
98 | 97 | feqmptd 6249 |
. . . . . . . . . . 11
|
99 | | fvres 6207 |
. . . . . . . . . . . 12
|
100 | 99 | mpteq2ia 4740 |
. . . . . . . . . . 11
|
101 | 98, 100 | syl6eq 2672 |
. . . . . . . . . 10
|
102 | 101 | oveq2d 6666 |
. . . . . . . . 9
|
103 | 94, 102 | syl5reqr 2671 |
. . . . . . . 8
|
104 | 87, 90, 93, 103 | dvmptneg 23729 |
. . . . . . 7
|
105 | | eqid 2622 |
. . . . . . . 8
ℂfld ℂfld |
106 | 105 | tgioo2 22606 |
. . . . . . 7
ℂfld
↾t |
107 | | iccntr 22624 |
. . . . . . . 8
|
108 | 2, 4, 107 | syl2anc 693 |
. . . . . . 7
|
109 | 87, 91, 92, 104, 15, 106, 105, 108 | dvmptres2 23725 |
. . . . . 6
|
110 | | isoeq1 6567 |
. . . . . 6
|
111 | 109, 110 | syl 17 |
. . . . 5
|
112 | 85, 111 | mpbird 247 |
. . . 4
|
113 | | simpr 477 |
. . . 4
|
114 | | eqid 2622 |
. . . 4
|
115 | 2, 4, 5, 39, 112, 113, 114 | dvcvx 23783 |
. . 3
|
116 | | ax-1cn 9994 |
. . . . . . . 8
|
117 | | elioore 12205 |
. . . . . . . . . 10
|
118 | 117 | adantl 482 |
. . . . . . . . 9
|
119 | 118 | recnd 10068 |
. . . . . . . 8
|
120 | | nncan 10310 |
. . . . . . . 8
|
121 | 116, 119,
120 | sylancr 695 |
. . . . . . 7
|
122 | 121 | oveq1d 6665 |
. . . . . 6
|
123 | 122 | oveq1d 6665 |
. . . . 5
|
124 | | ioossicc 12259 |
. . . . . . . 8
|
125 | 124, 113 | sseldi 3601 |
. . . . . . 7
|
126 | | iirev 22728 |
. . . . . . 7
|
127 | 125, 126 | syl 17 |
. . . . . 6
|
128 | | lincmb01cmp 12315 |
. . . . . 6
|
129 | 2, 4, 5, 127, 128 | syl31anc 1329 |
. . . . 5
|
130 | 123, 129 | eqeltrrd 2702 |
. . . 4
|
131 | | fveq2 6191 |
. . . . . 6
|
132 | 131 | negeqd 10275 |
. . . . 5
|
133 | | negex 10279 |
. . . . 5
|
134 | 132, 19, 133 | fvmpt 6282 |
. . . 4
|
135 | 130, 134 | syl 17 |
. . 3
|
136 | 1 | rpxrd 11873 |
. . . . . . . . 9
|
137 | 3 | rpxrd 11873 |
. . . . . . . . 9
|
138 | 2, 4, 5 | ltled 10185 |
. . . . . . . . 9
|
139 | | lbicc2 12288 |
. . . . . . . . 9
|
140 | 136, 137,
138, 139 | syl3anc 1326 |
. . . . . . . 8
|
141 | | fveq2 6191 |
. . . . . . . . . 10
|
142 | 141 | negeqd 10275 |
. . . . . . . . 9
|
143 | | negex 10279 |
. . . . . . . . 9
|
144 | 142, 19, 143 | fvmpt 6282 |
. . . . . . . 8
|
145 | 140, 144 | syl 17 |
. . . . . . 7
|
146 | 145 | oveq2d 6666 |
. . . . . 6
|
147 | 1 | relogcld 24369 |
. . . . . . . 8
|
148 | 147 | recnd 10068 |
. . . . . . 7
|
149 | 119, 148 | mulneg2d 10484 |
. . . . . 6
|
150 | 146, 149 | eqtrd 2656 |
. . . . 5
|
151 | | ubicc2 12289 |
. . . . . . . . 9
|
152 | 136, 137,
138, 151 | syl3anc 1326 |
. . . . . . . 8
|
153 | | fveq2 6191 |
. . . . . . . . . 10
|
154 | 153 | negeqd 10275 |
. . . . . . . . 9
|
155 | | negex 10279 |
. . . . . . . . 9
|
156 | 154, 19, 155 | fvmpt 6282 |
. . . . . . . 8
|
157 | 152, 156 | syl 17 |
. . . . . . 7
|
158 | 157 | oveq2d 6666 |
. . . . . 6
|
159 | | 1re 10039 |
. . . . . . . . 9
|
160 | | resubcl 10345 |
. . . . . . . . 9
|
161 | 159, 118,
160 | sylancr 695 |
. . . . . . . 8
|
162 | 161 | recnd 10068 |
. . . . . . 7
|
163 | 3 | relogcld 24369 |
. . . . . . . 8
|
164 | 163 | recnd 10068 |
. . . . . . 7
|
165 | 162, 164 | mulneg2d 10484 |
. . . . . 6
|
166 | 158, 165 | eqtrd 2656 |
. . . . 5
|
167 | 150, 166 | oveq12d 6668 |
. . . 4
|
168 | 118, 147 | remulcld 10070 |
. . . . . 6
|
169 | 168 | recnd 10068 |
. . . . 5
|
170 | 161, 163 | remulcld 10070 |
. . . . . 6
|
171 | 170 | recnd 10068 |
. . . . 5
|
172 | 169, 171 | negdid 10405 |
. . . 4
|
173 | 167, 172 | eqtr4d 2659 |
. . 3
|
174 | 115, 135,
173 | 3brtr3d 4684 |
. 2
|
175 | 168, 170 | readdcld 10069 |
. . 3
|
176 | 15, 130 | sseldd 3604 |
. . . 4
|
177 | 176 | relogcld 24369 |
. . 3
|
178 | 175, 177 | ltnegd 10605 |
. 2
|
179 | 174, 178 | mpbird 247 |
1
|