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	1	elfzelzd	$⊢ ((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 ℤ$
3	2	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 ℝ$
4		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 ℤ$
5	4	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 ℝ$
6		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)$
7		elfzel1	$⊢ A \in (B \dots C) \to B \in ℤ$
8	6 7	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 ℤ$
9	8	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 ℝ$
10	5 9	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 ℝ$
11	3 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 D - (F - B) \in ℝ$
12	6	elfzelzd	$⊢ ((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 ℤ$
13	12	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 ℝ$
14		elfzle2	$⊢ D \in (E \dots F) \to D \leq F$
15	1 14	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$
16	3 5 10 15	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)$
17	5	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 ℂ$
18	9	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 ℂ$
19	17 18	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$
20	16 19	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$
21		elfzle1	$⊢ A \in (B \dots C) \to B \leq A$
22	6 21	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$
23	11 9 13 20 22	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$
24		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 ℤ$
25	24	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 ℝ$
26	3 10	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 ℝ$
27		elfzle2	$⊢ A \in (B \dots C) \to A \leq C$
28	6 27	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$
29	25 3	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 ℝ$
30		elfzel1	$⊢ D \in (E \dots F) \to E \in ℤ$
31	1 30	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 ℤ$
32	31	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 ℝ$
33	25 32	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 ℝ$
34		elfzle1	$⊢ D \in (E \dots F) \to E \leq D$
35	1 34	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$
36	32 3 25 35	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$
37		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$
38	29 33 10 36 37	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$
39	25 3 10	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)$
40	38 39	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$
41	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 F - B \in ℂ$
42	3	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 ℂ$
43	41 42	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$
44	40 43	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$
45	13 25 26 28 44	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$
46	13 3 10	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))$
47	23 45 46	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