Metamath Proof Explorer

Theorem smup0

Description: The initial element of the partial sum sequence. (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
Assertion smup0 ⊢ φ → P ⁡ 0 = ∅

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 0z ⊢ 0 ∈ ℤ
5 3 fveq1i ⊢ P ⁡ 0 = seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
6 seq1 ⊢ 0 ∈ ℤ → seq 0 p ∈ 𝒫 ℕ 0 , m ∈ ℕ 0 ⟼ p sadd n ∈ ℕ 0 | m ∈ A ∧ n − m ∈ B n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
7 5 6 eqtrid ⊢ 0 ∈ ℤ → P ⁡ 0 = n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
8 4 7 mp1i ⊢ φ → P ⁡ 0 = n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0
9 0nn0 ⊢ 0 ∈ ℕ 0
10 iftrue ⊢ n = 0 → if n = 0 ∅ n − 1 = ∅
11 eqid ⊢ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
12 0ex ⊢ ∅ ∈ V
13 10 11 12 fvmpt ⊢ 0 ∈ ℕ 0 → n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = ∅
14 9 13 mp1i ⊢ φ → n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = ∅
15 8 14 eqtrd ⊢ φ → P ⁡ 0 = ∅