Step | Hyp | Ref
| Expression |
1 | | bcval2 12487 |
. . . 4
                
          |
2 | 1 | adantl 468 |
. . 3
        
                      |
3 | | mulcl 9620 |
. . . . . . . . 9
 
     |
4 | 3 | adantl 468 |
. . . . . . . 8
   


    
          |
5 | | mulass 9624 |
. . . . . . . . 9
 
           |
6 | 5 | adantl 468 |
. . . . . . . 8
   


    
                |
7 | | simplr 761 |
. . . . . . . . . . . . 13
        
  |
8 | | elfzuz3 11794 |
. . . . . . . . . . . . . 14
           |
9 | 8 | adantl 468 |
. . . . . . . . . . . . 13
        
      |
10 | | eluznn 11226 |
. . . . . . . . . . . . 13
 
    
  |
11 | 7, 9, 10 | syl2anc 666 |
. . . . . . . . . . . 12
        
  |
12 | 11 | adantrr 722 |
. . . . . . . . . . 11
        
      |
13 | | simplr 761 |
. . . . . . . . . . 11
        
      |
14 | | nnre 10613 |
. . . . . . . . . . . 12
   |
15 | | nnrp 11308 |
. . . . . . . . . . . 12
   |
16 | | ltsubrp 11332 |
. . . . . . . . . . . 12
 
  
  |
17 | 14, 15, 16 | syl2an 480 |
. . . . . . . . . . 11
 
  
  |
18 | 12, 13, 17 | syl2anc 666 |
. . . . . . . . . 10
        
    
   |
19 | 12 | nnzd 11036 |
. . . . . . . . . . . 12
        
      |
20 | | nnz 10956 |
. . . . . . . . . . . . 13
   |
21 | 20 | ad2antlr 732 |
. . . . . . . . . . . 12
        
      |
22 | 19, 21 | zsubcld 11042 |
. . . . . . . . . . 11
        
    
   |
23 | | zltp1le 10983 |
. . . . . . . . . . 11
   
           |
24 | 22, 19, 23 | syl2anc 666 |
. . . . . . . . . 10
        
      
 
     |
25 | 18, 24 | mpbid 214 |
. . . . . . . . 9
        
          |
26 | 22 | peano2zd 11040 |
. . . . . . . . . 10
        
          |
27 | | eluz 11169 |
. . . . . . . . . 10
     
         
 
     |
28 | 26, 19, 27 | syl2anc 666 |
. . . . . . . . 9
        
    
       
 
     |
29 | 25, 28 | mpbird 236 |
. . . . . . . 8
        
        
     |
30 | | simprr 765 |
. . . . . . . . 9
        
    
   |
31 | | nnuz 11191 |
. . . . . . . . 9
     |
32 | 30, 31 | syl6eleq 2538 |
. . . . . . . 8
        
    
       |
33 | | fvi 5920 |
. . . . . . . . . 10
         |
34 | | elfzelz 11797 |
. . . . . . . . . . 11
       |
35 | 34 | zcnd 11038 |
. . . . . . . . . 10
       |
36 | 33, 35 | eqeltrd 2528 |
. . . . . . . . 9
         |
37 | 36 | adantl 468 |
. . . . . . . 8
   


    
            |
38 | 4, 6, 29, 32, 37 | seqsplit 12243 |
. . . . . . 7
        
                             |
39 | | facnn 12458 |
. . . . . . . 8
    
       |
40 | 12, 39 | syl 17 |
. . . . . . 7
        
       
       |
41 | | facnn 12458 |
. . . . . . . . 9
                  |
42 | 30, 41 | syl 17 |
. . . . . . . 8
        
                   |
43 | 42 | oveq1d 6303 |
. . . . . . 7
        
        
                 
              |
44 | 38, 40, 43 | 3eqtr4d 2494 |
. . . . . 6
        
                           |
45 | 44 | expr 619 |
. . . . 5
        
 

        
               |
46 | | simpll 759 |
. . . . . . . . 9
        
  |
47 | | faccl 12466 |
. . . . . . . . 9

      |
48 | | nncn 10614 |
. . . . . . . . 9
           |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . 8
        
      |
50 | 49 | mulid2d 9658 |
. . . . . . 7
        
            |
51 | 11, 39 | syl 17 |
. . . . . . . 8
        
           |
52 | 51 | oveq2d 6304 |
. . . . . . 7
        
               |
53 | 50, 52 | eqtr3d 2486 |
. . . . . 6
        
             |
54 | | fveq2 5863 |
. . . . . . . . 9
               |
55 | | fac0 12459 |
. . . . . . . . 9
     |
56 | 54, 55 | syl6eq 2500 |
. . . . . . . 8
           |
57 | | oveq1 6295 |
. . . . . . . . . . 11
           |
58 | | 0p1e1 10718 |
. . . . . . . . . . 11
   |
59 | 57, 58 | syl6eq 2500 |
. . . . . . . . . 10
         |
60 | 59 | seqeq1d 12216 |
. . . . . . . . 9
        
    |
61 | 60 | fveq1d 5865 |
. . . . . . . 8
                   |
62 | 56, 61 | oveq12d 6306 |
. . . . . . 7
       
                     |
63 | 62 | eqeq2d 2460 |
. . . . . 6
                                       |
64 | 53, 63 | syl5ibrcom 226 |
. . . . 5
        
 
                         |
65 | | fznn0sub 11828 |
. . . . . . 7
     
   |
66 | 65 | adantl 468 |
. . . . . 6
        
    |
67 | | elnn0 10868 |
. . . . . 6
  
        |
68 | 66, 67 | sylib 200 |
. . . . 5
        
 
      |
69 | 45, 64, 68 | mpjaod 383 |
. . . 4
        
        
              |
70 | 69 | oveq1d 6303 |
. . 3
        
                                        
          |
71 | | eqid 2450 |
. . . . . 6
                 |
72 | | nn0z 10957 |
. . . . . . . . 9

  |
73 | | zsubcl 10976 |
. . . . . . . . 9
 
     |
74 | 72, 20, 73 | syl2an 480 |
. . . . . . . 8
 
     |
75 | 74 | peano2zd 11040 |
. . . . . . 7
 
       |
76 | 75 | adantr 467 |
. . . . . 6
        
 
    |
77 | | fvi 5920 |
. . . . . . . 8
        
    |
78 | | eluzelcn 11167 |
. . . . . . . 8
        
  |
79 | 77, 78 | eqeltrd 2528 |
. . . . . . 7
        
    |
80 | 79 | adantl 468 |
. . . . . 6
   

         
   
    |
81 | 3 | adantl 468 |
. . . . . 6
   

     
 
    |
82 | 71, 76, 80, 81 | seqf 12231 |
. . . . 5
        
                    |
83 | 11, 7, 17 | syl2anc 666 |
. . . . . . 7
        
    |
84 | 74 | adantr 467 |
. . . . . . . 8
        
    |
85 | 11 | nnzd 11036 |
. . . . . . . 8
        
  |
86 | 84, 85, 23 | syl2anc 666 |
. . . . . . 7
        
 
        |
87 | 83, 86 | mpbid 214 |
. . . . . 6
        
 
    |
88 | 76, 85, 27 | syl2anc 666 |
. . . . . 6
        
     
      
   |
89 | 87, 88 | mpbird 236 |
. . . . 5
        
    
     |
90 | 82, 89 | ffvelrnd 6021 |
. . . 4
        
           |
91 | | elfznn0 11884 |
. . . . . . 7
       |
92 | 91 | adantl 468 |
. . . . . 6
        
  |
93 | | faccl 12466 |
. . . . . 6

      |
94 | 92, 93 | syl 17 |
. . . . 5
        
      |
95 | 94 | nncnd 10622 |
. . . 4
        
      |
96 | | faccl 12466 |
. . . . . 6
  
        |
97 | 66, 96 | syl 17 |
. . . . 5
        
        |
98 | 97 | nncnd 10622 |
. . . 4
        
        |
99 | 94 | nnne0d 10651 |
. . . 4
        
      |
100 | 97 | nnne0d 10651 |
. . . 4
        
        |
101 | 90, 95, 98, 99, 100 | divcan5d 10406 |
. . 3
        
     
                                          |
102 | 2, 70, 101 | 3eqtrd 2488 |
. 2
        
                   |
103 | | nnnn0 10873 |
. . . . 5
   |
104 | 103 | ad2antlr 732 |
. . . 4
           |
105 | | nncn 10614 |
. . . . 5
           |
106 | | nnne0 10639 |
. . . . 5
           |
107 | 105, 106 | div0d 10379 |
. . . 4
             |
108 | 104, 93, 107 | 3syl 18 |
. . 3
                 |
109 | 3 | adantl 468 |
. . . . 5
   

     
 
    |
110 | | fvi 5920 |
. . . . . . 7
             |
111 | | elfzelz 11797 |
. . . . . . . 8
           |
112 | 111 | zcnd 11038 |
. . . . . . 7
           |
113 | 110, 112 | eqeltrd 2528 |
. . . . . 6
             |
114 | 113 | adantl 468 |
. . . . 5
   

                  |
115 | | mul02 9808 |
. . . . . 6
     |
116 | 115 | adantl 468 |
. . . . 5
   

          |
117 | | mul01 9809 |
. . . . . 6
     |
118 | 117 | adantl 468 |
. . . . 5
   

          |
119 | | simpr 463 |
. . . . . . . . 9
        
      |
120 | | nn0uz 11190 |
. . . . . . . . . . . 12
     |
121 | 104, 120 | syl6eleq 2538 |
. . . . . . . . . . 11
               |
122 | 72 | ad2antrr 731 |
. . . . . . . . . . 11
           |
123 | | elfz5 11789 |
. . . . . . . . . . 11
       
   
   |
124 | 121, 122,
123 | syl2anc 666 |
. . . . . . . . . 10
         
   
   |
125 | | nn0re 10875 |
. . . . . . . . . . . 12

  |
126 | 125 | ad2antrr 731 |
. . . . . . . . . . 11
           |
127 | | nnre 10613 |
. . . . . . . . . . . 12
   |
128 | 127 | ad2antlr 732 |
. . . . . . . . . . 11
           |
129 | 126, 128 | subge0d 10200 |
. . . . . . . . . 10
         
 
   |
130 | 124, 129 | bitr4d 260 |
. . . . . . . . 9
         
   
     |
131 | 119, 130 | mtbid 302 |
. . . . . . . 8
             |
132 | 74 | adantr 467 |
. . . . . . . . . 10
         
   |
133 | 132 | zred 11037 |
. . . . . . . . 9
         
   |
134 | | 0re 9640 |
. . . . . . . . 9
 |
135 | | ltnle 9710 |
. . . . . . . . 9
   
   
     |
136 | 133, 134,
135 | sylancl 667 |
. . . . . . . 8
           
     |
137 | 131, 136 | mpbird 236 |
. . . . . . 7
         
   |
138 | | 0z 10945 |
. . . . . . . 8
 |
139 | | zltp1le 10983 |
. . . . . . . 8
   
           |
140 | 132, 138,
139 | sylancl 667 |
. . . . . . 7
           
 
     |
141 | 137, 140 | mpbid 214 |
. . . . . 6
               |
142 | | nn0ge0 10892 |
. . . . . . 7

  |
143 | 142 | ad2antrr 731 |
. . . . . 6
           |
144 | | 0zd 10946 |
. . . . . . 7
           |
145 | 75 | adantr 467 |
. . . . . . 7
               |
146 | | elfz 11787 |
. . . . . . 7
     
              
    |
147 | 144, 145,
122, 146 | syl3anc 1267 |
. . . . . 6
                 
         |
148 | 141, 143,
147 | mpbir2and 932 |
. . . . 5
                   |
149 | | simpll 759 |
. . . . 5
           |
150 | | 0cn 9632 |
. . . . . 6
 |
151 | | fvi 5920 |
. . . . . 6
     |
152 | 150, 151 | mp1i 13 |
. . . . 5
             |
153 | 109, 114,
116, 118, 148, 149, 152 | seqz 12258 |
. . . 4
                    |
154 | 153 | oveq1d 6303 |
. . 3
                                |
155 | | bcval3 12488 |
. . . . 5
 
         |
156 | 20, 155 | syl3an2 1301 |
. . . 4
 
         |
157 | 156 | 3expa 1207 |
. . 3
             |
158 | 108, 154,
157 | 3eqtr4rd 2495 |
. 2
                            |
159 | 102, 158 | pm2.61dan 799 |
1
 
                    |