Theorem dyadval

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

	Ref	Expression
Hypothesis	dyadmbl.1	$$⊢F=\left(x\in \mathbb{Z},y\in {\mathbb{N}}_0⟼⟨\frac{x}{2^y},\frac{x+1}{2^y}⟩\right)$$
Assertion	dyadval	$$⊢\left(A\in \mathbb{Z}\wedge B\in {\mathbb{N}}_0\right)\to AFB=⟨\frac{A}{2^B},\frac{A+1}{2^B}⟩$$

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	$$⊢F=\left(x\in \mathbb{Z},y\in {\mathbb{N}}_0⟼⟨\frac{x}{2^y},\frac{x+1}{2^y}⟩\right)$$
2		id	$$⊢x=A\to x=A$$
3		oveq2	$$⊢y=B\to 2^y=2^B$$
4	2 3	oveqan12d	$$⊢\left(x=A\wedge y=B\right)\to \frac{x}{2^y}=\frac{A}{2^B}$$
5		oveq1	$$⊢x=A\to x+1=A+1$$
6	5 3	oveqan12d	$$⊢\left(x=A\wedge y=B\right)\to \frac{x+1}{2^y}=\frac{A+1}{2^B}$$
7	4 6	opeq12d	$$⊢\left(x=A\wedge y=B\right)\to ⟨\frac{x}{2^y},\frac{x+1}{2^y}⟩=⟨\frac{A}{2^B},\frac{A+1}{2^B}⟩$$
8		opex	$$⊢⟨\frac{A}{2^B},\frac{A+1}{2^B}⟩\in \mathrm{V}$$
9	7 1 8	ovmpoa	$$⊢\left(A\in \mathbb{Z}\wedge B\in {\mathbb{N}}_0\right)\to AFB=⟨\frac{A}{2^B},\frac{A+1}{2^B}⟩$$