This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suppssnn0

Description: Show that the support of a function is contained in an half-open nonnegative integer range. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses suppssnn0.f 
|- ( ph -> F Fn NN0 )
suppssnn0.n 
|- ( ( ( ph /\ k e. NN0 ) /\ N <_ k ) -> ( F ` k ) = Z )
suppssnn0.1 
|- ( ph -> N e. ZZ )
Assertion suppssnn0 
|- ( ph -> ( F supp Z ) C_ ( 0 ..^ N ) )

Proof

Step Hyp Ref Expression
1 suppssnn0.f 
 |-  ( ph -> F Fn NN0 )
2 suppssnn0.n 
 |-  ( ( ( ph /\ k e. NN0 ) /\ N <_ k ) -> ( F ` k ) = Z )
3 suppssnn0.1 
 |-  ( ph -> N e. ZZ )
4 dffn3 
 |-  ( F Fn NN0 <-> F : NN0 --> ran F )
5 1 4 sylib 
 |-  ( ph -> F : NN0 --> ran F )
6 simpl 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> ph )
7 eldifi 
 |-  ( k e. ( NN0 \ ( 0 ..^ N ) ) -> k e. NN0 )
8 7 adantl 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> k e. NN0 )
9 3 zred 
 |-  ( ph -> N e. RR )
10 9 adantr 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> N e. RR )
11 8 nn0red 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> k e. RR )
12 3 adantr 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> N e. ZZ )
13 simpr 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> k e. ( NN0 \ ( 0 ..^ N ) ) )
14 12 13 nn0difffzod 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> -. k < N )
15 10 11 14 nltled 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> N <_ k )
16 6 8 15 2 syl21anc 
 |-  ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> ( F ` k ) = Z )
17 5 16 suppss 
 |-  ( ph -> ( F supp Z ) C_ ( 0 ..^ N ) )