fzmaxdif

Description: Bound on the difference between two integers constrained to two possibly overlapping finite ranges. (Contributed by Stefan O'Rear, 4-Oct-2014)

		Ref	Expression
	Assertion	fzmaxdif	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to \|A - D\| \leq F - B$

Proof

Step	Hyp	Ref	Expression
1		simp2r	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D \in (E \dots F)$
2		elfzelz	$⊢ D \in (E \dots F) \to D \in ℤ$
3	1 2	syl	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D \in ℤ$
4	3	zred	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D \in ℝ$
5		simp2l	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to F \in ℤ$
6	5	zred	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to F \in ℝ$
7		simp1r	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to A \in (B \dots C)$
8		elfzel1	$⊢ A \in (B \dots C) \to B \in ℤ$
9	7 8	syl	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to B \in ℤ$
10	9	zred	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to B \in ℝ$
11	6 10	resubcld	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to F - B \in ℝ$
12	4 11	resubcld	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D - (F - B) \in ℝ$
13		elfzelz	$⊢ A \in (B \dots C) \to A \in ℤ$
14	7 13	syl	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to A \in ℤ$
15	14	zred	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to A \in ℝ$
16		elfzle2	$⊢ D \in (E \dots F) \to D \leq F$
17	1 16	syl	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D \leq F$
18	4 6 11 17	lesub1dd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D - (F - B) \leq F - (F - B)$
19	6	recnd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to F \in ℂ$
20	10	recnd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to B \in ℂ$
21	19 20	nncand	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to F - (F - B) = B$
22	18 21	breqtrd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D - (F - B) \leq B$
23		elfzle1	$⊢ A \in (B \dots C) \to B \leq A$
24	7 23	syl	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to B \leq A$
25	12 10 15 22 24	letrd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D - (F - B) \leq A$
26		simp1l	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to C \in ℤ$
27	26	zred	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to C \in ℝ$
28	4 11	readdcld	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D + F - B \in ℝ$
29		elfzle2	$⊢ A \in (B \dots C) \to A \leq C$
30	7 29	syl	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to A \leq C$
31	27 4	resubcld	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to C - D \in ℝ$
32		elfzel1	$⊢ D \in (E \dots F) \to E \in ℤ$
33	1 32	syl	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to E \in ℤ$
34	33	zred	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to E \in ℝ$
35	27 34	resubcld	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to C - E \in ℝ$
36		elfzle1	$⊢ D \in (E \dots F) \to E \leq D$
37	1 36	syl	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to E \leq D$
38	34 4 27 37	lesub2dd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to C - D \leq C - E$
39		simp3	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to C - E \leq F - B$
40	31 35 11 38 39	letrd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to C - D \leq F - B$
41	27 4 11	lesubaddd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to (C - D \leq F - B \leftrightarrow C \leq F - B + D)$
42	40 41	mpbid	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to C \leq F - B + D$
43	11	recnd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to F - B \in ℂ$
44	4	recnd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to D \in ℂ$
45	43 44	addcomd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to F - B + D = D + F - B$
46	42 45	breqtrd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to C \leq D + F - B$
47	15 27 28 30 46	letrd	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to A \leq D + F - B$
48	15 4 11	absdifled	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to (\|A - D\| \leq F - B \leftrightarrow (D - (F - B) \leq A \land A \leq D + F - B))$
49	25 47 48	mpbir2and	$⊢ ((C \in ℤ \land A \in (B \dots C)) \land (F \in ℤ \land D \in (E \dots F)) \land C - E \leq F - B) \to \|A - D\| \leq F - B$

Metamath Proof Explorer

Theorem fzmaxdif

Proof