Proof of Theorem cxpcn3lem
Step | Hyp | Ref
| Expression |
1 | | cxpcn3.t |
. . 3
                |
2 | | cxpcn3.u |
. . . . 5
                |
3 | | cxpcn3.d |
. . . . . . . . . . 11
      |
4 | 3 | eleq2i 2541 |
. . . . . . . . . 10

       |
5 | | ref 13252 |
. . . . . . . . . . 11
     |
6 | | ffn 5739 |
. . . . . . . . . . 11
       |
7 | | elpreima 6017 |
. . . . . . . . . . 11
 
    
         |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . . . 10
     
        |
9 | 4, 8 | bitri 257 |
. . . . . . . . 9

        |
10 | 9 | simprbi 471 |
. . . . . . . 8
       |
11 | 10 | adantr 472 |
. . . . . . 7
 
       |
12 | | 1rp 11329 |
. . . . . . 7
 |
13 | | ifcl 3914 |
. . . . . . 7
                      |
14 | 11, 12, 13 | sylancl 675 |
. . . . . 6
 
                |
15 | 14 | rphalfcld 11376 |
. . . . 5
 
                  |
16 | 2, 15 | syl5eqel 2553 |
. . . 4
 

  |
17 | | simpr 468 |
. . . . 5
 

  |
18 | 16 | rpreccld 11374 |
. . . . . 6
 
     |
19 | 18 | rpred 11364 |
. . . . 5
 
     |
20 | 17, 19 | rpcxpcld 23754 |
. . . 4
 
        |
21 | 16, 20 | ifcld 3915 |
. . 3
 
                  |
22 | 1, 21 | syl5eqel 2553 |
. 2
 

  |
23 | | elrege0 11764 |
. . . 4
   
    |
24 | | 0red 9662 |
. . . . . . 7
 
   |
25 | | leloe 9738 |
. . . . . . 7
 
       |
26 | 24, 25 | sylan 479 |
. . . . . 6
  

       |
27 | | elrp 11327 |
. . . . . . . . 9

    |
28 | | simp2l 1056 |
. . . . . . . . . . . . . 14
  
           
 
 
  |
29 | | simp2r 1057 |
. . . . . . . . . . . . . . 15
  
           
 
 
  |
30 | | cnvimass 5194 |
. . . . . . . . . . . . . . . . . 18
      |
31 | 5 | fdmi 5746 |
. . . . . . . . . . . . . . . . . 18
 |
32 | 30, 31 | sseqtri 3450 |
. . . . . . . . . . . . . . . . 17
      |
33 | 3, 32 | eqsstri 3448 |
. . . . . . . . . . . . . . . 16
 |
34 | 33 | sseli 3414 |
. . . . . . . . . . . . . . 15
   |
35 | 29, 34 | syl 17 |
. . . . . . . . . . . . . 14
  
           
 
 
  |
36 | | abscxp 23716 |
. . . . . . . . . . . . . 14
                   |
37 | 28, 35, 36 | syl2anc 673 |
. . . . . . . . . . . . 13
  
           
 
 
                |
38 | 35 | recld 13334 |
. . . . . . . . . . . . . . . 16
  
           
 
 
      |
39 | 28, 38 | rpcxpcld 23754 |
. . . . . . . . . . . . . . 15
  
           
 
 
 
       |
40 | 39 | rpred 11364 |
. . . . . . . . . . . . . 14
  
           
 
 
 
       |
41 | 16 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
  |
42 | 41 | rpred 11364 |
. . . . . . . . . . . . . . . 16
  
           
 
 
  |
43 | 28, 42 | rpcxpcld 23754 |
. . . . . . . . . . . . . . 15
  
           
 
 
 
   |
44 | 43 | rpred 11364 |
. . . . . . . . . . . . . 14
  
           
 
 
 
   |
45 | | simp1r 1055 |
. . . . . . . . . . . . . . 15
  
           
 
 
  |
46 | 45 | rpred 11364 |
. . . . . . . . . . . . . 14
  
           
 
 
  |
47 | | simp1l 1054 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
  |
48 | 9 | simplbi 467 |
. . . . . . . . . . . . . . . . . . 19
   |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
  |
50 | 49 | recld 13334 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
      |
51 | 50 | rehalfcld 10882 |
. . . . . . . . . . . . . . . 16
  
           
 
 
        |
52 | | 1re 9660 |
. . . . . . . . . . . . . . . . . . 19
 |
53 | | min1 11506 |
. . . . . . . . . . . . . . . . . . 19
     
                    |
54 | 50, 52, 53 | sylancl 675 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
     
             |
55 | 14 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . 20
  
           
 
 
     
         |
56 | 55 | rpred 11364 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
     
         |
57 | | 2re 10701 |
. . . . . . . . . . . . . . . . . . . 20
 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
  |
59 | | 2pos 10723 |
. . . . . . . . . . . . . . . . . . . 20
 |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
  |
61 | | lediv1 10492 |
. . . . . . . . . . . . . . . . . . 19
                     
             
   
                        |
62 | 56, 50, 58, 60, 61 | syl112anc 1296 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
             
   
                        |
63 | 54, 62 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
                       |
64 | 2, 63 | syl5eqbr 4429 |
. . . . . . . . . . . . . . . 16
  
           
 
 
        |
65 | 50 | recnd 9687 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
      |
66 | 65 | 2halvesd 10881 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
                    |
67 | 49, 35 | resubd 13356 |
. . . . . . . . . . . . . . . . . . . 20
  
           
 
 
                  |
68 | 49, 35 | subcld 10005 |
. . . . . . . . . . . . . . . . . . . . . 22
  
           
 
 
    |
69 | 68 | recld 13334 |
. . . . . . . . . . . . . . . . . . . . 21
  
           
 
 
        |
70 | 68 | abscld 13575 |
. . . . . . . . . . . . . . . . . . . . . 22
  
           
 
 
        |
71 | 68 | releabsd 13590 |
. . . . . . . . . . . . . . . . . . . . . 22
  
           
 
 
              |
72 | | simp3r 1059 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
           
 
 
        |
73 | 72, 1 | syl6breq 4435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
           
 
 
       
               |
74 | 20 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
           
 
 
 
     |
75 | 74 | rpred 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
           
 
 
 
     |
76 | | ltmin 11511 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
 
          
 
                         
 
 
       |
77 | 70, 42, 75, 76 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
           
 
 
                          
 
               |
78 | 73, 77 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
           
 
 
      
              |
79 | 78 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . 22
  
           
 
 
        |
80 | 69, 70, 42, 71, 79 | lelttrd 9810 |
. . . . . . . . . . . . . . . . . . . . 21
  
           
 
 
        |
81 | 69, 42, 51, 80, 64 | ltletrd 9812 |
. . . . . . . . . . . . . . . . . . . 20
  
           
 
 
              |
82 | 67, 81 | eqbrtrrd 4418 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
                  |
83 | 50, 38, 51 | ltsubadd2d 10232 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
                
                   |
84 | 82, 83 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
                  |
85 | 66, 84 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
                            |
86 | 51, 38, 51 | ltadd1d 10227 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
          
                             |
87 | 85, 86 | mpbird 240 |
. . . . . . . . . . . . . . . 16
  
           
 
 
            |
88 | 42, 51, 38, 64, 87 | lelttrd 9810 |
. . . . . . . . . . . . . . 15
  
           
 
 
      |
89 | 28 | rpred 11364 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
  |
90 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
  |
91 | 28 | rprege0d 11371 |
. . . . . . . . . . . . . . . . . . . . . 22
  
           
 
 
    |
92 | | absid 13436 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
  
           
 
 
      |
94 | | simp3l 1058 |
. . . . . . . . . . . . . . . . . . . . 21
  
           
 
 
      |
95 | 93, 94 | eqbrtrrd 4418 |
. . . . . . . . . . . . . . . . . . . 20
  
           
 
 
  |
96 | 95, 1 | syl6breq 4435 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
                 |
97 | | ltmin 11511 |
. . . . . . . . . . . . . . . . . . . 20
 
        
            
          |
98 | 89, 42, 75, 97 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
                
         |
99 | 96, 98 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
         |
100 | 99 | simpld 466 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
  |
101 | | rehalfcl 10862 |
. . . . . . . . . . . . . . . . . . 19
     |
102 | 52, 101 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
    |
103 | | min2 11507 |
. . . . . . . . . . . . . . . . . . . . 21
     
                |
104 | 50, 52, 103 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . 20
  
           
 
 
     
         |
105 | | lediv1 10492 |
. . . . . . . . . . . . . . . . . . . . 21
                 
             
                    |
106 | 56, 90, 58, 60, 105 | syl112anc 1296 |
. . . . . . . . . . . . . . . . . . . 20
  
           
 
 
             
                    |
107 | 104, 106 | mpbid 215 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
                   |
108 | 2, 107 | syl5eqbr 4429 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
    |
109 | | halflt1 10854 |
. . . . . . . . . . . . . . . . . . 19
   |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
    |
111 | 42, 102, 90, 108, 110 | lelttrd 9810 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
  |
112 | 89, 42, 90, 100, 111 | lttrd 9813 |
. . . . . . . . . . . . . . . 16
  
           
 
 
  |
113 | 28, 42, 112, 38 | cxplt3d 23756 |
. . . . . . . . . . . . . . 15
  
           
 
 
                  |
114 | 88, 113 | mpbid 215 |
. . . . . . . . . . . . . 14
  
           
 
 
 
          |
115 | 41 | rpcnne0d 11373 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
    |
116 | | recid 10306 |
. . . . . . . . . . . . . . . . . . 19
         |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
      |
118 | 117 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
 
          |
119 | 41 | rpreccld 11374 |
. . . . . . . . . . . . . . . . . . 19
  
           
 
 
    |
120 | 119 | rpcnd 11366 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
    |
121 | 28, 42, 120 | cxpmuld 23758 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
 
               |
122 | 28 | rpcnd 11366 |
. . . . . . . . . . . . . . . . . 18
  
           
 
 
  |
123 | 122 | cxp1d 23730 |
. . . . . . . . . . . . . . . . 17
  
           
 
 
 
   |
124 | 118, 121,
123 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . . 16
  
           
 
 
          |
125 | 99 | simprd 470 |
. . . . . . . . . . . . . . . 16
  
           
 
 
       |
126 | 124, 125 | eqbrtrd 4416 |
. . . . . . . . . . . . . . 15
  
           
 
 
               |
127 | 43 | rprege0d 11371 |
. . . . . . . . . . . . . . . 16
  
           
 
 
          |
128 | 45 | rprege0d 11371 |
. . . . . . . . . . . . . . . 16
  
           
 
 
    |
129 | | cxplt2 23722 |
. . . . . . . . . . . . . . . 16
     
 
 
                         |
130 | 127, 128,
119, 129 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
  
           
 
 
   
                |
131 | 126, 130 | mpbird 240 |
. . . . . . . . . . . . . 14
  
           
 
 
 
   |
132 | 40, 44, 46, 114, 131 | lttrd 9813 |
. . . . . . . . . . . . 13
  
           
 
 
 
       |
133 | 37, 132 | eqbrtrd 4416 |
. . . . . . . . . . . 12
  
           
 
 
         |
134 | 133 | 3expia 1233 |
. . . . . . . . . . 11
  
   
     
                 |
135 | 134 | anassrs 660 |
. . . . . . . . . 10
    
       
                 |
136 | 135 | ralrimiva 2809 |
. . . . . . . . 9
  

           
 
           |
137 | 27, 136 | sylan2br 484 |
. . . . . . . 8
  
   

     
                 |
138 | 137 | expr 626 |
. . . . . . 7
  

 

     
                  |
139 | | elpreima 6017 |
. . . . . . . . . . . . . . . . . . 19
                |
140 | 5, 6, 139 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
     
        |
141 | 140 | simprbi 471 |
. . . . . . . . . . . . . . . . 17
            |
142 | 141, 3 | eleq2s 2567 |
. . . . . . . . . . . . . . . 16
       |
143 | 142 | rpne0d 11369 |
. . . . . . . . . . . . . . 15
       |
144 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
           |
145 | | re0 13292 |
. . . . . . . . . . . . . . . . 17
     |
146 | 144, 145 | syl6eq 2521 |
. . . . . . . . . . . . . . . 16
       |
147 | 146 | necon3i 2675 |
. . . . . . . . . . . . . . 15
       |
148 | 143, 147 | syl 17 |
. . . . . . . . . . . . . 14
   |
149 | 34, 148 | 0cxpd 23734 |
. . . . . . . . . . . . 13
      |
150 | 149 | adantl 473 |
. . . . . . . . . . . 12
    
       |
151 | 150 | abs00bd 13431 |
. . . . . . . . . . 11
    
           |
152 | | simpllr 777 |
. . . . . . . . . . . 12
    
    |
153 | 152 | rpgt0d 11367 |
. . . . . . . . . . 11
    
    |
154 | 151, 153 | eqbrtrd 4416 |
. . . . . . . . . 10
    
           |
155 | | oveq1 6315 |
. . . . . . . . . . . 12
         |
156 | 155 | fveq2d 5883 |
. . . . . . . . . . 11
                 |
157 | 156 | breq1d 4405 |
. . . . . . . . . 10
                   |
158 | 154, 157 | syl5ibcom 228 |
. . . . . . . . 9
    
             |
159 | 158 | a1dd 46 |
. . . . . . . 8
    
            
 
            |
160 | 159 | ralrimdva 2812 |
. . . . . . 7
  

 

     
                  |
161 | 138, 160 | jaod 387 |
. . . . . 6
  

    
         
 
            |
162 | 26, 161 | sylbid 223 |
. . . . 5
  

 

     
                  |
163 | 162 | expimpd 614 |
. . . 4
 
    
     
                  |
164 | 23, 163 | syl5bi 225 |
. . 3
 
               
 
            |
165 | 164 | ralrimiv 2808 |
. 2
 
 
 
  
         
 
           |
166 | | breq2 4399 |
. . . . . 6
     
       |
167 | | breq2 4399 |
. . . . . 6
     
 
         |
168 | 166, 167 | anbi12d 725 |
. . . . 5
      
      
    
          |
169 | 168 | imbi1d 324 |
. . . 4
           
 
                                 |
170 | 169 | 2ralbidv 2832 |
. . 3
  
 
  
         
 
              
         
 
            |
171 | 170 | rspcev 3136 |
. 2
  
    
     
                                
 
           |
172 | 22, 165, 171 | syl2anc 673 |
1
 
 
               
 
           |