Metamath Proof Explorer

Theorem aks6d1c7lem2

Description: Contradiction to Claim 2 and Claim 7. We assumed in Claim 2 that there are two different prime numbers P and Q . (Contributed by metakunt, 16-May-2025)

Ref Expression
Hypotheses aks6d1c7lem2.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks6d1c7lem2.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c7lem2.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c7lem2.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c7lem2.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c7lem2.6 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks6d1c7lem2.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c7lem2.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c7lem2.9 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
aks6d1c7lem2.10 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
aks6d1c7lem2.11 ⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
aks6d1c7lem2.12 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
aks6d1c7lem2.13 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
aks6d1c7lem2.14 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
aks6d1c7lem2.15 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
aks6d1c7lem2.16 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
aks6d1c7lem2.17 ⊢ 𝐵 = ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
aks6d1c7lem2.18 ⊢ 𝐶 = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) )
aks6d1c7lem2.19 ⊢ ( 𝜑 → ( 𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁 ) )
aks6d1c7lem2.20 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
aks6d1c7lem2.21 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c7lem2.22 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
aks6d1c7lem2.23 ⊢ 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) }
Assertion aks6d1c7lem2 ( 𝜑 → 𝑃 = 𝑄 )

Proof

Step Hyp Ref Expression
1 aks6d1c7lem2.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2 aks6d1c7lem2.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks6d1c7lem2.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
4 aks6d1c7lem2.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 aks6d1c7lem2.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6 aks6d1c7lem2.6 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
7 aks6d1c7lem2.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8 aks6d1c7lem2.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9 aks6d1c7lem2.9 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
10 aks6d1c7lem2.10 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
11 aks6d1c7lem2.11 ⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
12 aks6d1c7lem2.12 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
13 aks6d1c7lem2.13 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
14 aks6d1c7lem2.14 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
15 aks6d1c7lem2.15 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
16 aks6d1c7lem2.16 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
17 aks6d1c7lem2.17 ⊢ 𝐵 = ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
18 aks6d1c7lem2.18 ⊢ 𝐶 = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) )
19 aks6d1c7lem2.19 ⊢ ( 𝜑 → ( 𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁 ) )
20 aks6d1c7lem2.20 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
21 aks6d1c7lem2.21 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
22 aks6d1c7lem2.22 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
23 aks6d1c7lem2.23 ⊢ 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) }
24 simpr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → 𝑃 = 𝑄 )
25 3 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝐾 ∈ Field )
26 4 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ ℙ )
27 5 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑅 ∈ ℕ )
28 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
29 6 28 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
30 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
31 3re ⊢ 3 ∈ ℝ
32 31 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
33 29 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
34 3pos ⊢ 0 < 3
35 34 a1i ⊢ ( 𝜑 → 0 < 3 )
36 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
37 6 36 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
38 30 32 33 35 37 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
39 29 38 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
40 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
41 39 40 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑁 ∈ ℕ )
43 7 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∥ 𝑁 )
44 8 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝑁 gcd 𝑅 ) = 1 )
45 5 phicld ⊢ ( 𝜑 → ( ϕ ‘ 𝑅 ) ∈ ℕ )
46 45 nnred ⊢ ( 𝜑 → ( ϕ ‘ 𝑅 ) ∈ ℝ )
47 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
48 0le1 ⊢ 0 ≤ 1
49 48 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
50 45 nnge1d ⊢ ( 𝜑 → 1 ≤ ( ϕ ‘ 𝑅 ) )
51 30 47 46 49 50 letrd ⊢ ( 𝜑 → 0 ≤ ( ϕ ‘ 𝑅 ) )
52 46 51 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ϕ ‘ 𝑅 ) ) ∈ ℝ )
53 2re ⊢ 2 ∈ ℝ
54 53 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
55 2pos ⊢ 0 < 2
56 55 a1i ⊢ ( 𝜑 → 0 < 2 )
57 1lt2 ⊢ 1 < 2
58 57 a1i ⊢ ( 𝜑 → 1 < 2 )
59 47 58 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
60 59 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
61 54 56 33 38 60 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
62 52 61 remulcld ⊢ ( 𝜑 → ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ )
63 62 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ )
64 46 51 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ ( ϕ ‘ 𝑅 ) ) )
65 54 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
66 30 56 gtned ⊢ ( 𝜑 → 2 ≠ 0 )
67 logb1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 1 ) = 0 )
68 65 66 60 67 syl3anc ⊢ ( 𝜑 → ( 2 logb 1 ) = 0 )
69 68 eqcomd ⊢ ( 𝜑 → 0 = ( 2 logb 1 ) )
70 2z ⊢ 2 ∈ ℤ
71 70 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
72 54 leidd ⊢ ( 𝜑 → 2 ≤ 2 )
73 0lt1 ⊢ 0 < 1
74 73 a1i ⊢ ( 𝜑 → 0 < 1 )
75 41 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑁 )
76 71 72 47 74 33 38 75 logblebd ⊢ ( 𝜑 → ( 2 logb 1 ) ≤ ( 2 logb 𝑁 ) )
77 69 76 eqbrtrd ⊢ ( 𝜑 → 0 ≤ ( 2 logb 𝑁 ) )
78 52 61 64 77 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
79 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
80 flge ⊢ ( ( ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
81 62 79 80 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
82 78 81 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) )
83 63 82 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
84 elnn0z ⊢ ( ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
85 83 84 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℕ0 )
86 12 85 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝐴 ∈ ℕ0 )
88 22 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
89 14 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
90 15 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
91 19 simpld ⊢ ( 𝜑 → 𝑄 ∈ ℙ )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ ℙ )
93 19 simprd ⊢ ( 𝜑 → 𝑄 ∥ 𝑁 )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∥ 𝑁 )
95 simpr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ≠ 𝑄 )
96 92 94 95 3jca ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁 ∧ 𝑃 ≠ 𝑄 ) )
97 1 2 25 26 27 42 43 44 21 87 9 10 88 89 90 16 17 18 96 aks6d1c2 ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) )
98 41 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
99 eqid ⊢ ( ℤ/nℤ ‘ 𝑅 ) = ( ℤ/nℤ ‘ 𝑅 )
100 41 4 7 5 8 9 10 99 hashscontpowcl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )
101 100 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ )
102 100 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
103 101 102 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ )
104 103 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℤ )
105 101 102 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
106 flge ⊢ ( ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↔ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
107 103 79 106 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↔ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
108 105 107 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
109 104 108 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
110 elnn0z ⊢ ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
111 109 110 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℕ0 )
112 17 111 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
113 98 112 zexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐵 ) ∈ ℤ )
114 113 zred ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐵 ) ∈ ℝ )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝑁 ↑ 𝐵 ) ∈ ℝ )
116 115 rexrd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝑁 ↑ 𝐵 ) ∈ ℝ* )
117 100 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )
118 11 117 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝐷 ∈ ℕ0 )
119 118 87 nn0addcld ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝐷 + 𝐴 ) ∈ ℕ0 )
120 118 nn0zd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝐷 ∈ ℤ )
121 1zzd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 1 ∈ ℤ )
122 120 121 zsubcld ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝐷 − 1 ) ∈ ℤ )
123 bccl ⊢ ( ( ( 𝐷 + 𝐴 ) ∈ ℕ0 ∧ ( 𝐷 − 1 ) ∈ ℤ ) → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ∈ ℕ0 )
124 119 122 123 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ∈ ℕ0 )
125 124 nn0red ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ∈ ℝ )
126 125 rexrd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ∈ ℝ* )
127 ovexd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∈ V )
128 127 mptexd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) ) ∈ V )
129 16 128 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝐻 ∈ V )
130 129 imaexd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∈ V )
131 hashxrcl ⊢ ( ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∈ V → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ∈ ℝ* )
132 130 131 syl ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ∈ ℝ* )
133 eqcom ⊢ ( 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ↔ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) = 𝐷 )
134 11 133 mpbi ⊢ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) = 𝐷
135 134 fveq2i ⊢ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) = ( √ ‘ 𝐷 )
136 135 fveq2i ⊢ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ⌊ ‘ ( √ ‘ 𝐷 ) )
137 17 136 eqtri ⊢ 𝐵 = ( ⌊ ‘ ( √ ‘ 𝐷 ) )
138 137 a1i ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝐵 = ( ⌊ ‘ ( √ ‘ 𝐷 ) ) )
139 138 oveq2d ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝑁 ↑ 𝐵 ) = ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) )
140 6 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
141 13 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
142 26 27 140 43 44 9 10 11 12 141 aks6d1c7lem1 ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) )
143 139 142 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝑁 ↑ 𝐵 ) < ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) )
144 20 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
145 eqid ⊢ ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) = ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) )
146 eqid ⊢ { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } = { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) }
147 nfcv ⊢ Ⅎ 𝑏 ∪ ( ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ ℎ )
148 nfcv ⊢ Ⅎ ℎ ∪ ( ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ 𝑏 )
149 imaeq2 ⊢ ( ℎ = 𝑏 → ( ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ ℎ ) = ( ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ 𝑏 ) )
150 149 unieqd ⊢ ( ℎ = 𝑏 → ∪ ( ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ ℎ ) = ∪ ( ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ 𝑏 ) )
151 147 148 150 cbvmpt ⊢ ( ℎ ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ↾s ran ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) ) ) } ) ) ) ) ↦ ∪ ( ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ ℎ ) ) = ( 𝑏 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ↾s ran ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) ) ) } ) ) ) ) ↦ ∪ ( ( 𝑐 ∈ ℤ ↦ ( 𝑐 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s { 𝑗 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑚 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑗 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) } ) ) 𝑀 ) ) “ 𝑏 ) )
152 1 2 25 26 27 42 43 44 144 21 12 9 10 88 89 90 16 11 23 145 146 151 aks6d1c6lem5 ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ≤ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) )
153 116 126 132 143 152 xrltletrd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( 𝑁 ↑ 𝐵 ) < ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) )
154 xrltnle ⊢ ( ( ( 𝑁 ↑ 𝐵 ) ∈ ℝ* ∧ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ∈ ℝ* ) → ( ( 𝑁 ↑ 𝐵 ) < ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ↔ ¬ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) ) )
155 116 132 154 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑁 ↑ 𝐵 ) < ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ↔ ¬ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) ) )
156 153 155 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → ¬ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) )
157 97 156 pm2.21dd ⊢ ( ( 𝜑 ∧ 𝑃 ≠ 𝑄 ) → 𝑃 = 𝑄 )
158 24 157 pm2.61dane ⊢ ( 𝜑 → 𝑃 = 𝑄 )