Step | Hyp | Ref
| Expression |
1 | | ltrelpr 7504 |
. . . . . . . 8
   |
2 | 1 | brel 4679 |
. . . . . . 7

    |
3 | 2 | simprd 114 |
. . . . . 6

  |
4 | | prop 7474 |
. . . . . 6
              |
5 | 3, 4 | syl 14 |
. . . . 5

             |
6 | | prnmaddl 7489 |
. . . . 5
                  

       |
7 | 5, 6 | sylan 283 |
. . . 4
 
     

       |
8 | 2 | simpld 112 |
. . . . . . . 8

  |
9 | | prop 7474 |
. . . . . . . 8
              |
10 | 8, 9 | syl 14 |
. . . . . . 7

             |
11 | | prarloc 7502 |
. . . . . . 7
                         
    |
12 | 10, 11 | sylan 283 |
. . . . . 6
 
            
    |
13 | 12 | ad2ant2r 509 |
. . . . 5
  
                         
    |
14 | | simplll 533 |
. . . . . . . . . . 11
                               |
15 | 14 | adantr 276 |
. . . . . . . . . 10
    
      
           
           |
16 | | simplrl 535 |
. . . . . . . . . 10
    
      
           
               |
17 | | elprnql 7480 |
. . . . . . . . . . 11
                    |
18 | 10, 17 | sylan 283 |
. . . . . . . . . 10
 
       |
19 | 15, 16, 18 | syl2anc 411 |
. . . . . . . . 9
    
      
           
           |
20 | | elprnql 7480 |
. . . . . . . . . . 11
                 
  |
21 | 5, 20 | sylan 283 |
. . . . . . . . . 10
 
    
  |
22 | 21 | ad3antrrr 492 |
. . . . . . . . 9
    
      
           
           |
23 | | nqtri3or 7395 |
. . . . . . . . 9
 
 
   |
24 | 19, 22, 23 | syl2anc 411 |
. . . . . . . 8
    
      
           
         
   |
25 | | ltexnqq 7407 |
. . . . . . . . . . . . 13
 
        |
26 | 19, 22, 25 | syl2anc 411 |
. . . . . . . . . . . 12
    
      
           
         
      |
27 | 26 | biimpa 296 |
. . . . . . . . . . 11
     
                  
               |
28 | | simprr 531 |
. . . . . . . . . . . 12
      
                  
              
    |
29 | 16 | ad2antrr 488 |
. . . . . . . . . . . . 13
      
                  
              
      |
30 | | simprl 529 |
. . . . . . . . . . . . . 14
      
                  
              
  |
31 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
    
      
           
             |
32 | | simplrr 536 |
. . . . . . . . . . . . . . . . . 18
    
      
           
               |
33 | | prcunqu 7484 |
. . . . . . . . . . . . . . . . . . 19
                              |
34 | 10, 33 | sylan 283 |
. . . . . . . . . . . . . . . . . 18
 
                 |
35 | 15, 32, 34 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
    
      
           
                     |
36 | 31, 35 | mpd 13 |
. . . . . . . . . . . . . . . 16
    
      
           
                 |
37 | 36 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
      
                  
              
        |
38 | 19 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
      
                  
              
  |
39 | | simplrl 535 |
. . . . . . . . . . . . . . . . . 18
                               |
40 | 39 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . 17
      
                  
              
  |
41 | | addcomnqg 7380 |
. . . . . . . . . . . . . . . . . 18
 
       |
42 | 41 | adantl 277 |
. . . . . . . . . . . . . . . . 17
                                                   |
43 | | addassnqg 7381 |
. . . . . . . . . . . . . . . . . 18
 
           |
44 | 43 | adantl 277 |
. . . . . . . . . . . . . . . . 17
                                                       |
45 | 38, 40, 30, 42, 44 | caov32d 6055 |
. . . . . . . . . . . . . . . 16
      
                  
              
          |
46 | | simplrr 536 |
. . . . . . . . . . . . . . . . . 18
                                     |
47 | 46 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . 17
      
                  
              
        |
48 | | oveq1 5882 |
. . . . . . . . . . . . . . . . . . 19
           |
49 | 48 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . 18
           
         |
50 | 28, 49 | syl 14 |
. . . . . . . . . . . . . . . . 17
      
                  
              
                  |
51 | 47, 50 | mpbird 167 |
. . . . . . . . . . . . . . . 16
      
                  
              
          |
52 | 45, 51 | eqeltrd 2254 |
. . . . . . . . . . . . . . 15
      
                  
              
          |
53 | | eleq1 2240 |
. . . . . . . . . . . . . . . . . 18
       
         |
54 | | oveq1 5882 |
. . . . . . . . . . . . . . . . . . 19
           |
55 | 54 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . 18
         
           |
56 | 53, 55 | anbi12d 473 |
. . . . . . . . . . . . . . . . 17
                      
            |
57 | 56 | spcegv 2826 |
. . . . . . . . . . . . . . . 16
      
                                  |
58 | 57 | anabsi5 579 |
. . . . . . . . . . . . . . 15
                                 |
59 | 37, 52, 58 | syl2anc 411 |
. . . . . . . . . . . . . 14
      
                  
              
                |
60 | | ltexprlem.1 |
. . . . . . . . . . . . . . 15
        
                
          |
61 | 60 | ltexprlemell 7597 |
. . . . . . . . . . . . . 14
     
                 |
62 | 30, 59, 61 | sylanbrc 417 |
. . . . . . . . . . . . 13
      
                  
              
      |
63 | 15, 8 | syl 14 |
. . . . . . . . . . . . . . 15
    
      
           
           |
64 | 63 | ad2antrr 488 |
. . . . . . . . . . . . . 14
      
                  
              
  |
65 | 60 | ltexprlempr 7607 |
. . . . . . . . . . . . . . . 16

  |
66 | 15, 65 | syl 14 |
. . . . . . . . . . . . . . 15
    
      
           
           |
67 | 66 | ad2antrr 488 |
. . . . . . . . . . . . . 14
      
                  
              
  |
68 | | df-iplp 7467 |
. . . . . . . . . . . . . . 15


            
                
       |
69 | | addclnq 7374 |
. . . . . . . . . . . . . . 15
 
     |
70 | 68, 69 | genpprecll 7513 |
. . . . . . . . . . . . . 14
 
      
    
           |
71 | 64, 67, 70 | syl2anc 411 |
. . . . . . . . . . . . 13
      
                  
              
                      |
72 | 29, 62, 71 | mp2and 433 |
. . . . . . . . . . . 12
      
                  
              
          |
73 | 28, 72 | eqeltrrd 2255 |
. . . . . . . . . . 11
      
                  
              
        |
74 | 27, 73 | rexlimddv 2599 |
. . . . . . . . . 10
     
                  
                  |
75 | 74 | ex 115 |
. . . . . . . . 9
    
      
           
                   |
76 | 14 | ad2antrr 488 |
. . . . . . . . . . 11
     
                  
            |
77 | | simpr 110 |
. . . . . . . . . . . 12
     
                  
            |
78 | 16 | adantr 276 |
. . . . . . . . . . . 12
     
                  
                |
79 | 77, 78 | eqeltrrd 2255 |
. . . . . . . . . . 11
     
                  
                |
80 | | ltaddpr 7596 |
. . . . . . . . . . . . 13
 

    |
81 | 8, 65, 80 | syl2anc 411 |
. . . . . . . . . . . 12

    |
82 | | ltprordil 7588 |
. . . . . . . . . . . . 13
  
            |
83 | 82 | sseld 3155 |
. . . . . . . . . . . 12
  
    
         |
84 | 81, 83 | syl 14 |
. . . . . . . . . . 11

    
         |
85 | 76, 79, 84 | sylc 62 |
. . . . . . . . . 10
     
                  
                  |
86 | 85 | ex 115 |
. . . . . . . . 9
    
      
           
         
         |
87 | | prcdnql 7483 |
. . . . . . . . . . . 12
                          |
88 | 10, 87 | sylan 283 |
. . . . . . . . . . 11
 
             |
89 | 15, 16, 88 | syl2anc 411 |
. . . . . . . . . 10
    
      
           
                 |
90 | 15, 89, 84 | sylsyld 58 |
. . . . . . . . 9
    
      
           
                   |
91 | 75, 86, 90 | 3jaod 1304 |
. . . . . . . 8
    
      
           
          
          |
92 | 24, 91 | mpd 13 |
. . . . . . 7
    
      
           
                 |
93 | 92 | ex 115 |
. . . . . 6
                                         |
94 | 93 | rexlimdvva 2602 |
. . . . 5
  
                                      |
95 | 13, 94 | mpd 13 |
. . . 4
  
                      |
96 | 7, 95 | rexlimddv 2599 |
. . 3
 
    
        |
97 | 96 | ex 115 |
. 2

    
         |
98 | 97 | ssrdv 3162 |
1

            |