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 𝐹 = ( 𝑥𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
Assertion oddpwdcv ( 𝑊 ∈ ( 𝐽 × ℕ0 ) → ( 𝐹𝑊 ) = ( ( 2 ↑ ( 2nd𝑊 ) ) · ( 1st𝑊 ) ) )

Proof

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