Metamath Proof Explorer

Theorem ndvdssub

Description: Corollary of the division algorithm. If an integer D greater than 1 divides N , then it does not divide any of N - 1 , N - 2 ... N - ( D - 1 ) . (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion ndvdssub 
|- ( ( N e. ZZ /\ D e. NN /\ ( K e. NN /\ K < D ) ) -> ( D || N -> -. D || ( N - K ) ) )

Proof

Step Hyp Ref Expression
1 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
2 nnne0 
 |-  ( K e. NN -> K =/= 0 )
3 1 2 jca 
 |-  ( K e. NN -> ( K e. NN0 /\ K =/= 0 ) )
4 df-ne 
 |-  ( K =/= 0 <-> -. K = 0 )
5 4 anbi2i 
 |-  ( ( K < D /\ K =/= 0 ) <-> ( K < D /\ -. K = 0 ) )
6 divalg2 
 |-  ( ( N e. ZZ /\ D e. NN ) -> E! r e. NN0 ( r < D /\ D || ( N - r ) ) )
7 breq1 
 |-  ( r = x -> ( r < D <-> x < D ) )
8 oveq2 
 |-  ( r = x -> ( N - r ) = ( N - x ) )
9 8 breq2d 
 |-  ( r = x -> ( D || ( N - r ) <-> D || ( N - x ) ) )
10 7 9 anbi12d 
 |-  ( r = x -> ( ( r < D /\ D || ( N - r ) ) <-> ( x < D /\ D || ( N - x ) ) ) )
11 10 reu4 
 |-  ( E! r e. NN0 ( r < D /\ D || ( N - r ) ) <-> ( E. r e. NN0 ( r < D /\ D || ( N - r ) ) /\ A. r e. NN0 A. x e. NN0 ( ( ( r < D /\ D || ( N - r ) ) /\ ( x < D /\ D || ( N - x ) ) ) -> r = x ) ) )
12 6 11 sylib 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( E. r e. NN0 ( r < D /\ D || ( N - r ) ) /\ A. r e. NN0 A. x e. NN0 ( ( ( r < D /\ D || ( N - r ) ) /\ ( x < D /\ D || ( N - x ) ) ) -> r = x ) ) )
13 nngt0 
 |-  ( D e. NN -> 0 < D )
14 13 3ad2ant2 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> 0 < D )
15 zcn 
 |-  ( N e. ZZ -> N e. CC )
16 15 subid1d 
 |-  ( N e. ZZ -> ( N - 0 ) = N )
17 16 breq2d 
 |-  ( N e. ZZ -> ( D || ( N - 0 ) <-> D || N ) )
18 17 biimpar 
 |-  ( ( N e. ZZ /\ D || N ) -> D || ( N - 0 ) )
19 18 3adant2 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> D || ( N - 0 ) )
20 14 19 jca 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> ( 0 < D /\ D || ( N - 0 ) ) )
21 20 3expa 
 |-  ( ( ( N e. ZZ /\ D e. NN ) /\ D || N ) -> ( 0 < D /\ D || ( N - 0 ) ) )
22 21 anim1ci 
 |-  ( ( ( ( N e. ZZ /\ D e. NN ) /\ D || N ) /\ ( r < D /\ D || ( N - r ) ) ) -> ( ( r < D /\ D || ( N - r ) ) /\ ( 0 < D /\ D || ( N - 0 ) ) ) )
23 0nn0 
 |-  0 e. NN0
24 breq1 
 |-  ( x = 0 -> ( x < D <-> 0 < D ) )
25 oveq2 
 |-  ( x = 0 -> ( N - x ) = ( N - 0 ) )
26 25 breq2d 
 |-  ( x = 0 -> ( D || ( N - x ) <-> D || ( N - 0 ) ) )
27 24 26 anbi12d 
 |-  ( x = 0 -> ( ( x < D /\ D || ( N - x ) ) <-> ( 0 < D /\ D || ( N - 0 ) ) ) )
28 27 anbi2d 
 |-  ( x = 0 -> ( ( ( r < D /\ D || ( N - r ) ) /\ ( x < D /\ D || ( N - x ) ) ) <-> ( ( r < D /\ D || ( N - r ) ) /\ ( 0 < D /\ D || ( N - 0 ) ) ) ) )
29 eqeq2 
 |-  ( x = 0 -> ( r = x <-> r = 0 ) )
30 28 29 imbi12d 
 |-  ( x = 0 -> ( ( ( ( r < D /\ D || ( N - r ) ) /\ ( x < D /\ D || ( N - x ) ) ) -> r = x ) <-> ( ( ( r < D /\ D || ( N - r ) ) /\ ( 0 < D /\ D || ( N - 0 ) ) ) -> r = 0 ) ) )
31 30 rspcv 
 |-  ( 0 e. NN0 -> ( A. x e. NN0 ( ( ( r < D /\ D || ( N - r ) ) /\ ( x < D /\ D || ( N - x ) ) ) -> r = x ) -> ( ( ( r < D /\ D || ( N - r ) ) /\ ( 0 < D /\ D || ( N - 0 ) ) ) -> r = 0 ) ) )
32 23 31 ax-mp 
 |-  ( A. x e. NN0 ( ( ( r < D /\ D || ( N - r ) ) /\ ( x < D /\ D || ( N - x ) ) ) -> r = x ) -> ( ( ( r < D /\ D || ( N - r ) ) /\ ( 0 < D /\ D || ( N - 0 ) ) ) -> r = 0 ) )
33 22 32 syl5 
 |-  ( A. x e. NN0 ( ( ( r < D /\ D || ( N - r ) ) /\ ( x < D /\ D || ( N - x ) ) ) -> r = x ) -> ( ( ( ( N e. ZZ /\ D e. NN ) /\ D || N ) /\ ( r < D /\ D || ( N - r ) ) ) -> r = 0 ) )
34 33 expd 
 |-  ( A. x e. NN0 ( ( ( r < D /\ D || ( N - r ) ) /\ ( x < D /\ D || ( N - x ) ) ) -> r = x ) -> ( ( ( N e. ZZ /\ D e. NN ) /\ D || N ) -> ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) ) )
35 34 ralimi 
 |-  ( A. r e. NN0 A. x e. NN0 ( ( ( r < D /\ D || ( N - r ) ) /\ ( x < D /\ D || ( N - x ) ) ) -> r = x ) -> A. r e. NN0 ( ( ( N e. ZZ /\ D e. NN ) /\ D || N ) -> ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) ) )
36 12 35 simpl2im 
 |-  ( ( N e. ZZ /\ D e. NN ) -> A. r e. NN0 ( ( ( N e. ZZ /\ D e. NN ) /\ D || N ) -> ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) ) )
37 r19.21v 
 |-  ( A. r e. NN0 ( ( ( N e. ZZ /\ D e. NN ) /\ D || N ) -> ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) ) <-> ( ( ( N e. ZZ /\ D e. NN ) /\ D || N ) -> A. r e. NN0 ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) ) )
38 36 37 sylib 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( ( ( N e. ZZ /\ D e. NN ) /\ D || N ) -> A. r e. NN0 ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) ) )
39 38 expd 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( ( N e. ZZ /\ D e. NN ) -> ( D || N -> A. r e. NN0 ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) ) ) )
40 39 pm2.43i 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( D || N -> A. r e. NN0 ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) ) )
41 40 3impia 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> A. r e. NN0 ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) )
42 breq1 
 |-  ( r = K -> ( r < D <-> K < D ) )
43 oveq2 
 |-  ( r = K -> ( N - r ) = ( N - K ) )
44 43 breq2d 
 |-  ( r = K -> ( D || ( N - r ) <-> D || ( N - K ) ) )
45 42 44 anbi12d 
 |-  ( r = K -> ( ( r < D /\ D || ( N - r ) ) <-> ( K < D /\ D || ( N - K ) ) ) )
46 eqeq1 
 |-  ( r = K -> ( r = 0 <-> K = 0 ) )
47 45 46 imbi12d 
 |-  ( r = K -> ( ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) <-> ( ( K < D /\ D || ( N - K ) ) -> K = 0 ) ) )
48 47 rspcv 
 |-  ( K e. NN0 -> ( A. r e. NN0 ( ( r < D /\ D || ( N - r ) ) -> r = 0 ) -> ( ( K < D /\ D || ( N - K ) ) -> K = 0 ) ) )
49 41 48 syl5com 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> ( K e. NN0 -> ( ( K < D /\ D || ( N - K ) ) -> K = 0 ) ) )
50 pm4.14 
 |-  ( ( ( K < D /\ D || ( N - K ) ) -> K = 0 ) <-> ( ( K < D /\ -. K = 0 ) -> -. D || ( N - K ) ) )
51 49 50 syl6ib 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> ( K e. NN0 -> ( ( K < D /\ -. K = 0 ) -> -. D || ( N - K ) ) ) )
52 5 51 syl7bi 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> ( K e. NN0 -> ( ( K < D /\ K =/= 0 ) -> -. D || ( N - K ) ) ) )
53 52 exp4a 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> ( K e. NN0 -> ( K < D -> ( K =/= 0 -> -. D || ( N - K ) ) ) ) )
54 53 com23 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> ( K < D -> ( K e. NN0 -> ( K =/= 0 -> -. D || ( N - K ) ) ) ) )
55 54 imp4a 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> ( K < D -> ( ( K e. NN0 /\ K =/= 0 ) -> -. D || ( N - K ) ) ) )
56 3 55 syl7 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> ( K < D -> ( K e. NN -> -. D || ( N - K ) ) ) )
57 56 impcomd 
 |-  ( ( N e. ZZ /\ D e. NN /\ D || N ) -> ( ( K e. NN /\ K < D ) -> -. D || ( N - K ) ) )
58 57 3expia 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( D || N -> ( ( K e. NN /\ K < D ) -> -. D || ( N - K ) ) ) )
59 58 com23 
 |-  ( ( N e. ZZ /\ D e. NN ) -> ( ( K e. NN /\ K < D ) -> ( D || N -> -. D || ( N - K ) ) ) )
60 59 3impia 
 |-  ( ( N e. ZZ /\ D e. NN /\ ( K e. NN /\ K < D ) ) -> ( D || N -> -. D || ( N - K ) ) )