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 ‘ 𝑊 ) ) ) |