Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aks6d1c2 Structured version   Visualization version   GIF version

Theorem aks6d1c2 42112
Description: Claim 2 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 2-May-2025.)
Hypotheses
Ref Expression
aks6d1c2a.1 = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1𝐾)‘𝑓)‘𝑦)) = (((eval1𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))}
aks6d1c2a.2 𝑃 = (chr‘𝐾)
aks6d1c2a.3 (𝜑𝐾 ∈ Field)
aks6d1c2a.4 (𝜑𝑃 ∈ ℙ)
aks6d1c2a.5 (𝜑𝑅 ∈ ℕ)
aks6d1c2a.6 (𝜑𝑁 ∈ ℕ)
aks6d1c2a.7 (𝜑𝑃𝑁)
aks6d1c2a.8 (𝜑 → (𝑁 gcd 𝑅) = 1)
aks6d1c2a.10 𝐺 = (𝑔 ∈ (ℕ0m (0...𝐴)) ↦ ((mulGrp‘(Poly1𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔𝑖)(.g‘(mulGrp‘(Poly1𝐾)))((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
aks6d1c2a.11 (𝜑𝐴 ∈ ℕ0)
aks6d1c2a.12 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))
aks6d1c2a.13 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))
aks6d1c2a.14 (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
aks6d1c2a.15 (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
aks6d1c2a.16 (𝜑𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
aks6d1c2a.17 𝐻 = ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀))
aks6d1c2a.18 𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))
aks6d1c2a.19 𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵)))
aks6d1c2a.20 (𝜑 → (𝑄 ∈ ℙ ∧ 𝑄𝑁𝑃𝑄))
Assertion
Ref Expression
aks6d1c2 (𝜑 → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
Distinct variable groups:   ,𝑎   𝐴,𝑎   𝐴,𝑔,𝑖   𝐴,   𝐴,𝑘,𝑙   𝑥,𝐴   𝐵,𝑎   𝐵,𝑔,𝑖   𝐵,𝑘,𝑙   𝑥,𝐵   𝐶,𝑎   𝐶,𝑔,𝑖   𝐶,   𝐶,𝑘,𝑙   𝑥,𝐶   𝐸,𝑎   𝑔,𝐸,𝑖   𝑘,𝐸,𝑙   𝑥,𝐸   𝑒,𝐺,𝑓,𝑦   ,𝐺   𝐾,𝑎   𝑒,𝐾,𝑓,𝑦   𝑔,𝐾,𝑖   ,𝐾   𝑥,𝐾   ,𝑀   𝑦,𝑀   𝑁,𝑎   𝑒,𝑁,𝑓,𝑦   𝑘,𝑁,𝑙   𝑥,𝑁   𝑃,𝑒,𝑓,𝑦   𝑃,𝑘,𝑙   𝑥,𝑃   𝑅,𝑎   𝑅,𝑒,𝑓,𝑦   𝑅,𝑔,𝑖   𝑅,   𝑅,𝑘,𝑙   𝑥,𝑅   𝜑,𝑎   𝜑,𝑔,𝑖   𝜑,   𝜑,𝑘,𝑙   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑦,𝑒,𝑓)   𝐴(𝑦,𝑒,𝑓)   𝐵(𝑦,𝑒,𝑓,)   𝐶(𝑦,𝑒,𝑓)   𝑃(𝑔,,𝑖,𝑎)   𝑄(𝑥,𝑦,𝑒,𝑓,𝑔,,𝑖,𝑘,𝑎,𝑙)   (𝑥,𝑦,𝑒,𝑓,𝑔,,𝑖,𝑘,𝑙)   𝐸(𝑦,𝑒,𝑓,)   𝐺(𝑥,𝑔,𝑖,𝑘,𝑎,𝑙)   𝐻(𝑥,𝑦,𝑒,𝑓,𝑔,,𝑖,𝑘,𝑎,𝑙)   𝐾(𝑘,𝑙)   𝐿(𝑥,𝑦,𝑒,𝑓,𝑔,,𝑖,𝑘,𝑎,𝑙)   𝑀(𝑥,𝑒,𝑓,𝑔,𝑖,𝑘,𝑎,𝑙)   𝑁(𝑔,,𝑖)

Proof of Theorem aks6d1c2
Dummy variables 𝑏 𝑐 𝑑 𝑗 𝑢 𝑤 𝑠 𝑡 𝑜 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 482 . . . . 5 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → ((𝜑𝑏𝐶) ∧ 𝑐𝐶))
2 simprl 771 . . . . 5 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → 𝑏 < 𝑐)
31, 2jca 511 . . . 4 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → (((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐))
4 simprr 773 . . . 4 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))
53, 4jca 511 . . 3 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))))
6 aks6d1c2a.1 . . . . . . 7 = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ (Base‘(Poly1𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1𝐾)‘𝑓)‘𝑦)) = (((eval1𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))}
7 aks6d1c2a.2 . . . . . . 7 𝑃 = (chr‘𝐾)
8 aks6d1c2a.3 . . . . . . . 8 (𝜑𝐾 ∈ Field)
98ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝐾 ∈ Field)
10 aks6d1c2a.4 . . . . . . . 8 (𝜑𝑃 ∈ ℙ)
1110ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑃 ∈ ℙ)
12 aks6d1c2a.5 . . . . . . . 8 (𝜑𝑅 ∈ ℕ)
1312ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑅 ∈ ℕ)
14 aks6d1c2a.6 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
1514ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑁 ∈ ℕ)
16 aks6d1c2a.7 . . . . . . . 8 (𝜑𝑃𝑁)
1716ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑃𝑁)
18 aks6d1c2a.8 . . . . . . . 8 (𝜑 → (𝑁 gcd 𝑅) = 1)
1918ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (𝑁 gcd 𝑅) = 1)
20 0nn0 12539 . . . . . . . . 9 0 ∈ ℕ0
2120a1i 11 . . . . . . . 8 (((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) ∧ 𝑗 ∈ (0...𝐴)) → 0 ∈ ℕ0)
22 eqid 2735 . . . . . . . 8 (𝑗 ∈ (0...𝐴) ↦ 0) = (𝑗 ∈ (0...𝐴) ↦ 0)
2321, 22fmptd 7134 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (𝑗 ∈ (0...𝐴) ↦ 0):(0...𝐴)⟶ℕ0)
24 aks6d1c2a.10 . . . . . . 7 𝐺 = (𝑔 ∈ (ℕ0m (0...𝐴)) ↦ ((mulGrp‘(Poly1𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔𝑖)(.g‘(mulGrp‘(Poly1𝐾)))((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
25 aks6d1c2a.11 . . . . . . . 8 (𝜑𝐴 ∈ ℕ0)
2625ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝐴 ∈ ℕ0)
27 aks6d1c2a.12 . . . . . . 7 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))
28 aks6d1c2a.13 . . . . . . 7 𝐿 = (ℤRHom‘(ℤ/nℤ‘𝑅))
29 aks6d1c2a.14 . . . . . . . 8 (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
3029ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → ∀𝑎 ∈ (1...𝐴)𝑁 ((var1𝐾)(+g‘(Poly1𝐾))((algSc‘(Poly1𝐾))‘((ℤRHom‘𝐾)‘𝑎))))
31 aks6d1c2a.15 . . . . . . . 8 (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
3231ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾))
33 aks6d1c2a.16 . . . . . . . 8 (𝜑𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
3433ad5antr 734 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅))
35 aks6d1c2a.17 . . . . . . 7 𝐻 = ( ∈ (ℕ0m (0...𝐴)) ↦ (((eval1𝐾)‘(𝐺))‘𝑀))
36 aks6d1c2a.18 . . . . . . 7 𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))
37 aks6d1c2a.19 . . . . . . 7 𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵)))
38 simp-5r 786 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑏𝐶)
39 simp-4r 784 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑐𝐶)
40 simpllr 776 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑏 < 𝑐)
41 eqid 2735 . . . . . . 7 (.g‘(mulGrp‘(Poly1𝐾))) = (.g‘(mulGrp‘(Poly1𝐾)))
42 eqid 2735 . . . . . . 7 (var1𝐾) = (var1𝐾)
43 eqid 2735 . . . . . . 7 ((𝑐(.g‘(mulGrp‘(Poly1𝐾)))(var1𝐾))(-g‘(Poly1𝐾))(𝑏(.g‘(mulGrp‘(Poly1𝐾)))(var1𝐾))) = ((𝑐(.g‘(mulGrp‘(Poly1𝐾)))(var1𝐾))(-g‘(Poly1𝐾))(𝑏(.g‘(mulGrp‘(Poly1𝐾)))(var1𝐾)))
44 simplr 769 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑑 ∈ ℕ)
45 simpr 484 . . . . . . 7 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑐 = (𝑏 + (𝑑 · 𝑅)))
466, 7, 9, 11, 13, 15, 17, 19, 23, 24, 26, 27, 28, 30, 32, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45aks6d1c2lem4 42109 . . . . . 6 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
4746ex 412 . . . . 5 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) → (𝑐 = (𝑏 + (𝑑 · 𝑅)) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵)))
4847rexlimdva 3153 . . . 4 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) → (∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵)))
4948imp 406 . . 3 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
505, 49syl 17 . 2 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
51 simprr 773 . . . 4 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑏 < 𝑐)
52 nfcv 2903 . . . . . . . . . . . . 13 𝑠(𝐿𝑡)
53 nfcv 2903 . . . . . . . . . . . . 13 𝑡(𝐿𝑠)
54 fveq2 6907 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (𝐿𝑡) = (𝐿𝑠))
5552, 53, 54cbvmpt 5259 . . . . . . . . . . . 12 (𝑡𝐶 ↦ (𝐿𝑡)) = (𝑠𝐶 ↦ (𝐿𝑠))
5655a1i 11 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑡𝐶 ↦ (𝐿𝑡)) = (𝑠𝐶 ↦ (𝐿𝑠)))
57 simpr 484 . . . . . . . . . . . 12 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑏) → 𝑠 = 𝑏)
5857fveq2d 6911 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑏) → (𝐿𝑠) = (𝐿𝑏))
59 simpllr 776 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑏𝐶)
60 fvexd 6922 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑏) ∈ V)
6156, 58, 59, 60fvmptd 7023 . . . . . . . . . 10 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = (𝐿𝑏))
6261eqcomd 2741 . . . . . . . . 9 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏))
63 simprl 771 . . . . . . . . . 10 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐))
64 simpr 484 . . . . . . . . . . . 12 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑐) → 𝑠 = 𝑐)
6564fveq2d 6911 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑐) → (𝐿𝑠) = (𝐿𝑐))
66 simplr 769 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑐𝐶)
67 fvexd 6922 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑐) ∈ V)
6856, 65, 66, 67fvmptd 7023 . . . . . . . . . 10 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) = (𝐿𝑐))
6963, 68eqtrd 2775 . . . . . . . . 9 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = (𝐿𝑐))
7062, 69eqtrd 2775 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑏) = (𝐿𝑐))
7170eqcomd 2741 . . . . . . 7 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑐) = (𝐿𝑏))
7212nnnn0d 12585 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℕ0)
7372adantr 480 . . . . . . . . . 10 ((𝜑𝑏𝐶) → 𝑅 ∈ ℕ0)
7473adantr 480 . . . . . . . . 9 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑅 ∈ ℕ0)
7574adantr 480 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∈ ℕ0)
76 fz0ssnn0 13659 . . . . . . . . . . . . . . . . . 18 (0...𝐵) ⊆ ℕ0
7776a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (0...𝐵) ⊆ ℕ0)
7877, 77jca 511 . . . . . . . . . . . . . . . 16 (𝜑 → ((0...𝐵) ⊆ ℕ0 ∧ (0...𝐵) ⊆ ℕ0))
79 eqid 2735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅)
8014, 10, 16, 12, 18, 27, 28, 79hashscontpowcl 42102 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0)
8180nn0red 12586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ)
8280nn0ge0d 12588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
8381, 82resqrtcld 15453 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ∈ ℝ)
8483flcld 13835 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℤ)
8581, 82sqrtge0d 15456 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 0 ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))
86 0zd 12623 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 0 ∈ ℤ)
87 flge 13842 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ↔ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))))
8883, 86, 87syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (0 ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ↔ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))))
8985, 88mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))))
9084, 89jca 511 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℤ ∧ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))))
91 elnn0z 12624 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℕ0 ↔ ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℤ ∧ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))))
9290, 91sylibr 234 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℕ0)
9336a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))))
9493eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐵 ∈ ℕ0 ↔ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℕ0))
9592, 94mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ ℕ0)
9695nn0ge0d 12588 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ 𝐵)
9795nn0zd 12637 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ ℤ)
98 eluz 12890 . . . . . . . . . . . . . . . . . . . . . 22 ((0 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ∈ (ℤ‘0) ↔ 0 ≤ 𝐵))
9986, 97, 98syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 ∈ (ℤ‘0) ↔ 0 ≤ 𝐵))
10096, 99mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (ℤ‘0))
101 fzn0 13575 . . . . . . . . . . . . . . . . . . . 20 ((0...𝐵) ≠ ∅ ↔ 𝐵 ∈ (ℤ‘0))
102100, 101sylibr 234 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0...𝐵) ≠ ∅)
103102, 102jca 511 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((0...𝐵) ≠ ∅ ∧ (0...𝐵) ≠ ∅))
104 xpnz 6181 . . . . . . . . . . . . . . . . . . 19 (((0...𝐵) ≠ ∅ ∧ (0...𝐵) ≠ ∅) ↔ ((0...𝐵) × (0...𝐵)) ≠ ∅)
105104biimpi 216 . . . . . . . . . . . . . . . . . 18 (((0...𝐵) ≠ ∅ ∧ (0...𝐵) ≠ ∅) → ((0...𝐵) × (0...𝐵)) ≠ ∅)
106103, 105syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0...𝐵) × (0...𝐵)) ≠ ∅)
107 ssxpb 6196 . . . . . . . . . . . . . . . . 17 (((0...𝐵) × (0...𝐵)) ≠ ∅ → (((0...𝐵) × (0...𝐵)) ⊆ (ℕ0 × ℕ0) ↔ ((0...𝐵) ⊆ ℕ0 ∧ (0...𝐵) ⊆ ℕ0)))
108106, 107syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (((0...𝐵) × (0...𝐵)) ⊆ (ℕ0 × ℕ0) ↔ ((0...𝐵) ⊆ ℕ0 ∧ (0...𝐵) ⊆ ℕ0)))
10978, 108mpbird 257 . . . . . . . . . . . . . . 15 (𝜑 → ((0...𝐵) × (0...𝐵)) ⊆ (ℕ0 × ℕ0))
110 imass2 6123 . . . . . . . . . . . . . . 15 (((0...𝐵) × (0...𝐵)) ⊆ (ℕ0 × ℕ0) → (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ (𝐸 “ (ℕ0 × ℕ0)))
111109, 110syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ (𝐸 “ (ℕ0 × ℕ0)))
112 nfv 1912 . . . . . . . . . . . . . . 15 𝑜𝜑
113 aks6d1c2a.20 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑄 ∈ ℙ ∧ 𝑄𝑁𝑃𝑄))
114113simp1d 1141 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑄 ∈ ℙ)
115113simp2d 1142 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑄𝑁)
116113simp3d 1143 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑃𝑄)
11714, 10, 16, 27, 114, 115, 116aks6d1c2p2 42101 . . . . . . . . . . . . . . . . . 18 (𝜑𝐸:(ℕ0 × ℕ0)–1-1→ℕ)
118 f1f 6805 . . . . . . . . . . . . . . . . . 18 (𝐸:(ℕ0 × ℕ0)–1-1→ℕ → 𝐸:(ℕ0 × ℕ0)⟶ℕ)
119117, 118syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐸:(ℕ0 × ℕ0)⟶ℕ)
120119ffnd 6738 . . . . . . . . . . . . . . . 16 (𝜑𝐸 Fn (ℕ0 × ℕ0))
121120fnfund 6670 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐸)
122119ffvelcdmda 7104 . . . . . . . . . . . . . . 15 ((𝜑𝑜 ∈ (ℕ0 × ℕ0)) → (𝐸𝑜) ∈ ℕ)
123112, 121, 122funimassd 6975 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℕ)
124111, 123sstrd 4006 . . . . . . . . . . . . 13 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ ℕ)
12537a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵))))
126125sseq1d 4027 . . . . . . . . . . . . 13 (𝜑 → (𝐶 ⊆ ℕ ↔ (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ ℕ))
127124, 126mpbird 257 . . . . . . . . . . . 12 (𝜑𝐶 ⊆ ℕ)
128127ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝐶 ⊆ ℕ)
129 simpr 484 . . . . . . . . . . 11 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑐𝐶)
130128, 129sseldd 3996 . . . . . . . . . 10 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑐 ∈ ℕ)
131130nnzd 12638 . . . . . . . . 9 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑐 ∈ ℤ)
132131adantr 480 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑐 ∈ ℤ)
133 simplr 769 . . . . . . . . . . 11 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑏𝐶)
134128, 133sseldd 3996 . . . . . . . . . 10 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑏 ∈ ℕ)
135134nnzd 12638 . . . . . . . . 9 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑏 ∈ ℤ)
136135adantr 480 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑏 ∈ ℤ)
13779, 28zndvds 21586 . . . . . . . 8 ((𝑅 ∈ ℕ0𝑐 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((𝐿𝑐) = (𝐿𝑏) ↔ 𝑅 ∥ (𝑐𝑏)))
13875, 132, 136, 137syl3anc 1370 . . . . . . 7 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝐿𝑐) = (𝐿𝑏) ↔ 𝑅 ∥ (𝑐𝑏)))
13971, 138mpbid 232 . . . . . 6 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∥ (𝑐𝑏))
14075nn0zd 12637 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∈ ℤ)
141132, 136zsubcld 12725 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑐𝑏) ∈ ℤ)
142 divides 16289 . . . . . . . 8 ((𝑅 ∈ ℤ ∧ (𝑐𝑏) ∈ ℤ) → (𝑅 ∥ (𝑐𝑏) ↔ ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐𝑏)))
143140, 141, 142syl2anc 584 . . . . . . 7 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑅 ∥ (𝑐𝑏) ↔ ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐𝑏)))
144143biimpd 229 . . . . . 6 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑅 ∥ (𝑐𝑏) → ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐𝑏)))
145139, 144mpd 15 . . . . 5 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐𝑏))
146 simprl 771 . . . . . . 7 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑑 ∈ ℤ)
147130ad2antrr 726 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑐 ∈ ℕ)
148147nnred 12279 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑐 ∈ ℝ)
149134ad2antrr 726 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑏 ∈ ℕ)
150149nnred 12279 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑏 ∈ ℝ)
151148, 150resubcld 11689 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑐𝑏) ∈ ℝ)
15212nnrpd 13073 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ ℝ+)
153152adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑏𝐶) → 𝑅 ∈ ℝ+)
154153adantr 480 . . . . . . . . . . . 12 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑅 ∈ ℝ+)
155154adantr 480 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∈ ℝ+)
156155adantr 480 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑅 ∈ ℝ+)
157156rpred 13075 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑅 ∈ ℝ)
15851adantr 480 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑏 < 𝑐)
159150, 148posdifd 11848 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑏 < 𝑐 ↔ 0 < (𝑐𝑏)))
160158, 159mpbid 232 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 0 < (𝑐𝑏))
161156rpgt0d 13078 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 0 < 𝑅)
162151, 157, 160, 161divgt0d 12201 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 0 < ((𝑐𝑏) / 𝑅))
163157recnd 11287 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑅 ∈ ℂ)
164146zred 12720 . . . . . . . . . . . 12 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑑 ∈ ℝ)
165164recnd 11287 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑑 ∈ ℂ)
166163, 165mulcomd 11280 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑅 · 𝑑) = (𝑑 · 𝑅))
167 simprr 773 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑑 · 𝑅) = (𝑐𝑏))
168166, 167eqtrd 2775 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑅 · 𝑑) = (𝑐𝑏))
169151recnd 11287 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑐𝑏) ∈ ℂ)
170161gt0ne0d 11825 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑅 ≠ 0)
171169, 163, 165, 170divmuld 12063 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (((𝑐𝑏) / 𝑅) = 𝑑 ↔ (𝑅 · 𝑑) = (𝑐𝑏)))
172168, 171mpbird 257 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → ((𝑐𝑏) / 𝑅) = 𝑑)
173162, 172breqtrd 5174 . . . . . . 7 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 0 < 𝑑)
174146, 173jca 511 . . . . . 6 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑑 ∈ ℤ ∧ 0 < 𝑑))
175 elnnz 12621 . . . . . 6 (𝑑 ∈ ℕ ↔ (𝑑 ∈ ℤ ∧ 0 < 𝑑))
176174, 175sylibr 234 . . . . 5 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑑 ∈ ℕ)
177167eqcomd 2741 . . . . . . 7 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑐𝑏) = (𝑑 · 𝑅))
178148recnd 11287 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑐 ∈ ℂ)
179150recnd 11287 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑏 ∈ ℂ)
180167, 169eqeltrd 2839 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑑 · 𝑅) ∈ ℂ)
181178, 179, 180subaddd 11636 . . . . . . 7 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → ((𝑐𝑏) = (𝑑 · 𝑅) ↔ (𝑏 + (𝑑 · 𝑅)) = 𝑐))
182177, 181mpbid 232 . . . . . 6 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑏 + (𝑑 · 𝑅)) = 𝑐)
183182eqcomd 2741 . . . . 5 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑐 = (𝑏 + (𝑑 · 𝑅)))
184145, 176, 183reximssdv 3171 . . . 4 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))
18551, 184jca 511 . . 3 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))))
186 fzfid 14011 . . . . . . 7 (𝜑 → (0...𝐵) ∈ Fin)
187 xpfi 9356 . . . . . . 7 (((0...𝐵) ∈ Fin ∧ (0...𝐵) ∈ Fin) → ((0...𝐵) × (0...𝐵)) ∈ Fin)
188186, 186, 187syl2anc 584 . . . . . 6 (𝜑 → ((0...𝐵) × (0...𝐵)) ∈ Fin)
189 imafi 9351 . . . . . 6 ((Fun 𝐸 ∧ ((0...𝐵) × (0...𝐵)) ∈ Fin) → (𝐸 “ ((0...𝐵) × (0...𝐵))) ∈ Fin)
190121, 188, 189syl2anc 584 . . . . 5 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) ∈ Fin)
191125eleq1d 2824 . . . . 5 (𝜑 → (𝐶 ∈ Fin ↔ (𝐸 “ ((0...𝐵) × (0...𝐵))) ∈ Fin))
192190, 191mpbird 257 . . . 4 (𝜑𝐶 ∈ Fin)
19379zncrng 21581 . . . . . . . . . 10 (𝑅 ∈ ℕ0 → (ℤ/nℤ‘𝑅) ∈ CRing)
19472, 193syl 17 . . . . . . . . 9 (𝜑 → (ℤ/nℤ‘𝑅) ∈ CRing)
195 crngring 20263 . . . . . . . . 9 ((ℤ/nℤ‘𝑅) ∈ CRing → (ℤ/nℤ‘𝑅) ∈ Ring)
196194, 195syl 17 . . . . . . . 8 (𝜑 → (ℤ/nℤ‘𝑅) ∈ Ring)
19728zrhrhm 21540 . . . . . . . 8 ((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤring RingHom (ℤ/nℤ‘𝑅)))
198196, 197syl 17 . . . . . . 7 (𝜑𝐿 ∈ (ℤring RingHom (ℤ/nℤ‘𝑅)))
199198imaexd 7939 . . . . . 6 (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ V)
200 hashclb 14394 . . . . . 6 ((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ V → ((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ Fin ↔ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0))
201199, 200syl 17 . . . . 5 (𝜑 → ((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ Fin ↔ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0))
20280, 201mpbird 257 . . . 4 (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ Fin)
203 hashcl 14392 . . . . . . . . . . . . 13 ((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ Fin → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0)
204202, 203syl 17 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0)
205204nn0red 12586 . . . . . . . . . . 11 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ)
206204nn0ge0d 12588 . . . . . . . . . . 11 (𝜑 → 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
207 sqrtmsq 15306 . . . . . . . . . . 11 (((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ ∧ 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) → (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
208205, 206, 207syl2anc 584 . . . . . . . . . 10 (𝜑 → (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
209208eqcomd 2741 . . . . . . . . 9 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) = (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))))
210205, 206jca 511 . . . . . . . . . . 11 (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ ∧ 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))
211 sqrtmul 15295 . . . . . . . . . . 11 ((((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ ∧ 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ∧ ((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ ∧ 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) → (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) = ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))))
212210, 210, 211syl2anc 584 . . . . . . . . . 10 (𝜑 → (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) = ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))))
213205, 206resqrtcld 15453 . . . . . . . . . . 11 (𝜑 → (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ∈ ℝ)
214213flcld 13835 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℤ)
215205, 206sqrtge0d 15456 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))
216213, 86, 87syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → (0 ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ↔ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))))
217215, 216mpbid 232 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))))
218214, 217jca 511 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℤ ∧ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))))
219218, 91sylibr 234 . . . . . . . . . . . . . 14 (𝜑 → (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℕ0)
220219, 94mpbird 257 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℕ0)
221220nn0red 12586 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
222 1red 11260 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
223221, 222readdcld 11288 . . . . . . . . . . 11 (𝜑 → (𝐵 + 1) ∈ ℝ)
224 flltp1 13837 . . . . . . . . . . . . 13 ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ∈ ℝ → (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) < ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) + 1))
225213, 224syl 17 . . . . . . . . . . . 12 (𝜑 → (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) < ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) + 1))
22693oveq1d 7446 . . . . . . . . . . . 12 (𝜑 → (𝐵 + 1) = ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) + 1))
227225, 226breqtrrd 5176 . . . . . . . . . . 11 (𝜑 → (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) < (𝐵 + 1))
228213, 223, 213, 223, 215, 227, 215, 227ltmul12ad 12207 . . . . . . . . . 10 (𝜑 → ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) < ((𝐵 + 1) · (𝐵 + 1)))
229212, 228eqbrtrd 5170 . . . . . . . . 9 (𝜑 → (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) < ((𝐵 + 1) · (𝐵 + 1)))
230209, 229eqbrtrd 5170 . . . . . . . 8 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < ((𝐵 + 1) · (𝐵 + 1)))
231 hashfz0 14468 . . . . . . . . . 10 (𝐵 ∈ ℕ0 → (♯‘(0...𝐵)) = (𝐵 + 1))
232220, 231syl 17 . . . . . . . . 9 (𝜑 → (♯‘(0...𝐵)) = (𝐵 + 1))
233232, 232oveq12d 7449 . . . . . . . 8 (𝜑 → ((♯‘(0...𝐵)) · (♯‘(0...𝐵))) = ((𝐵 + 1) · (𝐵 + 1)))
234230, 233breqtrrd 5176 . . . . . . 7 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < ((♯‘(0...𝐵)) · (♯‘(0...𝐵))))
235186, 186jca 511 . . . . . . . 8 (𝜑 → ((0...𝐵) ∈ Fin ∧ (0...𝐵) ∈ Fin))
236 hashxp 14470 . . . . . . . 8 (((0...𝐵) ∈ Fin ∧ (0...𝐵) ∈ Fin) → (♯‘((0...𝐵) × (0...𝐵))) = ((♯‘(0...𝐵)) · (♯‘(0...𝐵))))
237235, 236syl 17 . . . . . . 7 (𝜑 → (♯‘((0...𝐵) × (0...𝐵))) = ((♯‘(0...𝐵)) · (♯‘(0...𝐵))))
238234, 237breqtrrd 5176 . . . . . 6 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < (♯‘((0...𝐵) × (0...𝐵))))
239 ovexd 7466 . . . . . . . . . . 11 (𝜑 → (0...𝐵) ∈ V)
240239, 239jca 511 . . . . . . . . . 10 (𝜑 → ((0...𝐵) ∈ V ∧ (0...𝐵) ∈ V))
241 xpexg 7769 . . . . . . . . . 10 (((0...𝐵) ∈ V ∧ (0...𝐵) ∈ V) → ((0...𝐵) × (0...𝐵)) ∈ V)
242240, 241syl 17 . . . . . . . . 9 (𝜑 → ((0...𝐵) × (0...𝐵)) ∈ V)
243242mptexd 7244 . . . . . . . 8 (𝜑 → (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)) ∈ V)
244120adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ((0...𝐵) × (0...𝐵))) → 𝐸 Fn (ℕ0 × ℕ0))
245109sselda 3995 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ((0...𝐵) × (0...𝐵))) → 𝑤 ∈ (ℕ0 × ℕ0))
246 simpr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ((0...𝐵) × (0...𝐵))) → 𝑤 ∈ ((0...𝐵) × (0...𝐵)))
247244, 245, 246fnfvimad 7254 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ((0...𝐵) × (0...𝐵))) → (𝐸𝑤) ∈ (𝐸 “ ((0...𝐵) × (0...𝐵))))
248 eqid 2735 . . . . . . . . . . . . . 14 (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)) = (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤))
249247, 248fmptd 7134 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))⟶(𝐸 “ ((0...𝐵) × (0...𝐵))))
250119, 109feqresmpt 6978 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 ↾ ((0...𝐵) × (0...𝐵))) = (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)))
251250feq1d 6721 . . . . . . . . . . . . 13 (𝜑 → ((𝐸 ↾ ((0...𝐵) × (0...𝐵))):((0...𝐵) × (0...𝐵))⟶(𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))⟶(𝐸 “ ((0...𝐵) × (0...𝐵)))))
252249, 251mpbird 257 . . . . . . . . . . . 12 (𝜑 → (𝐸 ↾ ((0...𝐵) × (0...𝐵))):((0...𝐵) × (0...𝐵))⟶(𝐸 “ ((0...𝐵) × (0...𝐵))))
253 f1resf1 6813 . . . . . . . . . . . 12 ((𝐸:(ℕ0 × ℕ0)–1-1→ℕ ∧ ((0...𝐵) × (0...𝐵)) ⊆ (ℕ0 × ℕ0) ∧ (𝐸 ↾ ((0...𝐵) × (0...𝐵))):((0...𝐵) × (0...𝐵))⟶(𝐸 “ ((0...𝐵) × (0...𝐵)))) → (𝐸 ↾ ((0...𝐵) × (0...𝐵))):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵))))
254117, 109, 252, 253syl3anc 1370 . . . . . . . . . . 11 (𝜑 → (𝐸 ↾ ((0...𝐵) × (0...𝐵))):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵))))
255 eqidd 2736 . . . . . . . . . . . 12 (𝜑 → ((0...𝐵) × (0...𝐵)) = ((0...𝐵) × (0...𝐵)))
256 eqidd 2736 . . . . . . . . . . . 12 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) = (𝐸 “ ((0...𝐵) × (0...𝐵))))
257250, 255, 256f1eq123d 6841 . . . . . . . . . . 11 (𝜑 → ((𝐸 ↾ ((0...𝐵) × (0...𝐵))):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵)))))
258254, 257mpbid 232 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵))))
259 df-ima 5702 . . . . . . . . . . . 12 (𝐸 “ ((0...𝐵) × (0...𝐵))) = ran (𝐸 ↾ ((0...𝐵) × (0...𝐵)))
260259a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) = ran (𝐸 ↾ ((0...𝐵) × (0...𝐵))))
261250rneqd 5952 . . . . . . . . . . 11 (𝜑 → ran (𝐸 ↾ ((0...𝐵) × (0...𝐵))) = ran (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)))
262260, 261eqtr2d 2776 . . . . . . . . . 10 (𝜑 → ran (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)) = (𝐸 “ ((0...𝐵) × (0...𝐵))))
263258, 262jca 511 . . . . . . . . 9 (𝜑 → ((𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵))) ∧ ran (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)) = (𝐸 “ ((0...𝐵) × (0...𝐵)))))
264 dff1o5 6858 . . . . . . . . 9 ((𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))–1-1-onto→(𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ ((𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵))) ∧ ran (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)) = (𝐸 “ ((0...𝐵) × (0...𝐵)))))
265263, 264sylibr 234 . . . . . . . 8 (𝜑 → (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))–1-1-onto→(𝐸 “ ((0...𝐵) × (0...𝐵))))
266 f1oeq1 6837 . . . . . . . 8 (𝑢 = (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)) → (𝑢:((0...𝐵) × (0...𝐵))–1-1-onto→(𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))–1-1-onto→(𝐸 “ ((0...𝐵) × (0...𝐵)))))
267243, 265, 266spcedv 3598 . . . . . . 7 (𝜑 → ∃𝑢 𝑢:((0...𝐵) × (0...𝐵))–1-1-onto→(𝐸 “ ((0...𝐵) × (0...𝐵))))
268 hasheqf1oi 14387 . . . . . . . 8 (((0...𝐵) × (0...𝐵)) ∈ V → (∃𝑢 𝑢:((0...𝐵) × (0...𝐵))–1-1-onto→(𝐸 “ ((0...𝐵) × (0...𝐵))) → (♯‘((0...𝐵) × (0...𝐵))) = (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵))))))
269242, 268syl 17 . . . . . . 7 (𝜑 → (∃𝑢 𝑢:((0...𝐵) × (0...𝐵))–1-1-onto→(𝐸 “ ((0...𝐵) × (0...𝐵))) → (♯‘((0...𝐵) × (0...𝐵))) = (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵))))))
270267, 269mpd 15 . . . . . 6 (𝜑 → (♯‘((0...𝐵) × (0...𝐵))) = (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵)))))
271238, 270breqtrd 5174 . . . . 5 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵)))))
272125fveq2d 6911 . . . . 5 (𝜑 → (♯‘𝐶) = (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵)))))
273271, 272breqtrrd 5176 . . . 4 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < (♯‘𝐶))
274 zringbas 21482 . . . . . . . . . 10 ℤ = (Base‘ℤring)
275 eqid 2735 . . . . . . . . . 10 (Base‘(ℤ/nℤ‘𝑅)) = (Base‘(ℤ/nℤ‘𝑅))
276274, 275rhmf 20502 . . . . . . . . 9 (𝐿 ∈ (ℤring RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
277198, 276syl 17 . . . . . . . 8 (𝜑𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
278277ffnd 6738 . . . . . . 7 (𝜑𝐿 Fn ℤ)
279278adantr 480 . . . . . 6 ((𝜑𝑡𝐶) → 𝐿 Fn ℤ)
280 resss 6022 . . . . . . . . . . . 12 (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ 𝐸
281280a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ 𝐸)
282 rnss 5953 . . . . . . . . . . 11 ((𝐸 ↾ (ℕ0 × ℕ0)) ⊆ 𝐸 → ran (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ ran 𝐸)
283281, 282syl 17 . . . . . . . . . 10 (𝜑 → ran (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ ran 𝐸)
284 df-ima 5702 . . . . . . . . . . . 12 (𝐸 “ (ℕ0 × ℕ0)) = ran (𝐸 ↾ (ℕ0 × ℕ0))
285284a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) = ran (𝐸 ↾ (ℕ0 × ℕ0)))
286285sseq1d 4027 . . . . . . . . . 10 (𝜑 → ((𝐸 “ (ℕ0 × ℕ0)) ⊆ ran 𝐸 ↔ ran (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ ran 𝐸))
287283, 286mpbird 257 . . . . . . . . 9 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ran 𝐸)
288 frn 6744 . . . . . . . . . 10 (𝐸:(ℕ0 × ℕ0)⟶ℕ → ran 𝐸 ⊆ ℕ)
289119, 288syl 17 . . . . . . . . 9 (𝜑 → ran 𝐸 ⊆ ℕ)
290287, 289sstrd 4006 . . . . . . . 8 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℕ)
291 nnssz 12633 . . . . . . . . 9 ℕ ⊆ ℤ
292291a1i 11 . . . . . . . 8 (𝜑 → ℕ ⊆ ℤ)
293290, 292sstrd 4006 . . . . . . 7 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℤ)
294293adantr 480 . . . . . 6 ((𝜑𝑡𝐶) → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℤ)
295125sseq1d 4027 . . . . . . . . 9 (𝜑 → (𝐶 ⊆ (𝐸 “ (ℕ0 × ℕ0)) ↔ (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ (𝐸 “ (ℕ0 × ℕ0))))
296111, 295mpbird 257 . . . . . . . 8 (𝜑𝐶 ⊆ (𝐸 “ (ℕ0 × ℕ0)))
297296sseld 3994 . . . . . . 7 (𝜑 → (𝑡𝐶𝑡 ∈ (𝐸 “ (ℕ0 × ℕ0))))
298297imp 406 . . . . . 6 ((𝜑𝑡𝐶) → 𝑡 ∈ (𝐸 “ (ℕ0 × ℕ0)))
299 fnfvima 7253 . . . . . 6 ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℤ ∧ 𝑡 ∈ (𝐸 “ (ℕ0 × ℕ0))) → (𝐿𝑡) ∈ (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))
300279, 294, 298, 299syl3anc 1370 . . . . 5 ((𝜑𝑡𝐶) → (𝐿𝑡) ∈ (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))
301 eqid 2735 . . . . 5 (𝑡𝐶 ↦ (𝐿𝑡)) = (𝑡𝐶 ↦ (𝐿𝑡))
302300, 301fmptd 7134 . . . 4 (𝜑 → (𝑡𝐶 ↦ (𝐿𝑡)):𝐶⟶(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))
303 nnssre 12268 . . . . . 6 ℕ ⊆ ℝ
304303a1i 11 . . . . 5 (𝜑 → ℕ ⊆ ℝ)
305127, 304sstrd 4006 . . . 4 (𝜑𝐶 ⊆ ℝ)
306192, 202, 273, 302, 305hashnexinjle 42111 . . 3 (𝜑 → ∃𝑏𝐶𝑐𝐶 (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐))
307185, 306reximddv2 3213 . 2 (𝜑 → ∃𝑏𝐶𝑐𝐶 (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))))
30850, 307r19.29vva 3214 1 (𝜑 → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wex 1776  wcel 2106  wne 2938  wral 3059  wrex 3068  Vcvv 3478  wss 3963  c0 4339   class class class wbr 5148  {copab 5210  cmpt 5231   × cxp 5687  ran crn 5690  cres 5691  cima 5692  Fun wfun 6557   Fn wfn 6558  wf 6559  1-1wf1 6560  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  cmpo 7433  m cmap 8865  Fincfn 8984  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   · cmul 11158   < clt 11293  cle 11294  cmin 11490   / cdiv 11918  cn 12264  0cn0 12524  cz 12611  cuz 12876  +crp 13032  ...cfz 13544  cfl 13827  cexp 14099  chash 14366  csqrt 15269  cdvds 16287   gcd cgcd 16528  cprime 16705  Basecbs 17245  +gcplusg 17298   Σg cgsu 17487  -gcsg 18966  .gcmg 19098  mulGrpcmgp 20152  Ringcrg 20251  CRingccrg 20252   RingHom crh 20486   RingIso crs 20487  Fieldcfield 20747  ringczring 21475  ℤRHomczrh 21528  chrcchr 21530  ℤ/nczn 21531  algSccascl 21890  var1cv1 22193  Poly1cpl1 22194  eval1ce1 22334   PrimRoots cprimroots 42073
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231  ax-addf 11232  ax-mulf 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-ofr 7698  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-tpos 8250  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-oadd 8509  df-er 8744  df-ec 8746  df-qs 8750  df-map 8867  df-pm 8868  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-sup 9480  df-inf 9481  df-oi 9548  df-dju 9939  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-xnn0 12598  df-z 12612  df-dec 12732  df-uz 12877  df-q 12989  df-rp 13033  df-fz 13545  df-fzo 13692  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100  df-fac 14310  df-bc 14339  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-dvds 16288  df-gcd 16529  df-prm 16706  df-phi 16800  df-pc 16871  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-0g 17488  df-gsum 17489  df-prds 17494  df-pws 17496  df-imas 17555  df-qus 17556  df-mre 17631  df-mrc 17632  df-acs 17634  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-mhm 18809  df-submnd 18810  df-grp 18967  df-minusg 18968  df-sbg 18969  df-mulg 19099  df-subg 19154  df-nsg 19155  df-eqg 19156  df-ghm 19244  df-cntz 19348  df-od 19561  df-cmn 19815  df-abl 19816  df-mgp 20153  df-rng 20171  df-ur 20200  df-srg 20205  df-ring 20253  df-cring 20254  df-oppr 20351  df-dvdsr 20374  df-unit 20375  df-invr 20405  df-dvr 20418  df-rhm 20489  df-rim 20490  df-nzr 20530  df-subrng 20563  df-subrg 20587  df-rlreg 20711  df-domn 20712  df-idom 20713  df-drng 20748  df-field 20749  df-lmod 20877  df-lss 20948  df-lsp 20988  df-sra 21190  df-rgmod 21191  df-lidl 21236  df-rsp 21237  df-2idl 21278  df-cnfld 21383  df-zring 21476  df-zrh 21532  df-chr 21534  df-zn 21535  df-assa 21891  df-asp 21892  df-ascl 21893  df-psr 21947  df-mvr 21948  df-mpl 21949  df-opsr 21951  df-evls 22116  df-evl 22117  df-psr1 22197  df-vr1 22198  df-ply1 22199  df-coe1 22200  df-evl1 22336  df-mdeg 26109  df-deg1 26110  df-mon1 26185  df-uc1p 26186  df-q1p 26187  df-r1p 26188  df-primroots 42074
This theorem is referenced by:  aks6d1c7lem2  42163
  Copyright terms: Public domain W3C validator