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

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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑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 mulridi ⊢ ( ( ♯ ‘ ( 0 ..^ 𝑆 ) ) · 1 ) = ( ♯ ‘ ( 0 ..^ 𝑆 ) )
39 34 38 eqtri ⊢ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 1 = ( ♯ ‘ ( 0 ..^ 𝑆 ) )
40 hashfzo0 ⊢ ( 𝑆 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 )
41 3 40 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 )
42 39 41 eqtrid ⊢ ( 𝜑 → Σ 𝑎 ∈ ( 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 ‘ 𝑆 ) 𝑀 ) = ∅ )