Step | Hyp | Ref
| Expression |
1 | | oveq2 6303 |
. . . . 5

          |
2 | | oveq2 6303 |
. . . . . 6

      |
3 | 2 | oveq2d 6311 |
. . . . 5

          |
4 | 1, 3 | eqeq12d 2468 |
. . . 4

      
 
   
       |
5 | | oveq2 6303 |
. . . . 5
           |
6 | | oveq2 6303 |
. . . . . 6
       |
7 | 6 | oveq2d 6311 |
. . . . 5
           |
8 | 5, 7 | eqeq12d 2468 |
. . . 4
         
           |
9 | | oveq2 6303 |
. . . . 5
           |
10 | | oveq2 6303 |
. . . . . 6
       |
11 | 10 | oveq2d 6311 |
. . . . 5
      
    |
12 | 9, 11 | eqeq12d 2468 |
. . . 4
                     |
13 | | oveq2 6303 |
. . . . 5
           |
14 | | oveq2 6303 |
. . . . . 6
       |
15 | 14 | oveq2d 6311 |
. . . . 5
           |
16 | 13, 15 | eqeq12d 2468 |
. . . 4
         
           |
17 | | oacl 7242 |
. . . . . 6
 
     |
18 | | oa0 7223 |
. . . . . 6
           |
19 | 17, 18 | syl 17 |
. . . . 5
 
         |
20 | | oa0 7223 |
. . . . . . 7
     |
21 | 20 | oveq2d 6311 |
. . . . . 6
         |
22 | 21 | adantl 468 |
. . . . 5
 
         |
23 | 19, 22 | eqtr4d 2490 |
. . . 4
 
           |
24 | | suceq 5491 |
. . . . . 6
      
            |
25 | | oasuc 7231 |
. . . . . . . 8
   
           |
26 | 17, 25 | sylan 474 |
. . . . . . 7
               |
27 | | oasuc 7231 |
. . . . . . . . . . 11
 
   
   |
28 | 27 | oveq2d 6311 |
. . . . . . . . . 10
 
           |
29 | 28 | adantl 468 |
. . . . . . . . 9
  
 
     
    |
30 | | oacl 7242 |
. . . . . . . . . 10
 
     |
31 | | oasuc 7231 |
. . . . . . . . . 10
  
      
     |
32 | 30, 31 | sylan2 477 |
. . . . . . . . 9
  
 
     
    |
33 | 29, 32 | eqtrd 2487 |
. . . . . . . 8
  
 
     
    |
34 | 33 | anassrs 654 |
. . . . . . 7
      
  
     |
35 | 26, 34 | eqeq12d 2468 |
. . . . . 6
           
 
     
     |
36 | 24, 35 | syl5ibr 225 |
. . . . 5
                         |
37 | 36 | expcom 437 |
. . . 4
                         |
38 | | vex 3050 |
. . . . . . . . . 10
 |
39 | | oalim 7239 |
. . . . . . . . . 10
    
      
      |
40 | 38, 39 | mpanr1 690 |
. . . . . . . . 9
                |
41 | 17, 40 | sylan 474 |
. . . . . . . 8
         
      |
42 | 41 | ancoms 455 |
. . . . . . 7
  
      
      |
43 | 42 | adantr 467 |
. . . . . 6
   
  
        
    
      |
44 | | oalimcl 7266 |
. . . . . . . . . . . . 13
  
 
    |
45 | 38, 44 | mpanr1 690 |
. . . . . . . . . . . 12
   
   |
46 | 45 | ancoms 455 |
. . . . . . . . . . 11
   
   |
47 | | ovex 6323 |
. . . . . . . . . . . 12
   |
48 | | oalim 7239 |
. . . . . . . . . . . 12
          
  
       |
49 | 47, 48 | mpanr1 690 |
. . . . . . . . . . 11
                 |
50 | 46, 49 | sylan2 477 |
. . . . . . . . . 10
                 |
51 | | limelon 5489 |
. . . . . . . . . . . . . . . . . 18
     |
52 | 38, 51 | mpan 677 |
. . . . . . . . . . . . . . . . 17

  |
53 | | oacl 7242 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
54 | 53 | ancoms 455 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     |
55 | | onelon 5451 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
     |
56 | 55 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
57 | 54, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
58 | 57 | adantld 469 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
59 | 58 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
  
 
 
      |
60 | | 0ellim 5488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
61 | | onelss 5468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   |
62 | 20 | sseq2d 3462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
 
   |
63 | 61, 62 | sylibrd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
     |
64 | 63 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

    |
65 | | oveq2 6303 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

      |
66 | 65 | sseq2d 3462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  

    |
67 | 66 | rspcev 3152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   

   |
68 | 60, 64, 67 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
  
    |
69 | 68 | expr 620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
     |
70 | 69 | adantrl 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
 



    |
71 | 70 | adantrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
          |
72 | | oawordex 7263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
        |
73 | 72 | ad2ant2l 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
  
      |
74 | | oaord 7253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
 
       |
75 | 74 | 3expb 1210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
  
 

       |
76 | | eleq1 2519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       

    |
77 | 75, 76 | sylan9bb 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         

    |
78 | 77 | an32s 814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
               |
79 | 78 | biimpar 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       
 

    |
80 | | eqimss2 3487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
81 | 80 | ad3antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       
 

      |
82 | 79, 81 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       
 

        |
83 | 82 | anasss 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             
     |
84 | 83 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      
  
   
     |
85 | 84 | reximdv2 2860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
 
 


    |
86 | 85 | adantrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
   

 
     |
87 | 73, 86 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
   

    |
88 | 87 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
          |
89 | | eloni 5436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
90 | | eloni 5436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
91 | | ordtri2or 5521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  

   |
92 | 89, 90, 91 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
 
   |
93 | 92 | ad2ant2l 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
      |
94 | 93 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
   
   |
95 | 71, 88, 94 | mpjaod 383 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
   
    |
96 | 95 | exp45 619 |
. . . . . . . . . . . . . . . . . . . . . . . 24

 
    


      |
97 | 96 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
 
  



     |
98 | 97 | adantld 469 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 
 
           |
99 | 98 | imp32 435 |
. . . . . . . . . . . . . . . . . . . . 21
   
   
  
 


   |
100 | | simplrr 772 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
  
 
   |
101 | | onelon 5451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
102 | 101, 30 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
 
    |
103 | 102 | exp32 610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
104 | 103 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       |
105 | 104 | imp31 434 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
    |
106 | 105 | adantll 721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
       |
107 | 106 | adantlr 722 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
  
 
     |
108 | | simpll 761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
109 | 108 | ad2antlr 734 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
  
 
   |
110 | | oaword 7255 |
. . . . . . . . . . . . . . . . . . . . . . 23
  

   
         |
111 | 100, 107,
109, 110 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . . . . . 22
        
  
 
 
 
         |
112 | 111 | rexbidva 2900 |
. . . . . . . . . . . . . . . . . . . . 21
   
   
  
 
 
   

       |
113 | 99, 112 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . 20
   
   
  
 

        |
114 | 113 | exp32 610 |
. . . . . . . . . . . . . . . . . . 19
  
 
 
        
      |
115 | 59, 114 | mpdd 41 |
. . . . . . . . . . . . . . . . . 18
  
 
 
   
         |
116 | 115 | exp32 610 |
. . . . . . . . . . . . . . . . 17



 
   
           |
117 | 52, 116 | mpd 15 |
. . . . . . . . . . . . . . . 16


 
   
          |
118 | 117 | exp4a 611 |
. . . . . . . . . . . . . . 15



  

           |
119 | 118 | imp31 434 |
. . . . . . . . . . . . . 14
  

   

         |
120 | 119 | ralrimiv 2802 |
. . . . . . . . . . . . 13
  

      

      |
121 | | iunss2 4326 |
. . . . . . . . . . . . 13
 
   
      
      
     |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . 12
  

      
  
    |
123 | 122 | ancoms 455 |
. . . . . . . . . . 11
     
      
     |
124 | | oaordi 7252 |
. . . . . . . . . . . . . . . . . . 19
 
         |
125 | 124 | anim1d 568 |
. . . . . . . . . . . . . . . . . 18
 
       
    

       |
126 | | oveq2 6303 |
. . . . . . . . . . . . . . . . . . . 20
           |
127 | 126 | eleq2d 2516 |
. . . . . . . . . . . . . . . . . . 19
     

      |
128 | 127 | rspcev 3152 |
. . . . . . . . . . . . . . . . . 18
     
     
       |
129 | 125, 128 | syl6 34 |
. . . . . . . . . . . . . . . . 17
 
       
         |
130 | 129 | expd 438 |
. . . . . . . . . . . . . . . 16
 
                 |
131 | 130 | rexlimdv 2879 |
. . . . . . . . . . . . . . 15
 
                |
132 | | eliun 4286 |
. . . . . . . . . . . . . . 15
   
 


     |
133 | | eliun 4286 |
. . . . . . . . . . . . . . 15
      
        |
134 | 131, 132,
133 | 3imtr4g 274 |
. . . . . . . . . . . . . 14
 
  
   
         |
135 | 134 | ssrdv 3440 |
. . . . . . . . . . . . 13
 
  
           |
136 | 52, 135 | sylan 474 |
. . . . . . . . . . . 12
   
            |
137 | 136 | adantl 468 |
. . . . . . . . . . 11
     

           |
138 | 123, 137 | eqssd 3451 |
. . . . . . . . . 10
     
       
    |
139 | 50, 138 | eqtrd 2487 |
. . . . . . . . 9
           
    |
140 | 139 | an12s 811 |
. . . . . . . 8
  
        
    |
141 | 140 | adantr 467 |
. . . . . . 7
   
  
        
    
      |
142 | | iuneq2 4298 |
. . . . . . . 8
 
     
  
    
      |
143 | 142 | adantl 468 |
. . . . . . 7
   
  
        
     
      |
144 | 141, 143 | eqtr4d 2490 |
. . . . . 6
   
  
        
    
      |
145 | 43, 144 | eqtr4d 2490 |
. . . . 5
   
  
        
          |
146 | 145 | exp31 609 |
. . . 4

 
  
                    |
147 | 4, 8, 12, 16, 23, 37, 146 | tfinds3 6696 |
. . 3
               |
148 | 147 | com12 32 |
. 2
 
             |
149 | 148 | 3impia 1206 |
1
 
      
    |