difelfznle

Description: The difference of two integers from a finite set of sequential nonnegative integers increased by the upper bound is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018)

		Ref	Expression
	Assertion	difelfznle	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to M + N - K \in (0 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	$⊢ M \in (0 \dots N) \leftrightarrow (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
2		nn0addcl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M + N \in ℕ_{0}$
3	2	nn0zd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M + N \in ℤ$
4	3	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to M + N \in ℤ$
5	1 4	sylbi	$⊢ M \in (0 \dots N) \to M + N \in ℤ$
6		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
7		zsubcl	$⊢ (M + N \in ℤ \land K \in ℤ) \to M + N - K \in ℤ$
8	5 6 7	syl2anr	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to M + N - K \in ℤ$
9	8	3adant3	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to M + N - K \in ℤ$
10	6	zred	$⊢ K \in (0 \dots N) \to K \in ℝ$
11	10	adantr	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to K \in ℝ$
12		elfzel2	$⊢ K \in (0 \dots N) \to N \in ℤ$
13	12	zred	$⊢ K \in (0 \dots N) \to N \in ℝ$
14	13	adantr	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to N \in ℝ$
15		nn0readdcl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M + N \in ℝ$
16	15	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to M + N \in ℝ$
17	1 16	sylbi	$⊢ M \in (0 \dots N) \to M + N \in ℝ$
18	17	adantl	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to M + N \in ℝ$
19		elfzle2	$⊢ K \in (0 \dots N) \to K \leq N$
20		elfzle1	$⊢ M \in (0 \dots N) \to 0 \leq M$
21		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
22		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
23	21 22	anim12ci	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \in ℝ \land M \in ℝ)$
24	23	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (N \in ℝ \land M \in ℝ)$
25	1 24	sylbi	$⊢ M \in (0 \dots N) \to (N \in ℝ \land M \in ℝ)$
26		addge02	$⊢ (N \in ℝ \land M \in ℝ) \to (0 \leq M \leftrightarrow N \leq M + N)$
27	25 26	syl	$⊢ M \in (0 \dots N) \to (0 \leq M \leftrightarrow N \leq M + N)$
28	20 27	mpbid	$⊢ M \in (0 \dots N) \to N \leq M + N$
29	19 28	anim12i	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to (K \leq N \land N \leq M + N)$
30		letr	$⊢ (K \in ℝ \land N \in ℝ \land M + N \in ℝ) \to ((K \leq N \land N \leq M + N) \to K \leq M + N)$
31	30	imp	$⊢ ((K \in ℝ \land N \in ℝ \land M + N \in ℝ) \land (K \leq N \land N \leq M + N)) \to K \leq M + N$
32	11 14 18 29 31	syl31anc	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to K \leq M + N$
33	32	3adant3	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to K \leq M + N$
34		zre	$⊢ K \in ℤ \to K \in ℝ$
35	21 22	anim12i	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \in ℝ \land N \in ℝ)$
36	35	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (M \in ℝ \land N \in ℝ)$
37	1 36	sylbi	$⊢ M \in (0 \dots N) \to (M \in ℝ \land N \in ℝ)$
38		readdcl	$⊢ (M \in ℝ \land N \in ℝ) \to M + N \in ℝ$
39	37 38	syl	$⊢ M \in (0 \dots N) \to M + N \in ℝ$
40	34 39	anim12ci	$⊢ (K \in ℤ \land M \in (0 \dots N)) \to (M + N \in ℝ \land K \in ℝ)$
41	6 40	sylan	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to (M + N \in ℝ \land K \in ℝ)$
42	41	3adant3	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to (M + N \in ℝ \land K \in ℝ)$
43		subge0	$⊢ (M + N \in ℝ \land K \in ℝ) \to (0 \leq M + N - K \leftrightarrow K \leq M + N)$
44	42 43	syl	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to (0 \leq M + N - K \leftrightarrow K \leq M + N)$
45	33 44	mpbird	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to 0 \leq M + N - K$
46		elnn0z	$⊢ M + N - K \in ℕ_{0} \leftrightarrow (M + N - K \in ℤ \land 0 \leq M + N - K)$
47	9 45 46	sylanbrc	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to M + N - K \in ℕ_{0}$
48		elfz3nn0	$⊢ K \in (0 \dots N) \to N \in ℕ_{0}$
49	48	3ad2ant1	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to N \in ℕ_{0}$
50		elfzelz	$⊢ M \in (0 \dots N) \to M \in ℤ$
51		zre	$⊢ M \in ℤ \to M \in ℝ$
52		ltnle	$⊢ (M \in ℝ \land K \in ℝ) \to (M < K \leftrightarrow \neg K \leq M)$
53	52	ancoms	$⊢ (K \in ℝ \land M \in ℝ) \to (M < K \leftrightarrow \neg K \leq M)$
54		ltle	$⊢ (M \in ℝ \land K \in ℝ) \to (M < K \to M \leq K)$
55	54	ancoms	$⊢ (K \in ℝ \land M \in ℝ) \to (M < K \to M \leq K)$
56	53 55	sylbird	$⊢ (K \in ℝ \land M \in ℝ) \to (\neg K \leq M \to M \leq K)$
57	34 51 56	syl2an	$⊢ (K \in ℤ \land M \in ℤ) \to (\neg K \leq M \to M \leq K)$
58	6 50 57	syl2an	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to (\neg K \leq M \to M \leq K)$
59	58	3impia	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to M \leq K$
60	50	zred	$⊢ M \in (0 \dots N) \to M \in ℝ$
61	60	adantl	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to M \in ℝ$
62	61 11 14	leadd1d	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to (M \leq K \leftrightarrow M + N \leq K + N)$
63	62	3adant3	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to (M \leq K \leftrightarrow M + N \leq K + N)$
64	59 63	mpbid	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to M + N \leq K + N$
65	18 11 14	lesubadd2d	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N)) \to (M + N - K \leq N \leftrightarrow M + N \leq K + N)$
66	65	3adant3	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to (M + N - K \leq N \leftrightarrow M + N \leq K + N)$
67	64 66	mpbird	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to M + N - K \leq N$
68		elfz2nn0	$⊢ M + N - K \in (0 \dots N) \leftrightarrow (M + N - K \in ℕ_{0} \land N \in ℕ_{0} \land M + N - K \leq N)$
69	47 49 67 68	syl3anbrc	$⊢ (K \in (0 \dots N) \land M \in (0 \dots N) \land \neg K \leq M) \to M + N - K \in (0 \dots N)$

Metamath Proof Explorer

Theorem difelfznle

Proof