Step | Hyp | Ref
| Expression |
1 | | df-nqqs 6332 |
. . 3
     |
2 | | breq1 3758 |
. . . 4
                        |
3 | | oveq1 5462 |
. . . . . 6
            
    |
4 | 3 | eqeq1d 2045 |
. . . . 5
             
      
       |
5 | 4 | rexbidv 2321 |
. . . 4
              
       
       |
6 | 2, 5 | imbi12d 223 |
. . 3
                 
                   
          |
7 | | breq2 3759 |
. . . 4
      
        |
8 | | eqeq2 2046 |
. . . . 5
        
          |
9 | 8 | rexbidv 2321 |
. . . 4
        

       
   |
10 | 7, 9 | imbi12d 223 |
. . 3
              

     
       |
11 | | ordpipqqs 6358 |
. . . 4
                         |
12 | | mulclpi 6312 |
. . . . . . . . 9
 
  
  |
13 | | mulclpi 6312 |
. . . . . . . . 9
 
  
  |
14 | 12, 13 | anim12i 321 |
. . . . . . . 8
         
     |
15 | 14 | an42s 523 |
. . . . . . 7
         
     |
16 | | ltexpi 6321 |
. . . . . . 7
   
    
  
    
     |
17 | 15, 16 | syl 14 |
. . . . . 6
                      |
18 | | df-rex 2306 |
. . . . . 6
 
 
        
       |
19 | 17, 18 | syl6bb 185 |
. . . . 5
                
        |
20 | | simpll 481 |
. . . . . . . . . . . 12
   


 
     |
21 | | simpr 103 |
. . . . . . . . . . . 12
   


 
   |
22 | | simpr 103 |
. . . . . . . . . . . . . . 15
 
   |
23 | | simpr 103 |
. . . . . . . . . . . . . . 15
 
   |
24 | 22, 23 | anim12i 321 |
. . . . . . . . . . . . . 14
       
   |
25 | 24 | adantr 261 |
. . . . . . . . . . . . 13
   


 
     |
26 | | mulclpi 6312 |
. . . . . . . . . . . . 13
 
  
  |
27 | 25, 26 | syl 14 |
. . . . . . . . . . . 12
   


 
  
  |
28 | 20, 21, 27 | jca32 293 |
. . . . . . . . . . 11
   


 
  


      |
29 | 28 | adantrr 448 |
. . . . . . . . . 10
   


  
  

     


      |
30 | | addpipqqs 6354 |
. . . . . . . . . 10
      
                           
     |
31 | 29, 30 | syl 14 |
. . . . . . . . 9
   


  
  

                     
 
     
     |
32 | | simplll 485 |
. . . . . . . . . . . . . . 15
   


  
  

      |
33 | | simpllr 486 |
. . . . . . . . . . . . . . 15
   


  
  

      |
34 | | simplrr 488 |
. . . . . . . . . . . . . . 15
   


  
  

      |
35 | | mulcompig 6315 |
. . . . . . . . . . . . . . . 16
 
  
    |
36 | 35 | adantl 262 |
. . . . . . . . . . . . . . 15
      
  
  

        
    |
37 | | mulasspig 6316 |
. . . . . . . . . . . . . . . 16
 
  
        |
38 | 37 | adantl 262 |
. . . . . . . . . . . . . . 15
      
  
  

    
     
      |
39 | 32, 33, 34, 36, 38 | caov12d 5624 |
. . . . . . . . . . . . . 14
   


  
  

         
    |
40 | 39 | oveq1d 5470 |
. . . . . . . . . . . . 13
   


  
  

      
 
             |
41 | 32, 34, 12 | syl2anc 391 |
. . . . . . . . . . . . . 14
   


  
  

     
  |
42 | | simprl 483 |
. . . . . . . . . . . . . 14
   


  
  

      |
43 | | distrpig 6317 |
. . . . . . . . . . . . . 14
  

                 |
44 | 33, 41, 42, 43 | syl3anc 1134 |
. . . . . . . . . . . . 13
   


  
  

      
             |
45 | 40, 44 | eqtr4d 2072 |
. . . . . . . . . . . 12
   


  
  

      
 
           |
46 | 45 | opeq1d 3546 |
. . . . . . . . . . 11
   


  
  

               
  
         
     |
47 | 46 | eceq1d 6078 |
. . . . . . . . . 10
   


  
  

                
              
     |
48 | | simpllr 486 |
. . . . . . . . . . . . 13
   


 
   |
49 | 12 | ad2ant2rl 480 |
. . . . . . . . . . . . . 14
        
  |
50 | | addclpi 6311 |
. . . . . . . . . . . . . 14
   
  
    |
51 | 49, 50 | sylan 267 |
. . . . . . . . . . . . 13
   


 
   

  |
52 | 48, 51, 27 | 3jca 1083 |
. . . . . . . . . . . 12
   


 
    

     |
53 | 52 | adantrr 448 |
. . . . . . . . . . 11
   


  
  

       

     |
54 | | mulcanenqec 6370 |
. . . . . . . . . . 11
     
                      
 
     |
55 | 53, 54 | syl 14 |
. . . . . . . . . 10
   


  
  

              
                |
56 | 47, 55 | eqtrd 2069 |
. . . . . . . . 9
   


  
  

                
                |
57 | | 3anass 888 |
. . . . . . . . . . . . . 14
 
  
    |
58 | 57 | biimpri 124 |
. . . . . . . . . . . . 13
  
  
   |
59 | 58 | adantll 445 |
. . . . . . . . . . . 12
       
   |
60 | 59 | anim1i 323 |
. . . . . . . . . . 11
   


        
 
   

     |
61 | 60 | adantrl 447 |
. . . . . . . . . 10
   


  
  

     
    
     |
62 | | opeq1 3540 |
. . . . . . . . . . . 12
                   
     |
63 | 62 | eceq1d 6078 |
. . . . . . . . . . 11
          
                 |
64 | | mulcanenqec 6370 |
. . . . . . . . . . 11
 
     
          |
65 | 63, 64 | sylan9eqr 2091 |
. . . . . . . . . 10
  
   

                    |
66 | 61, 65 | syl 14 |
. . . . . . . . 9
   


  
  

                     |
67 | 31, 56, 66 | 3eqtrd 2073 |
. . . . . . . 8
   


  
  

                       |
68 | 33, 34, 26 | syl2anc 391 |
. . . . . . . . . . 11
   


  
  

     
  |
69 | | opelxpi 4319 |
. . . . . . . . . . . 12
  

          |
70 | | enqex 6344 |
. . . . . . . . . . . . 13
 |
71 | 70 | ecelqsi 6096 |
. . . . . . . . . . . 12
     
               |
72 | 69, 71 | syl 14 |
. . . . . . . . . . 11
  

              |
73 | 42, 68, 72 | syl2anc 391 |
. . . . . . . . . 10
   


  
  

                 |
74 | 73, 1 | syl6eleqr 2128 |
. . . . . . . . 9
   


  
  

             |
75 | | oveq2 5463 |
. . . . . . . . . . 11
              
     
         |
76 | 75 | eqeq1d 2045 |
. . . . . . . . . 10
               
                         |
77 | 76 | adantl 262 |
. . . . . . . . 9
      
  
  

   
              
          
              |
78 | 74, 77 | rspcedv 2654 |
. . . . . . . 8
   


  
  

                       
      
       |
79 | 67, 78 | mpd 13 |
. . . . . . 7
   


  
  

           
      |
80 | 79 | ex 108 |
. . . . . 6
          
    
               |
81 | 80 | exlimdv 1697 |
. . . . 5
          
  

   
      
       |
82 | 19, 81 | sylbid 139 |
. . . 4
                   
       |
83 | 11, 82 | sylbid 139 |
. . 3
                  
      
       |
84 | 1, 6, 10, 83 | 2ecoptocl 6130 |
. 2
 
        |
85 | | ltaddnq 6390 |
. . . . 5
 

    |
86 | | breq2 3759 |
. . . . 5
     
   |
87 | 85, 86 | syl5ibcom 144 |
. . . 4
 
   
   |
88 | 87 | rexlimdva 2427 |
. . 3
  


   |
89 | 88 | adantr 261 |
. 2
 
    
   |
90 | 84, 89 | impbid 120 |
1
 
    
   |