hashscontpow

Description: If a set contains all N -th powers, then the size of the image under the ZR homomorphism is greater than the R -th order of N . (Contributed by metakunt, 28-Apr-2025)

	Ref	Expression
Hypotheses	hashscontpow.1	$⊢ φ \to E \subseteq ℤ$
	hashscontpow.2	$⊢ φ \to N \in ℕ$
	hashscontpow.3	$⊢ φ \to \forall k \in ℕ_{0} N^{k} \in E$
	hashscontpow.4	$⊢ φ \to R \in ℕ$
	hashscontpow.5	$⊢ φ \to N \gcd R = 1$
	hashscontpow.6	$⊢ L = ℤRHom (Y)$
	hashscontpow.7	$⊢ Y = ℤ / R ℤ$
Assertion	hashscontpow	$⊢ φ \to {od}_{ℤ} (R) (N) \leq \|L [E]\|$

Proof

Step	Hyp	Ref	Expression
1		hashscontpow.1	$⊢ φ \to E \subseteq ℤ$
2		hashscontpow.2	$⊢ φ \to N \in ℕ$
3		hashscontpow.3	$⊢ φ \to \forall k \in ℕ_{0} N^{k} \in E$
4		hashscontpow.4	$⊢ φ \to R \in ℕ$
5		hashscontpow.5	$⊢ φ \to N \gcd R = 1$
6		hashscontpow.6	$⊢ L = ℤRHom (Y)$
7		hashscontpow.7	$⊢ Y = ℤ / R ℤ$
8	2	nnzd	$⊢ φ \to N \in ℤ$
9		odzcl	$⊢ (R \in ℕ \land N \in ℤ \land N \gcd R = 1) \to {od}_{ℤ} (R) (N) \in ℕ$
10	4 8 5 9	syl3anc	$⊢ φ \to {od}_{ℤ} (R) (N) \in ℕ$
11	10	nnnn0d	$⊢ φ \to {od}_{ℤ} (R) (N) \in ℕ_{0}$
12		hashfz1	$⊢ {od}_{ℤ} (R) (N) \in ℕ_{0} \to \|(1 \dots {od}_{ℤ} (R) (N))\| = {od}_{ℤ} (R) (N)$
13	11 12	syl	$⊢ φ \to \|(1 \dots {od}_{ℤ} (R) (N))\| = {od}_{ℤ} (R) (N)$
14		ovexd	$⊢ φ \to (1 \dots {od}_{ℤ} (R) (N)) \in V$
15	14	mptexd	$⊢ φ \to (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) \in V$
16	6	fvexi	$⊢ L \in V$
17	16	a1i	$⊢ φ \to L \in V$
18		imaexg	$⊢ L \in V \to L [E] \in V$
19	17 18	syl	$⊢ φ \to L [E] \in V$
20	4	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
21	7	zncrng	$⊢ R \in ℕ_{0} \to Y \in CRing$
22	20 21	syl	$⊢ φ \to Y \in CRing$
23		crngring	$⊢ Y \in CRing \to Y \in Ring$
24	6	zrhrhm	$⊢ Y \in Ring \to L \in (ℤ_{ring} RingHom Y)$
25		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
26		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
27	25 26	rhmf	$⊢ L \in (ℤ_{ring} RingHom Y) \to L : ℤ ⟶ {Base}_{Y}$
28	22 23 24 27	4syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Y}$
29	28	ffnd	$⊢ φ \to L Fn ℤ$
30	29	adantr	$⊢ (φ \land x \in (1 \dots {od}_{ℤ} (R) (N))) \to L Fn ℤ$
31	8	adantr	$⊢ (φ \land x \in (1 \dots {od}_{ℤ} (R) (N))) \to N \in ℤ$
32		elfznn	$⊢ x \in (1 \dots {od}_{ℤ} (R) (N)) \to x \in ℕ$
33	32	adantl	$⊢ (φ \land x \in (1 \dots {od}_{ℤ} (R) (N))) \to x \in ℕ$
34	33	nnnn0d	$⊢ (φ \land x \in (1 \dots {od}_{ℤ} (R) (N))) \to x \in ℕ_{0}$
35	31 34	zexpcld	$⊢ (φ \land x \in (1 \dots {od}_{ℤ} (R) (N))) \to N^{x} \in ℤ$
36		oveq2	$⊢ k = x \to N^{k} = N^{x}$
37	36	eleq1d	$⊢ k = x \to (N^{k} \in E \leftrightarrow N^{x} \in E)$
38	3	adantr	$⊢ (φ \land x \in (1 \dots {od}_{ℤ} (R) (N))) \to \forall k \in ℕ_{0} N^{k} \in E$
39	37 38 34	rspcdva	$⊢ (φ \land x \in (1 \dots {od}_{ℤ} (R) (N))) \to N^{x} \in E$
40	30 35 39	fnfvimad	$⊢ (φ \land x \in (1 \dots {od}_{ℤ} (R) (N))) \to L (N^{x}) \in L [E]$
41	40	fmpttd	$⊢ φ \to (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) : (1 \dots {od}_{ℤ} (R) (N)) ⟶ L [E]$
42	2	ad3antrrr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land a < b) \to N \in ℕ$
43		simpllr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land a < b) \to a \in (1 \dots {od}_{ℤ} (R) (N))$
44		simplr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land a < b) \to b \in (1 \dots {od}_{ℤ} (R) (N))$
45	4	ad3antrrr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land a < b) \to R \in ℕ$
46	5	ad3antrrr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land a < b) \to N \gcd R = 1$
47		simpr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land a < b) \to a < b$
48	42 43 44 45 46 6 7 47	hashscontpow1	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land a < b) \to L (N^{a}) \neq L (N^{b})$
49	2	ad3antrrr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land b < a) \to N \in ℕ$
50		simplr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land b < a) \to b \in (1 \dots {od}_{ℤ} (R) (N))$
51		simpllr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land b < a) \to a \in (1 \dots {od}_{ℤ} (R) (N))$
52	4	ad3antrrr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land b < a) \to R \in ℕ$
53	5	ad3antrrr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land b < a) \to N \gcd R = 1$
54		simpr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land b < a) \to b < a$
55	49 50 51 52 53 6 7 54	hashscontpow1	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land b < a) \to L (N^{b}) \neq L (N^{a})$
56	55	necomd	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land b < a) \to L (N^{a}) \neq L (N^{b})$
57	48 56	jaodan	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land (a < b \lor b < a)) \to L (N^{a}) \neq L (N^{b})$
58	57	ex	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to ((a < b \lor b < a) \to L (N^{a}) \neq L (N^{b}))$
59		biidd	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to (a = b \leftrightarrow a = b)$
60	59	necon3bbid	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to (\neg a = b \leftrightarrow a \neq b)$
61		elfzelz	$⊢ a \in (1 \dots {od}_{ℤ} (R) (N)) \to a \in ℤ$
62	61	adantl	$⊢ (φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \to a \in ℤ$
63	62	adantr	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to a \in ℤ$
64	63	zred	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to a \in ℝ$
65		elfzelz	$⊢ b \in (1 \dots {od}_{ℤ} (R) (N)) \to b \in ℤ$
66	65	zred	$⊢ b \in (1 \dots {od}_{ℤ} (R) (N)) \to b \in ℝ$
67	66	adantl	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to b \in ℝ$
68		lttri2	$⊢ (a \in ℝ \land b \in ℝ) \to (a \neq b \leftrightarrow (a < b \lor b < a))$
69	64 67 68	syl2anc	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to (a \neq b \leftrightarrow (a < b \lor b < a))$
70	60 69	bitrd	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to (\neg a = b \leftrightarrow (a < b \lor b < a))$
71	70	imbi1d	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to ((\neg a = b \to L (N^{a}) \neq L (N^{b})) \leftrightarrow ((a < b \lor b < a) \to L (N^{a}) \neq L (N^{b})))$
72	58 71	mpbird	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to (\neg a = b \to L (N^{a}) \neq L (N^{b}))$
73	72	imp	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to L (N^{a}) \neq L (N^{b})$
74		eqidd	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) = (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x}))$
75		simpr	$⊢ ((((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \land x = a) \to x = a$
76	75	oveq2d	$⊢ ((((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \land x = a) \to N^{x} = N^{a}$
77	76	fveq2d	$⊢ ((((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \land x = a) \to L (N^{x}) = L (N^{a})$
78		simpllr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to a \in (1 \dots {od}_{ℤ} (R) (N))$
79		fvexd	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to L (N^{a}) \in V$
80	74 77 78 79	fvmptd	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) = L (N^{a})$
81		simpr	$⊢ ((((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \land x = b) \to x = b$
82	81	oveq2d	$⊢ ((((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \land x = b) \to N^{x} = N^{b}$
83	82	fveq2d	$⊢ ((((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \land x = b) \to L (N^{x}) = L (N^{b})$
84		simplr	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to b \in (1 \dots {od}_{ℤ} (R) (N))$
85		fvexd	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to L (N^{b}) \in V$
86	74 83 84 85	fvmptd	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b) = L (N^{b})$
87	80 86	neeq12d	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to ((x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) \neq (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b) \leftrightarrow L (N^{a}) \neq L (N^{b}))$
88	73 87	mpbird	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) \neq (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b)$
89	88	neneqd	$⊢ (((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \land \neg a = b) \to \neg (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) = (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b)$
90	89	ex	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to (\neg a = b \to \neg (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) = (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b))$
91	90	con4d	$⊢ ((φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \land b \in (1 \dots {od}_{ℤ} (R) (N))) \to ((x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) = (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b) \to a = b)$
92	91	ralrimiva	$⊢ (φ \land a \in (1 \dots {od}_{ℤ} (R) (N))) \to \forall b \in (1 \dots {od}_{ℤ} (R) (N)) ((x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) = (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b) \to a = b)$
93	92	ralrimiva	$⊢ φ \to \forall a \in (1 \dots {od}_{ℤ} (R) (N)) \forall b \in (1 \dots {od}_{ℤ} (R) (N)) ((x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) = (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b) \to a = b)$
94	41 93	jca	$⊢ φ \to ((x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) : (1 \dots {od}_{ℤ} (R) (N)) ⟶ L [E] \land \forall a \in (1 \dots {od}_{ℤ} (R) (N)) \forall b \in (1 \dots {od}_{ℤ} (R) (N)) ((x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) = (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b) \to a = b))$
95		dff13	$⊢ (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) : (1 \dots {od}_{ℤ} (R) (N)) \underset{1-1}{⟶} L [E] \leftrightarrow ((x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) : (1 \dots {od}_{ℤ} (R) (N)) ⟶ L [E] \land \forall a \in (1 \dots {od}_{ℤ} (R) (N)) \forall b \in (1 \dots {od}_{ℤ} (R) (N)) ((x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (a) = (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) (b) \to a = b))$
96	94 95	sylibr	$⊢ φ \to (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) : (1 \dots {od}_{ℤ} (R) (N)) \underset{1-1}{⟶} L [E]$
97		hashf1dmcdm	$⊢ ((x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) \in V \land L [E] \in V \land (x \in (1 \dots {od}_{ℤ} (R) (N)) ⟼ L (N^{x})) : (1 \dots {od}_{ℤ} (R) (N)) \underset{1-1}{⟶} L [E]) \to \|(1 \dots {od}_{ℤ} (R) (N))\| \leq \|L [E]\|$
98	15 19 96 97	syl3anc	$⊢ φ \to \|(1 \dots {od}_{ℤ} (R) (N))\| \leq \|L [E]\|$
99	13 98	eqbrtrrd	$⊢ φ \to {od}_{ℤ} (R) (N) \leq \|L [E]\|$

Metamath Proof Explorer

Theorem hashscontpow

Proof