Metamath Proof Explorer

Theorem reprlt

Description: There are no representations of M with more than M terms. Remark of Nathanson p. 123. (Contributed by Thierry Arnoux, 7-Dec-2021)

Ref Expression
Hypotheses reprval.a ⊢ φ → A ⊆ ℕ
reprval.m ⊢ φ → M ∈ ℤ
reprval.s ⊢ φ → S ∈ ℕ 0
reprlt.1 ⊢ φ → M < S
Assertion reprlt ⊢ φ → A repr ⁡ S M = ∅

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ φ → A ⊆ ℕ
2 reprval.m ⊢ φ → M ∈ ℤ
3 reprval.s ⊢ φ → S ∈ ℕ 0
4 reprlt.1 ⊢ φ → M < S
5 1 2 3 reprval ⊢ φ → A repr ⁡ S M = c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
6 2 zred ⊢ φ → M ∈ ℝ
7 6 adantr ⊢ φ ∧ c ∈ A 0 ..^ S → M ∈ ℝ
8 3 nn0red ⊢ φ → S ∈ ℝ
9 8 adantr ⊢ φ ∧ c ∈ A 0 ..^ S → S ∈ ℝ
10 fzofi ⊢ 0 ..^ S ∈ Fin
11 10 a1i ⊢ φ ∧ c ∈ A 0 ..^ S → 0 ..^ S ∈ Fin
12 nnssre ⊢ ℕ ⊆ ℝ
13 12 a1i ⊢ φ → ℕ ⊆ ℝ
14 1 13 sstrd ⊢ φ → A ⊆ ℝ
15 14 ad2antrr ⊢ φ ∧ c ∈ A 0 ..^ S ∧ a ∈ 0 ..^ S → A ⊆ ℝ
16 nnex ⊢ ℕ ∈ V
17 16 a1i ⊢ φ → ℕ ∈ V
18 17 1 ssexd ⊢ φ → A ∈ V
19 18 adantr ⊢ φ ∧ c ∈ A 0 ..^ S → A ∈ V
20 10 elexi ⊢ 0 ..^ S ∈ V
21 20 a1i ⊢ φ ∧ c ∈ A 0 ..^ S → 0 ..^ S ∈ V
22 simpr ⊢ φ ∧ c ∈ A 0 ..^ S → c ∈ A 0 ..^ S
23 elmapg ⊢ A ∈ V ∧ 0 ..^ S ∈ V → c ∈ A 0 ..^ S ↔ c : 0 ..^ S ⟶ A
24 23 biimpa ⊢ A ∈ V ∧ 0 ..^ S ∈ V ∧ c ∈ A 0 ..^ S → c : 0 ..^ S ⟶ A
25 19 21 22 24 syl21anc ⊢ φ ∧ c ∈ A 0 ..^ S → c : 0 ..^ S ⟶ A
26 25 adantr ⊢ φ ∧ c ∈ A 0 ..^ S ∧ a ∈ 0 ..^ S → c : 0 ..^ S ⟶ A
27 simpr ⊢ φ ∧ c ∈ A 0 ..^ S ∧ a ∈ 0 ..^ S → a ∈ 0 ..^ S
28 26 27 ffvelcdmd ⊢ φ ∧ c ∈ A 0 ..^ S ∧ a ∈ 0 ..^ S → c ⁡ a ∈ A
29 15 28 sseldd ⊢ φ ∧ c ∈ A 0 ..^ S ∧ a ∈ 0 ..^ S → c ⁡ a ∈ ℝ
30 11 29 fsumrecl ⊢ φ ∧ c ∈ A 0 ..^ S → ∑ a ∈ 0 ..^ S c ⁡ a ∈ ℝ
31 4 adantr ⊢ φ ∧ c ∈ A 0 ..^ S → M < S
32 ax-1cn ⊢ 1 ∈ ℂ
33 fsumconst ⊢ 0 ..^ S ∈ Fin ∧ 1 ∈ ℂ → ∑ a ∈ 0 ..^ S 1 = 0 ..^ S ⋅ 1
34 10 32 33 mp2an ⊢ ∑ a ∈ 0 ..^ S 1 = 0 ..^ S ⋅ 1
35 hashcl ⊢ 0 ..^ S ∈ Fin → 0 ..^ S ∈ ℕ 0
36 10 35 ax-mp ⊢ 0 ..^ S ∈ ℕ 0
37 36 nn0cni ⊢ 0 ..^ S ∈ ℂ
38 37 mulridi ⊢ 0 ..^ S ⋅ 1 = 0 ..^ S
39 34 38 eqtri ⊢ ∑ a ∈ 0 ..^ S 1 = 0 ..^ S
40 hashfzo0 ⊢ S ∈ ℕ 0 → 0 ..^ S = S
41 3 40 syl ⊢ φ → 0 ..^ S = S
42 39 41 eqtrid ⊢ φ → ∑ a ∈ 0 ..^ S 1 = S
43 42 adantr ⊢ φ ∧ c ∈ A 0 ..^ S → ∑ a ∈ 0 ..^ S 1 = S
44 1red ⊢ φ ∧ c ∈ A 0 ..^ S ∧ a ∈ 0 ..^ S → 1 ∈ ℝ
45 1 ad2antrr ⊢ φ ∧ c ∈ A 0 ..^ S ∧ a ∈ 0 ..^ S → A ⊆ ℕ
46 45 28 sseldd ⊢ φ ∧ c ∈ A 0 ..^ S ∧ a ∈ 0 ..^ S → c ⁡ a ∈ ℕ
47 nnge1 ⊢ c ⁡ a ∈ ℕ → 1 ≤ c ⁡ a
48 46 47 syl ⊢ φ ∧ c ∈ A 0 ..^ S ∧ a ∈ 0 ..^ S → 1 ≤ c ⁡ a
49 11 44 29 48 fsumle ⊢ φ ∧ c ∈ A 0 ..^ S → ∑ a ∈ 0 ..^ S 1 ≤ ∑ a ∈ 0 ..^ S c ⁡ a
50 43 49 eqbrtrrd ⊢ φ ∧ c ∈ A 0 ..^ S → S ≤ ∑ a ∈ 0 ..^ S c ⁡ a
51 7 9 30 31 50 ltletrd ⊢ φ ∧ c ∈ A 0 ..^ S → M < ∑ a ∈ 0 ..^ S c ⁡ a
52 7 51 ltned ⊢ φ ∧ c ∈ A 0 ..^ S → M ≠ ∑ a ∈ 0 ..^ S c ⁡ a
53 52 necomd ⊢ φ ∧ c ∈ A 0 ..^ S → ∑ a ∈ 0 ..^ S c ⁡ a ≠ M
54 53 neneqd ⊢ φ ∧ c ∈ A 0 ..^ S → ¬ ∑ a ∈ 0 ..^ S c ⁡ a = M
55 54 ralrimiva ⊢ φ → ∀ c ∈ A 0 ..^ S ¬ ∑ a ∈ 0 ..^ S c ⁡ a = M
56 rabeq0 ⊢ c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M = ∅ ↔ ∀ c ∈ A 0 ..^ S ¬ ∑ a ∈ 0 ..^ S c ⁡ a = M
57 55 56 sylibr ⊢ φ → c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M = ∅
58 5 57 eqtrd ⊢ φ → A repr ⁡ S M = ∅