Step | Hyp | Ref
| Expression |
1 | | oveq2 5883 |
. . . . . . 7
       |
2 | 1 | oveq2d 5891 |
. . . . . 6
           |
3 | | oveq2 5883 |
. . . . . . 7
       |
4 | 3 | oveq2d 5891 |
. . . . . 6
               |
5 | 2, 4 | eqeq12d 2192 |
. . . . 5
           
             |
6 | 5 | imbi2d 230 |
. . . 4
   

                            |
7 | | oveq2 5883 |
. . . . . . 7

      |
8 | 7 | oveq2d 5891 |
. . . . . 6

          |
9 | | oveq2 5883 |
. . . . . . 7

      |
10 | 9 | oveq2d 5891 |
. . . . . 6

              |
11 | 8, 10 | eqeq12d 2192 |
. . . . 5

          
             |
12 | | oveq2 5883 |
. . . . . . 7
       |
13 | 12 | oveq2d 5891 |
. . . . . 6
           |
14 | | oveq2 5883 |
. . . . . . 7
       |
15 | 14 | oveq2d 5891 |
. . . . . 6
               |
16 | 13, 15 | eqeq12d 2192 |
. . . . 5
           
             |
17 | | oveq2 5883 |
. . . . . . 7
       |
18 | 17 | oveq2d 5891 |
. . . . . 6
      
    |
19 | | oveq2 5883 |
. . . . . . 7
       |
20 | 19 | oveq2d 5891 |
. . . . . 6
               |
21 | 18, 20 | eqeq12d 2192 |
. . . . 5
   
                     |
22 | | nna0 6475 |
. . . . . . . . 9
     |
23 | 22 | adantl 277 |
. . . . . . . 8
 
     |
24 | 23 | oveq2d 5891 |
. . . . . . 7
 
         |
25 | | nnmcl 6482 |
. . . . . . . 8
 
     |
26 | | nna0 6475 |
. . . . . . . 8
           |
27 | 25, 26 | syl 14 |
. . . . . . 7
 
         |
28 | 24, 27 | eqtr4d 2213 |
. . . . . 6
 
           |
29 | | nnm0 6476 |
. . . . . . . 8
     |
30 | 29 | adantr 276 |
. . . . . . 7
 
     |
31 | 30 | oveq2d 5891 |
. . . . . 6
 
             |
32 | 28, 31 | eqtr4d 2213 |
. . . . 5
 
             |
33 | | oveq1 5882 |
. . . . . . . . 9
                           |
34 | | nnasuc 6477 |
. . . . . . . . . . . . 13
 
   
   |
35 | 34 | 3adant1 1015 |
. . . . . . . . . . . 12
 
       |
36 | 35 | oveq2d 5891 |
. . . . . . . . . . 11
 
      
    |
37 | | nnacl 6481 |
. . . . . . . . . . . . 13
 
     |
38 | | nnmsuc 6478 |
. . . . . . . . . . . . 13
  
   
          |
39 | 37, 38 | sylan2 286 |
. . . . . . . . . . . 12
  
 
      
     |
40 | 39 | 3impb 1199 |
. . . . . . . . . . 11
 
             |
41 | 36, 40 | eqtrd 2210 |
. . . . . . . . . 10
 
       
     |
42 | | nnmsuc 6478 |
. . . . . . . . . . . . 13
 
         |
43 | 42 | 3adant2 1016 |
. . . . . . . . . . . 12
 
         |
44 | 43 | oveq2d 5891 |
. . . . . . . . . . 11
 
                 |
45 | | nnmcl 6482 |
. . . . . . . . . . . . . . . . . 18
 
     |
46 | | nnaass 6486 |
. . . . . . . . . . . . . . . . . . 19
    

                   |
47 | 25, 46 | syl3an1 1271 |
. . . . . . . . . . . . . . . . . 18
     
                   |
48 | 45, 47 | syl3an2 1272 |
. . . . . . . . . . . . . . . . 17
     
                   |
49 | 48 | 3exp 1202 |
. . . . . . . . . . . . . . . 16
 
  


                    |
50 | 49 | exp4b 367 |
. . . . . . . . . . . . . . 15
 
                         |
51 | 50 | pm2.43a 51 |
. . . . . . . . . . . . . 14
 
                       |
52 | 51 | com4r 86 |
. . . . . . . . . . . . 13
 
                       |
53 | 52 | pm2.43i 49 |
. . . . . . . . . . . 12
 
                     |
54 | 53 | 3imp 1193 |
. . . . . . . . . . 11
 
                   |
55 | 44, 54 | eqtr4d 2213 |
. . . . . . . . . 10
 
                 |
56 | 41, 55 | eqeq12d 2192 |
. . . . . . . . 9
 
           
                 |
57 | 33, 56 | imbitrrid 156 |
. . . . . . . 8
 
                         |
58 | 57 | 3exp 1202 |
. . . . . . 7
 
                           |
59 | 58 | com3r 79 |
. . . . . 6
 
                           |
60 | 59 | impd 254 |
. . . . 5
      
         
            |
61 | 11, 16, 21, 32, 60 | finds2 4601 |
. . . 4
                 |
62 | 6, 61 | vtoclga 2804 |
. . 3
                 |
63 | 62 | expdcom 1442 |
. 2
 
               |
64 | 63 | 3imp 1193 |
1
 
             |