Step | Hyp | Ref
| Expression |
1 | | breq2 4009 |
. . . . 5
 
   |
2 | | fveq2 5517 |
. . . . . . 7
           |
3 | 2 | oveq1d 5892 |
. . . . . 6
               |
4 | 3 | eleq1d 2246 |
. . . . 5
       
         |
5 | 1, 4 | imbi12d 234 |
. . . 4
                     |
6 | 5 | imbi2d 230 |
. . 3
            

           |
7 | | breq2 4009 |
. . . . 5
 
   |
8 | | fveq2 5517 |
. . . . . . 7
           |
9 | 8 | oveq1d 5892 |
. . . . . 6
               |
10 | 9 | eleq1d 2246 |
. . . . 5
       
         |
11 | 7, 10 | imbi12d 234 |
. . . 4
                     |
12 | 11 | imbi2d 230 |
. . 3
            

           |
13 | | breq2 4009 |
. . . . 5
   
     |
14 | | fveq2 5517 |
. . . . . . 7
               |
15 | 14 | oveq1d 5892 |
. . . . . 6
                   |
16 | 15 | eleq1d 2246 |
. . . . 5
         
           |
17 | 13, 16 | imbi12d 234 |
. . . 4
                           |
18 | 17 | imbi2d 230 |
. . 3
              
  
             |
19 | | breq2 4009 |
. . . . 5
 
   |
20 | | fveq2 5517 |
. . . . . . 7
           |
21 | 20 | oveq1d 5892 |
. . . . . 6
               |
22 | 21 | eleq1d 2246 |
. . . . 5
       
         |
23 | 19, 22 | imbi12d 234 |
. . . 4
                     |
24 | 23 | imbi2d 230 |
. . 3
            

           |
25 | | nngt0 8946 |
. . . . 5
   |
26 | | 0z 9266 |
. . . . . 6
 |
27 | | nnz 9274 |
. . . . . 6
   |
28 | | zltnle 9301 |
. . . . . 6
 
 
   |
29 | 26, 27, 28 | sylancr 414 |
. . . . 5
 
   |
30 | 25, 29 | mpbid 147 |
. . . 4
   |
31 | 30 | pm2.21d 619 |
. . 3
           |
32 | | peano2nn0 9218 |
. . . . . . . . . . . . 13

    |
33 | 32 | nn0zd 9375 |
. . . . . . . . . . . 12

    |
34 | | zleloe 9302 |
. . . . . . . . . . . 12
                 |
35 | 27, 33, 34 | syl2an 289 |
. . . . . . . . . . 11
 
             |
36 | | nnnn0 9185 |
. . . . . . . . . . . . . 14
   |
37 | | nn0leltp1 9318 |
. . . . . . . . . . . . . 14
 
       |
38 | 36, 37 | sylan 283 |
. . . . . . . . . . . . 13
 
       |
39 | | nn0p1nn 9217 |
. . . . . . . . . . . . . . . . . . 19

    |
40 | | nnmulcl 8942 |
. . . . . . . . . . . . . . . . . . 19
                       |
41 | 39, 40 | sylan2 286 |
. . . . . . . . . . . . . . . . . 18
       
             |
42 | 41 | expcom 116 |
. . . . . . . . . . . . . . . . 17

                    |
43 | 42 | adantl 277 |
. . . . . . . . . . . . . . . 16
 
                     |
44 | | faccl 10717 |
. . . . . . . . . . . . . . . . . . . 20

      |
45 | 44 | nncnd 8935 |
. . . . . . . . . . . . . . . . . . 19

      |
46 | 45 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
 
       |
47 | 32 | nn0cnd 9233 |
. . . . . . . . . . . . . . . . . . 19

    |
48 | 47 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
 
     |
49 | | nncn 8929 |
. . . . . . . . . . . . . . . . . . 19
   |
50 | 49 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
 

  |
51 | | nnap0 8950 |
. . . . . . . . . . . . . . . . . . 19
 #   |
52 | 51 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
 
 #   |
53 | 46, 48, 50, 52 | div23apd 8787 |
. . . . . . . . . . . . . . . . 17
 
                       |
54 | 53 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
 
                         |
55 | 43, 54 | sylibrd 169 |
. . . . . . . . . . . . . . 15
 
                     |
56 | 55 | imim2d 54 |
. . . . . . . . . . . . . 14
 
  
       
              |
57 | 56 | com23 78 |
. . . . . . . . . . . . 13
 
   
                     |
58 | 38, 57 | sylbird 170 |
. . . . . . . . . . . 12
 
                           |
59 | 46, 50, 52 | divcanap4d 8755 |
. . . . . . . . . . . . . . 15
 
               |
60 | 44 | adantl 277 |
. . . . . . . . . . . . . . 15
 
       |
61 | 59, 60 | eqeltrd 2254 |
. . . . . . . . . . . . . 14
 
           |
62 | | oveq2 5885 |
. . . . . . . . . . . . . . . 16
                   |
63 | 62 | oveq1d 5892 |
. . . . . . . . . . . . . . 15
                       |
64 | 63 | eleq1d 2246 |
. . . . . . . . . . . . . 14
           
             |
65 | 61, 64 | syl5ibcom 155 |
. . . . . . . . . . . . 13
 
                 |
66 | 65 | a1dd 48 |
. . . . . . . . . . . 12
 
                           |
67 | 58, 66 | jaod 717 |
. . . . . . . . . . 11
 
                               |
68 | 35, 67 | sylbid 150 |
. . . . . . . . . 10
 
                           |
69 | 68 | ex 115 |
. . . . . . . . 9
  
   
                      |
70 | 69 | com34 83 |
. . . . . . . 8
             
               |
71 | 70 | com12 30 |
. . . . . . 7

            
               |
72 | 71 | imp4d 352 |
. . . . . 6

   
                        |
73 | | facp1 10712 |
. . . . . . . 8

                |
74 | 73 | oveq1d 5892 |
. . . . . . 7

                    |
75 | 74 | eleq1d 2246 |
. . . . . 6

        
             |
76 | 72, 75 | sylibrd 169 |
. . . . 5

   
                      |
77 | 76 | exp4d 369 |
. . . 4

            
             |
78 | 77 | a2d 26 |
. . 3

  
        
  
             |
79 | 6, 12, 18, 24, 31, 78 | nn0ind 9369 |
. 2

            |
80 | 79 | 3imp 1193 |
1
 
         |