Step | Hyp | Ref
| Expression |
1 | | eldmg 5049 |
. . . 4
      
    
           |
2 | 1 | ibi 249 |
. . 3
                |
3 | | ulmcau.z |
. . . . . . . 8
     |
4 | | ulmcau.m |
. . . . . . . . 9
   |
5 | 4 | ad2antrr 737 |
. . . . . . . 8
          

  |
6 | | ulmcau.f |
. . . . . . . . 9
         |
7 | 6 | ad2antrr 737 |
. . . . . . . 8
          
         |
8 | | eqidd 2463 |
. . . . . . . 8
                                  |
9 | | eqidd 2463 |
. . . . . . . 8
             
          |
10 | | simplr 767 |
. . . . . . . 8
          
          |
11 | | rphalfcl 11356 |
. . . . . . . . 9

    |
12 | 11 | adantl 472 |
. . . . . . . 8
          
     |
13 | 3, 5, 7, 8, 9, 10,
12 | ulmi 23390 |
. . . . . . 7
          
 

     
                      |
14 | | simpr 467 |
. . . . . . . . . . 11
             
  |
15 | 14, 3 | syl6eleq 2550 |
. . . . . . . . . 10
             
      |
16 | | eluzelz 11197 |
. . . . . . . . . 10
    
  |
17 | | uzid 11202 |
. . . . . . . . . 10
       |
18 | | fveq2 5888 |
. . . . . . . . . . . . . . . 16
           |
19 | 18 | fveq1d 5890 |
. . . . . . . . . . . . . . 15
                   |
20 | 19 | oveq1d 6330 |
. . . . . . . . . . . . . 14
                               |
21 | 20 | fveq2d 5892 |
. . . . . . . . . . . . 13
                                       |
22 | 21 | breq1d 4426 |
. . . . . . . . . . . 12
                     
                       |
23 | 22 | ralbidv 2839 |
. . . . . . . . . . 11
  
                   

                       |
24 | 23 | rspcv 3158 |
. . . . . . . . . 10
    
 
     
                                            |
25 | 15, 16, 17, 24 | 4syl 19 |
. . . . . . . . 9
             
 
     
                                            |
26 | | r19.26 2929 |
. . . . . . . . . . . . . . 15
 
                                         
 
                   

                       |
27 | 7 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
        |
28 | 27 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
    
        |
29 | | elmapi 7519 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
              
    
          |
31 | 30 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . . . . 21
     
              
           |
32 | | ulmcl 23385 |
. . . . . . . . . . . . . . . . . . . . . . 23
              |
33 | 32 | ad4antlr 744 |
. . . . . . . . . . . . . . . . . . . . . 22
              
    
      |
34 | 33 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . . . . 21
     
              
       |
35 | 31, 34 | abssubd 13564 |
. . . . . . . . . . . . . . . . . . . 20
     
              
                                       |
36 | 35 | breq1d 4426 |
. . . . . . . . . . . . . . . . . . 19
     
              
                     
                       |
37 | 36 | biimpd 212 |
. . . . . . . . . . . . . . . . . 18
     
              
                                             |
38 | 3 | uztrn2 11205 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
39 | | ffvelrn 6043 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
         |
40 | 7, 38, 39 | syl2an 484 |
. . . . . . . . . . . . . . . . . . . . . 22
                            |
41 | 40 | anassrs 658 |
. . . . . . . . . . . . . . . . . . . . 21
              
    
        |
42 | | elmapi 7519 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
              
    
          |
44 | 43 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . . 19
     
              
           |
45 | | rpre 11337 |
. . . . . . . . . . . . . . . . . . . 20

  |
46 | 45 | ad4antlr 744 |
. . . . . . . . . . . . . . . . . . 19
     
              
   |
47 | | abs3lem 13450 |
. . . . . . . . . . . . . . . . . . 19
                                                                                               |
48 | 44, 31, 34, 46, 47 | syl22anc 1277 |
. . . . . . . . . . . . . . . . . 18
     
              
                                                                     |
49 | 37, 48 | sylan2d 489 |
. . . . . . . . . . . . . . . . 17
     
              
                                                                     |
50 | 49 | ancomsd 460 |
. . . . . . . . . . . . . . . 16
     
              
                                                                     |
51 | 50 | ralimdva 2808 |
. . . . . . . . . . . . . . 15
              
    
 
                                          
                         |
52 | 26, 51 | syl5bir 226 |
. . . . . . . . . . . . . 14
              
    
  
                    
                     
                         |
53 | 52 | expdimp 443 |
. . . . . . . . . . . . 13
     
              

                    
 
                   

                         |
54 | 53 | an32s 818 |
. . . . . . . . . . . 12
     
          
                         
 
                   

                         |
55 | 54 | ralimdva 2808 |
. . . . . . . . . . 11
              

                    
 
     
                          
                         |
56 | 55 | ex 440 |
. . . . . . . . . 10
             
 
                   
 
     
                          
                          |
57 | 56 | com23 81 |
. . . . . . . . 9
             
 
     
                     
                          
                          |
58 | 25, 57 | mpdd 41 |
. . . . . . . 8
             
 
     
                          
                         |
59 | 58 | reximdva 2874 |
. . . . . . 7
          
         
                    
      
                         |
60 | 13, 59 | mpd 15 |
. . . . . 6
          
 

     
                        |
61 | 60 | ralrimiva 2814 |
. . . . 5
 
                
                        |
62 | 61 | ex 440 |
. . . 4
         

      
                         |
63 | 62 | exlimdv 1790 |
. . 3
                  
                         |
64 | 2, 63 | syl5 33 |
. 2
         
     
                         |
65 | | ulmrel 23382 |
. . . 4
      |
66 | | ulmcau.s |
. . . . . . . . . 10
   |
67 | 3, 4, 66, 6 | ulmcaulem 23398 |
. . . . . . . . 9
    
     
                        
           
                         |
68 | 67 | biimpa 491 |
. . . . . . . 8
 
        
                       

      
     
                        |
69 | | rphalfcl 11356 |
. . . . . . . 8

    |
70 | | breq2 4420 |
. . . . . . . . . . . . 13
                         
                           |
71 | 70 | ralbidv 2839 |
. . . . . . . . . . . 12
    
                     

                           |
72 | 71 | 2ralbidv 2844 |
. . . . . . . . . . 11
    
     
     
                                  
                           |
73 | 72 | rexbidv 2913 |
. . . . . . . . . 10
    

     
     
                       
           
                           |
74 | | ralcom 2963 |
. . . . . . . . . . . . . 14
 

                             
     
                          |
75 | | fveq2 5888 |
. . . . . . . . . . . . . . 15
           |
76 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . 20
                   |
77 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . 20
                   |
78 | 76, 77 | oveq12d 6333 |
. . . . . . . . . . . . . . . . . . 19
                                       |
79 | 78 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . 18
                                               |
80 | 79 | breq1d 4426 |
. . . . . . . . . . . . . . . . 17
                         
                           |
81 | 80 | cbvralv 3031 |
. . . . . . . . . . . . . . . 16
 
                                                   |
82 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . 21
           |
83 | 82 | fveq1d 5890 |
. . . . . . . . . . . . . . . . . . . 20
                   |
84 | 83 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . 19
                                       |
85 | 84 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . 18
                                               |
86 | 85 | breq1d 4426 |
. . . . . . . . . . . . . . . . 17
                         
                           |
87 | 86 | ralbidv 2839 |
. . . . . . . . . . . . . . . 16
  
                       

                           |
88 | 81, 87 | syl5bb 265 |
. . . . . . . . . . . . . . 15
  
                       

                           |
89 | 75, 88 | raleqbidv 3013 |
. . . . . . . . . . . . . 14
  
     
                              
                           |
90 | 74, 89 | syl5bb 265 |
. . . . . . . . . . . . 13
  

                            
      
                           |
91 | 90 | cbvralv 3031 |
. . . . . . . . . . . 12
 
     
                             
      
     
                          |
92 | | fveq2 5888 |
. . . . . . . . . . . . 13
           |
93 | 92 | raleqdv 3005 |
. . . . . . . . . . . 12
  
     
     
                        
     
     
                           |
94 | 91, 93 | syl5bb 265 |
. . . . . . . . . . 11
  
     

                             
     
     
                           |
95 | 94 | cbvrexv 3032 |
. . . . . . . . . 10
  
     
                             

      
     
                          |
96 | 73, 95 | syl6bbr 271 |
. . . . . . . . 9
    

     
     
                       
     
                                 |
97 | 96 | rspccva 3161 |
. . . . . . . 8
    
           
                         
      

                               |
98 | 68, 69, 97 | syl2an 484 |
. . . . . . 7
   

      
                      
 

     

                               |
99 | 3 | uztrn2 11205 |
. . . . . . . . . . 11
 
       |
100 | | eqid 2462 |
. . . . . . . . . . . . . 14
         |
101 | | eluzelz 11197 |
. . . . . . . . . . . . . . . 16
    
  |
102 | 101, 3 | eleq2s 2558 |
. . . . . . . . . . . . . . 15
   |
103 | 102 | ad2antlr 738 |
. . . . . . . . . . . . . 14
       
     
                      
     |
104 | 69 | adantl 472 |
. . . . . . . . . . . . . . 15
   

      
                      
     |
105 | 104 | ad2antrr 737 |
. . . . . . . . . . . . . 14
       
     
                      
       |
106 | | simplr 767 |
. . . . . . . . . . . . . . . 16
       
     
                      
     |
107 | 3 | uztrn2 11205 |
. . . . . . . . . . . . . . . 16
 
    
  |
108 | 106, 107 | sylan 478 |
. . . . . . . . . . . . . . 15
     
        
                      



    
  |
109 | | fveq2 5888 |
. . . . . . . . . . . . . . . . 17
           |
110 | 109 | fveq1d 5890 |
. . . . . . . . . . . . . . . 16
                   |
111 | | eqid 2462 |
. . . . . . . . . . . . . . . 16
                     |
112 | | fvex 5898 |
. . . . . . . . . . . . . . . 16
         |
113 | 110, 111,
112 | fvmpt 5971 |
. . . . . . . . . . . . . . 15
                         |
114 | 108, 113 | syl 17 |
. . . . . . . . . . . . . 14
     
        
                      



    
                        |
115 | 6 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
        
                               |
116 | 115 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

      
                      
         |
117 | | elmapi 7519 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

      
                      
           |
119 | 118 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
     
      
                      


          |
120 | 119 | an32s 818 |
. . . . . . . . . . . . . . . . . . . . 21
     
      
                      


          |
121 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
122 | 120, 121 | fmptd 6069 |
. . . . . . . . . . . . . . . . . . . 20
   

      
                      
                 |
123 | 122 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . . 19
     
      
                      


                |
124 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
125 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
126 | 124, 125 | oveq12d 6333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                       |
127 | 126 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                               |
128 | 127 | breq1d 4426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                       
                         |
129 | 128 | rspcv 3158 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
                                               |
130 | 129 | ralimdv 2810 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
     
                     
                               |
131 | 130 | reximdv 2873 |
. . . . . . . . . . . . . . . . . . . . . . 23
  

     
                     

                               |
132 | 131 | ralimdv 2810 |
. . . . . . . . . . . . . . . . . . . . . 22
  

      
                                                       |
133 | 132 | impcom 436 |
. . . . . . . . . . . . . . . . . . . . 21
    
     
                     

                                |
134 | 133 | adantll 725 |
. . . . . . . . . . . . . . . . . . . 20
   

      
                      
   
                             |
135 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                               |
136 | 135 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                                               |
137 | 136 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                                                       |
138 | 137 | breq1d 4426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                                         |
139 | 138 | cbvralv 3031 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                                      
                                          |
140 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                               |
141 | 140 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                                               |
142 | 141 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                                                       |
143 | 142 | breq1d 4426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                                         |
144 | 92, 143 | raleqbidv 3013 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
                                                                                  |
145 | 139, 144 | syl5bb 265 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
                                                                                  |
146 | 145 | cbvrexv 3032 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
                                      

                                          |
147 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
148 | 147 | fveq1d 5890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   |
149 | | fvex 5898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
150 | 148, 121,
149 | fvmpt 5971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                         |
151 | 38, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
                             |
152 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
153 | 152 | fveq1d 5890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   |
154 | | fvex 5898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
155 | 153, 121,
154 | fvmpt 5971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                         |
156 | 155 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
                             |
157 | 151, 156 | oveq12d 6333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
                                                       |
158 | 157 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                                                               |
159 | 158 | breq1d 4426 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                                                                 |
160 | 159 | ralbidva 2836 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
                                                                      |
161 | 160 | rexbiia 2900 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
                                      

                              |
162 | 146, 161 | bitri 257 |
. . . . . . . . . . . . . . . . . . . . . 22
  
                                      

                              |
163 | | breq2 4420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       
                         |
164 | 163 | ralbidv 2839 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
                          
                               |
165 | 164 | rexbidv 2913 |
. . . . . . . . . . . . . . . . . . . . . 22
  

                          

                               |
166 | 162, 165 | syl5bb 265 |
. . . . . . . . . . . . . . . . . . . . 21
  

                                        
                              |
167 | 166 | cbvralv 3031 |
. . . . . . . . . . . . . . . . . . . 20
 

                                          
                             |
168 | 134, 167 | sylibr 217 |
. . . . . . . . . . . . . . . . . . 19
   

      
                      
   
                                         |
169 | | fvex 5898 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
170 | 3, 169 | eqeltri 2536 |
. . . . . . . . . . . . . . . . . . . . 21
 |
171 | 170 | mptex 6161 |
. . . . . . . . . . . . . . . . . . . 20
           |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
   

      
                      
             |
173 | 3, 123, 168, 172 | caucvg 13794 |
. . . . . . . . . . . . . . . . . 18
   

      
                      
            |
174 | 173 | ralrimiva 2814 |
. . . . . . . . . . . . . . . . 17
 
        
                       

          |
175 | 174 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
     
      
                      

  
          |
176 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . 19
                   |
177 | 176 | mpteq2dv 4504 |
. . . . . . . . . . . . . . . . . 18
                       |
178 | 177 | eleq1d 2524 |
. . . . . . . . . . . . . . . . 17
                        |
179 | 178 | rspccva 3161 |
. . . . . . . . . . . . . . . 16
   
                     |
180 | 175, 179 | sylan 478 |
. . . . . . . . . . . . . . 15
       
     
                      
              |
181 | | climdm 13667 |
. . . . . . . . . . . . . . 15
          

          
            |
182 | 180, 181 | sylib 201 |
. . . . . . . . . . . . . 14
       
     
                      
                           |
183 | 100, 103,
105, 114, 182 | climi2 13624 |
. . . . . . . . . . . . 13
       
     
                      
         
                
                  |
184 | 100 | r19.29uz 13462 |
. . . . . . . . . . . . . . 15
                                
                                        
     
                                                             |
185 | 100 | r19.2uz 13463 |
. . . . . . . . . . . . . . 15
                                                 
                                                           
                   |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . 14
                                
                                        
                                         
                   |
187 | 6 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . 20
   

      
                      
         |
188 | 187 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . . 19
     
      
                      

         |
189 | | elmapi 7519 |
. . . . . . . . . . . . . . . . . . 19
                 |
190 | 188, 189 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     
      
                      

           |
191 | 190 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . 17
       
     
                      
             |
192 | 191 | adantr 471 |
. . . . . . . . . . . . . . . 16
     
        
                      



    
          |
193 | | climcl 13612 |
. . . . . . . . . . . . . . . . . 18
                                     |
194 | 182, 193 | syl 17 |
. . . . . . . . . . . . . . . . 17
       
     
                      
                 |
195 | 194 | adantr 471 |
. . . . . . . . . . . . . . . 16
     
        
                      



    
              |
196 | 6 | ad5antr 745 |
. . . . . . . . . . . . . . . . . . 19
     
        
                      



    
        |
197 | 196, 108 | ffvelrnd 6046 |
. . . . . . . . . . . . . . . . . 18
     
        
                      



    
        |
198 | | elmapi 7519 |
. . . . . . . . . . . . . . . . . 18
                 |
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . . . . . 17
     
        
                      



    
          |
200 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
     
        
                      



    
  |
201 | 199, 200 | ffvelrnd 6046 |
. . . . . . . . . . . . . . . 16
     
        
                      



    
          |
202 | | rpre 11337 |
. . . . . . . . . . . . . . . . 17

  |
203 | 202 | ad4antlr 744 |
. . . . . . . . . . . . . . . 16
     
        
                      



    
  |
204 | | abs3lem 13450 |
. . . . . . . . . . . . . . . 16
            
                                                                                                          |
205 | 192, 195,
201, 203, 204 | syl22anc 1277 |
. . . . . . . . . . . . . . 15
     
        
                      



    
                                     
                                              |
206 | 205 | rexlimdva 2891 |
. . . . . . . . . . . . . 14
       
     
                      
    
                                         
                                              |
207 | 186, 206 | syl5 33 |
. . . . . . . . . . . . 13
       
     
                      
                                                                                                         |
208 | 183, 207 | mpan2d 685 |
. . . . . . . . . . . 12
       
     
                      
    
                                                          |
209 | 208 | ralimdva 2808 |
. . . . . . . . . . 11
     
      
                      

                                 
           
                 |
210 | 99, 209 | sylan2 481 |
. . . . . . . . . 10
     
      
                      
 
     
 

                                         
                 |
211 | 210 | anassrs 658 |
. . . . . . . . 9
       
     
                      
      
 

                                         
                 |
212 | 211 | ralimdva 2808 |
. . . . . . . 8
     
      
                      

        

                                   
           
                 |
213 | 212 | reximdva 2874 |
. . . . . . 7
   

      
                      
         

                             
      
           
                 |
214 | 98, 213 | mpd 15 |
. . . . . 6
   

      
                      
 

     
                            |
215 | 214 | ralrimiva 2814 |
. . . . 5
 
        
                       

      
           
                |
216 | 4 | adantr 471 |
. . . . . 6
 
        
                      
  |
217 | | eqidd 2463 |
. . . . . 6
   

      
                       
                    |
218 | 177 | fveq2d 5892 |
. . . . . . . 8
              
            |
219 | | eqid 2462 |
. . . . . . . 8
                
            |
220 | | fvex 5898 |
. . . . . . . 8
             |
221 | 218, 219,
220 | fvmpt 5971 |
. . . . . . 7
    
                            |
222 | 221 | adantl 472 |
. . . . . 6
   

      
                      
                                 |
223 | | climdm 13667 |
. . . . . . . . 9
          

          
            |
224 | 173, 223 | sylib 201 |
. . . . . . . 8
   

      
                      
                         |
225 | | climcl 13612 |
. . . . . . . 8
                                     |
226 | 224, 225 | syl 17 |
. . . . . . 7
   

     |