dyadss

Description: Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015) (Proof shortened by Mario Carneiro, 26-Apr-2016)

		Ref	Expression
	Hypothesis	dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
	Assertion	dyadss	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \to ([.] (A F C) \subseteq [.] (B F D) \to D \leq C)$

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
2		simpr	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to [.] (A F C) \subseteq [.] (B F D)$
3		simpllr	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to B \in ℤ$
4		simplrr	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to D \in ℕ_{0}$
5	1	dyadval	$⊢ (B \in ℤ \land D \in ℕ_{0}) \to B F D = ⟨\frac{B}{2^{D}}, \frac{B + 1}{2^{D}}⟩$
6	3 4 5	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to B F D = ⟨\frac{B}{2^{D}}, \frac{B + 1}{2^{D}}⟩$
7	6	fveq2d	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to [.] (B F D) = [.] (⟨\frac{B}{2^{D}}, \frac{B + 1}{2^{D}}⟩)$
8		df-ov	$⊢ [\frac{B}{2^{D}}, \frac{B + 1}{2^{D}}] = [.] (⟨\frac{B}{2^{D}}, \frac{B + 1}{2^{D}}⟩)$
9	7 8	eqtr4di	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to [.] (B F D) = [\frac{B}{2^{D}}, \frac{B + 1}{2^{D}}]$
10	3	zred	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to B \in ℝ$
11		2nn	$⊢ 2 \in ℕ$
12		nnexpcl	$⊢ (2 \in ℕ \land D \in ℕ_{0}) \to 2^{D} \in ℕ$
13	11 4 12	sylancr	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to 2^{D} \in ℕ$
14	10 13	nndivred	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to \frac{B}{2^{D}} \in ℝ$
15		peano2re	$⊢ B \in ℝ \to B + 1 \in ℝ$
16	10 15	syl	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to B + 1 \in ℝ$
17	16 13	nndivred	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to \frac{B + 1}{2^{D}} \in ℝ$
18		iccssre	$⊢ (\frac{B}{2^{D}} \in ℝ \land \frac{B + 1}{2^{D}} \in ℝ) \to [\frac{B}{2^{D}}, \frac{B + 1}{2^{D}}] \subseteq ℝ$
19	14 17 18	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to [\frac{B}{2^{D}}, \frac{B + 1}{2^{D}}] \subseteq ℝ$
20	9 19	eqsstrd	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to [.] (B F D) \subseteq ℝ$
21		ovolss	$⊢ ([.] (A F C) \subseteq [.] (B F D) \land [.] (B F D) \subseteq ℝ) \to {vol}^{} ([.] (A F C)) \leq {vol}^{} ([.] (B F D))$
22	2 20 21	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to {vol}^{} ([.] (A F C)) \leq {vol}^{} ([.] (B F D))$
23		simplll	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to A \in ℤ$
24		simplrl	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to C \in ℕ_{0}$
25	1	dyadovol	$⊢ (A \in ℤ \land C \in ℕ_{0}) \to {vol}^{*} ([.] (A F C)) = \frac{1}{2^{C}}$
26	23 24 25	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to {vol}^{*} ([.] (A F C)) = \frac{1}{2^{C}}$
27	1	dyadovol	$⊢ (B \in ℤ \land D \in ℕ_{0}) \to {vol}^{*} ([.] (B F D)) = \frac{1}{2^{D}}$
28	3 4 27	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to {vol}^{*} ([.] (B F D)) = \frac{1}{2^{D}}$
29	22 26 28	3brtr3d	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to \frac{1}{2^{C}} \leq \frac{1}{2^{D}}$
30		nnexpcl	$⊢ (2 \in ℕ \land C \in ℕ_{0}) \to 2^{C} \in ℕ$
31	11 24 30	sylancr	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to 2^{C} \in ℕ$
32		nnre	$⊢ 2^{D} \in ℕ \to 2^{D} \in ℝ$
33		nngt0	$⊢ 2^{D} \in ℕ \to 0 < 2^{D}$
34	32 33	jca	$⊢ 2^{D} \in ℕ \to (2^{D} \in ℝ \land 0 < 2^{D})$
35		nnre	$⊢ 2^{C} \in ℕ \to 2^{C} \in ℝ$
36		nngt0	$⊢ 2^{C} \in ℕ \to 0 < 2^{C}$
37	35 36	jca	$⊢ 2^{C} \in ℕ \to (2^{C} \in ℝ \land 0 < 2^{C})$
38		lerec	$⊢ ((2^{D} \in ℝ \land 0 < 2^{D}) \land (2^{C} \in ℝ \land 0 < 2^{C})) \to (2^{D} \leq 2^{C} \leftrightarrow \frac{1}{2^{C}} \leq \frac{1}{2^{D}})$
39	34 37 38	syl2an	$⊢ (2^{D} \in ℕ \land 2^{C} \in ℕ) \to (2^{D} \leq 2^{C} \leftrightarrow \frac{1}{2^{C}} \leq \frac{1}{2^{D}})$
40	13 31 39	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to (2^{D} \leq 2^{C} \leftrightarrow \frac{1}{2^{C}} \leq \frac{1}{2^{D}})$
41	29 40	mpbird	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to 2^{D} \leq 2^{C}$
42		2re	$⊢ 2 \in ℝ$
43	42	a1i	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to 2 \in ℝ$
44	4	nn0zd	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to D \in ℤ$
45	24	nn0zd	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to C \in ℤ$
46		1lt2	$⊢ 1 < 2$
47	46	a1i	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to 1 < 2$
48	43 44 45 47	leexp2d	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to (D \leq C \leftrightarrow 2^{D} \leq 2^{C})$
49	41 48	mpbird	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land [.] (A F C) \subseteq [.] (B F D)) \to D \leq C$
50	49	ex	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \to ([.] (A F C) \subseteq [.] (B F D) \to D \leq C)$

Metamath Proof Explorer

Theorem dyadss

Proof