Metamath Proof Explorer

Theorem aks5lem7

Description: Lemma for aks5. We clean up the hypotheses compared to aks5lem6 . (Contributed by metakunt, 9-Aug-2025)

Ref Expression
Hypotheses aks5lem7.1 ⊢ ( 𝜑 → ( ♯ ‘ ( Base ‘ 𝐾 ) ) ∈ ℕ )
aks5lem7.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks5lem7.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks5lem7.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks5lem7.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks5lem7.6 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks5lem7.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks5lem7.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks5lem7.9 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
aks5lem7.10 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
aks5lem7.11 ⊢ ( 𝜑 → 𝑅 ∥ ( ( ♯ ‘ ( Base ‘ 𝐾 ) ) − 1 ) )
aks5lem7.12 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
aks5lem7.13 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
aks5lem7.14 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
aks5lem7.15 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
aks5lem7.16 ⊢ 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
Assertion aks5lem7 ( 𝜑 → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 aks5lem7.1 ⊢ ( 𝜑 → ( ♯ ‘ ( Base ‘ 𝐾 ) ) ∈ ℕ )
2 aks5lem7.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks5lem7.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
4 aks5lem7.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 aks5lem7.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6 aks5lem7.6 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
7 aks5lem7.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8 aks5lem7.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9 aks5lem7.9 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
10 aks5lem7.10 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
11 aks5lem7.11 ⊢ ( 𝜑 → 𝑅 ∥ ( ( ♯ ‘ ( Base ‘ 𝐾 ) ) − 1 ) )
12 aks5lem7.12 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
13 aks5lem7.13 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
14 aks5lem7.14 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
15 aks5lem7.15 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
16 aks5lem7.16 ⊢ 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
17 eqid ⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑙 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑙 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑙 ) ) ) } = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑙 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑙 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑙 ) ) ) }
18 3 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝐾 ∈ Field )
19 4 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑃 ∈ ℙ )
20 5 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑅 ∈ ℕ )
21 6 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
22 7 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑃 ∥ 𝑁 )
23 8 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → ( 𝑁 gcd 𝑅 ) = 1 )
24 10 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
25 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
26 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝐾 ) ) = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
27 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) )
28 fldidom ⊢ ( 𝐾 ∈ Field → 𝐾 ∈ IDomn )
29 3 28 syl ⊢ ( 𝜑 → 𝐾 ∈ IDomn )
30 29 idomcringd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
31 25 2 26 27 30 4 frobrhm ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingHom 𝐾 ) )
32 3 3 31 25 25 fldhmf1 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1→ ( Base ‘ 𝐾 ) )
33 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) ∈ V )
34 eqeng ⊢ ( ( Base ‘ 𝐾 ) ∈ V → ( ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) → ( Base ‘ 𝐾 ) ≈ ( Base ‘ 𝐾 ) ) )
35 33 25 34 mpisyl ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) ≈ ( Base ‘ 𝐾 ) )
36 1 nnnn0d ⊢ ( 𝜑 → ( ♯ ‘ ( Base ‘ 𝐾 ) ) ∈ ℕ0 )
37 hashclb ⊢ ( ( Base ‘ 𝐾 ) ∈ V → ( ( Base ‘ 𝐾 ) ∈ Fin ↔ ( ♯ ‘ ( Base ‘ 𝐾 ) ) ∈ ℕ0 ) )
38 33 37 syl ⊢ ( 𝜑 → ( ( Base ‘ 𝐾 ) ∈ Fin ↔ ( ♯ ‘ ( Base ‘ 𝐾 ) ) ∈ ℕ0 ) )
39 36 38 mpbird ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) ∈ Fin )
40 f1finf1o ⊢ ( ( ( Base ‘ 𝐾 ) ≈ ( Base ‘ 𝐾 ) ∧ ( Base ‘ 𝐾 ) ∈ Fin ) → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1→ ( Base ‘ 𝐾 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) )
41 35 39 40 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1→ ( Base ‘ 𝐾 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) )
42 32 41 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
43 31 42 jca ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingHom 𝐾 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) )
44 25 25 isrim ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingHom 𝐾 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) )
45 43 44 sylibr ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
47 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
48 13 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
49 16 oveq2i ⊢ ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) = ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
50 49 oveq1i ⊢ ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) )
51 50 sneqi ⊢ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } = { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) }
52 51 fveq2i ⊢ ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } ) = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
53 15 52 eqtri ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
54 12 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
55 17 2 18 19 20 21 22 23 9 24 46 47 48 14 53 16 54 aks5lem6 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )
56 55 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) ∧ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ) → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )
57 eqid ⊢ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) = ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) )
58 3 flddrngd ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
59 eqid ⊢ ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐾 )
60 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
61 25 59 60 isdrng ⊢ ( 𝐾 ∈ DivRing ↔ ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) )
62 61 biimpi ⊢ ( 𝐾 ∈ DivRing → ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) )
63 58 62 syl ⊢ ( 𝜑 → ( 𝐾 ∈ Ring ∧ ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) )
64 63 simprd ⊢ ( 𝜑 → ( Unit ‘ 𝐾 ) = ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) )
65 64 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( Unit ‘ 𝐾 ) ) = ( ♯ ‘ ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) )
66 63 simpld ⊢ ( 𝜑 → 𝐾 ∈ Ring )
67 ringgrp ⊢ ( 𝐾 ∈ Ring → 𝐾 ∈ Grp )
68 66 67 syl ⊢ ( 𝜑 → 𝐾 ∈ Grp )
69 25 60 grpidcl ⊢ ( 𝐾 ∈ Grp → ( 0g ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
70 68 69 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
71 hashdifsn ⊢ ( ( ( Base ‘ 𝐾 ) ∈ Fin ∧ ( 0g ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( ♯ ‘ ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) = ( ( ♯ ‘ ( Base ‘ 𝐾 ) ) − 1 ) )
72 39 70 71 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( Base ‘ 𝐾 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) = ( ( ♯ ‘ ( Base ‘ 𝐾 ) ) − 1 ) )
73 65 72 eqtr2d ⊢ ( 𝜑 → ( ( ♯ ‘ ( Base ‘ 𝐾 ) ) − 1 ) = ( ♯ ‘ ( Unit ‘ 𝐾 ) ) )
74 eqid ⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
75 74 25 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
76 75 eqcomi ⊢ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) = ( Base ‘ 𝐾 )
77 76 59 unitss ⊢ ( Unit ‘ 𝐾 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝐾 ) )
78 77 a1i ⊢ ( 𝜑 → ( Unit ‘ 𝐾 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
79 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
80 57 79 ressbas2 ⊢ ( ( Unit ‘ 𝐾 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) → ( Unit ‘ 𝐾 ) = ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) )
81 78 80 syl ⊢ ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) )
82 81 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( Unit ‘ 𝐾 ) ) = ( ♯ ‘ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) ) )
83 73 82 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ ( Base ‘ 𝐾 ) ) − 1 ) = ( ♯ ‘ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) ) )
84 11 83 breqtrd ⊢ ( 𝜑 → 𝑅 ∥ ( ♯ ‘ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s ( Unit ‘ 𝐾 ) ) ) ) )
85 57 29 39 5 84 unitscyglem5 ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ≠ ∅ )
86 n0rex ⊢ ( ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ≠ ∅ → ∃ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
87 85 86 syl ⊢ ( 𝜑 → ∃ 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) 𝑚 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
88 56 87 r19.29a ⊢ ( 𝜑 → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )