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 \in ℤ \land D \in ℕ \land (K \in ℕ \land K < D)) \to (D ∥ N \to \neg D ∥ (N - K))$

Proof

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

Metamath Proof Explorer

Theorem ndvdssub

Proof