Step | Hyp | Ref
| Expression |
1 | | ruc.6 |
. . 3
       |
2 | | ruc.1 |
. . . . . 6
       |
3 | | ruc.2 |
. . . . . 6
                   ![]_ ]_](_urbrack.gif)                               |
4 | | ruc.4 |
. . . . . 6
           |
5 | | ruc.5 |
. . . . . 6
      |
6 | 2, 3, 4, 5 | ruclem11 14347 |
. . . . 5
             |
7 | 6 | simp1d 1026 |
. . . 4
     |
8 | 6 | simp2d 1027 |
. . . 4
     |
9 | | 1re 9673 |
. . . . 5
 |
10 | 6 | simp3d 1028 |
. . . . 5
    
  |
11 | | breq2 4422 |
. . . . . . 7
 
   |
12 | 11 | ralbidv 2839 |
. . . . . 6
  
  
       |
13 | 12 | rspcev 3162 |
. . . . 5
       
      |
14 | 9, 10, 13 | sylancr 674 |
. . . 4
        |
15 | | suprcl 10602 |
. . . 4
      
             |
16 | 7, 8, 14, 15 | syl3anc 1276 |
. . 3
         |
17 | 1, 16 | syl5eqel 2544 |
. 2
   |
18 | 2 | adantr 471 |
. . . . . . . . 9
 

      |
19 | 3 | adantr 471 |
. . . . . . . . 9
 

                  ![]_ ]_](_urbrack.gif)  
                            |
20 | 2, 3, 4, 5 | ruclem6 14342 |
. . . . . . . . . . 11
         |
21 | | nnm1nn0 10945 |
. . . . . . . . . . 11
     |
22 | | ffvelrn 6048 |
. . . . . . . . . . 11
        
            |
23 | 20, 21, 22 | syl2an 484 |
. . . . . . . . . 10
 

          |
24 | | xp1st 6855 |
. . . . . . . . . 10
        
            |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
 

            |
26 | | xp2nd 6856 |
. . . . . . . . . 10
        
            |
27 | 23, 26 | syl 17 |
. . . . . . . . 9
 

            |
28 | 2 | ffvelrnda 6050 |
. . . . . . . . 9
 

      |
29 | | eqid 2462 |
. . . . . . . . 9
                                                                       |
30 | | eqid 2462 |
. . . . . . . . 9
                                                                       |
31 | 2, 3, 4, 5 | ruclem8 14344 |
. . . . . . . . . 10
 
         
               |
32 | 21, 31 | sylan2 481 |
. . . . . . . . 9
 

                
     |
33 | 18, 19, 25, 27, 28, 29, 30, 32 | ruclem3 14340 |
. . . . . . . 8
 

                                                   
                              |
34 | 2, 3, 4, 5 | ruclem7 14343 |
. . . . . . . . . . . . 13
 
                               |
35 | 21, 34 | sylan2 481 |
. . . . . . . . . . . 12
 

            
               |
36 | | nncn 10650 |
. . . . . . . . . . . . . . 15
   |
37 | 36 | adantl 472 |
. . . . . . . . . . . . . 14
 

  |
38 | | ax-1cn 9628 |
. . . . . . . . . . . . . 14
 |
39 | | npcan 9915 |
. . . . . . . . . . . . . 14
 
       |
40 | 37, 38, 39 | sylancl 673 |
. . . . . . . . . . . . 13
 

      |
41 | 40 | fveq2d 5896 |
. . . . . . . . . . . 12
 

              |
42 | | 1st2nd2 6862 |
. . . . . . . . . . . . . 14
        
                               |
43 | 23, 42 | syl 17 |
. . . . . . . . . . . . 13
 

                               |
44 | 40 | fveq2d 5896 |
. . . . . . . . . . . . 13
 

              |
45 | 43, 44 | oveq12d 6338 |
. . . . . . . . . . . 12
 

                                                   |
46 | 35, 41, 45 | 3eqtr3d 2504 |
. . . . . . . . . . 11
 

                                     |
47 | 46 | fveq2d 5896 |
. . . . . . . . . 10
 

                                             |
48 | 47 | breq2d 4430 |
. . . . . . . . 9
 

                            
                          |
49 | 46 | fveq2d 5896 |
. . . . . . . . . 10
 

                                             |
50 | 49 | breq1d 4428 |
. . . . . . . . 9
 

            
                                          |
51 | 48, 50 | orbi12d 721 |
. . . . . . . 8
 

     
                    
                                                   
                               |
52 | 33, 51 | mpbird 240 |
. . . . . . 7
 

                            |
53 | 7 | adantr 471 |
. . . . . . . . . . 11
 

    |
54 | 8 | adantr 471 |
. . . . . . . . . . 11
 

    |
55 | 14 | adantr 471 |
. . . . . . . . . . 11
 

       |
56 | | nnnn0 10910 |
. . . . . . . . . . . . 13
   |
57 | | fvco3 5970 |
. . . . . . . . . . . . 13
       
                 |
58 | 20, 56, 57 | syl2an 484 |
. . . . . . . . . . . 12
 

                |
59 | 20 | adantr 471 |
. . . . . . . . . . . . . 14
 

        |
60 | | 1stcof 6853 |
. . . . . . . . . . . . . 14
       
       |
61 | | ffn 5755 |
. . . . . . . . . . . . . 14
           |
62 | 59, 60, 61 | 3syl 18 |
. . . . . . . . . . . . 13
 

    |
63 | 56 | adantl 472 |
. . . . . . . . . . . . 13
 

  |
64 | | fnfvelrn 6047 |
. . . . . . . . . . . . 13
   
           |
65 | 62, 63, 64 | syl2anc 671 |
. . . . . . . . . . . 12
 

          |
66 | 58, 65 | eqeltrrd 2541 |
. . . . . . . . . . 11
 

            |
67 | | suprub 10603 |
. . . . . . . . . . 11
                               
        |
68 | 53, 54, 55, 66, 67 | syl31anc 1279 |
. . . . . . . . . 10
 

                |
69 | 68, 1 | syl6breqr 4459 |
. . . . . . . . 9
 

          |
70 | | ffvelrn 6048 |
. . . . . . . . . . . 12
       
         |
71 | 20, 56, 70 | syl2an 484 |
. . . . . . . . . . 11
 

        |
72 | | xp1st 6855 |
. . . . . . . . . . 11
      
          |
73 | 71, 72 | syl 17 |
. . . . . . . . . 10
 

          |
74 | 17 | adantr 471 |
. . . . . . . . . 10
 

  |
75 | | ltletr 9756 |
. . . . . . . . . 10
                                         
   |
76 | 28, 73, 74, 75 | syl3anc 1276 |
. . . . . . . . 9
 

     
                        |
77 | 69, 76 | mpan2d 685 |
. . . . . . . 8
 

            
       |
78 | | fvco3 5970 |
. . . . . . . . . . . . . . 15
       
                 |
79 | 59, 78 | sylan 478 |
. . . . . . . . . . . . . 14
      
              |
80 | 59 | ffvelrnda 6050 |
. . . . . . . . . . . . . . . 16
             |
81 | | xp1st 6855 |
. . . . . . . . . . . . . . . 16
      
          |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . 15
               |
83 | | xp2nd 6856 |
. . . . . . . . . . . . . . . . 17
      
          |
84 | 71, 83 | syl 17 |
. . . . . . . . . . . . . . . 16
 

          |
85 | 84 | adantr 471 |
. . . . . . . . . . . . . . 15
               |
86 | 18 | adantr 471 |
. . . . . . . . . . . . . . . 16
           |
87 | 19 | adantr 471 |
. . . . . . . . . . . . . . . 16
        
              ![]_ ]_](_urbrack.gif)                               |
88 | | simpr 467 |
. . . . . . . . . . . . . . . 16
       |
89 | 63 | adantr 471 |
. . . . . . . . . . . . . . . 16
       |
90 | 86, 87, 4, 5, 88, 89 | ruclem10 14346 |
. . . . . . . . . . . . . . 15
                       |
91 | 82, 85, 90 | ltled 9814 |
. . . . . . . . . . . . . 14
                       |
92 | 79, 91 | eqbrtrd 4439 |
. . . . . . . . . . . . 13
      
              |
93 | 92 | ralrimiva 2814 |
. . . . . . . . . . . 12
 

                 |
94 | | breq1 4421 |
. . . . . . . . . . . . . 14
       
       
                 |
95 | 94 | ralrn 6053 |
. . . . . . . . . . . . 13
  
 
                 
           |
96 | 62, 95 | syl 17 |
. . . . . . . . . . . 12
 

 
                 
           |
97 | 93, 96 | mpbird 240 |
. . . . . . . . . . 11
 

              |
98 | | suprleub 10606 |
. . . . . . . . . . . 12
                                        
           |
99 | 53, 54, 55, 84, 98 | syl31anc 1279 |
. . . . . . . . . . 11
 

                  
           |
100 | 97, 99 | mpbird 240 |
. . . . . . . . . 10
 

     
          |
101 | 1, 100 | syl5eqbr 4452 |
. . . . . . . . 9
 

          |
102 | | lelttr 9755 |
. . . . . . . . . 10
                                             |
103 | 74, 84, 28, 102 | syl3anc 1276 |
. . . . . . . . 9
 

 
                            |
104 | 101, 103 | mpand 686 |
. . . . . . . 8
 

                    |
105 | 77, 104 | orim12d 854 |
. . . . . . 7
 

     
                         
        |
106 | 52, 105 | mpd 15 |
. . . . . 6
 

            |
107 | 28, 74 | lttri2d 9805 |
. . . . . 6
 

    
             |
108 | 106, 107 | mpbird 240 |
. . . . 5
 

      |
109 | 108 | neneqd 2640 |
. . . 4
 

      |
110 | 109 | nrexdv 2855 |
. . 3
        |
111 | | risset 2927 |
. . . 4

   |
112 | | ffn 5755 |
. . . . 5
       |
113 | | eqeq1 2466 |
. . . . . 6
     
       |
114 | 113 | rexrn 6052 |
. . . . 5
  
        |
115 | 2, 112, 114 | 3syl 18 |
. . . 4
  
        |
116 | 111, 115 | syl5bb 265 |
. . 3
  
       |
117 | 110, 116 | mtbird 307 |
. 2
   |
118 | 17, 117 | eldifd 3427 |
1
 
   |