Theorem dyadovol

Description: Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015)

	Ref	Expression
Hypothesis	dyadmbl.1	⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
Assertion	dyadovol	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( vol* ‘ ( [,] ‘ ( 𝐴 𝐹 𝐵 ) ) ) = ( 1 / ( 2 ↑ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2	1	dyadval	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 𝐹 𝐵 ) = ⟨ ( 𝐴 / ( 2 ↑ 𝐵 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ⟩ )
3	2	fveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( [,] ‘ ( 𝐴 𝐹 𝐵 ) ) = ( [,] ‘ ⟨ ( 𝐴 / ( 2 ↑ 𝐵 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ⟩ ) )
4		df-ov	⊢ ( ( 𝐴 / ( 2 ↑ 𝐵 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ) = ( [,] ‘ ⟨ ( 𝐴 / ( 2 ↑ 𝐵 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ⟩ )
5	3 4	eqtr4di	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( [,] ‘ ( 𝐴 𝐹 𝐵 ) ) = ( ( 𝐴 / ( 2 ↑ 𝐵 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ) )
6	5	fveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( vol* ‘ ( [,] ‘ ( 𝐴 𝐹 𝐵 ) ) ) = ( vol* ‘ ( ( 𝐴 / ( 2 ↑ 𝐵 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ) ) )
7		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
8		2nn	⊢ 2 ∈ ℕ
9		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝐵 ∈ ℕ0 ) → ( 2 ↑ 𝐵 ) ∈ ℕ )
10	8 9	mpan	⊢ ( 𝐵 ∈ ℕ0 → ( 2 ↑ 𝐵 ) ∈ ℕ )
11		nndivre	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 ↑ 𝐵 ) ∈ ℕ ) → ( 𝐴 / ( 2 ↑ 𝐵 ) ) ∈ ℝ )
12	7 10 11	syl2an	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 / ( 2 ↑ 𝐵 ) ) ∈ ℝ )
13		peano2re	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
14	7 13	syl	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℝ )
15		nndivre	⊢ ( ( ( 𝐴 + 1 ) ∈ ℝ ∧ ( 2 ↑ 𝐵 ) ∈ ℕ ) → ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ∈ ℝ )
16	14 10 15	syl2an	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ∈ ℝ )
17	7	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
18	17	lep1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → 𝐴 ≤ ( 𝐴 + 1 ) )
19	17 13	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + 1 ) ∈ ℝ )
20	10	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 2 ↑ 𝐵 ) ∈ ℕ )
21	20	nnred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 2 ↑ 𝐵 ) ∈ ℝ )
22	20	nngt0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → 0 < ( 2 ↑ 𝐵 ) )
23		lediv1	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ∧ ( ( 2 ↑ 𝐵 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐵 ) ) ) → ( 𝐴 ≤ ( 𝐴 + 1 ) ↔ ( 𝐴 / ( 2 ↑ 𝐵 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ) )
24	17 19 21 22 23	syl112anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ≤ ( 𝐴 + 1 ) ↔ ( 𝐴 / ( 2 ↑ 𝐵 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ) )
25	18 24	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 / ( 2 ↑ 𝐵 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) )
26		ovolicc	⊢ ( ( ( 𝐴 / ( 2 ↑ 𝐵 ) ) ∈ ℝ ∧ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ∈ ℝ ∧ ( 𝐴 / ( 2 ↑ 𝐵 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ) → ( vol* ‘ ( ( 𝐴 / ( 2 ↑ 𝐵 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ) ) = ( ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) − ( 𝐴 / ( 2 ↑ 𝐵 ) ) ) )
27	12 16 25 26	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( vol* ‘ ( ( 𝐴 / ( 2 ↑ 𝐵 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ) ) = ( ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) − ( 𝐴 / ( 2 ↑ 𝐵 ) ) ) )
28	19	recnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + 1 ) ∈ ℂ )
29	17	recnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
30	21	recnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 2 ↑ 𝐵 ) ∈ ℂ )
31	20	nnne0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 2 ↑ 𝐵 ) ≠ 0 )
32	28 29 30 31	divsubdird	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐴 + 1 ) − 𝐴 ) / ( 2 ↑ 𝐵 ) ) = ( ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) − ( 𝐴 / ( 2 ↑ 𝐵 ) ) ) )
33		ax-1cn	⊢ 1 ∈ ℂ
34		pncan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 𝐴 ) = 1 )
35	29 33 34	sylancl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 + 1 ) − 𝐴 ) = 1 )
36	35	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐴 + 1 ) − 𝐴 ) / ( 2 ↑ 𝐵 ) ) = ( 1 / ( 2 ↑ 𝐵 ) ) )
37	32 36	eqtr3d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) − ( 𝐴 / ( 2 ↑ 𝐵 ) ) ) = ( 1 / ( 2 ↑ 𝐵 ) ) )
38	6 27 37	3eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( vol* ‘ ( [,] ‘ ( 𝐴 𝐹 𝐵 ) ) ) = ( 1 / ( 2 ↑ 𝐵 ) ) )