Metamath Proof Explorer

Theorem aks6d1c7

Description: N is a prime power if the hypotheses of the AKS algorithm hold. Claim 7 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf . (Contributed by metakunt, 16-May-2025)

Ref Expression
Hypotheses aks6d1c7.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks6d1c7.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c7.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c7.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c7.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c7.6 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks6d1c7.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c7.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c7.9 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
aks6d1c7.10 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
aks6d1c7.11 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
aks6d1c7.12 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
aks6d1c7.13 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
aks6d1c7.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
Assertion aks6d1c7 ( 𝜑 → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c7.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2 aks6d1c7.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks6d1c7.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
4 aks6d1c7.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 aks6d1c7.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6 aks6d1c7.6 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
7 aks6d1c7.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8 aks6d1c7.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9 aks6d1c7.9 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
10 aks6d1c7.10 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
11 aks6d1c7.11 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
12 aks6d1c7.12 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
13 aks6d1c7.13 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
14 aks6d1c7.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
15 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑞 = 𝑟 )
16 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → 𝑃 ∥ 𝑁 )
17 breq1 ⊢ ( 𝑠 = 𝑃 → ( 𝑠 ∥ 𝑁 ↔ 𝑃 ∥ 𝑁 ) )
18 eqeq1 ⊢ ( 𝑠 = 𝑃 → ( 𝑠 = 𝑟 ↔ 𝑃 = 𝑟 ) )
19 17 18 bibi12d ⊢ ( 𝑠 = 𝑃 → ( ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) ↔ ( 𝑃 ∥ 𝑁 ↔ 𝑃 = 𝑟 ) ) )
20 nfv ⊢ Ⅎ 𝑠 ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 )
21 nfv ⊢ Ⅎ 𝑝 ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 )
22 breq1 ⊢ ( 𝑝 = 𝑠 → ( 𝑝 ∥ 𝑁 ↔ 𝑠 ∥ 𝑁 ) )
23 equequ1 ⊢ ( 𝑝 = 𝑠 → ( 𝑝 = 𝑟 ↔ 𝑠 = 𝑟 ) )
24 22 23 bibi12d ⊢ ( 𝑝 = 𝑠 → ( ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ↔ ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) ) )
25 20 21 24 cbvralw ⊢ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ↔ ∀ 𝑠 ∈ ℙ ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) )
26 25 bilani ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ∀ 𝑠 ∈ ℙ ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) )
27 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → 𝑃 ∈ ℙ )
28 19 26 27 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ( 𝑃 ∥ 𝑁 ↔ 𝑃 = 𝑟 ) )
29 28 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ( 𝑃 ∥ 𝑁 → 𝑃 = 𝑟 ) )
30 16 29 mpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → 𝑃 = 𝑟 )
31 30 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑃 = 𝑟 )
32 31 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑟 = 𝑃 )
33 15 32 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑞 = 𝑃 )
34 33 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑞 pCnt 𝑁 ) = ( 𝑃 pCnt 𝑁 ) )
35 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
36 6 35 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
37 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
38 3re ⊢ 3 ∈ ℝ
39 38 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
40 36 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
41 3pos ⊢ 0 < 3
42 41 a1i ⊢ ( 𝜑 → 0 < 3 )
43 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
44 6 43 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
45 37 39 40 42 44 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
46 36 45 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
47 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
48 46 47 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
49 pcelnn ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ 𝑃 ∥ 𝑁 ) )
50 4 48 49 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ 𝑃 ∥ 𝑁 ) )
51 7 50 mpbird ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
52 51 nncnd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℂ )
53 52 mulridd ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝑁 ) · 1 ) = ( 𝑃 pCnt 𝑁 ) )
54 53 eqcomd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) = ( ( 𝑃 pCnt 𝑁 ) · 1 ) )
55 1nn0 ⊢ 1 ∈ ℕ0
56 55 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
57 pcidlem ⊢ ( ( 𝑃 ∈ ℙ ∧ 1 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) = 1 )
58 4 56 57 syl2anc ⊢ ( 𝜑 → ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) = 1 )
59 58 eqcomd ⊢ ( 𝜑 → 1 = ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) )
60 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
61 4 60 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
62 61 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
63 62 exp1d ⊢ ( 𝜑 → ( 𝑃 ↑ 1 ) = 𝑃 )
64 63 oveq2d ⊢ ( 𝜑 → ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) = ( 𝑃 pCnt 𝑃 ) )
65 59 64 eqtrd ⊢ ( 𝜑 → 1 = ( 𝑃 pCnt 𝑃 ) )
66 65 oveq2d ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝑁 ) · 1 ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
67 54 66 eqtrd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
69 68 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
70 27 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑃 ∈ ℙ )
71 nnq ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℚ )
72 61 71 syl ⊢ ( 𝜑 → 𝑃 ∈ ℚ )
73 61 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
74 72 73 jca ⊢ ( 𝜑 → ( 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → ( 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ) )
76 75 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ) )
77 51 nnzd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
79 78 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
80 79 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
81 80 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
82 pcexp ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ) ∧ ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
83 70 76 81 82 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
84 83 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) = ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
85 69 84 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) = ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
86 33 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑃 = 𝑞 )
87 86 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
88 85 87 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
89 34 88 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
90 breq1 ⊢ ( 𝑠 = 𝑞 → ( 𝑠 ∥ 𝑁 ↔ 𝑞 ∥ 𝑁 ) )
91 equequ1 ⊢ ( 𝑠 = 𝑞 → ( 𝑠 = 𝑟 ↔ 𝑞 = 𝑟 ) )
92 90 91 bibi12d ⊢ ( 𝑠 = 𝑞 → ( ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) ↔ ( 𝑞 ∥ 𝑁 ↔ 𝑞 = 𝑟 ) ) )
93 26 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ∀ 𝑠 ∈ ℙ ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) )
94 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑞 ∈ ℙ )
95 92 93 94 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∥ 𝑁 ↔ 𝑞 = 𝑟 ) )
96 95 bicomd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 = 𝑟 ↔ 𝑞 ∥ 𝑁 ) )
97 96 notbid ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( ¬ 𝑞 = 𝑟 ↔ ¬ 𝑞 ∥ 𝑁 ) )
98 97 biimpa ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ¬ 𝑞 ∥ 𝑁 )
99 94 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑞 ∈ ℙ )
100 48 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → 𝑁 ∈ ℕ )
101 100 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑁 ∈ ℕ )
102 pceq0 ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑞 pCnt 𝑁 ) = 0 ↔ ¬ 𝑞 ∥ 𝑁 ) )
103 99 101 102 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( ( 𝑞 pCnt 𝑁 ) = 0 ↔ ¬ 𝑞 ∥ 𝑁 ) )
104 98 103 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 pCnt 𝑁 ) = 0 )
105 neqne ⊢ ( ¬ 𝑞 = 𝑟 → 𝑞 ≠ 𝑟 )
106 105 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑞 ≠ 𝑟 )
107 16 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑃 ∥ 𝑁 )
108 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑃 ∈ ℙ )
109 19 93 108 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑃 ∥ 𝑁 ↔ 𝑃 = 𝑟 ) )
110 109 biimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑃 ∥ 𝑁 → 𝑃 = 𝑟 ) )
111 107 110 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑃 = 𝑟 )
112 111 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑃 = 𝑟 )
113 112 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑟 = 𝑃 )
114 106 113 neeqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑞 ≠ 𝑃 )
115 114 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ¬ 𝑞 = 𝑃 )
116 prmuz2 ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ( ℤ≥ ‘ 2 ) )
117 116 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑞 ∈ ( ℤ≥ ‘ 2 ) )
118 117 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑞 ∈ ( ℤ≥ ‘ 2 ) )
119 27 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑃 ∈ ℙ )
120 dvdsprm ⊢ ( ( 𝑞 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑞 ∥ 𝑃 ↔ 𝑞 = 𝑃 ) )
121 118 119 120 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 ∥ 𝑃 ↔ 𝑞 = 𝑃 ) )
122 115 121 mtbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ¬ 𝑞 ∥ 𝑃 )
123 61 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑃 ∈ ℕ )
124 123 nnzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑃 ∈ ℤ )
125 51 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
126 125 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
127 126 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
128 127 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
129 prmdvdsexp ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑃 ∈ ℤ ∧ ( 𝑃 pCnt 𝑁 ) ∈ ℕ ) → ( 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ↔ 𝑞 ∥ 𝑃 ) )
130 99 124 128 129 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ↔ 𝑞 ∥ 𝑃 ) )
131 122 130 mtbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ¬ 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )
132 119 101 pccld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
133 123 132 nnexpcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℕ )
134 pceq0 ⊢ ( ( 𝑞 ∈ ℙ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℕ ) → ( ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = 0 ↔ ¬ 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
135 99 133 134 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = 0 ↔ ¬ 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
136 131 135 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = 0 )
137 136 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 0 = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
138 104 137 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
139 89 138 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
140 139 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
141 1 2 3 4 5 6 7 8 9 10 11 12 13 14 aks6d1c7lem4 ⊢ ( 𝜑 → ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 )
142 reu6 ⊢ ( ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 ↔ ∃ 𝑟 ∈ ℙ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) )
143 141 142 sylib ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℙ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) )
144 140 143 r19.29a ⊢ ( 𝜑 → ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
145 48 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
146 61 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
147 4 48 pccld ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
148 146 147 nn0expcld ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℕ0 )
149 pc11 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℕ0 ) → ( 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) )
150 145 148 149 syl2anc ⊢ ( 𝜑 → ( 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) )
151 144 150 mpbird ⊢ ( 𝜑 → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )