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