dyadovol

Description: Volume of a dyadic rational interval. (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	dyadovol	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to {vol}^{*} ([.] (A F B)) = \frac{1}{2^{B}}$

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	dyadval	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to A F B = ⟨\frac{A}{2^{B}}, \frac{A + 1}{2^{B}}⟩$
3	2	fveq2d	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to [.] (A F B) = [.] (⟨\frac{A}{2^{B}}, \frac{A + 1}{2^{B}}⟩)$
4		df-ov	$⊢ [\frac{A}{2^{B}}, \frac{A + 1}{2^{B}}] = [.] (⟨\frac{A}{2^{B}}, \frac{A + 1}{2^{B}}⟩)$
5	3 4	eqtr4di	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to [.] (A F B) = [\frac{A}{2^{B}}, \frac{A + 1}{2^{B}}]$
6	5	fveq2d	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to {vol}^{} ([.] (A F B)) = {vol}^{} ([\frac{A}{2^{B}}, \frac{A + 1}{2^{B}}])$
7		zre	$⊢ A \in ℤ \to A \in ℝ$
8		2nn	$⊢ 2 \in ℕ$
9		nnexpcl	$⊢ (2 \in ℕ \land B \in ℕ_{0}) \to 2^{B} \in ℕ$
10	8 9	mpan	$⊢ B \in ℕ_{0} \to 2^{B} \in ℕ$
11		nndivre	$⊢ (A \in ℝ \land 2^{B} \in ℕ) \to \frac{A}{2^{B}} \in ℝ$
12	7 10 11	syl2an	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to \frac{A}{2^{B}} \in ℝ$
13		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
14	7 13	syl	$⊢ A \in ℤ \to A + 1 \in ℝ$
15		nndivre	$⊢ (A + 1 \in ℝ \land 2^{B} \in ℕ) \to \frac{A + 1}{2^{B}} \in ℝ$
16	14 10 15	syl2an	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to \frac{A + 1}{2^{B}} \in ℝ$
17	7	adantr	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to A \in ℝ$
18	17	lep1d	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to A \leq A + 1$
19	17 13	syl	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to A + 1 \in ℝ$
20	10	adantl	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to 2^{B} \in ℕ$
21	20	nnred	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to 2^{B} \in ℝ$
22	20	nngt0d	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to 0 < 2^{B}$
23		lediv1	$⊢ (A \in ℝ \land A + 1 \in ℝ \land (2^{B} \in ℝ \land 0 < 2^{B})) \to (A \leq A + 1 \leftrightarrow \frac{A}{2^{B}} \leq \frac{A + 1}{2^{B}})$
24	17 19 21 22 23	syl112anc	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to (A \leq A + 1 \leftrightarrow \frac{A}{2^{B}} \leq \frac{A + 1}{2^{B}})$
25	18 24	mpbid	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to \frac{A}{2^{B}} \leq \frac{A + 1}{2^{B}}$
26		ovolicc	$⊢ (\frac{A}{2^{B}} \in ℝ \land \frac{A + 1}{2^{B}} \in ℝ \land \frac{A}{2^{B}} \leq \frac{A + 1}{2^{B}}) \to {vol}^{*} ([\frac{A}{2^{B}}, \frac{A + 1}{2^{B}}]) = (\frac{A + 1}{2^{B}}) - (\frac{A}{2^{B}})$
27	12 16 25 26	syl3anc	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to {vol}^{*} ([\frac{A}{2^{B}}, \frac{A + 1}{2^{B}}]) = (\frac{A + 1}{2^{B}}) - (\frac{A}{2^{B}})$
28	19	recnd	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to A + 1 \in ℂ$
29	17	recnd	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to A \in ℂ$
30	21	recnd	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to 2^{B} \in ℂ$
31	20	nnne0d	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to 2^{B} \neq 0$
32	28 29 30 31	divsubdird	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to \frac{A + 1 - A}{2^{B}} = (\frac{A + 1}{2^{B}}) - (\frac{A}{2^{B}})$
33		ax-1cn	$⊢ 1 \in ℂ$
34		pncan2	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 - A = 1$
35	29 33 34	sylancl	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to A + 1 - A = 1$
36	35	oveq1d	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to \frac{A + 1 - A}{2^{B}} = \frac{1}{2^{B}}$
37	32 36	eqtr3d	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to (\frac{A + 1}{2^{B}}) - (\frac{A}{2^{B}}) = \frac{1}{2^{B}}$
38	6 27 37	3eqtrd	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to {vol}^{*} ([.] (A F B)) = \frac{1}{2^{B}}$

Metamath Proof Explorer

Theorem dyadovol

Proof