Step | Hyp | Ref
| Expression |
1 | | recexpr.1 |
. . . . . 6
                                |
2 | 1 | recexprlempr 7631 |
. . . . 5
   |
3 | | df-imp 7468 |
. . . . . 6
 
            
     
          
       |
4 | | mulclnq 7375 |
. . . . . 6
 
     |
5 | 3, 4 | genpelvu 7512 |
. . . . 5
 
        
                |
6 | 2, 5 | mpdan 421 |
. . . 4
       
                 |
7 | 1 | recexprlemelu 7622 |
. . . . . . . 8
       
           |
8 | | ltrelnq 7364 |
. . . . . . . . . . . . . 14
   |
9 | 8 | brel 4679 |
. . . . . . . . . . . . 13

    |
10 | 9 | simpld 112 |
. . . . . . . . . . . 12

  |
11 | | prop 7474 |
. . . . . . . . . . . . . . . . . 18
              |
12 | | elprnqu 7481 |
. . . . . . . . . . . . . . . . . 18
                    |
13 | 11, 12 | sylan 283 |
. . . . . . . . . . . . . . . . 17
 
       |
14 | | ltmnqi 7402 |
. . . . . . . . . . . . . . . . . 18
 
       |
15 | 14 | expcom 116 |
. . . . . . . . . . . . . . . . 17
         |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . . . 16
 
             |
17 | 16 | adantr 276 |
. . . . . . . . . . . . . . 15
       
         |
18 | | prltlu 7486 |
. . . . . . . . . . . . . . . . . . . 20
                                |
19 | 11, 18 | syl3an1 1271 |
. . . . . . . . . . . . . . . . . . 19
         
    
      |
20 | 19 | 3com23 1209 |
. . . . . . . . . . . . . . . . . 18
 
                   |
21 | 20 | 3expia 1205 |
. . . . . . . . . . . . . . . . 17
 
                     |
22 | 21 | adantr 276 |
. . . . . . . . . . . . . . . 16
       
                 |
23 | | ltmnqi 7402 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
24 | 23 | expcom 116 |
. . . . . . . . . . . . . . . . . . . 20
                 |
25 | 24 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
26 | | recidnq 7392 |
. . . . . . . . . . . . . . . . . . . . 21
         |
27 | 26 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
28 | | mulcomnqg 7382 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
29 | 27, 28 | breq12d 4017 |
. . . . . . . . . . . . . . . . . . 19
 
               |
30 | 25, 29 | sylibd 149 |
. . . . . . . . . . . . . . . . . 18
 
     
     |
31 | 30 | ancoms 268 |
. . . . . . . . . . . . . . . . 17
 
     
     |
32 | 13, 31 | sylan 283 |
. . . . . . . . . . . . . . . 16
       
     
     |
33 | 22, 32 | syld 45 |
. . . . . . . . . . . . . . 15
       
               |
34 | 17, 33 | anim12d 335 |
. . . . . . . . . . . . . 14
       
  
        
    
      |
35 | | ltsonq 7397 |
. . . . . . . . . . . . . . . 16
 |
36 | 35, 8 | sotri 5025 |
. . . . . . . . . . . . . . 15
 
           |
37 | 36 | ancoms 268 |
. . . . . . . . . . . . . 14
             |
38 | 34, 37 | syl6 33 |
. . . . . . . . . . . . 13
       
  
        
     |
39 | 38 | exp4b 367 |
. . . . . . . . . . . 12
 
                       |
40 | 10, 39 | syl5 32 |
. . . . . . . . . . 11
 
                       |
41 | 40 | pm2.43d 50 |
. . . . . . . . . 10
 
                     |
42 | 41 | impd 254 |
. . . . . . . . 9
 
      
        
     |
43 | 42 | exlimdv 1819 |
. . . . . . . 8
 
        
              |
44 | 7, 43 | biimtrid 152 |
. . . . . . 7
 
               |
45 | | breq2 4008 |
. . . . . . . 8
   
     |
46 | 45 | biimprcd 160 |
. . . . . . 7
  
      |
47 | 44, 46 | syl6 33 |
. . . . . 6
 
            
    |
48 | 47 | expimpd 363 |
. . . . 5
           
       |
49 | 48 | rexlimdvv 2601 |
. . . 4
  
            
   |
50 | 6, 49 | sylbid 150 |
. . 3
           |
51 | | 1pru 7555 |
. . . 4
       |
52 | 51 | abeq2i 2288 |
. . 3
    
  |
53 | 50, 52 | imbitrrdi 162 |
. 2
               |
54 | 53 | ssrdv 3162 |
1
             |