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 ‘ 𝑆 ) 𝑀 ) = ∅ )