Step | Hyp | Ref
| Expression |
1 | | recexpr.1 |
. . . . . 6
                                |
2 | 1 | recexprlempr 7191 |
. . . . 5
   |
3 | | df-imp 7028 |
. . . . . 6
 
            
     
          
       |
4 | | mulclnq 6935 |
. . . . . 6
 
     |
5 | 3, 4 | genpelvl 7071 |
. . . . 5
 
        
                |
6 | 2, 5 | mpdan 412 |
. . . 4
       
                 |
7 | 1 | recexprlemell 7181 |
. . . . . . . 8
       
           |
8 | | ltrelnq 6924 |
. . . . . . . . . . . . . 14
   |
9 | 8 | brel 4490 |
. . . . . . . . . . . . 13

    |
10 | 9 | simprd 112 |
. . . . . . . . . . . 12

  |
11 | | prop 7034 |
. . . . . . . . . . . . . . . . . 18
              |
12 | | elprnql 7040 |
. . . . . . . . . . . . . . . . . 18
                    |
13 | 11, 12 | sylan 277 |
. . . . . . . . . . . . . . . . 17
 
       |
14 | | ltmnqi 6962 |
. . . . . . . . . . . . . . . . . 18
 
       |
15 | 14 | expcom 114 |
. . . . . . . . . . . . . . . . 17
         |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . . . 16
 
             |
17 | 16 | adantr 270 |
. . . . . . . . . . . . . . 15
       
         |
18 | | prltlu 7046 |
. . . . . . . . . . . . . . . . . . 19
                                |
19 | 11, 18 | syl3an1 1207 |
. . . . . . . . . . . . . . . . . 18
 
                   |
20 | 19 | 3expia 1145 |
. . . . . . . . . . . . . . . . 17
 
                     |
21 | 20 | adantr 270 |
. . . . . . . . . . . . . . . 16
       
                 |
22 | | ltmnqi 6962 |
. . . . . . . . . . . . . . . . . . . . 21
 
               |
23 | 22 | expcom 114 |
. . . . . . . . . . . . . . . . . . . 20
                 |
24 | 23 | adantr 270 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
25 | | mulcomnqg 6942 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
26 | | recidnq 6952 |
. . . . . . . . . . . . . . . . . . . . 21
         |
27 | 26 | adantr 270 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
28 | 25, 27 | breq12d 3858 |
. . . . . . . . . . . . . . . . . . 19
 
               |
29 | 24, 28 | sylibd 147 |
. . . . . . . . . . . . . . . . . 18
 
           |
30 | 29 | ancoms 264 |
. . . . . . . . . . . . . . . . 17
 
           |
31 | 13, 30 | sylan 277 |
. . . . . . . . . . . . . . . 16
       
           |
32 | 21, 31 | syld 44 |
. . . . . . . . . . . . . . 15
       
               |
33 | 17, 32 | anim12d 328 |
. . . . . . . . . . . . . 14
       
  
        
    
      |
34 | | ltsonq 6957 |
. . . . . . . . . . . . . . 15
 |
35 | 34, 8 | sotri 4827 |
. . . . . . . . . . . . . 14
             |
36 | 33, 35 | syl6 33 |
. . . . . . . . . . . . 13
       
  
        
     |
37 | 36 | exp4b 359 |
. . . . . . . . . . . 12
 
                       |
38 | 10, 37 | syl5 32 |
. . . . . . . . . . 11
 
                       |
39 | 38 | pm2.43d 49 |
. . . . . . . . . 10
 
                     |
40 | 39 | impd 251 |
. . . . . . . . 9
 
      
        
     |
41 | 40 | exlimdv 1747 |
. . . . . . . 8
 
        
              |
42 | 7, 41 | syl5bi 150 |
. . . . . . 7
 
               |
43 | | breq1 3848 |
. . . . . . . 8
   
     |
44 | 43 | biimprcd 158 |
. . . . . . 7
  
      |
45 | 42, 44 | syl6 33 |
. . . . . 6
 
            
    |
46 | 45 | expimpd 355 |
. . . . 5
           
       |
47 | 46 | rexlimdvv 2495 |
. . . 4
  
            
   |
48 | 6, 47 | sylbid 148 |
. . 3
           |
49 | | 1prl 7114 |
. . . 4
       |
50 | 49 | abeq2i 2198 |
. . 3
    
  |
51 | 48, 50 | syl6ibr 160 |
. 2
               |
52 | 51 | ssrdv 3031 |
1
             |