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

Metamath Proof Explorer

Theorem reprgt

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

Ref Expression
Hypotheses reprgt.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
reprgt.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 1 ... 𝑁 ) )
reprgt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
reprgt.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
reprgt.1 ⊢ ( 𝜑 → ( 𝑆 · 𝑁 ) < 𝑀 )
Assertion reprgt ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = ∅ )

Proof

Step Hyp Ref Expression
1 reprgt.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 reprgt.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 1 ... 𝑁 ) )
3 reprgt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 reprgt.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
5 reprgt.1 ⊢ ( 𝜑 → ( 𝑆 · 𝑁 ) < 𝑀 )
6 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
7 2 6 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
8 7 3 4 reprval ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
9 fzofi ⊢ ( 0 ..^ 𝑆 ) ∈ Fin
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
11 nnssre ⊢ ℕ ⊆ ℝ
12 7 11 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
13 12 ralrimivw ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝐴 ⊆ ℝ )
14 13 ralrimivw ⊢ ( 𝜑 → ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∀ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝐴 ⊆ ℝ )
15 14 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ∀ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝐴 ⊆ ℝ )
16 15 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℝ )
17 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
18 17 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ V )
19 18 2 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝐴 ∈ V )
21 9 elexi ⊢ ( 0 ..^ 𝑆 ) ∈ V
22 21 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ( 0 ..^ 𝑆 ) ∈ V )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
24 elmapg ⊢ ( ( 𝐴 ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
25 24 biimpa ⊢ ( ( ( 𝐴 ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
26 20 22 23 25 syl21anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
28 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ 𝑆 ) )
29 27 28 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ 𝐴 )
30 16 29 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ℝ )
31 10 30 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ∈ ℝ )
32 4 nn0red ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑆 ∈ ℝ )
34 1 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑁 ∈ ℝ )
36 33 35 remulcld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ( 𝑆 · 𝑁 ) ∈ ℝ )
37 3 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑀 ∈ ℝ )
39 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑁 ∈ ℝ )
40 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ( 1 ... 𝑁 ) )
41 40 29 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
42 elfzle2 ⊢ ( ( 𝑐 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) → ( 𝑐 ‘ 𝑎 ) ≤ 𝑁 )
43 41 42 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ≤ 𝑁 )
44 10 30 39 43 fsumle ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ≤ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝑁 )
45 34 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
46 fsumconst ⊢ ( ( ( 0 ..^ 𝑆 ) ∈ Fin ∧ 𝑁 ∈ ℂ ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝑁 = ( ( ♯ ‘ ( 0 ..^ 𝑆 ) ) · 𝑁 ) )
47 9 45 46 sylancr ⊢ ( 𝜑 → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝑁 = ( ( ♯ ‘ ( 0 ..^ 𝑆 ) ) · 𝑁 ) )
48 hashfzo0 ⊢ ( 𝑆 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 )
49 4 48 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 )
50 49 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑆 ) ) · 𝑁 ) = ( 𝑆 · 𝑁 ) )
51 47 50 eqtrd ⊢ ( 𝜑 → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝑁 = ( 𝑆 · 𝑁 ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝑁 = ( 𝑆 · 𝑁 ) )
53 44 52 breqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ≤ ( 𝑆 · 𝑁 ) )
54 5 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ( 𝑆 · 𝑁 ) < 𝑀 )
55 31 36 38 53 54 lelttrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) < 𝑀 )
56 31 55 ltned ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) ≠ 𝑀 )
57 56 neneqd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ) → ¬ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 )
58 57 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ¬ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 )
59 rabeq0 ⊢ ( { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } = ∅ ↔ ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ¬ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 )
60 58 59 sylibr ⊢ ( 𝜑 → { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } = ∅ )
61 8 60 eqtrd ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = ∅ )