Step | Hyp | Ref
| Expression |
1 | | prarloclemarch 7074 |
. . 3
 
           |
2 | 1 | 3adant2 965 |
. 2
 
           |
3 | | pinn 6965 |
. . . . . . . 8
   |
4 | | 1pi 6971 |
. . . . . . . . . . . 12
 |
5 | 4 | elexi 2645 |
. . . . . . . . . . 11
 |
6 | 5 | sucid 4268 |
. . . . . . . . . 10
 |
7 | | df-2o 6220 |
. . . . . . . . . 10
 |
8 | 6, 7 | eleqtrri 2170 |
. . . . . . . . 9
 |
9 | | 2onn 6320 |
. . . . . . . . . . 11
 |
10 | | nnaword2 6313 |
. . . . . . . . . . 11
 

    |
11 | 9, 10 | mpan 416 |
. . . . . . . . . 10
     |
12 | 11 | sseld 3038 |
. . . . . . . . 9
       |
13 | 8, 12 | mpi 15 |
. . . . . . . 8
     |
14 | 3, 13 | syl 14 |
. . . . . . 7
     |
15 | | o1p1e2 6269 |
. . . . . . . . 9
   |
16 | | addpiord 6972 |
. . . . . . . . . . 11
    
    |
17 | 4, 4, 16 | mp2an 418 |
. . . . . . . . . 10
     |
18 | | addclpi 6983 |
. . . . . . . . . . 11
    
  |
19 | 4, 4, 18 | mp2an 418 |
. . . . . . . . . 10
   |
20 | 17, 19 | eqeltrri 2168 |
. . . . . . . . 9
   |
21 | 15, 20 | eqeltrri 2168 |
. . . . . . . 8
 |
22 | | addpiord 6972 |
. . . . . . . 8
    
    |
23 | 21, 22 | mpan2 417 |
. . . . . . 7
       |
24 | 14, 23 | eleqtrrd 2174 |
. . . . . 6
     |
25 | | addclpi 6983 |
. . . . . . . 8
    
  |
26 | 21, 25 | mpan2 417 |
. . . . . . 7
     |
27 | | ltpiord 6975 |
. . . . . . . 8
   
         |
28 | 4, 27 | mpan 416 |
. . . . . . 7
     
     |
29 | 26, 28 | syl 14 |
. . . . . 6
   
     |
30 | 24, 29 | mpbird 166 |
. . . . 5
     |
31 | 30 | adantl 272 |
. . . 4
  

     |
32 | 31 | adantrr 464 |
. . 3
  
 
             |
33 | | nna0 6275 |
. . . . . . . . . . . . . . . . 17
     |
34 | | 0lt1o 6242 |
. . . . . . . . . . . . . . . . . . . 20
 |
35 | | 1on 6226 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
36 | 35 | onsuci 4361 |
. . . . . . . . . . . . . . . . . . . . 21
 |
37 | | ontr1 4240 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
38 | 36, 37 | ax-mp 7 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
39 | 34, 6, 38 | mp2an 418 |
. . . . . . . . . . . . . . . . . . 19
 |
40 | 39, 7 | eleqtrri 2170 |
. . . . . . . . . . . . . . . . . 18
 |
41 | | nnaordi 6307 |
. . . . . . . . . . . . . . . . . . 19
 
 
       |
42 | 9, 41 | mpan 416 |
. . . . . . . . . . . . . . . . . 18
 
       |
43 | 40, 42 | mpi 15 |
. . . . . . . . . . . . . . . . 17
       |
44 | 33, 43 | eqeltrrd 2172 |
. . . . . . . . . . . . . . . 16
     |
45 | 3, 44 | syl 14 |
. . . . . . . . . . . . . . 15
     |
46 | 45, 23 | eleqtrrd 2174 |
. . . . . . . . . . . . . 14
     |
47 | | ltpiord 6975 |
. . . . . . . . . . . . . . 15
   
         |
48 | 26, 47 | mpdan 413 |
. . . . . . . . . . . . . 14
   
     |
49 | 46, 48 | mpbird 166 |
. . . . . . . . . . . . 13
     |
50 | | mulidpi 6974 |
. . . . . . . . . . . . 13
     |
51 | | mulcompig 6987 |
. . . . . . . . . . . . . . . 16
   
           |
52 | 4, 51 | mpan2 417 |
. . . . . . . . . . . . . . 15
             |
53 | 26, 52 | syl 14 |
. . . . . . . . . . . . . 14
           |
54 | | mulidpi 6974 |
. . . . . . . . . . . . . . 15
           |
55 | 26, 54 | syl 14 |
. . . . . . . . . . . . . 14
         |
56 | 53, 55 | eqtr3d 2129 |
. . . . . . . . . . . . 13
         |
57 | 49, 50, 56 | 3brtr4d 3897 |
. . . . . . . . . . . 12
         |
58 | | ordpipqqs 7030 |
. . . . . . . . . . . . . . 15
        
     
                |
59 | 4, 58 | mpanl2 427 |
. . . . . . . . . . . . . 14
      
     
                |
60 | 4, 59 | mpanr2 430 |
. . . . . . . . . . . . 13
   
           
           |
61 | 26, 60 | mpdan 413 |
. . . . . . . . . . . 12
                       |
62 | 57, 61 | mpbird 166 |
. . . . . . . . . . 11
              |
63 | 62 | adantl 272 |
. . . . . . . . . 10
 
              |
64 | | opelxpi 4499 |
. . . . . . . . . . . . . . . 16
   
          |
65 | 4, 64 | mpan2 417 |
. . . . . . . . . . . . . . 15
            |
66 | | enqex 7016 |
. . . . . . . . . . . . . . . 16
 |
67 | 66 | ecelqsi 6386 |
. . . . . . . . . . . . . . 15
    
                |
68 | 26, 65, 67 | 3syl 17 |
. . . . . . . . . . . . . 14
              |
69 | | df-nqqs 7004 |
. . . . . . . . . . . . . 14
     |
70 | 68, 69 | syl6eleqr 2188 |
. . . . . . . . . . . . 13
          |
71 | | opelxpi 4499 |
. . . . . . . . . . . . . . . . 17
          |
72 | 4, 71 | mpan2 417 |
. . . . . . . . . . . . . . . 16
   
    |
73 | 66 | ecelqsi 6386 |
. . . . . . . . . . . . . . . 16
                 |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . 15
            |
75 | 74, 69 | syl6eleqr 2188 |
. . . . . . . . . . . . . 14
        |
76 | | ltmnqg 7057 |
. . . . . . . . . . . . . 14
                         
             
     |
77 | 75, 76 | syl3an1 1214 |
. . . . . . . . . . . . 13
      
                           
     |
78 | 70, 77 | syl3an2 1215 |
. . . . . . . . . . . 12
 
                         
     |
79 | 78 | 3anidm12 1238 |
. . . . . . . . . . 11
 
           
             
     |
80 | 79 | ancoms 265 |
. . . . . . . . . 10
 
           
             
     |
81 | 63, 80 | mpbid 146 |
. . . . . . . . 9
 
                 |
82 | | mulcomnqg 7039 |
. . . . . . . . . 10
                       |
83 | 75, 82 | sylan2 281 |
. . . . . . . . 9
 
                |
84 | | mulcomnqg 7039 |
. . . . . . . . . 10
      
          
     
     |
85 | 70, 84 | sylan2 281 |
. . . . . . . . 9
 
      
 
     
     |
86 | 81, 83, 85 | 3brtr3d 3896 |
. . . . . . . 8
 
                   |
87 | 86 | 3ad2antl3 1110 |
. . . . . . 7
  

                   |
88 | 87 | adantrr 464 |
. . . . . 6
  
 
                           |
89 | | ltsonq 7054 |
. . . . . . . . . 10
 |
90 | | ltrelnq 7021 |
. . . . . . . . . 10
   |
91 | 89, 90 | sotri 4860 |
. . . . . . . . 9
 
                                   |
92 | 91 | ex 114 |
. . . . . . . 8
                        
            |
93 | 92 | adantl 272 |
. . . . . . 7
                          
            |
94 | 93 | adantl 272 |
. . . . . 6
  
 
                         
            |
95 | 88, 94 | mpd 13 |
. . . . 5
  
 
                    |
96 | | mulclnq 7032 |
. . . . . . . . . 10
                     |
97 | 70, 96 | sylan 278 |
. . . . . . . . 9
 
            |
98 | 97 | ancoms 265 |
. . . . . . . 8
 
            |
99 | 98 | 3ad2antl3 1110 |
. . . . . . 7
  

            |
100 | | simpl2 950 |
. . . . . . 7
  

   |
101 | | ltaddnq 7063 |
. . . . . . 7
                                  |
102 | 99, 100, 101 | syl2anc 404 |
. . . . . 6
  

                       |
103 | 102 | adantrr 464 |
. . . . 5
  
 
                        
      |
104 | 89, 90 | sotri 4860 |
. . . . 5
 
     
                  
                  |
105 | 95, 103, 104 | syl2anc 404 |
. . . 4
  
 
                      |
106 | | addcomnqg 7037 |
. . . . . . 7
                                    |
107 | 99, 100, 106 | syl2anc 404 |
. . . . . 6
  

       
                 |
108 | 107 | breq2d 3879 |
. . . . 5
  

            
              |
109 | 108 | adantrr 464 |
. . . 4
  
 
                
   
              |
110 | 105, 109 | mpbid 146 |
. . 3
  
 
                      |
111 | | simpr 109 |
. . . . 5
  

   |
112 | | breq2 3871 |
. . . . . . . 8
   
     |
113 | | opeq1 3644 |
. . . . . . . . . . . 12
     
       |
114 | 113 | eceq1d 6368 |
. . . . . . . . . . 11
                |
115 | 114 | oveq1d 5705 |
. . . . . . . . . 10
               
     |
116 | 115 | oveq2d 5706 |
. . . . . . . . 9
                         |
117 | 116 | breq2d 3879 |
. . . . . . . 8
            
      
       |
118 | 112, 117 | anbi12d 458 |
. . . . . . 7
    
                            |
119 | 118 | rspcev 2736 |
. . . . . 6
   
                 
            |
120 | 119 | ex 114 |
. . . . 5
                    
             |
121 | 111, 26, 120 | 3syl 17 |
. . . 4
  

                  
             |
122 | 121 | adantrr 464 |
. . 3
  
 
                          
             |
123 | 32, 110, 122 | mp2and 425 |
. 2
  
 
                       |
124 | 2, 123 | rexlimddv 2507 |
1
 
               |