dyaddisj

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)

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

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
2	1	dyadf	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$
3		ffn	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to F Fn (ℤ \times ℕ_{0})$
4		ovelrn	$⊢ F Fn (ℤ \times ℕ_{0}) \to (A \in ran F \leftrightarrow \exists a \in ℤ \exists c \in ℕ_{0} A = a F c)$
5		ovelrn	$⊢ F Fn (ℤ \times ℕ_{0}) \to (B \in ran F \leftrightarrow \exists b \in ℤ \exists d \in ℕ_{0} B = b F d)$
6	4 5	anbi12d	$⊢ F Fn (ℤ \times ℕ_{0}) \to ((A \in ran F \land B \in ran F) \leftrightarrow (\exists a \in ℤ \exists c \in ℕ_{0} A = a F c \land \exists b \in ℤ \exists d \in ℕ_{0} B = b F d))$
7	2 3 6	mp2b	$⊢ (A \in ran F \land B \in ran F) \leftrightarrow (\exists a \in ℤ \exists c \in ℕ_{0} A = a F c \land \exists b \in ℤ \exists d \in ℕ_{0} B = b F d)$
8		reeanv	$⊢ \exists a \in ℤ \exists b \in ℤ (\exists c \in ℕ_{0} A = a F c \land \exists d \in ℕ_{0} B = b F d) \leftrightarrow (\exists a \in ℤ \exists c \in ℕ_{0} A = a F c \land \exists b \in ℤ \exists d \in ℕ_{0} B = b F d)$
9	7 8	bitr4i	$⊢ (A \in ran F \land B \in ran F) \leftrightarrow \exists a \in ℤ \exists b \in ℤ (\exists c \in ℕ_{0} A = a F c \land \exists d \in ℕ_{0} B = b F d)$
10		reeanv	$⊢ \exists c \in ℕ_{0} \exists d \in ℕ_{0} (A = a F c \land B = b F d) \leftrightarrow (\exists c \in ℕ_{0} A = a F c \land \exists d \in ℕ_{0} B = b F d)$
11		nn0re	$⊢ c \in ℕ_{0} \to c \in ℝ$
12	11	ad2antrl	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℕ_{0} \land d \in ℕ_{0})) \to c \in ℝ$
13		nn0re	$⊢ d \in ℕ_{0} \to d \in ℝ$
14	13	ad2antll	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℕ_{0} \land d \in ℕ_{0})) \to d \in ℝ$
15	1	dyaddisjlem	$⊢ (((a \in ℤ \land b \in ℤ) \land (c \in ℕ_{0} \land d \in ℕ_{0})) \land c \leq d) \to ([.] (a F c) \subseteq [.] (b F d) \lor [.] (b F d) \subseteq [.] (a F c) \lor (.) (a F c) \cap (.) (b F d) = \emptyset)$
16		ancom	$⊢ (a \in ℤ \land b \in ℤ) \leftrightarrow (b \in ℤ \land a \in ℤ)$
17		ancom	$⊢ (c \in ℕ_{0} \land d \in ℕ_{0}) \leftrightarrow (d \in ℕ_{0} \land c \in ℕ_{0})$
18	16 17	anbi12i	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℕ_{0} \land d \in ℕ_{0})) \leftrightarrow ((b \in ℤ \land a \in ℤ) \land (d \in ℕ_{0} \land c \in ℕ_{0}))$
19	1	dyaddisjlem	$⊢ (((b \in ℤ \land a \in ℤ) \land (d \in ℕ_{0} \land c \in ℕ_{0})) \land d \leq c) \to ([.] (b F d) \subseteq [.] (a F c) \lor [.] (a F c) \subseteq [.] (b F d) \lor (.) (b F d) \cap (.) (a F c) = \emptyset)$
20	18 19	sylanb	$⊢ (((a \in ℤ \land b \in ℤ) \land (c \in ℕ_{0} \land d \in ℕ_{0})) \land d \leq c) \to ([.] (b F d) \subseteq [.] (a F c) \lor [.] (a F c) \subseteq [.] (b F d) \lor (.) (b F d) \cap (.) (a F c) = \emptyset)$
21		orcom	$⊢ ([.] (b F d) \subseteq [.] (a F c) \lor [.] (a F c) \subseteq [.] (b F d)) \leftrightarrow ([.] (a F c) \subseteq [.] (b F d) \lor [.] (b F d) \subseteq [.] (a F c))$
22		incom	$⊢ (.) (b F d) \cap (.) (a F c) = (.) (a F c) \cap (.) (b F d)$
23	22	eqeq1i	$⊢ (.) (b F d) \cap (.) (a F c) = \emptyset \leftrightarrow (.) (a F c) \cap (.) (b F d) = \emptyset$
24	21 23	orbi12i	$⊢ (([.] (b F d) \subseteq [.] (a F c) \lor [.] (a F c) \subseteq [.] (b F d)) \lor (.) (b F d) \cap (.) (a F c) = \emptyset) \leftrightarrow (([.] (a F c) \subseteq [.] (b F d) \lor [.] (b F d) \subseteq [.] (a F c)) \lor (.) (a F c) \cap (.) (b F d) = \emptyset)$
25		df-3or	$⊢ ([.] (b F d) \subseteq [.] (a F c) \lor [.] (a F c) \subseteq [.] (b F d) \lor (.) (b F d) \cap (.) (a F c) = \emptyset) \leftrightarrow (([.] (b F d) \subseteq [.] (a F c) \lor [.] (a F c) \subseteq [.] (b F d)) \lor (.) (b F d) \cap (.) (a F c) = \emptyset)$
26		df-3or	$⊢ ([.] (a F c) \subseteq [.] (b F d) \lor [.] (b F d) \subseteq [.] (a F c) \lor (.) (a F c) \cap (.) (b F d) = \emptyset) \leftrightarrow (([.] (a F c) \subseteq [.] (b F d) \lor [.] (b F d) \subseteq [.] (a F c)) \lor (.) (a F c) \cap (.) (b F d) = \emptyset)$
27	24 25 26	3bitr4i	$⊢ ([.] (b F d) \subseteq [.] (a F c) \lor [.] (a F c) \subseteq [.] (b F d) \lor (.) (b F d) \cap (.) (a F c) = \emptyset) \leftrightarrow ([.] (a F c) \subseteq [.] (b F d) \lor [.] (b F d) \subseteq [.] (a F c) \lor (.) (a F c) \cap (.) (b F d) = \emptyset)$
28	20 27	sylib	$⊢ (((a \in ℤ \land b \in ℤ) \land (c \in ℕ_{0} \land d \in ℕ_{0})) \land d \leq c) \to ([.] (a F c) \subseteq [.] (b F d) \lor [.] (b F d) \subseteq [.] (a F c) \lor (.) (a F c) \cap (.) (b F d) = \emptyset)$
29	12 14 15 28	lecasei	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℕ_{0} \land d \in ℕ_{0})) \to ([.] (a F c) \subseteq [.] (b F d) \lor [.] (b F d) \subseteq [.] (a F c) \lor (.) (a F c) \cap (.) (b F d) = \emptyset)$
30		simpl	$⊢ (A = a F c \land B = b F d) \to A = a F c$
31	30	fveq2d	$⊢ (A = a F c \land B = b F d) \to [.] (A) = [.] (a F c)$
32		simpr	$⊢ (A = a F c \land B = b F d) \to B = b F d$
33	32	fveq2d	$⊢ (A = a F c \land B = b F d) \to [.] (B) = [.] (b F d)$
34	31 33	sseq12d	$⊢ (A = a F c \land B = b F d) \to ([.] (A) \subseteq [.] (B) \leftrightarrow [.] (a F c) \subseteq [.] (b F d))$
35	33 31	sseq12d	$⊢ (A = a F c \land B = b F d) \to ([.] (B) \subseteq [.] (A) \leftrightarrow [.] (b F d) \subseteq [.] (a F c))$
36	30	fveq2d	$⊢ (A = a F c \land B = b F d) \to (.) (A) = (.) (a F c)$
37	32	fveq2d	$⊢ (A = a F c \land B = b F d) \to (.) (B) = (.) (b F d)$
38	36 37	ineq12d	$⊢ (A = a F c \land B = b F d) \to (.) (A) \cap (.) (B) = (.) (a F c) \cap (.) (b F d)$
39	38	eqeq1d	$⊢ (A = a F c \land B = b F d) \to ((.) (A) \cap (.) (B) = \emptyset \leftrightarrow (.) (a F c) \cap (.) (b F d) = \emptyset)$
40	34 35 39	3orbi123d	$⊢ (A = a F c \land B = b F d) \to (([.] (A) \subseteq [.] (B) \lor [.] (B) \subseteq [.] (A) \lor (.) (A) \cap (.) (B) = \emptyset) \leftrightarrow ([.] (a F c) \subseteq [.] (b F d) \lor [.] (b F d) \subseteq [.] (a F c) \lor (.) (a F c) \cap (.) (b F d) = \emptyset))$
41	29 40	syl5ibrcom	$⊢ ((a \in ℤ \land b \in ℤ) \land (c \in ℕ_{0} \land d \in ℕ_{0})) \to ((A = a F c \land B = b F d) \to ([.] (A) \subseteq [.] (B) \lor [.] (B) \subseteq [.] (A) \lor (.) (A) \cap (.) (B) = \emptyset))$
42	41	rexlimdvva	$⊢ (a \in ℤ \land b \in ℤ) \to (\exists c \in ℕ_{0} \exists d \in ℕ_{0} (A = a F c \land B = b F d) \to ([.] (A) \subseteq [.] (B) \lor [.] (B) \subseteq [.] (A) \lor (.) (A) \cap (.) (B) = \emptyset))$
43	10 42	biimtrrid	$⊢ (a \in ℤ \land b \in ℤ) \to ((\exists c \in ℕ_{0} A = a F c \land \exists d \in ℕ_{0} B = b F d) \to ([.] (A) \subseteq [.] (B) \lor [.] (B) \subseteq [.] (A) \lor (.) (A) \cap (.) (B) = \emptyset))$
44	43	rexlimivv	$⊢ \exists a \in ℤ \exists b \in ℤ (\exists c \in ℕ_{0} A = a F c \land \exists d \in ℕ_{0} B = b F d) \to ([.] (A) \subseteq [.] (B) \lor [.] (B) \subseteq [.] (A) \lor (.) (A) \cap (.) (B) = \emptyset)$
45	9 44	sylbi	$⊢ (A \in ran F \land B \in ran F) \to ([.] (A) \subseteq [.] (B) \lor [.] (B) \subseteq [.] (A) \lor (.) (A) \cap (.) (B) = \emptyset)$

Metamath Proof Explorer

Theorem dyaddisj

Proof