dyadf

Description: The function F returns the endpoints of a dyadic rational covering of the real line. (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	dyadf	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
2		zre	$⊢ x \in ℤ \to x \in ℝ$
3	2	adantr	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to x \in ℝ$
4	3	lep1d	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to x \leq x + 1$
5		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
6	3 5	syl	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to x + 1 \in ℝ$
7		2nn	$⊢ 2 \in ℕ$
8		nnexpcl	$⊢ (2 \in ℕ \land y \in ℕ_{0}) \to 2^{y} \in ℕ$
9	7 8	mpan	$⊢ y \in ℕ_{0} \to 2^{y} \in ℕ$
10	9	adantl	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to 2^{y} \in ℕ$
11	10	nnred	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to 2^{y} \in ℝ$
12	10	nngt0d	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to 0 < 2^{y}$
13		lediv1	$⊢ (x \in ℝ \land x + 1 \in ℝ \land (2^{y} \in ℝ \land 0 < 2^{y})) \to (x \leq x + 1 \leftrightarrow \frac{x}{2^{y}} \leq \frac{x + 1}{2^{y}})$
14	3 6 11 12 13	syl112anc	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to (x \leq x + 1 \leftrightarrow \frac{x}{2^{y}} \leq \frac{x + 1}{2^{y}})$
15	4 14	mpbid	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to \frac{x}{2^{y}} \leq \frac{x + 1}{2^{y}}$
16		df-br	$⊢ \frac{x}{2^{y}} \leq \frac{x + 1}{2^{y}} \leftrightarrow ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in \leq$
17	15 16	sylib	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in \leq$
18		nndivre	$⊢ (x \in ℝ \land 2^{y} \in ℕ) \to \frac{x}{2^{y}} \in ℝ$
19	2 9 18	syl2an	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to \frac{x}{2^{y}} \in ℝ$
20	2 5	syl	$⊢ x \in ℤ \to x + 1 \in ℝ$
21		nndivre	$⊢ (x + 1 \in ℝ \land 2^{y} \in ℕ) \to \frac{x + 1}{2^{y}} \in ℝ$
22	20 9 21	syl2an	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to \frac{x + 1}{2^{y}} \in ℝ$
23	19 22	opelxpd	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
24	17 23	elind	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in (\leq \cap ℝ^{2})$
25	24	rgen2	$⊢ \forall x \in ℤ \forall y \in ℕ_{0} ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in (\leq \cap ℝ^{2})$
26	1	fmpo	$⊢ \forall x \in ℤ \forall y \in ℕ_{0} ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in (\leq \cap ℝ^{2}) \leftrightarrow F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$
27	25 26	mpbi	$⊢ F : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$

Metamath Proof Explorer

Theorem dyadf

Proof