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 biimpi ⊢ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) → ∀ 𝑠 ∈ ℙ ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) )
27 26 adantl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ∀ 𝑠 ∈ ℙ ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) )
28 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → 𝑃 ∈ ℙ )
29 19 27 28 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ( 𝑃 ∥ 𝑁 ↔ 𝑃 = 𝑟 ) )
30 29 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ( 𝑃 ∥ 𝑁 → 𝑃 = 𝑟 ) )
31 16 30 mpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → 𝑃 = 𝑟 )
32 31 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑃 = 𝑟 )
33 32 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑟 = 𝑃 )
34 15 33 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑞 = 𝑃 )
35 34 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑞 pCnt 𝑁 ) = ( 𝑃 pCnt 𝑁 ) )
36 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
37 6 36 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
38 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
39 3re ⊢ 3 ∈ ℝ
40 39 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
41 37 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
42 3pos ⊢ 0 < 3
43 42 a1i ⊢ ( 𝜑 → 0 < 3 )
44 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
45 6 44 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
46 38 40 41 43 45 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
47 37 46 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
48 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
49 47 48 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
50 pcelnn ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ 𝑃 ∥ 𝑁 ) )
51 4 49 50 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ 𝑃 ∥ 𝑁 ) )
52 7 51 mpbird ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
53 52 nncnd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℂ )
54 53 mulridd ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝑁 ) · 1 ) = ( 𝑃 pCnt 𝑁 ) )
55 54 eqcomd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) = ( ( 𝑃 pCnt 𝑁 ) · 1 ) )
56 1nn0 ⊢ 1 ∈ ℕ0
57 56 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
58 pcidlem ⊢ ( ( 𝑃 ∈ ℙ ∧ 1 ∈ ℕ0 ) → ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) = 1 )
59 4 57 58 syl2anc ⊢ ( 𝜑 → ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) = 1 )
60 59 eqcomd ⊢ ( 𝜑 → 1 = ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) )
61 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
62 4 61 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
63 62 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
64 63 exp1d ⊢ ( 𝜑 → ( 𝑃 ↑ 1 ) = 𝑃 )
65 64 oveq2d ⊢ ( 𝜑 → ( 𝑃 pCnt ( 𝑃 ↑ 1 ) ) = ( 𝑃 pCnt 𝑃 ) )
66 60 65 eqtrd ⊢ ( 𝜑 → 1 = ( 𝑃 pCnt 𝑃 ) )
67 66 oveq2d ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝑁 ) · 1 ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
68 55 67 eqtrd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
70 69 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
71 28 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑃 ∈ ℙ )
72 nnq ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℚ )
73 62 72 syl ⊢ ( 𝜑 → 𝑃 ∈ ℚ )
74 62 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
75 73 74 jca ⊢ ( 𝜑 → ( 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ) )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → ( 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ) )
77 76 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ) )
78 52 nnzd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
80 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
81 80 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
82 81 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
83 pcexp ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 ∈ ℚ ∧ 𝑃 ≠ 0 ) ∧ ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
84 71 77 82 83 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) )
85 84 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( ( 𝑃 pCnt 𝑁 ) · ( 𝑃 pCnt 𝑃 ) ) = ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
86 70 85 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) = ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
87 34 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → 𝑃 = 𝑞 )
88 87 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
89 86 88 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
90 35 89 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 = 𝑟 ) → ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
91 breq1 ⊢ ( 𝑠 = 𝑞 → ( 𝑠 ∥ 𝑁 ↔ 𝑞 ∥ 𝑁 ) )
92 equequ1 ⊢ ( 𝑠 = 𝑞 → ( 𝑠 = 𝑟 ↔ 𝑞 = 𝑟 ) )
93 91 92 bibi12d ⊢ ( 𝑠 = 𝑞 → ( ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) ↔ ( 𝑞 ∥ 𝑁 ↔ 𝑞 = 𝑟 ) ) )
94 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ∀ 𝑠 ∈ ℙ ( 𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟 ) )
95 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑞 ∈ ℙ )
96 93 94 95 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∥ 𝑁 ↔ 𝑞 = 𝑟 ) )
97 96 bicomd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 = 𝑟 ↔ 𝑞 ∥ 𝑁 ) )
98 97 notbid ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( ¬ 𝑞 = 𝑟 ↔ ¬ 𝑞 ∥ 𝑁 ) )
99 98 biimpa ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ¬ 𝑞 ∥ 𝑁 )
100 95 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑞 ∈ ℙ )
101 49 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → 𝑁 ∈ ℕ )
102 101 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑁 ∈ ℕ )
103 pceq0 ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑞 pCnt 𝑁 ) = 0 ↔ ¬ 𝑞 ∥ 𝑁 ) )
104 100 102 103 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( ( 𝑞 pCnt 𝑁 ) = 0 ↔ ¬ 𝑞 ∥ 𝑁 ) )
105 99 104 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 pCnt 𝑁 ) = 0 )
106 neqne ⊢ ( ¬ 𝑞 = 𝑟 → 𝑞 ≠ 𝑟 )
107 106 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑞 ≠ 𝑟 )
108 16 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑃 ∥ 𝑁 )
109 28 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑃 ∈ ℙ )
110 19 94 109 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑃 ∥ 𝑁 ↔ 𝑃 = 𝑟 ) )
111 110 biimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑃 ∥ 𝑁 → 𝑃 = 𝑟 ) )
112 108 111 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑃 = 𝑟 )
113 112 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑃 = 𝑟 )
114 113 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑟 = 𝑃 )
115 107 114 neeqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑞 ≠ 𝑃 )
116 115 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ¬ 𝑞 = 𝑃 )
117 prmuz2 ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ( ℤ≥ ‘ 2 ) )
118 117 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → 𝑞 ∈ ( ℤ≥ ‘ 2 ) )
119 118 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑞 ∈ ( ℤ≥ ‘ 2 ) )
120 28 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑃 ∈ ℙ )
121 dvdsprm ⊢ ( ( 𝑞 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑞 ∥ 𝑃 ↔ 𝑞 = 𝑃 ) )
122 119 120 121 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 ∥ 𝑃 ↔ 𝑞 = 𝑃 ) )
123 116 122 mtbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ¬ 𝑞 ∥ 𝑃 )
124 62 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑃 ∈ ℕ )
125 124 nnzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 𝑃 ∈ ℤ )
126 52 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
127 126 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
128 127 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
129 128 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
130 prmdvdsexp ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑃 ∈ ℤ ∧ ( 𝑃 pCnt 𝑁 ) ∈ ℕ ) → ( 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ↔ 𝑞 ∥ 𝑃 ) )
131 100 125 129 130 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ↔ 𝑞 ∥ 𝑃 ) )
132 123 131 mtbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ¬ 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )
133 120 102 pccld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
134 124 133 nnexpcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℕ )
135 pceq0 ⊢ ( ( 𝑞 ∈ ℙ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℕ ) → ( ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = 0 ↔ ¬ 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
136 100 134 135 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = 0 ↔ ¬ 𝑞 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
137 132 136 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = 0 )
138 137 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → 0 = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
139 105 138 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ¬ 𝑞 = 𝑟 ) → ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
140 90 139 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
141 140 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℙ ) ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) ) → ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
142 1 2 3 4 5 6 7 8 9 10 11 12 13 14 aks6d1c7lem4 ⊢ ( 𝜑 → ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 )
143 reu6 ⊢ ( ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 ↔ ∃ 𝑟 ∈ ℙ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) )
144 142 143 sylib ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℙ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟 ) )
145 141 144 r19.29a ⊢ ( 𝜑 → ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
146 49 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
147 62 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
148 4 49 pccld ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
149 147 148 nn0expcld ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℕ0 )
150 pc11 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℕ0 ) → ( 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) )
151 146 149 150 syl2anc ⊢ ( 𝜑 → ( 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝑁 ) = ( 𝑞 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) )
152 145 151 mpbird ⊢ ( 𝜑 → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )