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 K ∈ ℕ
aks5lem7.2 ⊢ P = chr ⁡ K
aks5lem7.3 ⊢ φ → K ∈ Field
aks5lem7.4 ⊢ φ → P ∈ ℙ
aks5lem7.5 ⊢ φ → R ∈ ℕ
aks5lem7.6 ⊢ φ → N ∈ ℤ ≥ 3
aks5lem7.7 ⊢ φ → P ∥ N
aks5lem7.8 ⊢ φ → N gcd R = 1
aks5lem7.9 ⊢ A = ϕ ⁡ R ⁢ log 2 N
aks5lem7.10 ⊢ φ → log 2 N 2 < odℤ ⁡ R ⁡ N
aks5lem7.11 ⊢ φ → R ∥ Base K − 1
aks5lem7.12 ⊢ φ → ∀ a ∈ 1 … A N ⋅ mulGrp S X + S ℤRHom ⁡ S ⁡ a S ~ QG L = N ⋅ mulGrp S X + S ℤRHom ⁡ S ⁡ a S ~ QG L
aks5lem7.13 ⊢ φ → ∀ b ∈ 1 … A b gcd N = 1
aks5lem7.14 ⊢ S = Poly 1 ⁡ ℤ/Nℤ
aks5lem7.15 ⊢ L = RSpan ⁡ S ⁡ R ⋅ mulGrp S X - S 1 S
aks5lem7.16 ⊢ X = var 1 ⁡ ℤ/Nℤ
Assertion aks5lem7 ⊢ φ → N = P P pCnt N

Proof

Step Hyp Ref Expression
1 aks5lem7.1 ⊢ φ → Base K ∈ ℕ
2 aks5lem7.2 ⊢ P = chr ⁡ K
3 aks5lem7.3 ⊢ φ → K ∈ Field
4 aks5lem7.4 ⊢ φ → P ∈ ℙ
5 aks5lem7.5 ⊢ φ → R ∈ ℕ
6 aks5lem7.6 ⊢ φ → N ∈ ℤ ≥ 3
7 aks5lem7.7 ⊢ φ → P ∥ N
8 aks5lem7.8 ⊢ φ → N gcd R = 1
9 aks5lem7.9 ⊢ A = ϕ ⁡ R ⁢ log 2 N
10 aks5lem7.10 ⊢ φ → log 2 N 2 < odℤ ⁡ R ⁡ N
11 aks5lem7.11 ⊢ φ → R ∥ Base K − 1
12 aks5lem7.12 ⊢ φ → ∀ a ∈ 1 … A N ⋅ mulGrp S X + S ℤRHom ⁡ S ⁡ a S ~ QG L = N ⋅ mulGrp S X + S ℤRHom ⁡ S ⁡ a S ~ QG L
13 aks5lem7.13 ⊢ φ → ∀ b ∈ 1 … A b gcd N = 1
14 aks5lem7.14 ⊢ S = Poly 1 ⁡ ℤ/Nℤ
15 aks5lem7.15 ⊢ L = RSpan ⁡ S ⁡ R ⋅ mulGrp S X - S 1 S
16 aks5lem7.16 ⊢ X = var 1 ⁡ ℤ/Nℤ
17 eqid ⊢ e f | e ∈ ℕ ∧ f ∈ Base Poly 1 ⁡ K ∧ ∀ l ∈ mulGrp K PrimRoots R e ⋅ mulGrp K eval 1 ⁡ K ⁡ f ⁡ l = eval 1 ⁡ K ⁡ f ⁡ e ⋅ mulGrp K l = e f | e ∈ ℕ ∧ f ∈ Base Poly 1 ⁡ K ∧ ∀ l ∈ mulGrp K PrimRoots R e ⋅ mulGrp K eval 1 ⁡ K ⁡ f ⁡ l = eval 1 ⁡ K ⁡ f ⁡ e ⋅ mulGrp K l
18 3 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → K ∈ Field
19 4 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → P ∈ ℙ
20 5 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → R ∈ ℕ
21 6 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → N ∈ ℤ ≥ 3
22 7 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → P ∥ N
23 8 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → N gcd R = 1
24 10 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → log 2 N 2 < odℤ ⁡ R ⁡ N
25 eqid ⊢ Base K = Base K
26 eqid ⊢ ⋅ mulGrp K = ⋅ mulGrp K
27 eqid ⊢ x ∈ Base K ⟼ P ⋅ mulGrp K x = x ∈ Base K ⟼ P ⋅ mulGrp K x
28 fldidom ⊢ K ∈ Field → K ∈ IDomn
29 3 28 syl ⊢ φ → K ∈ IDomn
30 29 idomcringd ⊢ φ → K ∈ CRing
31 25 2 26 27 30 4 frobrhm ⊢ φ → x ∈ Base K ⟼ P ⋅ mulGrp K x ∈ K RingHom K
32 3 3 31 25 25 fldhmf1 ⊢ φ → x ∈ Base K ⟼ P ⋅ mulGrp K x : Base K ⟶ 1-1 Base K
33 fvexd ⊢ φ → Base K ∈ V
34 eqeng ⊢ Base K ∈ V → Base K = Base K → Base K ≈ Base K
35 33 25 34 mpisyl ⊢ φ → Base K ≈ Base K
36 1 nnnn0d ⊢ φ → Base K ∈ ℕ 0
37 hashclb ⊢ Base K ∈ V → Base K ∈ Fin ↔ Base K ∈ ℕ 0
38 33 37 syl ⊢ φ → Base K ∈ Fin ↔ Base K ∈ ℕ 0
39 36 38 mpbird ⊢ φ → Base K ∈ Fin
40 f1finf1o ⊢ Base K ≈ Base K ∧ Base K ∈ Fin → x ∈ Base K ⟼ P ⋅ mulGrp K x : Base K ⟶ 1-1 Base K ↔ x ∈ Base K ⟼ P ⋅ mulGrp K x : Base K ⟶ 1-1 onto Base K
41 35 39 40 syl2anc ⊢ φ → x ∈ Base K ⟼ P ⋅ mulGrp K x : Base K ⟶ 1-1 Base K ↔ x ∈ Base K ⟼ P ⋅ mulGrp K x : Base K ⟶ 1-1 onto Base K
42 32 41 mpbid ⊢ φ → x ∈ Base K ⟼ P ⋅ mulGrp K x : Base K ⟶ 1-1 onto Base K
43 31 42 jca ⊢ φ → x ∈ Base K ⟼ P ⋅ mulGrp K x ∈ K RingHom K ∧ x ∈ Base K ⟼ P ⋅ mulGrp K x : Base K ⟶ 1-1 onto Base K
44 25 25 isrim ⊢ x ∈ Base K ⟼ P ⋅ mulGrp K x ∈ K RingIso K ↔ x ∈ Base K ⟼ P ⋅ mulGrp K x ∈ K RingHom K ∧ x ∈ Base K ⟼ P ⋅ mulGrp K x : Base K ⟶ 1-1 onto Base K
45 43 44 sylibr ⊢ φ → x ∈ Base K ⟼ P ⋅ mulGrp K x ∈ K RingIso K
46 45 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → x ∈ Base K ⟼ P ⋅ mulGrp K x ∈ K RingIso K
47 simpr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → m ∈ mulGrp K PrimRoots R
48 13 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → ∀ b ∈ 1 … A b gcd N = 1
49 16 oveq2i ⊢ R ⋅ mulGrp S X = R ⋅ mulGrp S var 1 ⁡ ℤ/Nℤ
50 49 oveq1i ⊢ R ⋅ mulGrp S X - S 1 S = R ⋅ mulGrp S var 1 ⁡ ℤ/Nℤ - S 1 S
51 50 sneqi ⊢ R ⋅ mulGrp S X - S 1 S = R ⋅ mulGrp S var 1 ⁡ ℤ/Nℤ - S 1 S
52 51 fveq2i ⊢ RSpan ⁡ S ⁡ R ⋅ mulGrp S X - S 1 S = RSpan ⁡ S ⁡ R ⋅ mulGrp S var 1 ⁡ ℤ/Nℤ - S 1 S
53 15 52 eqtri ⊢ L = RSpan ⁡ S ⁡ R ⋅ mulGrp S var 1 ⁡ ℤ/Nℤ - S 1 S
54 12 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → ∀ a ∈ 1 … A N ⋅ mulGrp S X + S ℤRHom ⁡ S ⁡ a S ~ QG L = N ⋅ mulGrp S X + S ℤRHom ⁡ S ⁡ a S ~ QG L
55 17 2 18 19 20 21 22 23 9 24 46 47 48 14 53 16 54 aks5lem6 ⊢ φ ∧ m ∈ mulGrp K PrimRoots R → N = P P pCnt N
56 55 adantr ⊢ φ ∧ m ∈ mulGrp K PrimRoots R ∧ m ∈ mulGrp K PrimRoots R → N = P P pCnt N
57 eqid ⊢ mulGrp K ↾ 𝑠 Unit ⁡ K = mulGrp K ↾ 𝑠 Unit ⁡ K
58 3 flddrngd ⊢ φ → K ∈ DivRing
59 eqid ⊢ Unit ⁡ K = Unit ⁡ K
60 eqid ⊢ 0 K = 0 K
61 25 59 60 isdrng ⊢ K ∈ DivRing ↔ K ∈ Ring ∧ Unit ⁡ K = Base K ∖ 0 K
62 61 biimpi ⊢ K ∈ DivRing → K ∈ Ring ∧ Unit ⁡ K = Base K ∖ 0 K
63 58 62 syl ⊢ φ → K ∈ Ring ∧ Unit ⁡ K = Base K ∖ 0 K
64 63 simprd ⊢ φ → Unit ⁡ K = Base K ∖ 0 K
65 64 fveq2d ⊢ φ → Unit ⁡ K = Base K ∖ 0 K
66 63 simpld ⊢ φ → K ∈ Ring
67 ringgrp ⊢ K ∈ Ring → K ∈ Grp
68 66 67 syl ⊢ φ → K ∈ Grp
69 25 60 grpidcl ⊢ K ∈ Grp → 0 K ∈ Base K
70 68 69 syl ⊢ φ → 0 K ∈ Base K
71 hashdifsn ⊢ Base K ∈ Fin ∧ 0 K ∈ Base K → Base K ∖ 0 K = Base K − 1
72 39 70 71 syl2anc ⊢ φ → Base K ∖ 0 K = Base K − 1
73 65 72 eqtr2d ⊢ φ → Base K − 1 = Unit ⁡ K
74 eqid ⊢ mulGrp K = mulGrp K
75 74 25 mgpbas ⊢ Base K = Base mulGrp K
76 75 eqcomi ⊢ Base mulGrp K = Base K
77 76 59 unitss ⊢ Unit ⁡ K ⊆ Base mulGrp K
78 77 a1i ⊢ φ → Unit ⁡ K ⊆ Base mulGrp K
79 eqid ⊢ Base mulGrp K = Base mulGrp K
80 57 79 ressbas2 ⊢ Unit ⁡ K ⊆ Base mulGrp K → Unit ⁡ K = Base mulGrp K ↾ 𝑠 Unit ⁡ K
81 78 80 syl ⊢ φ → Unit ⁡ K = Base mulGrp K ↾ 𝑠 Unit ⁡ K
82 81 fveq2d ⊢ φ → Unit ⁡ K = Base mulGrp K ↾ 𝑠 Unit ⁡ K
83 73 82 eqtrd ⊢ φ → Base K − 1 = Base mulGrp K ↾ 𝑠 Unit ⁡ K
84 11 83 breqtrd ⊢ φ → R ∥ Base mulGrp K ↾ 𝑠 Unit ⁡ K
85 57 29 39 5 84 unitscyglem5 ⊢ φ → mulGrp K PrimRoots R ≠ ∅
86 n0rex ⊢ mulGrp K PrimRoots R ≠ ∅ → ∃ m ∈ mulGrp K PrimRoots R m ∈ mulGrp K PrimRoots R
87 85 86 syl ⊢ φ → ∃ m ∈ mulGrp K PrimRoots R m ∈ mulGrp K PrimRoots R
88 56 87 r19.29a ⊢ φ → N = P P pCnt N