Step | Hyp | Ref
| Expression |
1 | | recexpr.1 |
. . . . . 6
                                |
2 | 1 | recexprlempr 7254 |
. . . . 5
   |
3 | | df-imp 7091 |
. . . . . 6
 
            
     
          
       |
4 | | mulclnq 6998 |
. . . . . 6
 
     |
5 | 3, 4 | genpelvu 7135 |
. . . . 5
 
        
                |
6 | 2, 5 | mpdan 413 |
. . . 4
       
                 |
7 | 1 | recexprlemelu 7245 |
. . . . . . . 8
       
           |
8 | | ltrelnq 6987 |
. . . . . . . . . . . . . 14
   |
9 | 8 | brel 4505 |
. . . . . . . . . . . . 13

    |
10 | 9 | simpld 111 |
. . . . . . . . . . . 12

  |
11 | | prop 7097 |
. . . . . . . . . . . . . . . . . 18
              |
12 | | elprnqu 7104 |
. . . . . . . . . . . . . . . . . 18
                    |
13 | 11, 12 | sylan 278 |
. . . . . . . . . . . . . . . . 17
 
       |
14 | | ltmnqi 7025 |
. . . . . . . . . . . . . . . . . 18
 
       |
15 | 14 | expcom 115 |
. . . . . . . . . . . . . . . . 17
         |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . . . 16
 
             |
17 | 16 | adantr 271 |
. . . . . . . . . . . . . . 15
       
         |
18 | | prltlu 7109 |
. . . . . . . . . . . . . . . . . . . 20
                                |
19 | 11, 18 | syl3an1 1208 |
. . . . . . . . . . . . . . . . . . 19
         
    
      |
20 | 19 | 3com23 1150 |
. . . . . . . . . . . . . . . . . 18
 
                   |
21 | 20 | 3expia 1146 |
. . . . . . . . . . . . . . . . 17
 
                     |
22 | 21 | adantr 271 |
. . . . . . . . . . . . . . . 16
       
                 |
23 | | ltmnqi 7025 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
24 | 23 | expcom 115 |
. . . . . . . . . . . . . . . . . . . 20
                 |
25 | 24 | adantr 271 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
26 | | recidnq 7015 |
. . . . . . . . . . . . . . . . . . . . 21
         |
27 | 26 | adantr 271 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
28 | | mulcomnqg 7005 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
29 | 27, 28 | breq12d 3866 |
. . . . . . . . . . . . . . . . . . 19
 
               |
30 | 25, 29 | sylibd 148 |
. . . . . . . . . . . . . . . . . 18
 
     
     |
31 | 30 | ancoms 265 |
. . . . . . . . . . . . . . . . 17
 
     
     |
32 | 13, 31 | sylan 278 |
. . . . . . . . . . . . . . . 16
       
     
     |
33 | 22, 32 | syld 45 |
. . . . . . . . . . . . . . 15
       
               |
34 | 17, 33 | anim12d 329 |
. . . . . . . . . . . . . 14
       
  
        
    
      |
35 | | ltsonq 7020 |
. . . . . . . . . . . . . . . 16
 |
36 | 35, 8 | sotri 4842 |
. . . . . . . . . . . . . . 15
 
           |
37 | 36 | ancoms 265 |
. . . . . . . . . . . . . 14
             |
38 | 34, 37 | syl6 33 |
. . . . . . . . . . . . 13
       
  
        
     |
39 | 38 | exp4b 360 |
. . . . . . . . . . . 12
 
                       |
40 | 10, 39 | syl5 32 |
. . . . . . . . . . 11
 
                       |
41 | 40 | pm2.43d 50 |
. . . . . . . . . 10
 
                     |
42 | 41 | impd 252 |
. . . . . . . . 9
 
      
        
     |
43 | 42 | exlimdv 1748 |
. . . . . . . 8
 
        
              |
44 | 7, 43 | syl5bi 151 |
. . . . . . 7
 
               |
45 | | breq2 3857 |
. . . . . . . 8
   
     |
46 | 45 | biimprcd 159 |
. . . . . . 7
  
      |
47 | 44, 46 | syl6 33 |
. . . . . 6
 
            
    |
48 | 47 | expimpd 356 |
. . . . 5
           
       |
49 | 48 | rexlimdvv 2498 |
. . . 4
  
            
   |
50 | 6, 49 | sylbid 149 |
. . 3
           |
51 | | 1pru 7178 |
. . . 4
       |
52 | 51 | abeq2i 2199 |
. . 3
    
  |
53 | 50, 52 | syl6ibr 161 |
. 2
               |
54 | 53 | ssrdv 3034 |
1
             |