Metamath Proof Explorer

Theorem smuval

Description: Define the addition of two bit sequences, using df-had and df-cad bit operations. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses smuval.a ⊢ φ → A ⊆ ℕ 0
smuval.b ⊢ φ → B ⊆ ℕ 0
smuval.p ⊢ P = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
smuval.n ⊢ φ → N ∈ ℕ 0
Assertion smuval ⊢ φ → N ∈ A smul B ↔ N ∈ P ⁡ N + 1

Proof

Step Hyp Ref Expression
1 smuval.a ⊢ φ → A ⊆ ℕ 0
2 smuval.b ⊢ φ → B ⊆ ℕ 0
3 smuval.p ⊢ P = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
4 smuval.n ⊢ φ → N ∈ ℕ 0
5 1 2 3 smufval ⊢ φ → A smul B = k ∈ ℕ 0 | k ∈ P ⁡ k + 1
6 5 eleq2d ⊢ φ → N ∈ A smul B ↔ N ∈ k ∈ ℕ 0 | k ∈ P ⁡ k + 1
7 id ⊢ k = N → k = N
8 fvoveq1 ⊢ k = N → P ⁡ k + 1 = P ⁡ N + 1
9 7 8 eleq12d ⊢ k = N → k ∈ P ⁡ k + 1 ↔ N ∈ P ⁡ N + 1
10 9 elrab3 ⊢ N ∈ ℕ 0 → N ∈ k ∈ ℕ 0 | k ∈ P ⁡ k + 1 ↔ N ∈ P ⁡ N + 1
11 4 10 syl ⊢ φ → N ∈ k ∈ ℕ 0 | k ∈ P ⁡ k + 1 ↔ N ∈ P ⁡ N + 1
12 6 11 bitrd ⊢ φ → N ∈ A smul B ↔ N ∈ P ⁡ N + 1