Step | Hyp | Ref
| Expression |
1 | | elnn0 10696 |
. 2

    |
2 | | oveq1 6210 |
. . . . . . . 8
       |
3 | 2 | oveq2d 6219 |
. . . . . . 7
               |
4 | | fveq2 5802 |
. . . . . . . 8
           |
5 | 4 | oveq2d 6219 |
. . . . . . 7
                       |
6 | 3, 5 | breq12d 4416 |
. . . . . 6
       
         
                   |
7 | 6 | imbi2d 316 |
. . . . 5
        
          

                    |
8 | | oveq1 6210 |
. . . . . . . 8
       |
9 | 8 | oveq2d 6219 |
. . . . . . 7
               |
10 | | fveq2 5802 |
. . . . . . . 8
           |
11 | 10 | oveq2d 6219 |
. . . . . . 7
                       |
12 | 9, 11 | breq12d 4416 |
. . . . . 6
       
         
                   |
13 | 12 | imbi2d 316 |
. . . . 5
        
          

                    |
14 | | oveq1 6210 |
. . . . . . . 8
           |
15 | 14 | oveq2d 6219 |
. . . . . . 7
                   |
16 | | fveq2 5802 |
. . . . . . . 8
               |
17 | 16 | oveq2d 6219 |
. . . . . . 7
                           |
18 | 15, 17 | breq12d 4416 |
. . . . . 6
         
         
                       |
19 | 18 | imbi2d 316 |
. . . . 5
          
          

                        |
20 | | oveq1 6210 |
. . . . . . . 8
       |
21 | 20 | oveq2d 6219 |
. . . . . . 7
          
    |
22 | | fveq2 5802 |
. . . . . . . 8
           |
23 | 22 | oveq2d 6219 |
. . . . . . 7
                       |
24 | 21, 23 | breq12d 4416 |
. . . . . 6
       
         
                   |
25 | 24 | imbi2d 316 |
. . . . 5
        
          

                    |
26 | | nnre 10444 |
. . . . . . 7
   |
27 | | nnge1 10463 |
. . . . . . 7
   |
28 | | elnnuz 11012 |
. . . . . . . 8

      |
29 | 28 | biimpi 194 |
. . . . . . 7
       |
30 | 26, 27, 29 | leexp2ad 12161 |
. . . . . 6
           |
31 | | 0p1e1 10548 |
. . . . . . . 8
   |
32 | 31 | oveq2i 6214 |
. . . . . . 7
           |
33 | 32 | a1i 11 |
. . . . . 6
             |
34 | | fac0 12175 |
. . . . . . . 8
     |
35 | 34 | oveq2i 6214 |
. . . . . . 7
                 |
36 | | nnnn0 10701 |
. . . . . . . . . 10
   |
37 | 26, 36 | reexpcld 12146 |
. . . . . . . . 9
       |
38 | 37 | recnd 9527 |
. . . . . . . 8
       |
39 | 38 | mulid1d 9518 |
. . . . . . 7
             |
40 | 35, 39 | syl5eq 2507 |
. . . . . 6
                 |
41 | 30, 33, 40 | 3brtr4d 4433 |
. . . . 5
                   |
42 | 26 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
                        
   
  |
43 | | simpllr 758 |
. . . . . . . . . . . . . . 15
                        
   
  |
44 | | peano2nn0 10735 |
. . . . . . . . . . . . . . 15

    |
45 | 43, 44 | syl 16 |
. . . . . . . . . . . . . 14
                        
   
    |
46 | 42, 45 | reexpcld 12146 |
. . . . . . . . . . . . 13
                        
   
        |
47 | 36 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
                        
   
  |
48 | 42, 47 | reexpcld 12146 |
. . . . . . . . . . . . . 14
                        
   
      |
49 | | faccl 12182 |
. . . . . . . . . . . . . . . 16

      |
50 | 43, 49 | syl 16 |
. . . . . . . . . . . . . . 15
                        
   
      |
51 | 50 | nnred 10452 |
. . . . . . . . . . . . . 14
                        
   
      |
52 | 48, 51 | remulcld 9529 |
. . . . . . . . . . . . 13
                        
   
            |
53 | | nn0re 10703 |
. . . . . . . . . . . . . 14

  |
54 | | peano2re 9657 |
. . . . . . . . . . . . . 14
     |
55 | 43, 53, 54 | 3syl 20 |
. . . . . . . . . . . . 13
                        
   
    |
56 | | nngt0 10466 |
. . . . . . . . . . . . . . . 16
   |
57 | 56 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
                        
   
  |
58 | | 0re 9501 |
. . . . . . . . . . . . . . . 16
 |
59 | | ltle 9578 |
. . . . . . . . . . . . . . . 16
 
 
   |
60 | 58, 59 | mpan 670 |
. . . . . . . . . . . . . . 15
 
   |
61 | 42, 57, 60 | sylc 60 |
. . . . . . . . . . . . . 14
                        
   
  |
62 | 42, 45, 61 | expge0d 12147 |
. . . . . . . . . . . . 13
                        
   
        |
63 | | simplr 754 |
. . . . . . . . . . . . 13
                        
   
                  |
64 | | simprr 756 |
. . . . . . . . . . . . 13
                        
   
    |
65 | 46, 52, 42, 55, 62, 61, 63, 64 | lemul12ad 10390 |
. . . . . . . . . . . 12
                        
   
                        |
66 | 65 | anandis 826 |
. . . . . . . . . . 11
                                                 |
67 | | nncn 10445 |
. . . . . . . . . . . . 13
   |
68 | | expp1 11993 |
. . . . . . . . . . . . 13
                       |
69 | 67, 44, 68 | syl2an 477 |
. . . . . . . . . . . 12
 
                   |
70 | 69 | adantr 465 |
. . . . . . . . . . 11
                                           |
71 | | facp1 12177 |
. . . . . . . . . . . . . . 15

                |
72 | 71 | adantl 466 |
. . . . . . . . . . . . . 14
 
                 |
73 | 72 | oveq2d 6219 |
. . . . . . . . . . . . 13
 
                             |
74 | 38 | adantr 465 |
. . . . . . . . . . . . . 14
 
       |
75 | 49 | nncnd 10453 |
. . . . . . . . . . . . . . 15

      |
76 | 75 | adantl 466 |
. . . . . . . . . . . . . 14
 
       |
77 | | nn0cn 10704 |
. . . . . . . . . . . . . . . 16

  |
78 | | peano2cn 9656 |
. . . . . . . . . . . . . . . 16
     |
79 | 77, 78 | syl 16 |
. . . . . . . . . . . . . . 15

    |
80 | 79 | adantl 466 |
. . . . . . . . . . . . . 14
 
     |
81 | 74, 76, 80 | mulassd 9524 |
. . . . . . . . . . . . 13
 
                               |
82 | 73, 81 | eqtr4d 2498 |
. . . . . . . . . . . 12
 
                             |
83 | 82 | adantr 465 |
. . . . . . . . . . 11
                                                     |
84 | 66, 70, 83 | 3brtr4d 4433 |
. . . . . . . . . 10
                                               |
85 | 84 | exp32 605 |
. . . . . . . . 9
 
                    
                        |
86 | 85 | com23 78 |
. . . . . . . 8
 
                    
                        |
87 | | nn0ltp1le 10817 |
. . . . . . . . . . 11
   
           |
88 | 44, 36, 87 | syl2anr 478 |
. . . . . . . . . 10
 
           |
89 | | peano2nn0 10735 |
. . . . . . . . . . . . . . 15
  
      |
90 | 44, 89 | syl 16 |
. . . . . . . . . . . . . 14

      |
91 | | reexpcl 12003 |
. . . . . . . . . . . . . 14
                 |
92 | 26, 90, 91 | syl2an 477 |
. . . . . . . . . . . . 13
 
           |
93 | 92 | adantr 465 |
. . . . . . . . . . . 12
       
           |
94 | 37 | ad2antrr 725 |
. . . . . . . . . . . 12
       
       |
95 | | faccl 12182 |
. . . . . . . . . . . . . . . 16
  
        |
96 | 44, 95 | syl 16 |
. . . . . . . . . . . . . . 15

        |
97 | 96 | nnred 10452 |
. . . . . . . . . . . . . 14

        |
98 | | remulcl 9482 |
. . . . . . . . . . . . . 14
                           |
99 | 37, 97, 98 | syl2an 477 |
. . . . . . . . . . . . 13
 
               |
100 | 99 | adantr 465 |
. . . . . . . . . . . 12
       
               |
101 | 26 | ad2antrr 725 |
. . . . . . . . . . . . 13
       
   |
102 | 27 | ad2antrr 725 |
. . . . . . . . . . . . 13
       

  |
103 | | simpr 461 |
. . . . . . . . . . . . . 14
       
    
  |
104 | 90 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
       
       |
105 | 104 | nn0zd 10860 |
. . . . . . . . . . . . . . 15
       
       |
106 | | nnz 10783 |
. . . . . . . . . . . . . . . 16
   |
107 | 106 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
       
   |
108 | | eluz 10989 |
. . . . . . . . . . . . . . 15
     
         
       |
109 | 105, 107,
108 | syl2anc 661 |
. . . . . . . . . . . . . 14
       
         
       |
110 | 103, 109 | mpbird 232 |
. . . . . . . . . . . . 13
       
           |
111 | 101, 102,
110 | leexp2ad 12161 |
. . . . . . . . . . . 12
       
        
      |
112 | 37, 97 | anim12i 566 |
. . . . . . . . . . . . . 14
 
               |
113 | | nn0re 10703 |
. . . . . . . . . . . . . . . . 17

  |
114 | | id 22 |
. . . . . . . . . . . . . . . . 17

  |
115 | | nn0ge0 10720 |
. . . . . . . . . . . . . . . . 17

  |
116 | 113, 114,
115 | expge0d 12147 |
. . . . . . . . . . . . . . . 16

      |
117 | 36, 116 | syl 16 |
. . . . . . . . . . . . . . 15
       |
118 | 96 | nnge1d 10479 |
. . . . . . . . . . . . . . 15

        |
119 | 117, 118 | anim12i 566 |
. . . . . . . . . . . . . 14
 
               |
120 | | lemulge11 10306 |
. . . . . . . . . . . . . 14
                  
                          |
121 | 112, 119,
120 | syl2anc 661 |
. . . . . . . . . . . . 13
 
    
              |
122 | 121 | adantr 465 |
. . . . . . . . . . . 12
       
    
              |
123 | 93, 94, 100, 111, 122 | letrd 9643 |
. . . . . . . . . . 11
       
        
              |
124 | 123 | ex 434 |
. . . . . . . . . 10
 
             
               |
125 | 88, 124 | sylbid 215 |
. . . . . . . . 9
 
           
               |
126 | 125 | a1dd 46 |
. . . . . . . 8
 
                                             |
127 | 53, 54 | syl 16 |
. . . . . . . . 9

    |
128 | | lelttric 9596 |
. . . . . . . . 9
             |
129 | 26, 127, 128 | syl2an 477 |
. . . . . . . 8
 
         |
130 | 86, 126, 129 | mpjaod 381 |
. . . . . . 7
 
                                         |
131 | 130 | expcom 435 |
. . . . . 6

       
                                  |
132 | 131 | a2d 26 |
. . . . 5

                           
                |
133 | 7, 13, 19, 25, 41, 132 | nn0ind 10853 |
. . . 4

                    |
134 | 133 | impcom 430 |
. . 3
 
    
 
            |
135 | | faccl 12182 |
. . . . . . . 8

      |
136 | 135 | nnnn0d 10751 |
. . . . . . 7

      |
137 | 136 | nn0ge0d 10754 |
. . . . . 6

      |
138 | | nn0p1nn 10734 |
. . . . . . 7

    |
139 | 138 | 0expd 12145 |
. . . . . 6

        |
140 | | 0exp0e1 11991 |
. . . . . . . 8
     |
141 | 140 | oveq1i 6213 |
. . . . . . 7
                 |
142 | 135 | nncnd 10453 |
. . . . . . . 8

      |
143 | 142 | mulid2d 9519 |
. . . . . . 7

            |
144 | 141, 143 | syl5eq 2507 |
. . . . . 6

                |
145 | 137, 139,
144 | 3brtr4d 4433 |
. . . . 5

                  |
146 | | oveq1 6210 |
. . . . . 6
          
    |
147 | | oveq12 6212 |
. . . . . . . 8
             |
148 | 147 | anidms 645 |
. . . . . . 7
           |
149 | 148 | oveq1d 6218 |
. . . . . 6
                       |
150 | 146, 149 | breq12d 4416 |
. . . . 5
     
 
         
                   |
151 | 145, 150 | syl5ibr 221 |
. . . 4
 
                   |
152 | 151 | imp 429 |
. . 3
      
 
            |
153 | 134, 152 | jaoian 782 |
. 2
  


                  |
154 | 1, 153 | sylanb 472 |
1
 
    
 
            |