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

Metamath Proof Explorer

Theorem dyadval

Description: Value of the dyadic rational function F . (Contributed by Mario Carneiro, 26-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
3 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 2 ↑ 𝑦 ) = ( 2 ↑ 𝐵 ) )
4 2 3 oveqan12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 / ( 2 ↑ 𝑦 ) ) = ( 𝐴 / ( 2 ↑ 𝐵 ) ) )
5 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 + 1 ) = ( 𝐴 + 1 ) )
6 5 3 oveqan12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) = ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) )
7 4 6 opeq12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ = ⟨ ( 𝐴 / ( 2 ↑ 𝐵 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ⟩ )
8 opex ⊢ ⟨ ( 𝐴 / ( 2 ↑ 𝐵 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ⟩ ∈ V
9 7 1 8 ovmpoa ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 𝐹 𝐵 ) = ⟨ ( 𝐴 / ( 2 ↑ 𝐵 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐵 ) ) ⟩ )