Theorem 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	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
	aks6d1c6lem4.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
	aks6d1c6lem4.3	⊢ ( 𝜑 → 𝐾 ∈ Field )
	aks6d1c6lem4.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	aks6d1c6lem4.5	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	aks6d1c6lem4.6	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	aks6d1c6lem4.7	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	aks6d1c6lem4.8	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
	aks6d1c6lem4.9	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
	aks6d1c6lem4.10	⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
	aks6d1c6lem4.11	⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
	aksaks6dlem4.12	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
	aks6d1c6lem4.13	⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
	aks6d1c6lem4.14	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
	aks6d1c6lem4.15	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
	aks6d1c6lem4.16	⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
	aks6d1c6lem4.17	⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
	aks6d1c6lem4.18	⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
	aks6d1c6lem4.19	⊢ 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) }
	aks6d1c6lem4.20	⊢ 𝐽 = ( 𝑗 ∈ ℤ ↦ ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
	aks6d1c6lem4.21	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ♯ ‘ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
	aks6d1c6lem4.22	⊢ 𝑈 = { 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑛 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑛 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑚 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) }
Assertion	aks6d1c6lem4	⊢ ( 𝜑 → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ≤ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		aks6d1c6lem4.1	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2		aks6d1c6lem4.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
3		aks6d1c6lem4.3	⊢ ( 𝜑 → 𝐾 ∈ Field )
4		aks6d1c6lem4.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		aks6d1c6lem4.5	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6		aks6d1c6lem4.6	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7		aks6d1c6lem4.7	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8		aks6d1c6lem4.8	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9		aks6d1c6lem4.9	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
10		aks6d1c6lem4.10	⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
11		aks6d1c6lem4.11	⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
12		aksaks6dlem4.12	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
13		aks6d1c6lem4.13	⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
14		aks6d1c6lem4.14	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
15		aks6d1c6lem4.15	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
16		aks6d1c6lem4.16	⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
17		aks6d1c6lem4.17	⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
18		aks6d1c6lem4.18	⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
19		aks6d1c6lem4.19	⊢ 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) }
20		aks6d1c6lem4.20	⊢ 𝐽 = ( 𝑗 ∈ ℤ ↦ ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
21		aks6d1c6lem4.21	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ♯ ‘ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
22		aks6d1c6lem4.22	⊢ 𝑈 = { 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑛 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑛 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑚 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) }
23		simpr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝑃 ) → 𝐴 < 𝑃 )
24		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
25	4 24	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
26	25	nnred	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
27	5	phicld	⊢ ( 𝜑 → ( ϕ ‘ 𝑅 ) ∈ ℕ )
28	27	nnred	⊢ ( 𝜑 → ( ϕ ‘ 𝑅 ) ∈ ℝ )
29	27	nnnn0d	⊢ ( 𝜑 → ( ϕ ‘ 𝑅 ) ∈ ℕ0 )
30	29	nn0ge0d	⊢ ( 𝜑 → 0 ≤ ( ϕ ‘ 𝑅 ) )
31	28 30	resqrtcld	⊢ ( 𝜑 → ( √ ‘ ( ϕ ‘ 𝑅 ) ) ∈ ℝ )
32		2re	⊢ 2 ∈ ℝ
33	32	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
34		2pos	⊢ 0 < 2
35	34	a1i	⊢ ( 𝜑 → 0 < 2 )
36	6	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
37	6	nngt0d	⊢ ( 𝜑 → 0 < 𝑁 )
38		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
39		1lt2	⊢ 1 < 2
40	39	a1i	⊢ ( 𝜑 → 1 < 2 )
41	38 40	ltned	⊢ ( 𝜑 → 1 ≠ 2 )
42	41	necomd	⊢ ( 𝜑 → 2 ≠ 1 )
43	33 35 36 37 42	relogbcld	⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
44	31 43	remulcld	⊢ ( 𝜑 → ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ )
45	44	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ )
46	28 30	sqrtge0d	⊢ ( 𝜑 → 0 ≤ ( √ ‘ ( ϕ ‘ 𝑅 ) ) )
47	33	recnd	⊢ ( 𝜑 → 2 ∈ ℂ )
48	35	gt0ne0d	⊢ ( 𝜑 → 2 ≠ 0 )
49		logb1	⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 1 ) = 0 )
50	47 48 42 49	syl3anc	⊢ ( 𝜑 → ( 2 logb 1 ) = 0 )
51	50	eqcomd	⊢ ( 𝜑 → 0 = ( 2 logb 1 ) )
52		2z	⊢ 2 ∈ ℤ
53	52	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
54	33	leidd	⊢ ( 𝜑 → 2 ≤ 2 )
55		0lt1	⊢ 0 < 1
56	55	a1i	⊢ ( 𝜑 → 0 < 1 )
57	6	nnge1d	⊢ ( 𝜑 → 1 ≤ 𝑁 )
58	53 54 38 56 36 37 57	logblebd	⊢ ( 𝜑 → ( 2 logb 1 ) ≤ ( 2 logb 𝑁 ) )
59	51 58	eqbrtrd	⊢ ( 𝜑 → 0 ≤ ( 2 logb 𝑁 ) )
60	31 43 46 59	mulge0d	⊢ ( 𝜑 → 0 ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
61		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
62		flge	⊢ ( ( ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
63	44 61 62	syl2anc	⊢ ( 𝜑 → ( 0 ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
64	60 63	mpbid	⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) )
65	45 64	jca	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
66		elnn0z	⊢ ( ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
67	65 66	sylibr	⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℕ0 )
68	11 67	eqeltrid	⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
69	68	nn0red	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
70	26 69	lenltd	⊢ ( 𝜑 → ( 𝑃 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑃 ) )
71	70	biimpar	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝑃 ) → 𝑃 ≤ 𝐴 )
72		oveq1	⊢ ( 𝑏 = 𝑃 → ( 𝑏 gcd 𝑁 ) = ( 𝑃 gcd 𝑁 ) )
73	72	eqeq1d	⊢ ( 𝑏 = 𝑃 → ( ( 𝑏 gcd 𝑁 ) = 1 ↔ ( 𝑃 gcd 𝑁 ) = 1 ) )
74	9	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝐴 ) → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
75		1zzd	⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝐴 ) → 1 ∈ ℤ )
76	11 45	eqeltrid	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
77	76	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝐴 ) → 𝐴 ∈ ℤ )
78	25	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
79	78	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝐴 ) → 𝑃 ∈ ℤ )
80	25	nnge1d	⊢ ( 𝜑 → 1 ≤ 𝑃 )
81	80	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝐴 ) → 1 ≤ 𝑃 )
82		simpr	⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝐴 ) → 𝑃 ≤ 𝐴 )
83	75 77 79 81 82	elfzd	⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝐴 ) → 𝑃 ∈ ( 1 ... 𝐴 ) )
84	73 74 83	rspcdva	⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝐴 ) → ( 𝑃 gcd 𝑁 ) = 1 )
85	84	ex	⊢ ( 𝜑 → ( 𝑃 ≤ 𝐴 → ( 𝑃 gcd 𝑁 ) = 1 ) )
86	85	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝑃 ) → ( 𝑃 ≤ 𝐴 → ( 𝑃 gcd 𝑁 ) = 1 ) )
87	71 86	mpd	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝑃 ) → ( 𝑃 gcd 𝑁 ) = 1 )
88	6	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
89		coprm	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑁 ↔ ( 𝑃 gcd 𝑁 ) = 1 ) )
90	4 88 89	syl2anc	⊢ ( 𝜑 → ( ¬ 𝑃 ∥ 𝑁 ↔ ( 𝑃 gcd 𝑁 ) = 1 ) )
91	90	con1bid	⊢ ( 𝜑 → ( ¬ ( 𝑃 gcd 𝑁 ) = 1 ↔ 𝑃 ∥ 𝑁 ) )
92	91	bicomd	⊢ ( 𝜑 → ( 𝑃 ∥ 𝑁 ↔ ¬ ( 𝑃 gcd 𝑁 ) = 1 ) )
93	92	biimpd	⊢ ( 𝜑 → ( 𝑃 ∥ 𝑁 → ¬ ( 𝑃 gcd 𝑁 ) = 1 ) )
94	7 93	mpd	⊢ ( 𝜑 → ¬ ( 𝑃 gcd 𝑁 ) = 1 )
95	94	neqned	⊢ ( 𝜑 → ( 𝑃 gcd 𝑁 ) ≠ 1 )
96	95	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝑃 ) → ( 𝑃 gcd 𝑁 ) ≠ 1 )
97	96	neneqd	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝑃 ) → ¬ ( 𝑃 gcd 𝑁 ) = 1 )
98	87 97	pm2.21dd	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝑃 ) → 𝐴 < 𝑃 )
99	23 98	pm2.61dan	⊢ ( 𝜑 → 𝐴 < 𝑃 )
100		eqid	⊢ ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
101		imaco	⊢ ( ( 𝐽 ∘ 𝐸 ) “ ( ℕ0 × ℕ0 ) ) = ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
102	101	eqcomi	⊢ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) = ( ( 𝐽 ∘ 𝐸 ) “ ( ℕ0 × ℕ0 ) )
103		resima	⊢ ( ( ( 𝐽 ∘ 𝐸 ) ↾ ( ℕ0 × ℕ0 ) ) “ ( ℕ0 × ℕ0 ) ) = ( ( 𝐽 ∘ 𝐸 ) “ ( ℕ0 × ℕ0 ) )
104	103	eqcomi	⊢ ( ( 𝐽 ∘ 𝐸 ) “ ( ℕ0 × ℕ0 ) ) = ( ( ( 𝐽 ∘ 𝐸 ) ↾ ( ℕ0 × ℕ0 ) ) “ ( ℕ0 × ℕ0 ) )
105	104	a1i	⊢ ( 𝜑 → ( ( 𝐽 ∘ 𝐸 ) “ ( ℕ0 × ℕ0 ) ) = ( ( ( 𝐽 ∘ 𝐸 ) ↾ ( ℕ0 × ℕ0 ) ) “ ( ℕ0 × ℕ0 ) ) )
106	78	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → 𝑃 ∈ ℤ )
107		xp1st	⊢ ( 𝑣 ∈ ( ℕ0 × ℕ0 ) → ( 1st ‘ 𝑣 ) ∈ ℕ0 )
108	107	adantl	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → ( 1st ‘ 𝑣 ) ∈ ℕ0 )
109	106 108	zexpcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) ∈ ℤ )
110	25	nnne0d	⊢ ( 𝜑 → 𝑃 ≠ 0 )
111		dvdsval2	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℤ ) )
112	78 110 88 111	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℤ ) )
113	7 112	mpbid	⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℤ )
114	113	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑁 / 𝑃 ) ∈ ℤ )
115		xp2nd	⊢ ( 𝑣 ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ 𝑣 ) ∈ ℕ0 )
116	115	adantl	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → ( 2nd ‘ 𝑣 ) ∈ ℕ0 )
117	114 116	zexpcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ∈ ℤ )
118	109 117	zmulcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ∈ ℤ )
119		vex	⊢ 𝑘 ∈ V
120		vex	⊢ 𝑙 ∈ V
121	119 120	op1std	⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( 1st ‘ 𝑣 ) = 𝑘 )
122	121	oveq2d	⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) = ( 𝑃 ↑ 𝑘 ) )
123	119 120	op2ndd	⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( 2nd ‘ 𝑣 ) = 𝑙 )
124	123	oveq2d	⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) )
125	122 124	oveq12d	⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) = ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
126	125	mpompt	⊢ ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ) = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
127	12 126	eqtr4i	⊢ 𝐸 = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) )
128	127	a1i	⊢ ( 𝜑 → 𝐸 = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ) )
129	20	a1i	⊢ ( 𝜑 → 𝐽 = ( 𝑗 ∈ ℤ ↦ ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
130		oveq1	⊢ ( 𝑗 = ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) → ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
131	118 128 129 130	fmptco	⊢ ( 𝜑 → ( 𝐽 ∘ 𝐸 ) = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
132	131	reseq1d	⊢ ( 𝜑 → ( ( 𝐽 ∘ 𝐸 ) ↾ ( ℕ0 × ℕ0 ) ) = ( ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) ↾ ( ℕ0 × ℕ0 ) ) )
133		ssidd	⊢ ( 𝜑 → ( ℕ0 × ℕ0 ) ⊆ ( ℕ0 × ℕ0 ) )
134	133	resmptd	⊢ ( 𝜑 → ( ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) ↾ ( ℕ0 × ℕ0 ) ) = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
135	128 118	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑣 ) = ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) )
136	135	oveq1d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
137	136	mpteq2dva	⊢ ( 𝜑 → ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
138	137	eqcomd	⊢ ( 𝜑 → ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
139		ovexd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ∈ V )
140		eqid	⊢ ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
141	139 140	fmptd	⊢ ( 𝜑 → ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) : ( ℕ0 × ℕ0 ) ⟶ V )
142		ffn	⊢ ( ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) : ( ℕ0 × ℕ0 ) ⟶ V → ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) Fn ( ℕ0 × ℕ0 ) )
143	141 142	syl	⊢ ( 𝜑 → ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) Fn ( ℕ0 × ℕ0 ) )
144		ovexd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ V )
145	144 100	fmptd	⊢ ( 𝜑 → ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) : ( ℕ0 × ℕ0 ) ⟶ V )
146		ffn	⊢ ( ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) : ( ℕ0 × ℕ0 ) ⟶ V → ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) Fn ( ℕ0 × ℕ0 ) )
147	145 146	syl	⊢ ( 𝜑 → ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) Fn ( ℕ0 × ℕ0 ) )
148		eqidd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
149		simpr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑣 = 𝑐 ) → 𝑣 = 𝑐 )
150	149	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑣 = 𝑐 ) → ( 𝐸 ‘ 𝑣 ) = ( 𝐸 ‘ 𝑐 ) )
151	150	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑣 = 𝑐 ) → ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( ( 𝐸 ‘ 𝑐 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
152		simpr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → 𝑐 ∈ ( ℕ0 × ℕ0 ) )
153		ovexd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑐 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ∈ V )
154	148 151 152 153	fvmptd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) ‘ 𝑐 ) = ( ( 𝐸 ‘ 𝑐 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
155		eqid	⊢ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 )
156	22	ssrab3	⊢ 𝑈 ⊆ ( Base ‘ ( mulGrp ‘ 𝐾 ) )
157	156	a1i	⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
158	157	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → 𝑈 ⊆ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
159	3	fldcrngd	⊢ ( 𝜑 → 𝐾 ∈ CRing )
160		eqid	⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
161	160	crngmgp	⊢ ( 𝐾 ∈ CRing → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
162	159 161	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
163	162 5 22	primrootsunit	⊢ ( 𝜑 → ( ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) = ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) ∧ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Abel ) )
164	163	simpld	⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) = ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) )
165	16 164	eleqtrd	⊢ ( 𝜑 → 𝑀 ∈ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) )
166	163	simprd	⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Abel )
167		ablcmn	⊢ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Abel → ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ CMnd )
168	166 167	syl	⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ CMnd )
169	5	nnnn0d	⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
170		eqid	⊢ ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) = ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) )
171	168 169 170	isprimroot	⊢ ( 𝜑 → ( 𝑀 ∈ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) ↔ ( 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ∀ 𝑤 ∈ ℕ0 ( ( 𝑤 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) → 𝑅 ∥ 𝑤 ) ) ) )
172	171	biimpd	⊢ ( 𝜑 → ( 𝑀 ∈ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) → ( 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ∀ 𝑤 ∈ ℕ0 ( ( 𝑤 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) → 𝑅 ∥ 𝑤 ) ) ) )
173	165 172	mpd	⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ∀ 𝑤 ∈ ℕ0 ( ( 𝑤 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) → 𝑅 ∥ 𝑤 ) ) )
174	173	simp1d	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
175		eqid	⊢ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
176	155 175	ressbas2	⊢ ( 𝑈 ⊆ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) → 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
177	157 176	syl	⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
178	174 177	eleqtrrd	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
179	178	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → 𝑀 ∈ 𝑈 )
180	6 4 7 12	aks6d1c2p1	⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ )
181	180	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑐 ) ∈ ℕ )
182	155 158 179 181	ressmulgnnd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑐 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( ( 𝐸 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
183		eqidd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
184		simpr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑗 = 𝑐 ) → 𝑗 = 𝑐 )
185	184	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑗 = 𝑐 ) → ( 𝐸 ‘ 𝑗 ) = ( 𝐸 ‘ 𝑐 ) )
186	185	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑗 = 𝑐 ) → ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( ( 𝐸 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
187		ovexd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ V )
188	183 186 152 187	fvmptd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ‘ 𝑐 ) = ( ( 𝐸 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) )
189	188	eqcomd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ‘ 𝑐 ) )
190	154 182 189	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) ‘ 𝑐 ) = ( ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) ‘ 𝑐 ) )
191	143 147 190	eqfnfvd	⊢ ( 𝜑 → ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑣 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
192	138 191	eqtrd	⊢ ( 𝜑 → ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
193	134 192	eqtrd	⊢ ( 𝜑 → ( ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) ↾ ( ℕ0 × ℕ0 ) ) = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
194	132 193	eqtrd	⊢ ( 𝜑 → ( ( 𝐽 ∘ 𝐸 ) ↾ ( ℕ0 × ℕ0 ) ) = ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
195	194	imaeq1d	⊢ ( 𝜑 → ( ( ( 𝐽 ∘ 𝐸 ) ↾ ( ℕ0 × ℕ0 ) ) “ ( ℕ0 × ℕ0 ) ) = ( ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) “ ( ℕ0 × ℕ0 ) ) )
196	105 195	eqtrd	⊢ ( 𝜑 → ( ( 𝐽 ∘ 𝐸 ) “ ( ℕ0 × ℕ0 ) ) = ( ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) “ ( ℕ0 × ℕ0 ) ) )
197	102 196	eqtrid	⊢ ( 𝜑 → ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) = ( ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) “ ( ℕ0 × ℕ0 ) ) )
198	197	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) = ( ♯ ‘ ( ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) “ ( ℕ0 × ℕ0 ) ) ) )
199	21 198	breqtrd	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ♯ ‘ ( ( 𝑗 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝐸 ‘ 𝑗 ) ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) “ ( ℕ0 × ℕ0 ) ) ) )
200	1 2 3 4 5 6 7 8 99 10 68 12 13 14 15 16 17 18 19 100 199	aks6d1c6lem3	⊢ ( 𝜑 → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ≤ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) )