Metamath Proof Explorer

Theorem oddpwdcv

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

		Ref	Expression
	Hypotheses	oddpwdc.j	⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
		oddpwdc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ₀ ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
	Assertion	oddpwdcv	⊢ ( 𝑊 ∈ ( 𝐽 × ℕ₀ ) → ( 𝐹 ‘ 𝑊 ) = ( ( 2 ↑ ( 2^nd ‘ 𝑊 ) ) · ( 1^st ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oddpwdc.j	⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
2		oddpwdc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ₀ ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
3		1st2nd2	⊢ ( 𝑊 ∈ ( 𝐽 × ℕ₀ ) → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
4	3	fveq2d	⊢ ( 𝑊 ∈ ( 𝐽 × ℕ₀ ) → ( 𝐹 ‘ 𝑊 ) = ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ) )
5		df-ov	⊢ ( ( 1^st ‘ 𝑊 ) 𝐹 ( 2^nd ‘ 𝑊 ) ) = ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
6	5	a1i	⊢ ( 𝑊 ∈ ( 𝐽 × ℕ₀ ) → ( ( 1^st ‘ 𝑊 ) 𝐹 ( 2^nd ‘ 𝑊 ) ) = ( 𝐹 ‘ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ) )
7		elxp6	⊢ ( 𝑊 ∈ ( 𝐽 × ℕ₀ ) ↔ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∧ ( ( 1^st ‘ 𝑊 ) ∈ 𝐽 ∧ ( 2^nd ‘ 𝑊 ) ∈ ℕ₀ ) ) )
8	7	simprbi	⊢ ( 𝑊 ∈ ( 𝐽 × ℕ₀ ) → ( ( 1^st ‘ 𝑊 ) ∈ 𝐽 ∧ ( 2^nd ‘ 𝑊 ) ∈ ℕ₀ ) )
9		oveq2	⊢ ( 𝑥 = ( 1^st ‘ 𝑊 ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) = ( ( 2 ↑ 𝑦 ) · ( 1^st ‘ 𝑊 ) ) )
10		oveq2	⊢ ( 𝑦 = ( 2^nd ‘ 𝑊 ) → ( 2 ↑ 𝑦 ) = ( 2 ↑ ( 2^nd ‘ 𝑊 ) ) )
11	10	oveq1d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑊 ) → ( ( 2 ↑ 𝑦 ) · ( 1^st ‘ 𝑊 ) ) = ( ( 2 ↑ ( 2^nd ‘ 𝑊 ) ) · ( 1^st ‘ 𝑊 ) ) )
12		ovex	⊢ ( ( 2 ↑ ( 2^nd ‘ 𝑊 ) ) · ( 1^st ‘ 𝑊 ) ) ∈ V
13	9 11 2 12	ovmpo	⊢ ( ( ( 1^st ‘ 𝑊 ) ∈ 𝐽 ∧ ( 2^nd ‘ 𝑊 ) ∈ ℕ₀ ) → ( ( 1^st ‘ 𝑊 ) 𝐹 ( 2^nd ‘ 𝑊 ) ) = ( ( 2 ↑ ( 2^nd ‘ 𝑊 ) ) · ( 1^st ‘ 𝑊 ) ) )
14	8 13	syl	⊢ ( 𝑊 ∈ ( 𝐽 × ℕ₀ ) → ( ( 1^st ‘ 𝑊 ) 𝐹 ( 2^nd ‘ 𝑊 ) ) = ( ( 2 ↑ ( 2^nd ‘ 𝑊 ) ) · ( 1^st ‘ 𝑊 ) ) )
15	4 6 14	3eqtr2d	⊢ ( 𝑊 ∈ ( 𝐽 × ℕ₀ ) → ( 𝐹 ‘ 𝑊 ) = ( ( 2 ↑ ( 2^nd ‘ 𝑊 ) ) · ( 1^st ‘ 𝑊 ) ) )