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 
|- ( ph -> A C_ NN0 )
smuval.b 
|- ( ph -> B C_ NN0 )
smuval.p 
|- P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
Assertion smup0 
|- ( ph -> ( P ` 0 ) = (/) )

Proof

Step Hyp Ref Expression
1 smuval.a 
 |-  ( ph -> A C_ NN0 )
2 smuval.b 
 |-  ( ph -> B C_ NN0 )
3 smuval.p 
 |-  P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4 0z 
 |-  0 e. ZZ
5 3 fveq1i 
 |-  ( P ` 0 ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 )
6 seq1 
 |-  ( 0 e. ZZ -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) = ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) )
7 5 6 syl5eq 
 |-  ( 0 e. ZZ -> ( P ` 0 ) = ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) )
8 4 7 mp1i 
 |-  ( ph -> ( P ` 0 ) = ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) )
9 0nn0 
 |-  0 e. NN0
10 iftrue 
 |-  ( n = 0 -> if ( n = 0 , (/) , ( n - 1 ) ) = (/) )
11 eqid 
 |-  ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) = ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
12 0ex 
 |-  (/) e. _V
13 10 11 12 fvmpt 
 |-  ( 0 e. NN0 -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) = (/) )
14 9 13 mp1i 
 |-  ( ph -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` 0 ) = (/) )
15 8 14 eqtrd 
 |-  ( ph -> ( P ` 0 ) = (/) )