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

Metamath Proof Explorer

Theorem reprle

Description: Upper bound to the terms in the representations of M as the sum of S nonnegative integers from set A . (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Hypotheses reprval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
reprf.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
reprle.x ⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ 𝑆 ) )
Assertion reprle ( 𝜑 → ( 𝐶 ‘ 𝑋 ) ≤ 𝑀 )

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2 reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4 reprf.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
5 reprle.x ⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ 𝑆 ) )
6 fveq2 ⊢ ( 𝑎 = 𝑋 → ( 𝐶 ‘ 𝑎 ) = ( 𝐶 ‘ 𝑋 ) )
7 fzofi ⊢ ( 0 ..^ 𝑆 ) ∈ Fin
8 7 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑆 ) ∈ Fin )
9 1 2 3 4 reprsum ⊢ ( 𝜑 → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝐶 ‘ 𝑎 ) = 𝑀 )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℕ )
11 1 2 3 4 reprf ⊢ ( 𝜑 → 𝐶 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
12 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝐶 ‘ 𝑎 ) ∈ 𝐴 )
13 10 12 sseldd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝐶 ‘ 𝑎 ) ∈ ℕ )
14 13 nnrpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝐶 ‘ 𝑎 ) ∈ ℝ+ )
15 6 8 9 14 5 fsumub ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑋 ) ≤ 𝑀 )