Step | Hyp | Ref
| Expression |
1 | | df-1p 9412 |
. . . 4

  |
2 | 1 | abeq2i 2565 |
. . 3

  |
3 | | ltrnq 9409 |
. . . . . . 7
    
      |
4 | | mulcomnq 9383 |
. . . . . . . . 9
             |
5 | | 1nq 9358 |
. . . . . . . . . 10
 |
6 | | recclnq 9396 |
. . . . . . . . . 10
       |
7 | | mulidnq 9393 |
. . . . . . . . . 10
                 |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . . 9
           |
9 | | recidnq 9395 |
. . . . . . . . . 10
         |
10 | 5, 9 | ax-mp 5 |
. . . . . . . . 9
       |
11 | 4, 8, 10 | 3eqtr3i 2483 |
. . . . . . . 8
     |
12 | 11 | breq1i 4412 |
. . . . . . 7
        
      |
13 | 3, 12 | bitri 253 |
. . . . . 6

      |
14 | | prlem936 9477 |
. . . . . 6
       
        |
15 | 13, 14 | sylan2b 478 |
. . . . 5
   
        |
16 | | prnmax 9425 |
. . . . . . 7
 
    |
17 | 16 | ad2ant2r 754 |
. . . . . 6
  
          
  |
18 | | elprnq 9421 |
. . . . . . . . . . . . 13
 
   |
19 | 18 | ad2ant2r 754 |
. . . . . . . . . . . 12
  
            |
20 | 19 | 3adant3 1029 |
. . . . . . . . . . 11
  
        

  |
21 | | simp1r 1034 |
. . . . . . . . . . . 12
  
        

  |
22 | | ltrelnq 9356 |
. . . . . . . . . . . . . 14
   |
23 | 22 | brel 4886 |
. . . . . . . . . . . . 13

    |
24 | 23 | simpld 461 |
. . . . . . . . . . . 12

  |
25 | 21, 24 | syl 17 |
. . . . . . . . . . 11
  
        

  |
26 | | simp3 1011 |
. . . . . . . . . . 11
  
        

  |
27 | | simp2r 1036 |
. . . . . . . . . . 11
  
        

        |
28 | | ltrnq 9409 |
. . . . . . . . . . . . . . . . 17

          |
29 | | fvex 5880 |
. . . . . . . . . . . . . . . . . 18
     |
30 | | fvex 5880 |
. . . . . . . . . . . . . . . . . 18
     |
31 | | ltmnq 9402 |
. . . . . . . . . . . . . . . . . 18
 
       |
32 | | vex 3050 |
. . . . . . . . . . . . . . . . . 18
 |
33 | | mulcomnq 9383 |
. . . . . . . . . . . . . . . . . 18
     |
34 | 29, 30, 31, 32, 33 | caovord2 6486 |
. . . . . . . . . . . . . . . . 17
         
               |
35 | 28, 34 | syl5bb 261 |
. . . . . . . . . . . . . . . 16
 
               |
36 | 35 | adantl 468 |
. . . . . . . . . . . . . . 15
 
                 |
37 | 36 | biimpd 211 |
. . . . . . . . . . . . . 14
 
                 |
38 | | mulcomnq 9383 |
. . . . . . . . . . . . . . . . . . . . 21
             |
39 | | recidnq 9395 |
. . . . . . . . . . . . . . . . . . . . 21
         |
40 | 38, 39 | syl5eqr 2501 |
. . . . . . . . . . . . . . . . . . . 20
         |
41 | | recidnq 9395 |
. . . . . . . . . . . . . . . . . . . 20
         |
42 | 40, 41 | oveqan12d 6314 |
. . . . . . . . . . . . . . . . . . 19
 
                   |
43 | | vex 3050 |
. . . . . . . . . . . . . . . . . . . 20
 |
44 | | mulassnq 9389 |
. . . . . . . . . . . . . . . . . . . 20
         |
45 | | fvex 5880 |
. . . . . . . . . . . . . . . . . . . 20
     |
46 | 30, 43, 32, 33, 44, 45 | caov4 6505 |
. . . . . . . . . . . . . . . . . . 19
                             |
47 | | mulidnq 9393 |
. . . . . . . . . . . . . . . . . . . 20
     |
48 | 5, 47 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
   |
49 | 42, 46, 48 | 3eqtr3g 2510 |
. . . . . . . . . . . . . . . . . 18
 
                 |
50 | | recclnq 9396 |
. . . . . . . . . . . . . . . . . . . 20
       |
51 | | mulclnq 9377 |
. . . . . . . . . . . . . . . . . . . 20
     
         |
52 | 50, 51 | sylan 474 |
. . . . . . . . . . . . . . . . . . 19
 
         |
53 | | recmulnq 9394 |
. . . . . . . . . . . . . . . . . . 19
                       
                 |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
                                   |
55 | 49, 54 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
 
                   |
56 | 55 | eleq1d 2515 |
. . . . . . . . . . . . . . . 16
 
                     |
57 | 56 | notbid 296 |
. . . . . . . . . . . . . . 15
 
           
         |
58 | 57 | biimprd 227 |
. . . . . . . . . . . . . 14
 
       
             |
59 | 37, 58 | anim12d 566 |
. . . . . . . . . . . . 13
 
  
                                  |
60 | | ovex 6323 |
. . . . . . . . . . . . . . 15
       |
61 | | breq2 4409 |
. . . . . . . . . . . . . . . 16
             
               |
62 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . 18
                       |
63 | 62 | eleq1d 2515 |
. . . . . . . . . . . . . . . . 17
           
             |
64 | 63 | notbid 296 |
. . . . . . . . . . . . . . . 16
           
             |
65 | 61, 64 | anbi12d 718 |
. . . . . . . . . . . . . . 15
                                
              |
66 | 60, 65 | spcev 3143 |
. . . . . . . . . . . . . 14
                                 
       |
67 | | ovex 6323 |
. . . . . . . . . . . . . . 15
       |
68 | | breq1 4408 |
. . . . . . . . . . . . . . . . 17
       
         |
69 | 68 | anbi1d 712 |
. . . . . . . . . . . . . . . 16
                    
        |
70 | 69 | exbidv 1770 |
. . . . . . . . . . . . . . 15
               
                 |
71 | | reclempr.1 |
. . . . . . . . . . . . . . 15
           |
72 | 67, 70, 71 | elab2 3190 |
. . . . . . . . . . . . . 14
      
                |
73 | 66, 72 | sylibr 216 |
. . . . . . . . . . . . 13
                                 |
74 | 59, 73 | syl6 34 |
. . . . . . . . . . . 12
 
  
                |
75 | 74 | imp 431 |
. . . . . . . . . . 11
                     |
76 | 20, 25, 26, 27, 75 | syl22anc 1270 |
. . . . . . . . . 10
  
        

        |
77 | 22 | brel 4886 |
. . . . . . . . . . . . 13

    |
78 | 77 | simprd 465 |
. . . . . . . . . . . 12

  |
79 | 78 | 3ad2ant3 1032 |
. . . . . . . . . . 11
  
        

  |
80 | | mulcomnq 9383 |
. . . . . . . . . . . . 13
     |
81 | | mulidnq 9393 |
. . . . . . . . . . . . 13
     |
82 | 80, 81 | syl5reqr 2502 |
. . . . . . . . . . . 12
     |
83 | | mulassnq 9389 |
. . . . . . . . . . . . 13
                 |
84 | | recidnq 9395 |
. . . . . . . . . . . . . 14
         |
85 | 84 | oveq1d 6310 |
. . . . . . . . . . . . 13
             |
86 | 83, 85 | syl5reqr 2502 |
. . . . . . . . . . . 12
             |
87 | 82, 86 | sylan9eqr 2509 |
. . . . . . . . . . 11
 
           |
88 | 79, 25, 87 | syl2anc 667 |
. . . . . . . . . 10
  
        

          |
89 | | oveq2 6303 |
. . . . . . . . . . . 12
                   |
90 | 89 | eqeq2d 2463 |
. . . . . . . . . . 11
         
           |
91 | 90 | rspcev 3152 |
. . . . . . . . . 10
       
         
    |
92 | 76, 88, 91 | syl2anc 667 |
. . . . . . . . 9
  
        


    |
93 | 92 | 3expia 1211 |
. . . . . . . 8
  
           
     |
94 | 93 | reximdv 2863 |
. . . . . . 7
  
           


     |
95 | 71 | reclem2pr 9478 |
. . . . . . . . 9
   |
96 | | df-mp 9414 |
. . . . . . . . . 10
 



     |
97 | | mulclnq 9377 |
. . . . . . . . . 10
 
     |
98 | 96, 97 | genpelv 9430 |
. . . . . . . . 9
 
    

     |
99 | 95, 98 | mpdan 675 |
. . . . . . . 8
   


     |
100 | 99 | ad2antrr 733 |
. . . . . . 7
  
            


     |
101 | 94, 100 | sylibrd 238 |
. . . . . 6
  
           
     |
102 | 17, 101 | mpd 15 |
. . . . 5
  
              |
103 | 15, 102 | rexlimddv 2885 |
. . . 4
  
    |
104 | 103 | ex 436 |
. . 3
       |
105 | 2, 104 | syl5bi 221 |
. 2
       |
106 | 105 | ssrdv 3440 |
1
     |