2elfz2melfz

Description: If the sum of two integers of a 0-based finite set of sequential integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the 0-based finite set of sequential integers with the first integer as upper bound. (Contributed by Alexander van der Vekens, 7-Apr-2018) (Revised by Alexander van der Vekens, 31-May-2018)

		Ref	Expression
	Assertion	2elfz2melfz	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to (N < A + B \to B - (N - A) \in (0 \dots A))$

Proof

Step	Hyp	Ref	Expression
1		elfzelz	$⊢ A \in (0 \dots N) \to A \in ℤ$
2		elfzel2	$⊢ B \in (0 \dots N) \to N \in ℤ$
3		elfzelz	$⊢ B \in (0 \dots N) \to B \in ℤ$
4		simplr	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to B \in ℤ$
5		zsubcl	$⊢ (N \in ℤ \land A \in ℤ) \to N - A \in ℤ$
6	5	adantlr	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to N - A \in ℤ$
7	4 6	zsubcld	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to B - (N - A) \in ℤ$
8	7	adantr	$⊢ (((N \in ℤ \land B \in ℤ) \land A \in ℤ) \land N < A + B) \to B - (N - A) \in ℤ$
9		zre	$⊢ N \in ℤ \to N \in ℝ$
10	9	ad2antrr	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to N \in ℝ$
11		zaddcl	$⊢ (A \in ℤ \land B \in ℤ) \to A + B \in ℤ$
12	11	zred	$⊢ (A \in ℤ \land B \in ℤ) \to A + B \in ℝ$
13	12	expcom	$⊢ B \in ℤ \to (A \in ℤ \to A + B \in ℝ)$
14	13	adantl	$⊢ (N \in ℤ \land B \in ℤ) \to (A \in ℤ \to A + B \in ℝ)$
15	14	imp	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to A + B \in ℝ$
16	10 15 10	ltsub1d	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to (N < A + B \leftrightarrow N - N < A + B - N)$
17		zre	$⊢ B \in ℤ \to B \in ℝ$
18	9 17	anim12i	$⊢ (N \in ℤ \land B \in ℤ) \to (N \in ℝ \land B \in ℝ)$
19		zre	$⊢ A \in ℤ \to A \in ℝ$
20	18 19	anim12i	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to ((N \in ℝ \land B \in ℝ) \land A \in ℝ)$
21		id	$⊢ N \in ℝ \to N \in ℝ$
22	21 21	resubcld	$⊢ N \in ℝ \to N - N \in ℝ$
23	22	ad2antrr	$⊢ ((N \in ℝ \land B \in ℝ) \land A \in ℝ) \to N - N \in ℝ$
24		readdcl	$⊢ (A \in ℝ \land B \in ℝ) \to A + B \in ℝ$
25	24	expcom	$⊢ B \in ℝ \to (A \in ℝ \to A + B \in ℝ)$
26	25	adantl	$⊢ (N \in ℝ \land B \in ℝ) \to (A \in ℝ \to A + B \in ℝ)$
27	26	imp	$⊢ ((N \in ℝ \land B \in ℝ) \land A \in ℝ) \to A + B \in ℝ$
28		simpll	$⊢ ((N \in ℝ \land B \in ℝ) \land A \in ℝ) \to N \in ℝ$
29	27 28	resubcld	$⊢ ((N \in ℝ \land B \in ℝ) \land A \in ℝ) \to A + B - N \in ℝ$
30	23 29	jca	$⊢ ((N \in ℝ \land B \in ℝ) \land A \in ℝ) \to (N - N \in ℝ \land A + B - N \in ℝ)$
31		ltle	$⊢ (N - N \in ℝ \land A + B - N \in ℝ) \to (N - N < A + B - N \to N - N \leq A + B - N)$
32	20 30 31	3syl	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to (N - N < A + B - N \to N - N \leq A + B - N)$
33		zcn	$⊢ N \in ℤ \to N \in ℂ$
34	33	subidd	$⊢ N \in ℤ \to N - N = 0$
35	34	ad2antrr	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to N - N = 0$
36		zcn	$⊢ B \in ℤ \to B \in ℂ$
37	36	adantl	$⊢ (N \in ℤ \land B \in ℤ) \to B \in ℂ$
38	37	adantr	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to B \in ℂ$
39	33	ad2antrr	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to N \in ℂ$
40		zcn	$⊢ A \in ℤ \to A \in ℂ$
41	40	adantl	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to A \in ℂ$
42		simp3	$⊢ (B \in ℂ \land N \in ℂ \land A \in ℂ) \to A \in ℂ$
43		simp1	$⊢ (B \in ℂ \land N \in ℂ \land A \in ℂ) \to B \in ℂ$
44	42 43	addcomd	$⊢ (B \in ℂ \land N \in ℂ \land A \in ℂ) \to A + B = B + A$
45	44	oveq1d	$⊢ (B \in ℂ \land N \in ℂ \land A \in ℂ) \to A + B - N = B + A - N$
46		subsub3	$⊢ (B \in ℂ \land N \in ℂ \land A \in ℂ) \to B - (N - A) = B + A - N$
47	45 46	eqtr4d	$⊢ (B \in ℂ \land N \in ℂ \land A \in ℂ) \to A + B - N = B - (N - A)$
48	38 39 41 47	syl3anc	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to A + B - N = B - (N - A)$
49	35 48	breq12d	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to (N - N \leq A + B - N \leftrightarrow 0 \leq B - (N - A))$
50	32 49	sylibd	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to (N - N < A + B - N \to 0 \leq B - (N - A))$
51	16 50	sylbid	$⊢ ((N \in ℤ \land B \in ℤ) \land A \in ℤ) \to (N < A + B \to 0 \leq B - (N - A))$
52	51	imp	$⊢ (((N \in ℤ \land B \in ℤ) \land A \in ℤ) \land N < A + B) \to 0 \leq B - (N - A)$
53		elnn0z	$⊢ B - (N - A) \in ℕ_{0} \leftrightarrow (B - (N - A) \in ℤ \land 0 \leq B - (N - A))$
54	8 52 53	sylanbrc	$⊢ (((N \in ℤ \land B \in ℤ) \land A \in ℤ) \land N < A + B) \to B - (N - A) \in ℕ_{0}$
55	54	exp31	$⊢ (N \in ℤ \land B \in ℤ) \to (A \in ℤ \to (N < A + B \to B - (N - A) \in ℕ_{0}))$
56	2 3 55	syl2anc	$⊢ B \in (0 \dots N) \to (A \in ℤ \to (N < A + B \to B - (N - A) \in ℕ_{0}))$
57	1 56	mpan9	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to (N < A + B \to B - (N - A) \in ℕ_{0})$
58	57	imp	$⊢ ((A \in (0 \dots N) \land B \in (0 \dots N)) \land N < A + B) \to B - (N - A) \in ℕ_{0}$
59		elfznn0	$⊢ A \in (0 \dots N) \to A \in ℕ_{0}$
60	59	ad2antrr	$⊢ ((A \in (0 \dots N) \land B \in (0 \dots N)) \land N < A + B) \to A \in ℕ_{0}$
61		elfzle2	$⊢ B \in (0 \dots N) \to B \leq N$
62	61	adantl	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to B \leq N$
63		elfzel2	$⊢ A \in (0 \dots N) \to N \in ℤ$
64	63	zcnd	$⊢ A \in (0 \dots N) \to N \in ℂ$
65	1	zcnd	$⊢ A \in (0 \dots N) \to A \in ℂ$
66	64 65	jca	$⊢ A \in (0 \dots N) \to (N \in ℂ \land A \in ℂ)$
67	66	adantr	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to (N \in ℂ \land A \in ℂ)$
68		npcan	$⊢ (N \in ℂ \land A \in ℂ) \to N - A + A = N$
69	67 68	syl	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to N - A + A = N$
70	62 69	breqtrrd	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to B \leq N - A + A$
71	3	zred	$⊢ B \in (0 \dots N) \to B \in ℝ$
72	71	adantl	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to B \in ℝ$
73	63	zred	$⊢ A \in (0 \dots N) \to N \in ℝ$
74	1	zred	$⊢ A \in (0 \dots N) \to A \in ℝ$
75	73 74	resubcld	$⊢ A \in (0 \dots N) \to N - A \in ℝ$
76	75	adantr	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to N - A \in ℝ$
77	74	adantr	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to A \in ℝ$
78	72 76 77	lesubadd2d	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to (B - (N - A) \leq A \leftrightarrow B \leq N - A + A)$
79	70 78	mpbird	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to B - (N - A) \leq A$
80	79	adantr	$⊢ ((A \in (0 \dots N) \land B \in (0 \dots N)) \land N < A + B) \to B - (N - A) \leq A$
81		elfz2nn0	$⊢ B - (N - A) \in (0 \dots A) \leftrightarrow (B - (N - A) \in ℕ_{0} \land A \in ℕ_{0} \land B - (N - A) \leq A)$
82	58 60 80 81	syl3anbrc	$⊢ ((A \in (0 \dots N) \land B \in (0 \dots N)) \land N < A + B) \to B - (N - A) \in (0 \dots A)$
83	82	ex	$⊢ (A \in (0 \dots N) \land B \in (0 \dots N)) \to (N < A + B \to B - (N - A) \in (0 \dots A))$

Metamath Proof Explorer

Theorem 2elfz2melfz

Proof