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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	smuval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	smuval.p	⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
	smuval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	smuval	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smuval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		smuval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		smuval.p	⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4		smuval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5	1 2 3	smufval	⊢ ( 𝜑 → ( 𝐴 smul 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
6	5	eleq2d	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
7		id	⊢ ( 𝑘 = 𝑁 → 𝑘 = 𝑁 )
8		fvoveq1	⊢ ( 𝑘 = 𝑁 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
9	7 8	eleq12d	⊢ ( 𝑘 = 𝑁 → ( 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )
10	9	elrab3	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )
11	4 10	syl	⊢ ( 𝜑 → ( 𝑁 ∈ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )
12	6 11	bitrd	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )