This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↑ 𝐵 ) ) )