Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7335 |
. . 3
     |
2 | | breq1 4003 |
. . . 4
                
       |
3 | | oveq1 5876 |
. . . . . 6
                 |
4 | 3 | eqeq1d 2186 |
. . . . 5
                            |
5 | 4 | rexbidv 2478 |
. . . 4
                     
        |
6 | 2, 5 | imbi12d 234 |
. . 3
                              
                 |
7 | | breq2 4004 |
. . . 4
               |
8 | | eqeq2 2187 |
. . . . 5
                   |
9 | 8 | rexbidv 2478 |
. . . 4
                
    |
10 | 7, 9 | imbi12d 234 |
. . 3
            
       

       |
11 | | ordpipqqs 7361 |
. . . 4
      
     
            |
12 | | mulclpi 7315 |
. . . . . . . . 9
 
     |
13 | | mulclpi 7315 |
. . . . . . . . 9
 
     |
14 | 12, 13 | anim12i 338 |
. . . . . . . 8
      
        |
15 | 14 | an42s 589 |
. . . . . . 7
      
        |
16 | | ltexpi 7324 |
. . . . . . 7
            
         |
17 | 15, 16 | syl 14 |
. . . . . 6
      
               |
18 | | df-rex 2461 |
. . . . . 6
       
            |
19 | 17, 18 | bitrdi 196 |
. . . . 5
      
                  |
20 | | simpll 527 |
. . . . . . . . . . . 12
   


 

    |
21 | | simpr 110 |
. . . . . . . . . . . 12
   


 

  |
22 | | simpr 110 |
. . . . . . . . . . . . . . 15
 
   |
23 | | simpr 110 |
. . . . . . . . . . . . . . 15
 
   |
24 | 22, 23 | anim12i 338 |
. . . . . . . . . . . . . 14
      
    |
25 | 24 | adantr 276 |
. . . . . . . . . . . . 13
   


 

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


 

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


 

 
        |
29 | 28 | adantrr 479 |
. . . . . . . . . 10
   


 
          

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


 
                                        |
32 | | simplll 533 |
. . . . . . . . . . . . . . 15
   


 
           |
33 | | simpllr 534 |
. . . . . . . . . . . . . . 15
   


 
           |
34 | | simplrr 536 |
. . . . . . . . . . . . . . 15
   


 
           |
35 | | mulcompig 7318 |
. . . . . . . . . . . . . . . 16
 
       |
36 | 35 | adantl 277 |
. . . . . . . . . . . . . . 15
      
 
           
      |
37 | | mulasspig 7319 |
. . . . . . . . . . . . . . . 16
 
           |
38 | 37 | adantl 277 |
. . . . . . . . . . . . . . 15
      
 
         
 
          |
39 | 32, 33, 34, 36, 38 | caov12d 6050 |
. . . . . . . . . . . . . 14
   


 
                   |
40 | 39 | oveq1d 5884 |
. . . . . . . . . . . . 13
   


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


 
             |
42 | | simprl 529 |
. . . . . . . . . . . . . 14
   


 
        
  |
43 | | distrpig 7320 |
. . . . . . . . . . . . . 14
   
                 |
44 | 33, 41, 42, 43 | syl3anc 1238 |
. . . . . . . . . . . . 13
   


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


 
                         |
46 | 45 | opeq1d 3782 |
. . . . . . . . . . 11
   


 
                                       |
47 | 46 | eceq1d 6565 |
. . . . . . . . . 10
   


 
                                          |
48 | | simpllr 534 |
. . . . . . . . . . . . 13
   


 

  |
49 | 12 | ad2ant2rl 511 |
. . . . . . . . . . . . . 14
      
    |
50 | | addclpi 7314 |
. . . . . . . . . . . . . 14
   
       |
51 | 49, 50 | sylan 283 |
. . . . . . . . . . . . 13
   


 

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


 

          |
53 | 52 | adantrr 479 |
. . . . . . . . . . 11
   


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


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


 
                                      |
57 | | 3anass 982 |
. . . . . . . . . . . . . 14
 

      |
58 | 57 | biimpri 133 |
. . . . . . . . . . . . 13
  
 

   |
59 | 58 | adantll 476 |
. . . . . . . . . . . 12
      

   |
60 | 59 | anim1i 340 |
. . . . . . . . . . 11
   


 
        
          |
61 | 60 | adantrl 478 |
. . . . . . . . . 10
   


 
          
          |
62 | | opeq1 3776 |
. . . . . . . . . . . 12
                         |
63 | 62 | eceq1d 6565 |
. . . . . . . . . . 11
                            |
64 | | mulcanenqec 7373 |
. . . . . . . . . . 11
 
                |
65 | 63, 64 | sylan9eqr 2232 |
. . . . . . . . . 10
  
                         |
66 | 61, 65 | syl 14 |
. . . . . . . . 9
   


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


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


 
             |
69 | | opelxpi 4655 |
. . . . . . . . . . . 12
              |
70 | | enqex 7347 |
. . . . . . . . . . . . 13
 |
71 | 70 | ecelqsi 6583 |
. . . . . . . . . . . 12
                     |
72 | 69, 71 | syl 14 |
. . . . . . . . . . 11
                  |
73 | 42, 68, 72 | syl2anc 411 |
. . . . . . . . . 10
   


 
                      |
74 | 73, 1 | eleqtrrdi 2271 |
. . . . . . . . 9
   


 
                  |
75 | | oveq2 5877 |
. . . . . . . . . . 11
                              |
76 | 75 | eqeq1d 2186 |
. . . . . . . . . 10
                                         |
77 | 76 | adantl 277 |
. . . . . . . . 9
      
 
        
                                        |
78 | 74, 77 | rspcedv 2845 |
. . . . . . . 8
   


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


 
         
             |
80 | 79 | ex 115 |
. . . . . 6
      
                        |
81 | 80 | exlimdv 1819 |
. . . . 5
      
   
                      |
82 | 19, 81 | sylbid 150 |
. . . 4
      
    
               |
83 | 11, 82 | sylbid 150 |
. . 3
      
     
                    |
84 | 1, 6, 10, 83 | 2ecoptocl 6617 |
. 2
 
  

    |
85 | | ltaddnq 7394 |
. . . . 5
 

    |
86 | | breq2 4004 |
. . . . 5
     
   |
87 | 85, 86 | syl5ibcom 155 |
. . . 4
 
       |
88 | 87 | rexlimdva 2594 |
. . 3
  

    |
89 | 88 | adantr 276 |
. 2
 
        |
90 | 84, 89 | impbid 129 |
1
 
 
      |