This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem facndiv

Description: No positive integer (greater than one) divides the factorial plus one of an equal or larger number. (Contributed by NM, 3-May-2005)

Ref Expression
Assertion facndiv 
|- ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> -. ( ( ( ! ` M ) + 1 ) / N ) e. ZZ )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( N e. NN -> N e. RR )
2 recnz 
 |-  ( ( N e. RR /\ 1 < N ) -> -. ( 1 / N ) e. ZZ )
3 1 2 sylan 
 |-  ( ( N e. NN /\ 1 < N ) -> -. ( 1 / N ) e. ZZ )
4 3 ad2ant2lr 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> -. ( 1 / N ) e. ZZ )
5 facdiv 
 |-  ( ( M e. NN0 /\ N e. NN /\ N <_ M ) -> ( ( ! ` M ) / N ) e. NN )
6 5 3expa 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ N <_ M ) -> ( ( ! ` M ) / N ) e. NN )
7 6 nnzd 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ N <_ M ) -> ( ( ! ` M ) / N ) e. ZZ )
8 7 adantrl 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( ( ! ` M ) / N ) e. ZZ )
9 zsubcl 
 |-  ( ( ( ( ( ! ` M ) + 1 ) / N ) e. ZZ /\ ( ( ! ` M ) / N ) e. ZZ ) -> ( ( ( ( ! ` M ) + 1 ) / N ) - ( ( ! ` M ) / N ) ) e. ZZ )
10 9 ex 
 |-  ( ( ( ( ! ` M ) + 1 ) / N ) e. ZZ -> ( ( ( ! ` M ) / N ) e. ZZ -> ( ( ( ( ! ` M ) + 1 ) / N ) - ( ( ! ` M ) / N ) ) e. ZZ ) )
11 8 10 syl5com 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( ( ( ( ! ` M ) + 1 ) / N ) e. ZZ -> ( ( ( ( ! ` M ) + 1 ) / N ) - ( ( ! ` M ) / N ) ) e. ZZ ) )
12 faccl 
 |-  ( M e. NN0 -> ( ! ` M ) e. NN )
13 12 nncnd 
 |-  ( M e. NN0 -> ( ! ` M ) e. CC )
14 peano2cn 
 |-  ( ( ! ` M ) e. CC -> ( ( ! ` M ) + 1 ) e. CC )
15 13 14 syl 
 |-  ( M e. NN0 -> ( ( ! ` M ) + 1 ) e. CC )
16 15 ad2antrr 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( ( ! ` M ) + 1 ) e. CC )
17 13 ad2antrr 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( ! ` M ) e. CC )
18 nncn 
 |-  ( N e. NN -> N e. CC )
19 nnne0 
 |-  ( N e. NN -> N =/= 0 )
20 18 19 jca 
 |-  ( N e. NN -> ( N e. CC /\ N =/= 0 ) )
21 20 ad2antlr 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( N e. CC /\ N =/= 0 ) )
22 divsubdir 
 |-  ( ( ( ( ! ` M ) + 1 ) e. CC /\ ( ! ` M ) e. CC /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( ( ( ! ` M ) + 1 ) - ( ! ` M ) ) / N ) = ( ( ( ( ! ` M ) + 1 ) / N ) - ( ( ! ` M ) / N ) ) )
23 16 17 21 22 syl3anc 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( ( ( ( ! ` M ) + 1 ) - ( ! ` M ) ) / N ) = ( ( ( ( ! ` M ) + 1 ) / N ) - ( ( ! ` M ) / N ) ) )
24 ax-1cn 
 |-  1 e. CC
25 pncan2 
 |-  ( ( ( ! ` M ) e. CC /\ 1 e. CC ) -> ( ( ( ! ` M ) + 1 ) - ( ! ` M ) ) = 1 )
26 13 24 25 sylancl 
 |-  ( M e. NN0 -> ( ( ( ! ` M ) + 1 ) - ( ! ` M ) ) = 1 )
27 26 oveq1d 
 |-  ( M e. NN0 -> ( ( ( ( ! ` M ) + 1 ) - ( ! ` M ) ) / N ) = ( 1 / N ) )
28 27 ad2antrr 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( ( ( ( ! ` M ) + 1 ) - ( ! ` M ) ) / N ) = ( 1 / N ) )
29 23 28 eqtr3d 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( ( ( ( ! ` M ) + 1 ) / N ) - ( ( ! ` M ) / N ) ) = ( 1 / N ) )
30 29 eleq1d 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( ( ( ( ( ! ` M ) + 1 ) / N ) - ( ( ! ` M ) / N ) ) e. ZZ <-> ( 1 / N ) e. ZZ ) )
31 11 30 sylibd 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> ( ( ( ( ! ` M ) + 1 ) / N ) e. ZZ -> ( 1 / N ) e. ZZ ) )
32 4 31 mtod 
 |-  ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> -. ( ( ( ! ` M ) + 1 ) / N ) e. ZZ )