Step | Hyp | Ref
| Expression |
1 | | prarloclemarch 6401 |
. . 3
 
           |
2 | 1 | 3adant2 922 |
. 2
 
 
         |
3 | | pinn 6293 |
. . . . . . . 8
   |
4 | | 1pi 6299 |
. . . . . . . . . . . 12
 |
5 | 4 | elexi 2561 |
. . . . . . . . . . 11
 |
6 | 5 | sucid 4120 |
. . . . . . . . . 10
 |
7 | | df-2o 5941 |
. . . . . . . . . 10
 |
8 | 6, 7 | eleqtrri 2110 |
. . . . . . . . 9
 |
9 | | 2onn 6030 |
. . . . . . . . . . 11
 |
10 | | nnaword2 6023 |
. . . . . . . . . . 11
 

    |
11 | 9, 10 | mpan 400 |
. . . . . . . . . 10
     |
12 | 11 | sseld 2938 |
. . . . . . . . 9
       |
13 | 8, 12 | mpi 15 |
. . . . . . . 8
     |
14 | 3, 13 | syl 14 |
. . . . . . 7
     |
15 | | o1p1e2 5987 |
. . . . . . . . 9
   |
16 | | addpiord 6300 |
. . . . . . . . . . 11
   

    |
17 | 4, 4, 16 | mp2an 402 |
. . . . . . . . . 10
     |
18 | | addclpi 6311 |
. . . . . . . . . . 11
   

  |
19 | 4, 4, 18 | mp2an 402 |
. . . . . . . . . 10
   |
20 | 17, 19 | eqeltrri 2108 |
. . . . . . . . 9
   |
21 | 15, 20 | eqeltrri 2108 |
. . . . . . . 8
 |
22 | | addpiord 6300 |
. . . . . . . 8
   

    |
23 | 21, 22 | mpan2 401 |
. . . . . . 7
       |
24 | 14, 23 | eleqtrrd 2114 |
. . . . . 6
     |
25 | | addclpi 6311 |
. . . . . . . 8
   

  |
26 | 21, 25 | mpan2 401 |
. . . . . . 7
     |
27 | | ltpiord 6303 |
. . . . . . . 8
  

    
    |
28 | 4, 27 | mpan 400 |
. . . . . . 7
     

    |
29 | 26, 28 | syl 14 |
. . . . . 6
   

    |
30 | 24, 29 | mpbird 156 |
. . . . 5
     |
31 | 30 | adantl 262 |
. . . 4
  

     |
32 | 31 | adantrr 448 |
. . 3
  
 
     
  
    |
33 | | nna0 5992 |
. . . . . . . . . . . . . . . . 17
     |
34 | | 0lt1o 5962 |
. . . . . . . . . . . . . . . . . . . 20
 |
35 | | 1on 5947 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
36 | 35 | onsuci 4207 |
. . . . . . . . . . . . . . . . . . . . 21
 |
37 | | ontr1 4092 |
. . . . . . . . . . . . . . . . . . . . 21
  

   |
38 | 36, 37 | ax-mp 7 |
. . . . . . . . . . . . . . . . . . . 20
     |
39 | 34, 6, 38 | mp2an 402 |
. . . . . . . . . . . . . . . . . . 19
 |
40 | 39, 7 | eleqtrri 2110 |
. . . . . . . . . . . . . . . . . 18
 |
41 | | nnaordi 6017 |
. . . . . . . . . . . . . . . . . . 19
 
 
       |
42 | 9, 41 | mpan 400 |
. . . . . . . . . . . . . . . . . 18
         |
43 | 40, 42 | mpi 15 |
. . . . . . . . . . . . . . . . 17
       |
44 | 33, 43 | eqeltrrd 2112 |
. . . . . . . . . . . . . . . 16
     |
45 | 3, 44 | syl 14 |
. . . . . . . . . . . . . . 15
     |
46 | 45, 23 | eleqtrrd 2114 |
. . . . . . . . . . . . . 14
     |
47 | | ltpiord 6303 |
. . . . . . . . . . . . . . 15
  

         |
48 | 26, 47 | mpdan 398 |
. . . . . . . . . . . . . 14
   

    |
49 | 46, 48 | mpbird 156 |
. . . . . . . . . . . . 13
     |
50 | | mulidpi 6302 |
. . . . . . . . . . . . 13
     |
51 | | mulcompig 6315 |
. . . . . . . . . . . . . . . 16
   
  
        |
52 | 4, 51 | mpan2 401 |
. . . . . . . . . . . . . . 15
    
        |
53 | 26, 52 | syl 14 |
. . . . . . . . . . . . . 14
  
        |
54 | | mulidpi 6302 |
. . . . . . . . . . . . . . 15
    
      |
55 | 26, 54 | syl 14 |
. . . . . . . . . . . . . 14
  
      |
56 | 53, 55 | eqtr3d 2071 |
. . . . . . . . . . . . 13
         |
57 | 49, 50, 56 | 3brtr4d 3785 |
. . . . . . . . . . . 12
         |
58 | | ordpipqqs 6358 |
. . . . . . . . . . . . . . 15
      
                  
     |
59 | 4, 58 | mpanl2 411 |
. . . . . . . . . . . . . 14
    
               
  
     |
60 | 4, 59 | mpanr2 414 |
. . . . . . . . . . . . 13
  

           
  
  
     |
61 | 26, 60 | mpdan 398 |
. . . . . . . . . . . 12
              
  
     |
62 | 57, 61 | mpbird 156 |
. . . . . . . . . . 11
              |
63 | 62 | adantl 262 |
. . . . . . . . . 10
 
              |
64 | | opelxpi 4319 |
. . . . . . . . . . . . . . . 16
   
          |
65 | 4, 64 | mpan2 401 |
. . . . . . . . . . . . . . 15
            |
66 | | enqex 6344 |
. . . . . . . . . . . . . . . 16
 |
67 | 66 | ecelqsi 6096 |
. . . . . . . . . . . . . . 15
                     |
68 | 26, 65, 67 | 3syl 17 |
. . . . . . . . . . . . . 14
     
        |
69 | | df-nqqs 6332 |
. . . . . . . . . . . . . 14
     |
70 | 68, 69 | syl6eleqr 2128 |
. . . . . . . . . . . . 13
     
    |
71 | | opelxpi 4319 |
. . . . . . . . . . . . . . . . 17
          |
72 | 4, 71 | mpan2 401 |
. . . . . . . . . . . . . . . 16
        |
73 | 66 | ecelqsi 6096 |
. . . . . . . . . . . . . . . 16
                 |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . 15
            |
75 | 74, 69 | syl6eleqr 2128 |
. . . . . . . . . . . . . 14
        |
76 | | ltmnqg 6385 |
. . . . . . . . . . . . . 14
             
           
  
          
     |
77 | 75, 76 | syl3an1 1167 |
. . . . . . . . . . . . 13
      
                
          
     |
78 | 70, 77 | syl3an2 1168 |
. . . . . . . . . . . 12
 
              
          
     |
79 | 78 | 3anidm12 1191 |
. . . . . . . . . . 11
 
           
  
          
     |
80 | 79 | ancoms 255 |
. . . . . . . . . 10
 
           
  
          
     |
81 | 63, 80 | mpbid 135 |
. . . . . . . . 9
 
                 |
82 | | mulcomnqg 6367 |
. . . . . . . . . 10
                       |
83 | 75, 82 | sylan2 270 |
. . . . . . . . 9
 
                |
84 | | mulcomnqg 6367 |
. . . . . . . . . 10
      
                      |
85 | 70, 84 | sylan2 270 |
. . . . . . . . 9
 
      
 
     
     |
86 | 81, 83, 85 | 3brtr3d 3784 |
. . . . . . . 8
 
       
     
     |
87 | 86 | 3ad2antl3 1067 |
. . . . . . 7
  

               
   |
88 | 87 | adantrr 448 |
. . . . . 6
  
 
     
  
                  |
89 | | ltsonq 6382 |
. . . . . . . . . 10
 |
90 | | ltrelnq 6349 |
. . . . . . . . . 10
   |
91 | 89, 90 | sotri 4663 |
. . . . . . . . 9
 
     
       
     
               |
92 | 91 | ex 108 |
. . . . . . . 8
       
                             |
93 | 92 | adantl 262 |
. . . . . . 7
                 
     
               |
94 | 93 | adantl 262 |
. . . . . 6
  
 
     
  
                             |
95 | 88, 94 | mpd 13 |
. . . . 5
  
 
     
  
       
   |
96 | | mulclnq 6360 |
. . . . . . . . . 10
        
         
  |
97 | 70, 96 | sylan 267 |
. . . . . . . . 9
 
         
  |
98 | 97 | ancoms 255 |
. . . . . . . 8
 
         
  |
99 | 98 | 3ad2antl3 1067 |
. . . . . . 7
  

            |
100 | | simpl2 907 |
. . . . . . 7
  

   |
101 | | ltaddnq 6390 |
. . . . . . 7
          
         
        
    |
102 | 99, 100, 101 | syl2anc 391 |
. . . . . 6
  

                  
    |
103 | 102 | adantrr 448 |
. . . . 5
  
 
     
  
       
              |
104 | 89, 90 | sotri 4663 |
. . . . 5
 
     
          
            
         
   |
105 | 95, 103, 104 | syl2anc 391 |
. . . 4
  
 
     
  
         
   |
106 | | addcomnqg 6365 |
. . . . . . 7
          
           
             |
107 | 99, 100, 106 | syl2anc 391 |
. . . . . 6
  

       
   
             |
108 | 107 | breq2d 3767 |
. . . . 5
  

           

              |
109 | 108 | adantrr 448 |
. . . 4
  
 
     
  
       
   
              |
110 | 105, 109 | mpbid 135 |
. . 3
  
 
     
  
      
      |
111 | | simpr 103 |
. . . . 5
  

   |
112 | | breq2 3759 |
. . . . . . . 8
  
      |
113 | | opeq1 3540 |
. . . . . . . . . . . 12
  
  
       |
114 | 113 | eceq1d 6078 |
. . . . . . . . . . 11
  
             |
115 | 114 | oveq1d 5470 |
. . . . . . . . . 10
  
      
     
     |
116 | 115 | oveq2d 5471 |
. . . . . . . . 9
  
                 
    |
117 | 116 | breq2d 3767 |
. . . . . . . 8
  
         
      
       |
118 | 112, 117 | anbi12d 442 |
. . . . . . 7
  
 
                            |
119 | 118 | rspcev 2650 |
. . . . . 6
   
  
      
       
            |
120 | 119 | ex 108 |
. . . . 5
    
          
  
 
             |
121 | 111, 26, 120 | 3syl 17 |
. . . 4
  

                  
             |
122 | 121 | adantrr 448 |
. . 3
  
 
     
  
 
          
  
 
             |
123 | 32, 110, 122 | mp2and 409 |
. 2
  
 
     
  
 
            |
124 | 2, 123 | rexlimddv 2431 |
1
 
 
             |