aks6d1c6lem4

Description: Claim 6 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf Add hypothesis on coprimality, lift function to the integers so that group operations may be applied. Inline definition. (Contributed by metakunt, 14-May-2025)

	Ref	Expression
Hypotheses	aks6d1c6lem4.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
	aks6d1c6lem4.2	$⊢ P = chr (K)$
	aks6d1c6lem4.3	$⊢ φ \to K \in Field$
	aks6d1c6lem4.4	$⊢ φ \to P \in ℙ$
	aks6d1c6lem4.5	$⊢ φ \to R \in ℕ$
	aks6d1c6lem4.6	$⊢ φ \to N \in ℕ$
	aks6d1c6lem4.7	$⊢ φ \to P ∥ N$
	aks6d1c6lem4.8	$⊢ φ \to N \gcd R = 1$
	aks6d1c6lem4.9	$⊢ φ \to \forall b \in (1 \dots A) b \gcd N = 1$
	aks6d1c6lem4.10	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \cdot_{{mulGrp}_{{Poly}_{1} (K)}} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
	aks6d1c6lem4.11	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
	aksaks6dlem4.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
	aks6d1c6lem4.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
	aks6d1c6lem4.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
	aks6d1c6lem4.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
	aks6d1c6lem4.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
	aks6d1c6lem4.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
	aks6d1c6lem4.18	$⊢ D = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
	aks6d1c6lem4.19	$⊢ S = \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
	aks6d1c6lem4.20	$⊢ J = (j \in ℤ ⟼ j \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M)$
	aks6d1c6lem4.21	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|J [E [ℕ_{0} \times ℕ_{0}]]\|$
	aks6d1c6lem4.22	$⊢ U = \{m \in {Base}_{{mulGrp}_{K}} \| \exists n \in {Base}_{{mulGrp}_{K}} n +_{{mulGrp}_{K}} m = 0_{{mulGrp}_{K}}\}$
Assertion	aks6d1c6lem4	$⊢ φ \to (\binom{D + A}{D - 1}) \leq \|H [{ℕ_{0}}^{(0 \dots A)}]\|$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c6lem4.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
2		aks6d1c6lem4.2	$⊢ P = chr (K)$
3		aks6d1c6lem4.3	$⊢ φ \to K \in Field$
4		aks6d1c6lem4.4	$⊢ φ \to P \in ℙ$
5		aks6d1c6lem4.5	$⊢ φ \to R \in ℕ$
6		aks6d1c6lem4.6	$⊢ φ \to N \in ℕ$
7		aks6d1c6lem4.7	$⊢ φ \to P ∥ N$
8		aks6d1c6lem4.8	$⊢ φ \to N \gcd R = 1$
9		aks6d1c6lem4.9	$⊢ φ \to \forall b \in (1 \dots A) b \gcd N = 1$
10		aks6d1c6lem4.10	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \cdot_{{mulGrp}_{{Poly}_{1} (K)}} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
11		aks6d1c6lem4.11	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
12		aksaks6dlem4.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
13		aks6d1c6lem4.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
14		aks6d1c6lem4.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
15		aks6d1c6lem4.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
16		aks6d1c6lem4.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
17		aks6d1c6lem4.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
18		aks6d1c6lem4.18	$⊢ D = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
19		aks6d1c6lem4.19	$⊢ S = \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
20		aks6d1c6lem4.20	$⊢ J = (j \in ℤ ⟼ j \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M)$
21		aks6d1c6lem4.21	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|J [E [ℕ_{0} \times ℕ_{0}]]\|$
22		aks6d1c6lem4.22	$⊢ U = \{m \in {Base}_{{mulGrp}_{K}} \| \exists n \in {Base}_{{mulGrp}_{K}} n +_{{mulGrp}_{K}} m = 0_{{mulGrp}_{K}}\}$
23		simpr	$⊢ (φ \land A < P) \to A < P$
24		prmnn	$⊢ P \in ℙ \to P \in ℕ$
25	4 24	syl	$⊢ φ \to P \in ℕ$
26	25	nnred	$⊢ φ \to P \in ℝ$
27	5	phicld	$⊢ φ \to ϕ (R) \in ℕ$
28	27	nnred	$⊢ φ \to ϕ (R) \in ℝ$
29	27	nnnn0d	$⊢ φ \to ϕ (R) \in ℕ_{0}$
30	29	nn0ge0d	$⊢ φ \to 0 \leq ϕ (R)$
31	28 30	resqrtcld	$⊢ φ \to \sqrt{ϕ (R)} \in ℝ$
32		2re	$⊢ 2 \in ℝ$
33	32	a1i	$⊢ φ \to 2 \in ℝ$
34		2pos	$⊢ 0 < 2$
35	34	a1i	$⊢ φ \to 0 < 2$
36	6	nnred	$⊢ φ \to N \in ℝ$
37	6	nngt0d	$⊢ φ \to 0 < N$
38		1red	$⊢ φ \to 1 \in ℝ$
39		1lt2	$⊢ 1 < 2$
40	39	a1i	$⊢ φ \to 1 < 2$
41	38 40	ltned	$⊢ φ \to 1 \neq 2$
42	41	necomd	$⊢ φ \to 2 \neq 1$
43	33 35 36 37 42	relogbcld	$⊢ φ \to \log_{2} N \in ℝ$
44	31 43	remulcld	$⊢ φ \to \sqrt{ϕ (R)} \log_{2} N \in ℝ$
45	44	flcld	$⊢ φ \to ⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℤ$
46	28 30	sqrtge0d	$⊢ φ \to 0 \leq \sqrt{ϕ (R)}$
47	33	recnd	$⊢ φ \to 2 \in ℂ$
48	35	gt0ne0d	$⊢ φ \to 2 \neq 0$
49		logb1	$⊢ (2 \in ℂ \land 2 \neq 0 \land 2 \neq 1) \to \log_{2} 1 = 0$
50	47 48 42 49	syl3anc	$⊢ φ \to \log_{2} 1 = 0$
51	50	eqcomd	$⊢ φ \to 0 = \log_{2} 1$
52		2z	$⊢ 2 \in ℤ$
53	52	a1i	$⊢ φ \to 2 \in ℤ$
54	33	leidd	$⊢ φ \to 2 \leq 2$
55		0lt1	$⊢ 0 < 1$
56	55	a1i	$⊢ φ \to 0 < 1$
57	6	nnge1d	$⊢ φ \to 1 \leq N$
58	53 54 38 56 36 37 57	logblebd	$⊢ φ \to \log_{2} 1 \leq \log_{2} N$
59	51 58	eqbrtrd	$⊢ φ \to 0 \leq \log_{2} N$
60	31 43 46 59	mulge0d	$⊢ φ \to 0 \leq \sqrt{ϕ (R)} \log_{2} N$
61		0zd	$⊢ φ \to 0 \in ℤ$
62		flge	$⊢ (\sqrt{ϕ (R)} \log_{2} N \in ℝ \land 0 \in ℤ) \to (0 \leq \sqrt{ϕ (R)} \log_{2} N \leftrightarrow 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋)$
63	44 61 62	syl2anc	$⊢ φ \to (0 \leq \sqrt{ϕ (R)} \log_{2} N \leftrightarrow 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋)$
64	60 63	mpbid	$⊢ φ \to 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
65	45 64	jca	$⊢ φ \to (⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℤ \land 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋)$
66		elnn0z	$⊢ ⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℕ_{0} \leftrightarrow (⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℤ \land 0 \leq ⌊\sqrt{ϕ (R)} \log_{2} N⌋)$
67	65 66	sylibr	$⊢ φ \to ⌊\sqrt{ϕ (R)} \log_{2} N⌋ \in ℕ_{0}$
68	11 67	eqeltrid	$⊢ φ \to A \in ℕ_{0}$
69	68	nn0red	$⊢ φ \to A \in ℝ$
70	26 69	lenltd	$⊢ φ \to (P \leq A \leftrightarrow \neg A < P)$
71	70	biimpar	$⊢ (φ \land \neg A < P) \to P \leq A$
72		oveq1	$⊢ b = P \to b \gcd N = P \gcd N$
73	72	eqeq1d	$⊢ b = P \to (b \gcd N = 1 \leftrightarrow P \gcd N = 1)$
74	9	adantr	$⊢ (φ \land P \leq A) \to \forall b \in (1 \dots A) b \gcd N = 1$
75		1zzd	$⊢ (φ \land P \leq A) \to 1 \in ℤ$
76	11 45	eqeltrid	$⊢ φ \to A \in ℤ$
77	76	adantr	$⊢ (φ \land P \leq A) \to A \in ℤ$
78	25	nnzd	$⊢ φ \to P \in ℤ$
79	78	adantr	$⊢ (φ \land P \leq A) \to P \in ℤ$
80	25	nnge1d	$⊢ φ \to 1 \leq P$
81	80	adantr	$⊢ (φ \land P \leq A) \to 1 \leq P$
82		simpr	$⊢ (φ \land P \leq A) \to P \leq A$
83	75 77 79 81 82	elfzd	$⊢ (φ \land P \leq A) \to P \in (1 \dots A)$
84	73 74 83	rspcdva	$⊢ (φ \land P \leq A) \to P \gcd N = 1$
85	84	ex	$⊢ φ \to (P \leq A \to P \gcd N = 1)$
86	85	adantr	$⊢ (φ \land \neg A < P) \to (P \leq A \to P \gcd N = 1)$
87	71 86	mpd	$⊢ (φ \land \neg A < P) \to P \gcd N = 1$
88	6	nnzd	$⊢ φ \to N \in ℤ$
89		coprm	$⊢ (P \in ℙ \land N \in ℤ) \to (\neg P ∥ N \leftrightarrow P \gcd N = 1)$
90	4 88 89	syl2anc	$⊢ φ \to (\neg P ∥ N \leftrightarrow P \gcd N = 1)$
91	90	con1bid	$⊢ φ \to (\neg P \gcd N = 1 \leftrightarrow P ∥ N)$
92	91	bicomd	$⊢ φ \to (P ∥ N \leftrightarrow \neg P \gcd N = 1)$
93	92	biimpd	$⊢ φ \to (P ∥ N \to \neg P \gcd N = 1)$
94	7 93	mpd	$⊢ φ \to \neg P \gcd N = 1$
95	94	neqned	$⊢ φ \to P \gcd N \neq 1$
96	95	adantr	$⊢ (φ \land \neg A < P) \to P \gcd N \neq 1$
97	96	neneqd	$⊢ (φ \land \neg A < P) \to \neg P \gcd N = 1$
98	87 97	pm2.21dd	$⊢ (φ \land \neg A < P) \to A < P$
99	23 98	pm2.61dan	$⊢ φ \to A < P$
100		eqid	$⊢ (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
101		imaco	$⊢ (J \circ E) [ℕ_{0} \times ℕ_{0}] = J [E [ℕ_{0} \times ℕ_{0}]]$
102	101	eqcomi	$⊢ J [E [ℕ_{0} \times ℕ_{0}]] = (J \circ E) [ℕ_{0} \times ℕ_{0}]$
103		resima	$⊢ ({(J \circ E) ↾}_{(ℕ_{0} \times ℕ_{0})}) [ℕ_{0} \times ℕ_{0}] = (J \circ E) [ℕ_{0} \times ℕ_{0}]$
104	103	eqcomi	$⊢ (J \circ E) [ℕ_{0} \times ℕ_{0}] = ({(J \circ E) ↾}_{(ℕ_{0} \times ℕ_{0})}) [ℕ_{0} \times ℕ_{0}]$
105	104	a1i	$⊢ φ \to (J \circ E) [ℕ_{0} \times ℕ_{0}] = ({(J \circ E) ↾}_{(ℕ_{0} \times ℕ_{0})}) [ℕ_{0} \times ℕ_{0}]$
106	78	adantr	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to P \in ℤ$
107		xp1st	$⊢ v \in (ℕ_{0} \times ℕ_{0}) \to 1^{st} (v) \in ℕ_{0}$
108	107	adantl	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to 1^{st} (v) \in ℕ_{0}$
109	106 108	zexpcld	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (v)} \in ℤ$
110	25	nnne0d	$⊢ φ \to P \neq 0$
111		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land N \in ℤ) \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
112	78 110 88 111	syl3anc	$⊢ φ \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
113	7 112	mpbid	$⊢ φ \to \frac{N}{P} \in ℤ$
114	113	adantr	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to \frac{N}{P} \in ℤ$
115		xp2nd	$⊢ v \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (v) \in ℕ_{0}$
116	115	adantl	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to 2^{nd} (v) \in ℕ_{0}$
117	114 116	zexpcld	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to {(\frac{N}{P})}^{2^{nd} (v)} \in ℤ$
118	109 117	zmulcld	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \in ℤ$
119		vex	$⊢ k \in V$
120		vex	$⊢ l \in V$
121	119 120	op1std	$⊢ v = ⟨k, l⟩ \to 1^{st} (v) = k$
122	121	oveq2d	$⊢ v = ⟨k, l⟩ \to P^{1^{st} (v)} = P^{k}$
123	119 120	op2ndd	$⊢ v = ⟨k, l⟩ \to 2^{nd} (v) = l$
124	123	oveq2d	$⊢ v = ⟨k, l⟩ \to {(\frac{N}{P})}^{2^{nd} (v)} = {(\frac{N}{P})}^{l}$
125	122 124	oveq12d	$⊢ v = ⟨k, l⟩ \to P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} = P^{k} {(\frac{N}{P})}^{l}$
126	125	mpompt	$⊢ (v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)}) = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
127	12 126	eqtr4i	$⊢ E = (v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)})$
128	127	a1i	$⊢ φ \to E = (v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)})$
129	20	a1i	$⊢ φ \to J = (j \in ℤ ⟼ j \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M)$
130		oveq1	$⊢ j = P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \to j \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M$
131	118 128 129 130	fmptco	$⊢ φ \to J \circ E = (v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M)$
132	131	reseq1d	$⊢ φ \to {(J \circ E) ↾}_{(ℕ_{0} \times ℕ_{0})} = {(v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) ↾}_{(ℕ_{0} \times ℕ_{0})}$
133		ssidd	$⊢ φ \to ℕ_{0} \times ℕ_{0} \subseteq ℕ_{0} \times ℕ_{0}$
134	133	resmptd	$⊢ φ \to {(v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) ↾}_{(ℕ_{0} \times ℕ_{0})} = (v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M)$
135	128 118	fvmpt2d	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to E (v) = P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)}$
136	135	oveq1d	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M$
137	136	mpteq2dva	$⊢ φ \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) = (v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M)$
138	137	eqcomd	$⊢ φ \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) = (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M)$
139		ovexd	$⊢ (φ \land v \in (ℕ_{0} \times ℕ_{0})) \to E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M \in V$
140		eqid	$⊢ (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) = (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M)$
141	139 140	fmptd	$⊢ φ \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) : ℕ_{0} \times ℕ_{0} ⟶ V$
142		ffn	$⊢ (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) : ℕ_{0} \times ℕ_{0} ⟶ V \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) Fn (ℕ_{0} \times ℕ_{0})$
143	141 142	syl	$⊢ φ \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) Fn (ℕ_{0} \times ℕ_{0})$
144		ovexd	$⊢ (φ \land j \in (ℕ_{0} \times ℕ_{0})) \to E (j) \cdot_{{mulGrp}_{K}} M \in V$
145	144 100	fmptd	$⊢ φ \to (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) : ℕ_{0} \times ℕ_{0} ⟶ V$
146		ffn	$⊢ (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) : ℕ_{0} \times ℕ_{0} ⟶ V \to (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) Fn (ℕ_{0} \times ℕ_{0})$
147	145 146	syl	$⊢ φ \to (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) Fn (ℕ_{0} \times ℕ_{0})$
148		eqidd	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) = (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M)$
149		simpr	$⊢ ((φ \land c \in (ℕ_{0} \times ℕ_{0})) \land v = c) \to v = c$
150	149	fveq2d	$⊢ ((φ \land c \in (ℕ_{0} \times ℕ_{0})) \land v = c) \to E (v) = E (c)$
151	150	oveq1d	$⊢ ((φ \land c \in (ℕ_{0} \times ℕ_{0})) \land v = c) \to E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = E (c) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M$
152		simpr	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to c \in (ℕ_{0} \times ℕ_{0})$
153		ovexd	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to E (c) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M \in V$
154	148 151 152 153	fvmptd	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) (c) = E (c) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M$
155		eqid	$⊢ {mulGrp}_{K} ↾_{𝑠} U = {mulGrp}_{K} ↾_{𝑠} U$
156	22	ssrab3	$⊢ U \subseteq {Base}_{{mulGrp}_{K}}$
157	156	a1i	$⊢ φ \to U \subseteq {Base}_{{mulGrp}_{K}}$
158	157	adantr	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to U \subseteq {Base}_{{mulGrp}_{K}}$
159	3	fldcrngd	$⊢ φ \to K \in CRing$
160		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
161	160	crngmgp	$⊢ K \in CRing \to {mulGrp}_{K} \in CMnd$
162	159 161	syl	$⊢ φ \to {mulGrp}_{K} \in CMnd$
163	162 5 22	primrootsunit	$⊢ φ \to ({mulGrp}_{K} PrimRoots R = ({mulGrp}_{K} ↾_{𝑠} U) PrimRoots R \land {mulGrp}_{K} ↾_{𝑠} U \in Abel)$
164	163	simpld	$⊢ φ \to {mulGrp}_{K} PrimRoots R = ({mulGrp}_{K} ↾_{𝑠} U) PrimRoots R$
165	16 164	eleqtrd	$⊢ φ \to M \in (({mulGrp}_{K} ↾_{𝑠} U) PrimRoots R)$
166	163	simprd	$⊢ φ \to {mulGrp}_{K} ↾_{𝑠} U \in Abel$
167		ablcmn	$⊢ {mulGrp}_{K} ↾_{𝑠} U \in Abel \to {mulGrp}_{K} ↾_{𝑠} U \in CMnd$
168	166 167	syl	$⊢ φ \to {mulGrp}_{K} ↾_{𝑠} U \in CMnd$
169	5	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
170		eqid	$⊢ \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} = \cdot_{({mulGrp}_{K} ↾_{𝑠} U)}$
171	168 169 170	isprimroot	$⊢ φ \to (M \in (({mulGrp}_{K} ↾_{𝑠} U) PrimRoots R) \leftrightarrow (M \in {Base}_{({mulGrp}_{K} ↾_{𝑠} U)} \land R \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = 0_{({mulGrp}_{K} ↾_{𝑠} U)} \land \forall w \in ℕ_{0} (w \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = 0_{({mulGrp}_{K} ↾_{𝑠} U)} \to R ∥ w)))$
172	171	biimpd	$⊢ φ \to (M \in (({mulGrp}_{K} ↾_{𝑠} U) PrimRoots R) \to (M \in {Base}_{({mulGrp}_{K} ↾_{𝑠} U)} \land R \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = 0_{({mulGrp}_{K} ↾_{𝑠} U)} \land \forall w \in ℕ_{0} (w \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = 0_{({mulGrp}_{K} ↾_{𝑠} U)} \to R ∥ w)))$
173	165 172	mpd	$⊢ φ \to (M \in {Base}_{({mulGrp}_{K} ↾_{𝑠} U)} \land R \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = 0_{({mulGrp}_{K} ↾_{𝑠} U)} \land \forall w \in ℕ_{0} (w \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = 0_{({mulGrp}_{K} ↾_{𝑠} U)} \to R ∥ w))$
174	173	simp1d	$⊢ φ \to M \in {Base}_{({mulGrp}_{K} ↾_{𝑠} U)}$
175		eqid	$⊢ {Base}_{{mulGrp}_{K}} = {Base}_{{mulGrp}_{K}}$
176	155 175	ressbas2	$⊢ U \subseteq {Base}_{{mulGrp}_{K}} \to U = {Base}_{({mulGrp}_{K} ↾_{𝑠} U)}$
177	157 176	syl	$⊢ φ \to U = {Base}_{({mulGrp}_{K} ↾_{𝑠} U)}$
178	174 177	eleqtrrd	$⊢ φ \to M \in U$
179	178	adantr	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to M \in U$
180	6 4 7 12	aks6d1c2p1	$⊢ φ \to E : ℕ_{0} \times ℕ_{0} ⟶ ℕ$
181	180	ffvelcdmda	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to E (c) \in ℕ$
182	155 158 179 181	ressmulgnnd	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to E (c) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M = E (c) \cdot_{{mulGrp}_{K}} M$
183		eqidd	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
184		simpr	$⊢ ((φ \land c \in (ℕ_{0} \times ℕ_{0})) \land j = c) \to j = c$
185	184	fveq2d	$⊢ ((φ \land c \in (ℕ_{0} \times ℕ_{0})) \land j = c) \to E (j) = E (c)$
186	185	oveq1d	$⊢ ((φ \land c \in (ℕ_{0} \times ℕ_{0})) \land j = c) \to E (j) \cdot_{{mulGrp}_{K}} M = E (c) \cdot_{{mulGrp}_{K}} M$
187		ovexd	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to E (c) \cdot_{{mulGrp}_{K}} M \in V$
188	183 186 152 187	fvmptd	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) (c) = E (c) \cdot_{{mulGrp}_{K}} M$
189	188	eqcomd	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to E (c) \cdot_{{mulGrp}_{K}} M = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) (c)$
190	154 182 189	3eqtrd	$⊢ (φ \land c \in (ℕ_{0} \times ℕ_{0})) \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) (c) = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) (c)$
191	143 147 190	eqfnfvd	$⊢ φ \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ E (v) \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
192	138 191	eqtrd	$⊢ φ \to (v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
193	134 192	eqtrd	$⊢ φ \to {(v \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (v)} {(\frac{N}{P})}^{2^{nd} (v)} \cdot_{({mulGrp}_{K} ↾_{𝑠} U)} M) ↾}_{(ℕ_{0} \times ℕ_{0})} = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
194	132 193	eqtrd	$⊢ φ \to {(J \circ E) ↾}_{(ℕ_{0} \times ℕ_{0})} = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
195	194	imaeq1d	$⊢ φ \to ({(J \circ E) ↾}_{(ℕ_{0} \times ℕ_{0})}) [ℕ_{0} \times ℕ_{0}] = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) [ℕ_{0} \times ℕ_{0}]$
196	105 195	eqtrd	$⊢ φ \to (J \circ E) [ℕ_{0} \times ℕ_{0}] = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) [ℕ_{0} \times ℕ_{0}]$
197	102 196	eqtrid	$⊢ φ \to J [E [ℕ_{0} \times ℕ_{0}]] = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) [ℕ_{0} \times ℕ_{0}]$
198	197	fveq2d	$⊢ φ \to \|J [E [ℕ_{0} \times ℕ_{0}]]\| = \|(j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) [ℕ_{0} \times ℕ_{0}]\|$
199	21 198	breqtrd	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|(j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) [ℕ_{0} \times ℕ_{0}]\|$
200	1 2 3 4 5 6 7 8 99 10 68 12 13 14 15 16 17 18 19 100 199	aks6d1c6lem3	$⊢ φ \to (\binom{D + A}{D - 1}) \leq \|H [{ℕ_{0}}^{(0 \dots A)}]\|$

Metamath Proof Explorer

Theorem aks6d1c6lem4

Proof