oddpwdcv

Description: Lemma for eulerpart : value of the F function. (Contributed by Thierry Arnoux, 9-Sep-2017)

Step	Hyp	Ref	Expression
1		oddpwdc.j	$⊢ J = \{z \in ℕ \| \neg 2 ∥ z\}$
2		oddpwdc.f	$⊢ F = (x \in J, y \in ℕ_{0} ⟼ 2^{y} x)$
3		1st2nd2	$⊢ W \in (J \times ℕ_{0}) \to W = ⟨1^{st} (W), 2^{nd} (W)⟩$
4	3	fveq2d	$⊢ W \in (J \times ℕ_{0}) \to F (W) = F (⟨1^{st} (W), 2^{nd} (W)⟩)$
5		df-ov	$⊢ 1^{st} (W) F 2^{nd} (W) = F (⟨1^{st} (W), 2^{nd} (W)⟩)$
6	5	a1i	$⊢ W \in (J \times ℕ_{0}) \to 1^{st} (W) F 2^{nd} (W) = F (⟨1^{st} (W), 2^{nd} (W)⟩)$
7		elxp6	$⊢ W \in (J \times ℕ_{0}) \leftrightarrow (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in J \land 2^{nd} (W) \in ℕ_{0}))$
8	7	simprbi	$⊢ W \in (J \times ℕ_{0}) \to (1^{st} (W) \in J \land 2^{nd} (W) \in ℕ_{0})$
9		oveq2	$⊢ x = 1^{st} (W) \to 2^{y} x = 2^{y} 1^{st} (W)$
10		oveq2	$⊢ y = 2^{nd} (W) \to 2^{y} = 2^{2^{nd} (W)}$
11	10	oveq1d	$⊢ y = 2^{nd} (W) \to 2^{y} 1^{st} (W) = 2^{2^{nd} (W)} 1^{st} (W)$
12		ovex	$⊢ 2^{2^{nd} (W)} 1^{st} (W) \in V$
13	9 11 2 12	ovmpo	$⊢ (1^{st} (W) \in J \land 2^{nd} (W) \in ℕ_{0}) \to 1^{st} (W) F 2^{nd} (W) = 2^{2^{nd} (W)} 1^{st} (W)$
14	8 13	syl	$⊢ W \in (J \times ℕ_{0}) \to 1^{st} (W) F 2^{nd} (W) = 2^{2^{nd} (W)} 1^{st} (W)$
15	4 6 14	3eqtr2d	$⊢ W \in (J \times ℕ_{0}) \to F (W) = 2^{2^{nd} (W)} 1^{st} (W)$

Metamath Proof Explorer