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 ( 𝜑𝐴 ⊆ ℕ )
reprval.m ( 𝜑𝑀 ∈ ℤ )
reprval.s ( 𝜑𝑆 ∈ ℕ0 )
reprlt.1 ( 𝜑𝑀 < 𝑆 )
Assertion reprlt ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = ∅ )

Proof

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