Step | Hyp | Ref
| Expression |
1 | | ltrelsr 6666 |
. . . 4
   |
2 | 1 | brel 4335 |
. . 3
     |
3 | 2 | simprd 107 |
. 2
   |
4 | | df-nr 6655 |
. . 3
     |
5 | | breq2 3759 |
. . . 4
      
        |
6 | | oveq1 5462 |
. . . . . . 7
            
    |
7 | 6 | eqeq1d 2045 |
. . . . . 6
             


   |
8 | 7 | anbi2d 437 |
. . . . 5
              
   
    |
9 | 8 | rexbidv 2321 |
. . . 4
        
      
 



    |
10 | 5, 9 | imbi12d 223 |
. . 3
              
      
            |
11 | | gt0srpr 6676 |
. . . . 5
        |
12 | | ltexpri 6587 |
. . . . 5

  
  |
13 | 11, 12 | sylbi 114 |
. . . 4
      
    |
14 | | recexpr 6610 |
. . . . . . 7
 
    |
15 | 14 | adantl 262 |
. . . . . 6
   
   
  |
16 | | 1pr 6535 |
. . . . . . . . . . . . . 14
 |
17 | | addclpr 6520 |
. . . . . . . . . . . . . 14
   
   |
18 | 16, 17 | mpan2 401 |
. . . . . . . . . . . . 13
     |
19 | | enrex 6665 |
. . . . . . . . . . . . . 14
 |
20 | 19, 4 | ecopqsi 6097 |
. . . . . . . . . . . . 13
   
     
    |
21 | 18, 16, 20 | sylancl 392 |
. . . . . . . . . . . 12
     
    |
22 | 21 | adantl 262 |
. . . . . . . . . . 11
 
          |
23 | 22 | ad2antlr 458 |
. . . . . . . . . 10
   


    
             |
24 | | simprr 484 |
. . . . . . . . . . . 12
         |
25 | 24 | adantr 261 |
. . . . . . . . . . 11
   


    
   
  |
26 | | ltaddpr 6571 |
. . . . . . . . . . . . . 14
 

    |
27 | 16, 26 | mpan 400 |
. . . . . . . . . . . . 13
     |
28 | | addcomprg 6554 |
. . . . . . . . . . . . . 14
 
  
    |
29 | 16, 28 | mpan 400 |
. . . . . . . . . . . . 13
       |
30 | 27, 29 | breqtrd 3779 |
. . . . . . . . . . . 12
     |
31 | | gt0srpr 6676 |
. . . . . . . . . . . 12
       
    |
32 | 30, 31 | sylibr 137 |
. . . . . . . . . . 11
         |
33 | 25, 32 | syl 14 |
. . . . . . . . . 10
   


    
            |
34 | 18, 16 | jctir 296 |
. . . . . . . . . . . . . . . 16
  
    |
35 | 34 | anim2i 324 |
. . . . . . . . . . . . . . 15
   
     
     |
36 | 35 | adantr 261 |
. . . . . . . . . . . . . 14
   

  
               |
37 | | mulsrpr 6674 |
. . . . . . . . . . . . . 14
                   
 
   
   
       
      |
38 | 36, 37 | syl 14 |
. . . . . . . . . . . . 13
   

  
               
 
   
   
       
      |
39 | 38 | adantlrl 451 |
. . . . . . . . . . . 12
   


    
              
 
   
   
       
      |
40 | | oveq1 5462 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
41 | 40 | eqcomd 2042 |
. . . . . . . . . . . . . . . . . . . 20
       
   |
42 | 41 | ad2antll 460 |
. . . . . . . . . . . . . . . . . . 19
   


    
    
       |
43 | | mulcomprg 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
    |
44 | 43 | 3adant2 922 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
45 | | mulcomprg 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
    |
46 | 45 | 3adant1 921 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
47 | 44, 46 | oveq12d 5473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  
      
     |
48 | | distrprg 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
             |
49 | 48 | 3coml 1110 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
             |
50 | | simp3 905 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
51 | | addclpr 6520 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
  |
52 | 51 | 3adant3 923 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     |
53 | | mulcomprg 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
  
         |
54 | 50, 52, 53 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
           |
55 | 47, 49, 54 | 3eqtr2rd 2076 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  
    
     |
56 | 55 | adantl 262 |
. . . . . . . . . . . . . . . . . . . . . 22
   


  
     
 
      |
57 | | simplr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
58 | | simprl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
59 | 56, 57, 58, 24 | caovdird 5621 |
. . . . . . . . . . . . . . . . . . . . 21
          
 
      |
60 | | oveq2 5463 |
. . . . . . . . . . . . . . . . . . . . 21
    
          |
61 | 59, 60 | sylan9eq 2089 |
. . . . . . . . . . . . . . . . . . . 20
   


  
        
   |
62 | 61 | adantrr 448 |
. . . . . . . . . . . . . . . . . . 19
   


    
          
   |
63 | 42, 62 | eqtrd 2069 |
. . . . . . . . . . . . . . . . . 18
   


    
    
       |
64 | 63 | oveq1d 5470 |
. . . . . . . . . . . . . . . . 17
   


    
                            |
65 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . . . . 20
 
  
  |
66 | 57, 24, 65 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . 19
        
  |
67 | 16 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
         |
68 | | simpll 481 |
. . . . . . . . . . . . . . . . . . . . 21
         |
69 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . . . . . 21
   
   |
70 | 68, 16, 69 | sylancl 392 |
. . . . . . . . . . . . . . . . . . . 20
           |
71 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . . . . . 21
   
   |
72 | 57, 16, 71 | sylancl 392 |
. . . . . . . . . . . . . . . . . . . 20
           |
73 | | addclpr 6520 |
. . . . . . . . . . . . . . . . . . . 20
   
    
      |
74 | 70, 72, 73 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . 19
               |
75 | | addcomprg 6554 |
. . . . . . . . . . . . . . . . . . . 20
 
  
    |
76 | 75 | adantl 262 |
. . . . . . . . . . . . . . . . . . 19
   


  
   
    |
77 | | addassprg 6555 |
. . . . . . . . . . . . . . . . . . . 20
 
  
        |
78 | 77 | adantl 262 |
. . . . . . . . . . . . . . . . . . 19
   


  
     
      |
79 | 66, 67, 74, 76, 78 | caov32d 5623 |
. . . . . . . . . . . . . . . . . 18
             
                   |
80 | 79 | adantr 261 |
. . . . . . . . . . . . . . . . 17
   


    
       
                      |
81 | 64, 80 | eqtrd 2069 |
. . . . . . . . . . . . . . . 16
   


    
                            |
82 | 81 | oveq1d 5470 |
. . . . . . . . . . . . . . 15
   


    
       
            
           |
83 | | addclpr 6520 |
. . . . . . . . . . . . . . . . . 18
   
 
                 |
84 | 66, 74, 83 | syl2anc 391 |
. . . . . . . . . . . . . . . . 17
                   |
85 | 84 | adantr 261 |
. . . . . . . . . . . . . . . 16
   


    
                |
86 | 16 | a1i 9 |
. . . . . . . . . . . . . . . 16
   


    
      |
87 | | addassprg 6555 |
. . . . . . . . . . . . . . . 16
    
      
                  
       
    |
88 | 85, 86, 86, 87 | syl3anc 1134 |
. . . . . . . . . . . . . . 15
   


    
                                  |
89 | 82, 88 | eqtrd 2069 |
. . . . . . . . . . . . . 14
   


    
       
                        |
90 | | distrprg 6564 |
. . . . . . . . . . . . . . . . . . 19
 
             |
91 | 68, 24, 67, 90 | syl3anc 1134 |
. . . . . . . . . . . . . . . . . 18
        
          |
92 | 91 | oveq1d 5470 |
. . . . . . . . . . . . . . . . 17
                           |
93 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . . . 19
 
  
  |
94 | 68, 24, 93 | syl2anc 391 |
. . . . . . . . . . . . . . . . . 18
        
  |
95 | | addassprg 6555 |
. . . . . . . . . . . . . . . . . 18
   
 
                         |
96 | 94, 70, 72, 95 | syl3anc 1134 |
. . . . . . . . . . . . . . . . 17
                             |
97 | 92, 96 | eqtrd 2069 |
. . . . . . . . . . . . . . . 16
                           |
98 | 97 | oveq1d 5470 |
. . . . . . . . . . . . . . 15
             
                 |
99 | 98 | adantr 261 |
. . . . . . . . . . . . . 14
   


    
       
                    |
100 | | distrprg 6564 |
. . . . . . . . . . . . . . . . . . 19
 
             |
101 | 57, 24, 67, 100 | syl3anc 1134 |
. . . . . . . . . . . . . . . . . 18
        
          |
102 | 101 | oveq2d 5471 |
. . . . . . . . . . . . . . . . 17
                           |
103 | 70, 66, 72, 76, 78 | caov12d 5624 |
. . . . . . . . . . . . . . . . 17
           
       
         |
104 | 102, 103 | eqtrd 2069 |
. . . . . . . . . . . . . . . 16
                 
         |
105 | 104 | oveq1d 5470 |
. . . . . . . . . . . . . . 15
            
                      |
106 | 105 | adantr 261 |
. . . . . . . . . . . . . 14
   


    
             
                  |
107 | 89, 99, 106 | 3eqtr4d 2079 |
. . . . . . . . . . . . 13
   


    
       
           
        |
108 | 24, 16, 17 | sylancl 392 |
. . . . . . . . . . . . . . . . 17
           |
109 | | mulclpr 6553 |
. . . . . . . . . . . . . . . . 17
  
  
     |
110 | 68, 108, 109 | syl2anc 391 |
. . . . . . . . . . . . . . . 16
        
    |
111 | | addclpr 6520 |
. . . . . . . . . . . . . . . 16
          
   
    |
112 | 110, 72, 111 | syl2anc 391 |
. . . . . . . . . . . . . . 15
                 |
113 | 104, 84 | eqeltrd 2111 |
. . . . . . . . . . . . . . 15
                 |
114 | | addclpr 6520 |
. . . . . . . . . . . . . . . . 17
   
   |
115 | 16, 16, 114 | mp2an 402 |
. . . . . . . . . . . . . . . 16
   |
116 | 115 | a1i 9 |
. . . . . . . . . . . . . . 15
           |
117 | | enreceq 6664 |
. . . . . . . . . . . . . . 15
            
  
                         
                               
     |
118 | 112, 113,
116, 67, 117 | syl22anc 1135 |
. . . . . . . . . . . . . 14
                       
                               
     |
119 | 118 | adantr 261 |
. . . . . . . . . . . . 13
   


    
                                    
           
         |
120 | 107, 119 | mpbird 156 |
. . . . . . . . . . . 12
   


    
                                 |
121 | 39, 120 | eqtrd 2069 |
. . . . . . . . . . 11
   


    
              
 
        |
122 | | df-1r 6660 |
. . . . . . . . . . 11
        |
123 | 121, 122 | syl6eqr 2087 |
. . . . . . . . . 10
   


    
              
 
  |
124 | | breq2 3759 |
. . . . . . . . . . . 12
        
    
    |
125 | | oveq2 5463 |
. . . . . . . . . . . . 13
              
     
         |
126 | 125 | eqeq1d 2045 |
. . . . . . . . . . . 12
               
          
 
   |
127 | 124, 126 | anbi12d 442 |
. . . . . . . . . . 11
                
                   
 
    |
128 | 127 | rspcev 2650 |
. . . . . . . . . 10
         
                 
 
          
   |
129 | 23, 33, 123, 128 | syl12anc 1132 |
. . . . . . . . 9
   


    
    

      
   |
130 | 129 | exp32 347 |
. . . . . . . 8
             
       
     |
131 | 130 | anassrs 380 |
. . . . . . 7
   

   
  
 
       
     |
132 | 131 | rexlimdva 2427 |
. . . . . 6
   
    
  
 
      
     |
133 | 15, 132 | mpd 13 |
. . . . 5
   
            
    |
134 | 133 | rexlimdva 2427 |
. . . 4
 
    
 
      
    |
135 | 13, 134 | syl5 28 |
. . 3
 
        
      
    |
136 | 4, 10, 135 | ecoptocl 6129 |
. 2
  
       |
137 | 3, 136 | mpcom 32 |
1
    
   |