Step | Hyp | Ref
| Expression |
1 | | recexpr.1 |
. . . . . 6
                                |
2 | 1 | recexprlempr 7189 |
. . . . 5
   |
3 | | df-imp 7026 |
. . . . . 6
 
            
     
          
       |
4 | | mulclnq 6933 |
. . . . . 6
 
     |
5 | 3, 4 | genpelvu 7070 |
. . . . 5
 
        
                |
6 | 2, 5 | mpdan 412 |
. . . 4
       
                 |
7 | 1 | recexprlemelu 7180 |
. . . . . . . 8
       
           |
8 | | ltrelnq 6922 |
. . . . . . . . . . . . . 14
   |
9 | 8 | brel 4490 |
. . . . . . . . . . . . 13

    |
10 | 9 | simpld 110 |
. . . . . . . . . . . 12

  |
11 | | prop 7032 |
. . . . . . . . . . . . . . . . . 18
              |
12 | | elprnqu 7039 |
. . . . . . . . . . . . . . . . . 18
                    |
13 | 11, 12 | sylan 277 |
. . . . . . . . . . . . . . . . 17
 
       |
14 | | ltmnqi 6960 |
. . . . . . . . . . . . . . . . . 18
 
       |
15 | 14 | expcom 114 |
. . . . . . . . . . . . . . . . 17
         |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . . . 16
 
             |
17 | 16 | adantr 270 |
. . . . . . . . . . . . . . 15
       
         |
18 | | prltlu 7044 |
. . . . . . . . . . . . . . . . . . . 20
                                |
19 | 11, 18 | syl3an1 1207 |
. . . . . . . . . . . . . . . . . . 19
         
    
      |
20 | 19 | 3com23 1149 |
. . . . . . . . . . . . . . . . . 18
 
                   |
21 | 20 | 3expia 1145 |
. . . . . . . . . . . . . . . . 17
 
                     |
22 | 21 | adantr 270 |
. . . . . . . . . . . . . . . 16
       
                 |
23 | | ltmnqi 6960 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
24 | 23 | expcom 114 |
. . . . . . . . . . . . . . . . . . . 20
                 |
25 | 24 | adantr 270 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
26 | | recidnq 6950 |
. . . . . . . . . . . . . . . . . . . . 21
         |
27 | 26 | adantr 270 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
28 | | mulcomnqg 6940 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
29 | 27, 28 | breq12d 3858 |
. . . . . . . . . . . . . . . . . . 19
 
               |
30 | 25, 29 | sylibd 147 |
. . . . . . . . . . . . . . . . . 18
 
     
     |
31 | 30 | ancoms 264 |
. . . . . . . . . . . . . . . . 17
 
     
     |
32 | 13, 31 | sylan 277 |
. . . . . . . . . . . . . . . 16
       
     
     |
33 | 22, 32 | syld 44 |
. . . . . . . . . . . . . . 15
       
               |
34 | 17, 33 | anim12d 328 |
. . . . . . . . . . . . . 14
       
  
        
    
      |
35 | | ltsonq 6955 |
. . . . . . . . . . . . . . . 16
 |
36 | 35, 8 | sotri 4827 |
. . . . . . . . . . . . . . 15
 
           |
37 | 36 | ancoms 264 |
. . . . . . . . . . . . . 14
             |
38 | 34, 37 | syl6 33 |
. . . . . . . . . . . . 13
       
  
        
     |
39 | 38 | exp4b 359 |
. . . . . . . . . . . 12
 
                       |
40 | 10, 39 | syl5 32 |
. . . . . . . . . . 11
 
                       |
41 | 40 | pm2.43d 49 |
. . . . . . . . . 10
 
                     |
42 | 41 | impd 251 |
. . . . . . . . 9
 
      
        
     |
43 | 42 | exlimdv 1747 |
. . . . . . . 8
 
        
              |
44 | 7, 43 | syl5bi 150 |
. . . . . . 7
 
               |
45 | | breq2 3849 |
. . . . . . . 8
   
     |
46 | 45 | biimprcd 158 |
. . . . . . 7
  
      |
47 | 44, 46 | syl6 33 |
. . . . . 6
 
            
    |
48 | 47 | expimpd 355 |
. . . . 5
           
       |
49 | 48 | rexlimdvv 2495 |
. . . 4
  
            
   |
50 | 6, 49 | sylbid 148 |
. . 3
           |
51 | | 1pru 7113 |
. . . 4
       |
52 | 51 | abeq2i 2198 |
. . 3
    
  |
53 | 50, 52 | syl6ibr 160 |
. 2
               |
54 | 53 | ssrdv 3031 |
1
             |