Step | Hyp | Ref
| Expression |
1 | | ltrelsr 7728 |
. . . . 5
   |
2 | 1 | brel 4675 |
. . . 4

    |
3 | 2 | simprd 114 |
. . 3

  |
4 | 1 | brel 4675 |
. . . 4

    |
5 | 4 | simprd 114 |
. . 3

  |
6 | 3, 5 | anim12i 338 |
. 2
 
     |
7 | | df-nr 7717 |
. . 3
     |
8 | | breq2 4004 |
. . . . 5
               |
9 | 8 | anbi1d 465 |
. . . 4
                 
         |
10 | | oveq1 5876 |
. . . . 5
                         |
11 | 10 | breq2d 4012 |
. . . 4
                 
         |
12 | 9, 11 | imbi12d 234 |
. . 3
                                                |
13 | | breq2 4004 |
. . . . 5
               |
14 | 13 | anbi2d 464 |
. . . 4
                  |
15 | | oveq2 5877 |
. . . . 5
                |
16 | 15 | breq2d 4012 |
. . . 4
                  |
17 | 14, 16 | imbi12d 234 |
. . 3
        
           
         |
18 | | gt0srpr 7738 |
. . . . 5
     
  |
19 | | gt0srpr 7738 |
. . . . 5
     
  |
20 | 18, 19 | anbi12i 460 |
. . . 4
 
    
     
   |
21 | | ltexpri 7603 |
. . . . . . 7

     |
22 | | ltexpri 7603 |
. . . . . . . . 9

     |
23 | | addclpr 7527 |
. . . . . . . . . . . . . 14
 
     |
24 | 23 | adantl 277 |
. . . . . . . . . . . . 13
     
   
     
           |
25 | | simplrr 536 |
. . . . . . . . . . . . . . 15
      
 
     
   
    |
26 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
      
  |
27 | 26 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
      
 
     
   
  |
28 | | simplrl 535 |
. . . . . . . . . . . . . . . 16
      
 
     
   
  |
29 | 24, 27, 28 | caovcld 6022 |
. . . . . . . . . . . . . . 15
      
 
     
   
    |
30 | 25, 29 | eqeltrrd 2255 |
. . . . . . . . . . . . . 14
      
 
     
   
  |
31 | | simplrr 536 |
. . . . . . . . . . . . . . 15
   


 
    
  |
32 | 31 | adantr 276 |
. . . . . . . . . . . . . 14
      
 
     
   
  |
33 | | mulclpr 7562 |
. . . . . . . . . . . . . 14
 
     |
34 | 30, 32, 33 | syl2anc 411 |
. . . . . . . . . . . . 13
      
 
     
   
    |
35 | | simplrl 535 |
. . . . . . . . . . . . . . 15
   


 
       |
36 | 35 | adantr 276 |
. . . . . . . . . . . . . 14
      
 
     
   
  |
37 | | mulclpr 7562 |
. . . . . . . . . . . . . 14
 
     |
38 | 27, 36, 37 | syl2anc 411 |
. . . . . . . . . . . . 13
      
 
     
   
    |
39 | 24, 34, 38 | caovcld 6022 |
. . . . . . . . . . . 12
      
 
     
   
 
      |
40 | | simprl 529 |
. . . . . . . . . . . . 13
      
 
     
   
  |
41 | | mulclpr 7562 |
. . . . . . . . . . . . 13
 
     |
42 | 28, 40, 41 | syl2anc 411 |
. . . . . . . . . . . 12
      
 
     
   
    |
43 | | ltaddpr 7587 |
. . . . . . . . . . . 12
     
        
              |
44 | 39, 42, 43 | syl2anc 411 |
. . . . . . . . . . 11
      
 
     
   
 
        
 
     |
45 | | simprr 531 |
. . . . . . . . . . . . . . 15
      
 
     
   
    |
46 | | oveq12 5878 |
. . . . . . . . . . . . . . . 16
    
     
      |
47 | 46 | oveq1d 5884 |
. . . . . . . . . . . . . . 15
    
           
          
     |
48 | 25, 45, 47 | syl2anc 411 |
. . . . . . . . . . . . . 14
      
 
     
   
   
      
     
 
       |
49 | | distrprg 7578 |
. . . . . . . . . . . . . . . . . . 19
 
 
      
    |
50 | 27, 32, 40, 49 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . 18
      
 
     
   
      
     |
51 | | oveq2 5877 |
. . . . . . . . . . . . . . . . . . . 20
   
       |
52 | 51 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
  
   
      |
53 | 52 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
      
 
     
   
        |
54 | 50, 53 | eqtr3d 2212 |
. . . . . . . . . . . . . . . . 17
      
 
     
   
 
        |
55 | 54 | oveq1d 5884 |
. . . . . . . . . . . . . . . 16
      
 
     
   
   
      
     
 
       |
56 | | distrprg 7578 |
. . . . . . . . . . . . . . . . . . . 20
 
 
      
    |
57 | 56 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
     
   
     
        
          |
58 | | mulcomprg 7570 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
59 | 58 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
     
   
     
             |
60 | 57, 27, 28, 32, 24, 59 | caovdir2d 6045 |
. . . . . . . . . . . . . . . . . 18
      
 
     
   
 
    
     |
61 | 57, 27, 28, 40, 24, 59 | caovdir2d 6045 |
. . . . . . . . . . . . . . . . . 18
      
 
     
   
 
    
     |
62 | 60, 61 | oveq12d 5887 |
. . . . . . . . . . . . . . . . 17
      
 
     
   
   
          
 
 
       |
63 | | distrprg 7578 |
. . . . . . . . . . . . . . . . . 18
   
   
          
    |
64 | 29, 32, 40, 63 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
      
 
     
   
 
        
 
     |
65 | | mulclpr 7562 |
. . . . . . . . . . . . . . . . . . 19
 
     |
66 | 27, 32, 65 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
      
 
     
   
    |
67 | | mulclpr 7562 |
. . . . . . . . . . . . . . . . . . 19
 
     |
68 | 27, 40, 67 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
      
 
     
   
    |
69 | | mulclpr 7562 |
. . . . . . . . . . . . . . . . . . 19
 
     |
70 | 28, 32, 69 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
      
 
     
   
    |
71 | | addcomprg 7568 |
. . . . . . . . . . . . . . . . . . 19
 
       |
72 | 71 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
     
   
     
             |
73 | | addassprg 7569 |
. . . . . . . . . . . . . . . . . . 19
 
   
       |
74 | 73 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
     
   
     
                 |
75 | 66, 68, 70, 72, 74, 42, 24 | caov4d 6053 |
. . . . . . . . . . . . . . . . 17
      
 
     
   
   
      
       
 
 
       |
76 | 62, 64, 75 | 3eqtr4d 2220 |
. . . . . . . . . . . . . . . 16
      
 
     
   
 
        
 
 
       |
77 | 70, 38, 42, 72, 74 | caov12d 6050 |
. . . . . . . . . . . . . . . 16
      
 
     
   
 
    
     
 
       |
78 | 55, 76, 77 | 3eqtr4d 2220 |
. . . . . . . . . . . . . . 15
      
 
     
   
 
      
 
       |
79 | | oveq1 5876 |
. . . . . . . . . . . . . . . . . 18
     
     |
80 | 79 | adantl 277 |
. . . . . . . . . . . . . . . . 17
             |
81 | 80 | ad2antlr 489 |
. . . . . . . . . . . . . . . 16
      
 
     
   
 
      |
82 | 60, 81 | eqtr3d 2212 |
. . . . . . . . . . . . . . 15
      
 
     
   
 
        |
83 | 78, 82 | oveq12d 5887 |
. . . . . . . . . . . . . 14
      
 
     
   
   
      
         
         |
84 | 48, 83 | eqtr3d 2212 |
. . . . . . . . . . . . 13
      
 
     
   
 
    
         
         |
85 | | mulclpr 7562 |
. . . . . . . . . . . . . . . 16
 
     |
86 | 30, 36, 85 | syl2anc 411 |
. . . . . . . . . . . . . . 15
      
 
     
   
    |
87 | | addassprg 7569 |
. . . . . . . . . . . . . . 15
                
              |
88 | 86, 66, 70, 87 | syl3anc 1238 |
. . . . . . . . . . . . . 14
      
 
     
   
   
        
 
       |
89 | | addclpr 7527 |
. . . . . . . . . . . . . . . 16
          
    |
90 | 86, 66, 89 | syl2anc 411 |
. . . . . . . . . . . . . . 15
      
 
     
   
 
      |
91 | | addcomprg 7568 |
. . . . . . . . . . . . . . 15
     
            
              |
92 | 90, 70, 91 | syl2anc 411 |
. . . . . . . . . . . . . 14
      
 
     
   
   
        
 
       |
93 | 88, 92 | eqtr3d 2212 |
. . . . . . . . . . . . 13
      
 
     
   
 
    
     
 
       |
94 | 24, 38, 42 | caovcld 6022 |
. . . . . . . . . . . . . . 15
      
 
     
   
 
      |
95 | | addassprg 7569 |
. . . . . . . . . . . . . . 15
    
   
        
 
 
          
 
        |
96 | 70, 34, 94, 95 | syl3anc 1238 |
. . . . . . . . . . . . . 14
      
 
     
   
   
      
     
 
    
      |
97 | 70, 94, 34, 72, 74 | caov32d 6049 |
. . . . . . . . . . . . . 14
      
 
     
   
   
 
            
 
 
       |
98 | | addassprg 7569 |
. . . . . . . . . . . . . . . 16
                
              |
99 | 34, 38, 42, 98 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
      
 
     
   
   
        
 
       |
100 | 99 | oveq2d 5885 |
. . . . . . . . . . . . . 14
      
 
     
   
 
        
     
 
    
      |
101 | 96, 97, 100 | 3eqtr4d 2220 |
. . . . . . . . . . . . 13
      
 
     
   
   
 
          
   
         |
102 | 84, 93, 101 | 3eqtr3d 2218 |
. . . . . . . . . . . 12
      
 
     
   
 
    
     
   
         |
103 | 24, 39, 42 | caovcld 6022 |
. . . . . . . . . . . . 13
      
 
     
   
   
        |
104 | | addcanprg 7606 |
. . . . . . . . . . . . 13
       
         
          
     
   
          
     
         |
105 | 70, 90, 103, 104 | syl3anc 1238 |
. . . . . . . . . . . 12
      
 
     
   
   
 
            
 
              
 
      |
106 | 102, 105 | mpd 13 |
. . . . . . . . . . 11
      
 
     
   
 
        
 
     |
107 | 44, 106 | breqtrrd 4028 |
. . . . . . . . . 10
      
 
     
   
 
      
     |
108 | 107 | rexlimdvaa 2595 |
. . . . . . . . 9
   


 
                 
      |
109 | 22, 108 | syl5 32 |
. . . . . . . 8
   


 
         
           |
110 | 109 | rexlimdvaa 2595 |
. . . . . . 7
      
 



         
      |
111 | 21, 110 | syl5 32 |
. . . . . 6
      


 
      
       |
112 | 111 | impd 254 |
. . . . 5
      
     
      
     |
113 | | mulsrpr 7736 |
. . . . . . 7
      
          
    
       
     |
114 | 113 | breq2d 4012 |
. . . . . 6
      
           
     
             |
115 | | gt0srpr 7738 |
. . . . . 6
            
             
     |
116 | 114, 115 | bitrdi 196 |
. . . . 5
      
           
 
      
      |
117 | 112, 116 | sylibrd 169 |
. . . 4
      
                 |
118 | 20, 117 | biimtrid 152 |
. . 3
      
      
    
              |
119 | 7, 12, 17, 118 | 2ecoptocl 6617 |
. 2
 
         |
120 | 6, 119 | mpcom 36 |
1
 
     |