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 42131
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 12541 . . . . . . . . 9 0 ∈ ℕ0
2120a1i 11 . . . . . . . 8 (((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) ∧ 𝑗 ∈ (0...𝐴)) → 0 ∈ ℕ0)
22 eqid 2737 . . . . . . . 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 2737 . . . . . . 7 (.g‘(mulGrp‘(Poly1𝐾))) = (.g‘(mulGrp‘(Poly1𝐾)))
42 eqid 2737 . . . . . . 7 (var1𝐾) = (var1𝐾)
43 eqid 2737 . . . . . . 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 42128 . . . . . 6 ((((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
4746ex 412 . . . . 5 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) → (𝑐 = (𝑏 + (𝑑 · 𝑅)) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵)))
4847rexlimdva 3155 . . . 4 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) → (∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵)))
4948imp 406 . . 3 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ 𝑏 < 𝑐) ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
505, 49syl 17 . 2 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
51 simprr 773 . . . 4 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑏 < 𝑐)
52 nfcv 2905 . . . . . . . . . . . . 13 𝑠(𝐿𝑡)
53 nfcv 2905 . . . . . . . . . . . . 13 𝑡(𝐿𝑠)
54 fveq2 6906 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (𝐿𝑡) = (𝐿𝑠))
5552, 53, 54cbvmpt 5253 . . . . . . . . . . . 12 (𝑡𝐶 ↦ (𝐿𝑡)) = (𝑠𝐶 ↦ (𝐿𝑠))
5655a1i 11 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑡𝐶 ↦ (𝐿𝑡)) = (𝑠𝐶 ↦ (𝐿𝑠)))
57 simpr 484 . . . . . . . . . . . 12 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑏) → 𝑠 = 𝑏)
5857fveq2d 6910 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑏) → (𝐿𝑠) = (𝐿𝑏))
59 simpllr 776 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑏𝐶)
60 fvexd 6921 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑏) ∈ V)
6156, 58, 59, 60fvmptd 7023 . . . . . . . . . 10 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = (𝐿𝑏))
6261eqcomd 2743 . . . . . . . . 9 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏))
63 simprl 771 . . . . . . . . . 10 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐))
64 simpr 484 . . . . . . . . . . . 12 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑐) → 𝑠 = 𝑐)
6564fveq2d 6910 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑐) → (𝐿𝑠) = (𝐿𝑐))
66 simplr 769 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑐𝐶)
67 fvexd 6921 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑐) ∈ V)
6856, 65, 66, 67fvmptd 7023 . . . . . . . . . 10 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) = (𝐿𝑐))
6963, 68eqtrd 2777 . . . . . . . . 9 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = (𝐿𝑐))
7062, 69eqtrd 2777 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑏) = (𝐿𝑐))
7170eqcomd 2743 . . . . . . 7 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿𝑐) = (𝐿𝑏))
7212nnnn0d 12587 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℕ0)
7372adantr 480 . . . . . . . . . 10 ((𝜑𝑏𝐶) → 𝑅 ∈ ℕ0)
7473adantr 480 . . . . . . . . 9 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑅 ∈ ℕ0)
7574adantr 480 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∈ ℕ0)
76 fz0ssnn0 13662 . . . . . . . . . . . . . . . . . 18 (0...𝐵) ⊆ ℕ0
7776a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (0...𝐵) ⊆ ℕ0)
7877, 77jca 511 . . . . . . . . . . . . . . . 16 (𝜑 → ((0...𝐵) ⊆ ℕ0 ∧ (0...𝐵) ⊆ ℕ0))
79 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅)
8014, 10, 16, 12, 18, 27, 28, 79hashscontpowcl 42121 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0)
8180nn0red 12588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ)
8280nn0ge0d 12590 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
8381, 82resqrtcld 15456 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ∈ ℝ)
8483flcld 13838 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℤ)
8581, 82sqrtge0d 15459 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 0 ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))
86 0zd 12625 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 0 ∈ ℤ)
87 flge 13845 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12626 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℕ0 ↔ ((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℤ ∧ 0 ≤ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))))
9290, 91sylibr 234 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℕ0)
9336a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐵 = (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))))
9493eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐵 ∈ ℕ0 ↔ (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℕ0))
9592, 94mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ ℕ0)
9695nn0ge0d 12590 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ 𝐵)
9795nn0zd 12639 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ ℤ)
98 eluz 12892 . . . . . . . . . . . . . . . . . . . . . 22 ((0 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ∈ (ℤ‘0) ↔ 0 ≤ 𝐵))
9986, 97, 98syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 ∈ (ℤ‘0) ↔ 0 ≤ 𝐵))
10096, 99mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (ℤ‘0))
101 fzn0 13578 . . . . . . . . . . . . . . . . . . . 20 ((0...𝐵) ≠ ∅ ↔ 𝐵 ∈ (ℤ‘0))
102100, 101sylibr 234 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0...𝐵) ≠ ∅)
103102, 102jca 511 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((0...𝐵) ≠ ∅ ∧ (0...𝐵) ≠ ∅))
104 xpnz 6179 . . . . . . . . . . . . . . . . . . 19 (((0...𝐵) ≠ ∅ ∧ (0...𝐵) ≠ ∅) ↔ ((0...𝐵) × (0...𝐵)) ≠ ∅)
105104biimpi 216 . . . . . . . . . . . . . . . . . 18 (((0...𝐵) ≠ ∅ ∧ (0...𝐵) ≠ ∅) → ((0...𝐵) × (0...𝐵)) ≠ ∅)
106103, 105syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0...𝐵) × (0...𝐵)) ≠ ∅)
107 ssxpb 6194 . . . . . . . . . . . . . . . . 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 6120 . . . . . . . . . . . . . . 15 (((0...𝐵) × (0...𝐵)) ⊆ (ℕ0 × ℕ0) → (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ (𝐸 “ (ℕ0 × ℕ0)))
111109, 110syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ (𝐸 “ (ℕ0 × ℕ0)))
112 nfv 1914 . . . . . . . . . . . . . . 15 𝑜𝜑
113 aks6d1c2a.20 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑄 ∈ ℙ ∧ 𝑄𝑁𝑃𝑄))
114113simp1d 1143 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑄 ∈ ℙ)
115113simp2d 1144 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑄𝑁)
116113simp3d 1145 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑃𝑄)
11714, 10, 16, 27, 114, 115, 116aks6d1c2p2 42120 . . . . . . . . . . . . . . . . . 18 (𝜑𝐸:(ℕ0 × ℕ0)–1-1→ℕ)
118 f1f 6804 . . . . . . . . . . . . . . . . . 18 (𝐸:(ℕ0 × ℕ0)–1-1→ℕ → 𝐸:(ℕ0 × ℕ0)⟶ℕ)
119117, 118syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐸:(ℕ0 × ℕ0)⟶ℕ)
120119ffnd 6737 . . . . . . . . . . . . . . . 16 (𝜑𝐸 Fn (ℕ0 × ℕ0))
121120fnfund 6669 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐸)
122119ffvelcdmda 7104 . . . . . . . . . . . . . . 15 ((𝜑𝑜 ∈ (ℕ0 × ℕ0)) → (𝐸𝑜) ∈ ℕ)
123112, 121, 122funimassd 6975 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℕ)
124111, 123sstrd 3994 . . . . . . . . . . . . 13 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ ℕ)
12537a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵))))
126125sseq1d 4015 . . . . . . . . . . . . 13 (𝜑 → (𝐶 ⊆ ℕ ↔ (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ ℕ))
127124, 126mpbird 257 . . . . . . . . . . . 12 (𝜑𝐶 ⊆ ℕ)
128127ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝐶 ⊆ ℕ)
129 simpr 484 . . . . . . . . . . 11 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑐𝐶)
130128, 129sseldd 3984 . . . . . . . . . 10 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑐 ∈ ℕ)
131130nnzd 12640 . . . . . . . . 9 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑐 ∈ ℤ)
132131adantr 480 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑐 ∈ ℤ)
133 simplr 769 . . . . . . . . . . 11 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑏𝐶)
134128, 133sseldd 3984 . . . . . . . . . 10 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑏 ∈ ℕ)
135134nnzd 12640 . . . . . . . . 9 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑏 ∈ ℤ)
136135adantr 480 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑏 ∈ ℤ)
13779, 28zndvds 21568 . . . . . . . 8 ((𝑅 ∈ ℕ0𝑐 ∈ ℤ ∧ 𝑏 ∈ ℤ) → ((𝐿𝑐) = (𝐿𝑏) ↔ 𝑅 ∥ (𝑐𝑏)))
13875, 132, 136, 137syl3anc 1373 . . . . . . 7 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝐿𝑐) = (𝐿𝑏) ↔ 𝑅 ∥ (𝑐𝑏)))
13971, 138mpbid 232 . . . . . 6 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∥ (𝑐𝑏))
14075nn0zd 12639 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∈ ℤ)
141132, 136zsubcld 12727 . . . . . . . 8 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑐𝑏) ∈ ℤ)
142 divides 16292 . . . . . . . 8 ((𝑅 ∈ ℤ ∧ (𝑐𝑏) ∈ ℤ) → (𝑅 ∥ (𝑐𝑏) ↔ ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐𝑏)))
143140, 141, 142syl2anc 584 . . . . . . 7 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑅 ∥ (𝑐𝑏) ↔ ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐𝑏)))
144143biimpd 229 . . . . . 6 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑅 ∥ (𝑐𝑏) → ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐𝑏)))
145139, 144mpd 15 . . . . 5 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐𝑏))
146 simprl 771 . . . . . . 7 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑑 ∈ ℤ)
147130ad2antrr 726 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑐 ∈ ℕ)
148147nnred 12281 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑐 ∈ ℝ)
149134ad2antrr 726 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑏 ∈ ℕ)
150149nnred 12281 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑏 ∈ ℝ)
151148, 150resubcld 11691 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑐𝑏) ∈ ℝ)
15212nnrpd 13075 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ ℝ+)
153152adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑏𝐶) → 𝑅 ∈ ℝ+)
154153adantr 480 . . . . . . . . . . . 12 (((𝜑𝑏𝐶) ∧ 𝑐𝐶) → 𝑅 ∈ ℝ+)
155154adantr 480 . . . . . . . . . . 11 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∈ ℝ+)
156155adantr 480 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑅 ∈ ℝ+)
157156rpred 13077 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑅 ∈ ℝ)
15851adantr 480 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑏 < 𝑐)
159150, 148posdifd 11850 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑏 < 𝑐 ↔ 0 < (𝑐𝑏)))
160158, 159mpbid 232 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 0 < (𝑐𝑏))
161156rpgt0d 13080 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 0 < 𝑅)
162151, 157, 160, 161divgt0d 12203 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 0 < ((𝑐𝑏) / 𝑅))
163157recnd 11289 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑅 ∈ ℂ)
164146zred 12722 . . . . . . . . . . . 12 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑑 ∈ ℝ)
165164recnd 11289 . . . . . . . . . . 11 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑑 ∈ ℂ)
166163, 165mulcomd 11282 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑅 · 𝑑) = (𝑑 · 𝑅))
167 simprr 773 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑑 · 𝑅) = (𝑐𝑏))
168166, 167eqtrd 2777 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑅 · 𝑑) = (𝑐𝑏))
169151recnd 11289 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑐𝑏) ∈ ℂ)
170161gt0ne0d 11827 . . . . . . . . . 10 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑅 ≠ 0)
171169, 163, 165, 170divmuld 12065 . . . . . . . . 9 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (((𝑐𝑏) / 𝑅) = 𝑑 ↔ (𝑅 · 𝑑) = (𝑐𝑏)))
172168, 171mpbird 257 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → ((𝑐𝑏) / 𝑅) = 𝑑)
173162, 172breqtrd 5169 . . . . . . 7 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 0 < 𝑑)
174146, 173jca 511 . . . . . 6 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑑 ∈ ℤ ∧ 0 < 𝑑))
175 elnnz 12623 . . . . . 6 (𝑑 ∈ ℕ ↔ (𝑑 ∈ ℤ ∧ 0 < 𝑑))
176174, 175sylibr 234 . . . . 5 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑑 ∈ ℕ)
177167eqcomd 2743 . . . . . . 7 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑐𝑏) = (𝑑 · 𝑅))
178148recnd 11289 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑐 ∈ ℂ)
179150recnd 11289 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑏 ∈ ℂ)
180167, 169eqeltrd 2841 . . . . . . . 8 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑑 · 𝑅) ∈ ℂ)
181178, 179, 180subaddd 11638 . . . . . . 7 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → ((𝑐𝑏) = (𝑑 · 𝑅) ↔ (𝑏 + (𝑑 · 𝑅)) = 𝑐))
182177, 181mpbid 232 . . . . . 6 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → (𝑏 + (𝑑 · 𝑅)) = 𝑐)
183182eqcomd 2743 . . . . 5 (((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐𝑏))) → 𝑐 = (𝑏 + (𝑑 · 𝑅)))
184145, 176, 183reximssdv 3173 . . . 4 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))
18551, 184jca 511 . . 3 ((((𝜑𝑏𝐶) ∧ 𝑐𝐶) ∧ (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))))
186 fzfid 14014 . . . . . . 7 (𝜑 → (0...𝐵) ∈ Fin)
187 xpfi 9358 . . . . . . 7 (((0...𝐵) ∈ Fin ∧ (0...𝐵) ∈ Fin) → ((0...𝐵) × (0...𝐵)) ∈ Fin)
188186, 186, 187syl2anc 584 . . . . . 6 (𝜑 → ((0...𝐵) × (0...𝐵)) ∈ Fin)
189 imafi 9353 . . . . . 6 ((Fun 𝐸 ∧ ((0...𝐵) × (0...𝐵)) ∈ Fin) → (𝐸 “ ((0...𝐵) × (0...𝐵))) ∈ Fin)
190121, 188, 189syl2anc 584 . . . . 5 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) ∈ Fin)
191125eleq1d 2826 . . . . 5 (𝜑 → (𝐶 ∈ Fin ↔ (𝐸 “ ((0...𝐵) × (0...𝐵))) ∈ Fin))
192190, 191mpbird 257 . . . 4 (𝜑𝐶 ∈ Fin)
19379zncrng 21563 . . . . . . . . . 10 (𝑅 ∈ ℕ0 → (ℤ/nℤ‘𝑅) ∈ CRing)
19472, 193syl 17 . . . . . . . . 9 (𝜑 → (ℤ/nℤ‘𝑅) ∈ CRing)
195 crngring 20242 . . . . . . . . 9 ((ℤ/nℤ‘𝑅) ∈ CRing → (ℤ/nℤ‘𝑅) ∈ Ring)
196194, 195syl 17 . . . . . . . 8 (𝜑 → (ℤ/nℤ‘𝑅) ∈ Ring)
19728zrhrhm 21522 . . . . . . . 8 ((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤring RingHom (ℤ/nℤ‘𝑅)))
198196, 197syl 17 . . . . . . 7 (𝜑𝐿 ∈ (ℤring RingHom (ℤ/nℤ‘𝑅)))
199198imaexd 7938 . . . . . 6 (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ V)
200 hashclb 14397 . . . . . 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 14395 . . . . . . . . . . . . 13 ((𝐿 “ (𝐸 “ (ℕ0 × ℕ0))) ∈ Fin → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0)
204202, 203syl 17 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℕ0)
205204nn0red 12588 . . . . . . . . . . 11 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ)
206204nn0ge0d 12590 . . . . . . . . . . 11 (𝜑 → 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
207 sqrtmsq 15309 . . . . . . . . . . 11 (((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ ∧ 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) → (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
208205, 206, 207syl2anc 584 . . . . . . . . . 10 (𝜑 → (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) = (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))
209208eqcomd 2743 . . . . . . . . 9 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) = (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))))
210205, 206jca 511 . . . . . . . . . . 11 (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) ∈ ℝ ∧ 0 ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))))
211 sqrtmul 15298 . . . . . . . . . . 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 15456 . . . . . . . . . . 11 (𝜑 → (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) ∈ ℝ)
214213flcld 13838 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) ∈ ℤ)
215205, 206sqrtge0d 15459 . . . . . . . . . . . . . . . . 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 12588 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
222 1red 11262 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
223221, 222readdcld 11290 . . . . . . . . . . 11 (𝜑 → (𝐵 + 1) ∈ ℝ)
224 flltp1 13840 . . . . . . . . . . . . 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 5171 . . . . . . . . . . 11 (𝜑 → (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) < (𝐵 + 1))
228213, 223, 213, 223, 215, 227, 215, 227ltmul12ad 12209 . . . . . . . . . 10 (𝜑 → ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) < ((𝐵 + 1) · (𝐵 + 1)))
229212, 228eqbrtrd 5165 . . . . . . . . 9 (𝜑 → (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))))) < ((𝐵 + 1) · (𝐵 + 1)))
230209, 229eqbrtrd 5165 . . . . . . . 8 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < ((𝐵 + 1) · (𝐵 + 1)))
231 hashfz0 14471 . . . . . . . . . 10 (𝐵 ∈ ℕ0 → (♯‘(0...𝐵)) = (𝐵 + 1))
232220, 231syl 17 . . . . . . . . 9 (𝜑 → (♯‘(0...𝐵)) = (𝐵 + 1))
233232, 232oveq12d 7449 . . . . . . . 8 (𝜑 → ((♯‘(0...𝐵)) · (♯‘(0...𝐵))) = ((𝐵 + 1) · (𝐵 + 1)))
234230, 233breqtrrd 5171 . . . . . . 7 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < ((♯‘(0...𝐵)) · (♯‘(0...𝐵))))
235186, 186jca 511 . . . . . . . 8 (𝜑 → ((0...𝐵) ∈ Fin ∧ (0...𝐵) ∈ Fin))
236 hashxp 14473 . . . . . . . 8 (((0...𝐵) ∈ Fin ∧ (0...𝐵) ∈ Fin) → (♯‘((0...𝐵) × (0...𝐵))) = ((♯‘(0...𝐵)) · (♯‘(0...𝐵))))
237235, 236syl 17 . . . . . . 7 (𝜑 → (♯‘((0...𝐵) × (0...𝐵))) = ((♯‘(0...𝐵)) · (♯‘(0...𝐵))))
238234, 237breqtrrd 5171 . . . . . 6 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < (♯‘((0...𝐵) × (0...𝐵))))
239 ovexd 7466 . . . . . . . . . . 11 (𝜑 → (0...𝐵) ∈ V)
240239, 239jca 511 . . . . . . . . . 10 (𝜑 → ((0...𝐵) ∈ V ∧ (0...𝐵) ∈ V))
241 xpexg 7770 . . . . . . . . . 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 3983 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ((0...𝐵) × (0...𝐵))) → 𝑤 ∈ (ℕ0 × ℕ0))
246 simpr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ((0...𝐵) × (0...𝐵))) → 𝑤 ∈ ((0...𝐵) × (0...𝐵)))
247244, 245, 246fnfvimad 7254 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ((0...𝐵) × (0...𝐵))) → (𝐸𝑤) ∈ (𝐸 “ ((0...𝐵) × (0...𝐵))))
248 eqid 2737 . . . . . . . . . . . . . 14 (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)) = (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤))
249247, 248fmptd 7134 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)):((0...𝐵) × (0...𝐵))⟶(𝐸 “ ((0...𝐵) × (0...𝐵))))
250119, 109feqresmpt 6978 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 ↾ ((0...𝐵) × (0...𝐵))) = (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)))
251250feq1d 6720 . . . . . . . . . . . . 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 6812 . . . . . . . . . . . 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 1373 . . . . . . . . . . 11 (𝜑 → (𝐸 ↾ ((0...𝐵) × (0...𝐵))):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵))))
255 eqidd 2738 . . . . . . . . . . . 12 (𝜑 → ((0...𝐵) × (0...𝐵)) = ((0...𝐵) × (0...𝐵)))
256 eqidd 2738 . . . . . . . . . . . 12 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) = (𝐸 “ ((0...𝐵) × (0...𝐵))))
257250, 255, 256f1eq123d 6840 . . . . . . . . . . 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 5698 . . . . . . . . . . . 12 (𝐸 “ ((0...𝐵) × (0...𝐵))) = ran (𝐸 ↾ ((0...𝐵) × (0...𝐵)))
260259a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) = ran (𝐸 ↾ ((0...𝐵) × (0...𝐵))))
261250rneqd 5949 . . . . . . . . . . 11 (𝜑 → ran (𝐸 ↾ ((0...𝐵) × (0...𝐵))) = ran (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸𝑤)))
262260, 261eqtr2d 2778 . . . . . . . . . 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 6857 . . . . . . . . 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 6836 . . . . . . . 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 14390 . . . . . . . 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 5169 . . . . 5 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵)))))
272125fveq2d 6910 . . . . 5 (𝜑 → (♯‘𝐶) = (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵)))))
273271, 272breqtrrd 5171 . . . 4 (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 × ℕ0)))) < (♯‘𝐶))
274 zringbas 21464 . . . . . . . . . 10 ℤ = (Base‘ℤring)
275 eqid 2737 . . . . . . . . . 10 (Base‘(ℤ/nℤ‘𝑅)) = (Base‘(ℤ/nℤ‘𝑅))
276274, 275rhmf 20485 . . . . . . . . 9 (𝐿 ∈ (ℤring RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
277198, 276syl 17 . . . . . . . 8 (𝜑𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅)))
278277ffnd 6737 . . . . . . 7 (𝜑𝐿 Fn ℤ)
279278adantr 480 . . . . . 6 ((𝜑𝑡𝐶) → 𝐿 Fn ℤ)
280 resss 6019 . . . . . . . . . . . 12 (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ 𝐸
281280a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ 𝐸)
282 rnss 5950 . . . . . . . . . . 11 ((𝐸 ↾ (ℕ0 × ℕ0)) ⊆ 𝐸 → ran (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ ran 𝐸)
283281, 282syl 17 . . . . . . . . . 10 (𝜑 → ran (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ ran 𝐸)
284 df-ima 5698 . . . . . . . . . . . 12 (𝐸 “ (ℕ0 × ℕ0)) = ran (𝐸 ↾ (ℕ0 × ℕ0))
285284a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) = ran (𝐸 ↾ (ℕ0 × ℕ0)))
286285sseq1d 4015 . . . . . . . . . 10 (𝜑 → ((𝐸 “ (ℕ0 × ℕ0)) ⊆ ran 𝐸 ↔ ran (𝐸 ↾ (ℕ0 × ℕ0)) ⊆ ran 𝐸))
287283, 286mpbird 257 . . . . . . . . 9 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ran 𝐸)
288 frn 6743 . . . . . . . . . 10 (𝐸:(ℕ0 × ℕ0)⟶ℕ → ran 𝐸 ⊆ ℕ)
289119, 288syl 17 . . . . . . . . 9 (𝜑 → ran 𝐸 ⊆ ℕ)
290287, 289sstrd 3994 . . . . . . . 8 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℕ)
291 nnssz 12635 . . . . . . . . 9 ℕ ⊆ ℤ
292291a1i 11 . . . . . . . 8 (𝜑 → ℕ ⊆ ℤ)
293290, 292sstrd 3994 . . . . . . 7 (𝜑 → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℤ)
294293adantr 480 . . . . . 6 ((𝜑𝑡𝐶) → (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℤ)
295125sseq1d 4015 . . . . . . . . 9 (𝜑 → (𝐶 ⊆ (𝐸 “ (ℕ0 × ℕ0)) ↔ (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ (𝐸 “ (ℕ0 × ℕ0))))
296111, 295mpbird 257 . . . . . . . 8 (𝜑𝐶 ⊆ (𝐸 “ (ℕ0 × ℕ0)))
297296sseld 3982 . . . . . . 7 (𝜑 → (𝑡𝐶𝑡 ∈ (𝐸 “ (ℕ0 × ℕ0))))
298297imp 406 . . . . . 6 ((𝜑𝑡𝐶) → 𝑡 ∈ (𝐸 “ (ℕ0 × ℕ0)))
299 fnfvima 7253 . . . . . 6 ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ0 × ℕ0)) ⊆ ℤ ∧ 𝑡 ∈ (𝐸 “ (ℕ0 × ℕ0))) → (𝐿𝑡) ∈ (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))
300279, 294, 298, 299syl3anc 1373 . . . . 5 ((𝜑𝑡𝐶) → (𝐿𝑡) ∈ (𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))
301 eqid 2737 . . . . 5 (𝑡𝐶 ↦ (𝐿𝑡)) = (𝑡𝐶 ↦ (𝐿𝑡))
302300, 301fmptd 7134 . . . 4 (𝜑 → (𝑡𝐶 ↦ (𝐿𝑡)):𝐶⟶(𝐿 “ (𝐸 “ (ℕ0 × ℕ0))))
303 nnssre 12270 . . . . . 6 ℕ ⊆ ℝ
304303a1i 11 . . . . 5 (𝜑 → ℕ ⊆ ℝ)
305127, 304sstrd 3994 . . . 4 (𝜑𝐶 ⊆ ℝ)
306192, 202, 273, 302, 305hashnexinjle 42130 . . 3 (𝜑 → ∃𝑏𝐶𝑐𝐶 (((𝑡𝐶 ↦ (𝐿𝑡))‘𝑏) = ((𝑡𝐶 ↦ (𝐿𝑡))‘𝑐) ∧ 𝑏 < 𝑐))
307185, 306reximddv2 3215 . 2 (𝜑 → ∃𝑏𝐶𝑐𝐶 (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))))
30850, 307r19.29vva 3216 1 (𝜑 → (♯‘(𝐻 “ (ℕ0m (0...𝐴)))) ≤ (𝑁𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wex 1779  wcel 2108  wne 2940  wral 3061  wrex 3070  Vcvv 3480  wss 3951  c0 4333   class class class wbr 5143  {copab 5205  cmpt 5225   × cxp 5683  ran crn 5686  cres 5687  cima 5688  Fun wfun 6555   Fn wfn 6556  wf 6557  1-1wf1 6558  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  cmpo 7433  m cmap 8866  Fincfn 8985  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  0cn0 12526  cz 12613  cuz 12878  +crp 13034  ...cfz 13547  cfl 13830  cexp 14102  chash 14369  csqrt 15272  cdvds 16290   gcd cgcd 16531  cprime 16708  Basecbs 17247  +gcplusg 17297   Σg cgsu 17485  -gcsg 18953  .gcmg 19085  mulGrpcmgp 20137  Ringcrg 20230  CRingccrg 20231   RingHom crh 20469   RingIso crs 20470  Fieldcfield 20730  ringczring 21457  ℤRHomczrh 21510  chrcchr 21512  ℤ/nczn 21513  algSccascl 21872  var1cv1 22177  Poly1cpl1 22178  eval1ce1 22318   PrimRoots cprimroots 42092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234  ax-mulf 11235
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-ofr 7698  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-tpos 8251  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-ec 8747  df-qs 8751  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-xnn0 12600  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-dvds 16291  df-gcd 16532  df-prm 16709  df-phi 16803  df-pc 16875  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-0g 17486  df-gsum 17487  df-prds 17492  df-pws 17494  df-imas 17553  df-qus 17554  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mhm 18796  df-submnd 18797  df-grp 18954  df-minusg 18955  df-sbg 18956  df-mulg 19086  df-subg 19141  df-nsg 19142  df-eqg 19143  df-ghm 19231  df-cntz 19335  df-od 19546  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-srg 20184  df-ring 20232  df-cring 20233  df-oppr 20334  df-dvdsr 20357  df-unit 20358  df-invr 20388  df-dvr 20401  df-rhm 20472  df-rim 20473  df-nzr 20513  df-subrng 20546  df-subrg 20570  df-rlreg 20694  df-domn 20695  df-idom 20696  df-drng 20731  df-field 20732  df-lmod 20860  df-lss 20930  df-lsp 20970  df-sra 21172  df-rgmod 21173  df-lidl 21218  df-rsp 21219  df-2idl 21260  df-cnfld 21365  df-zring 21458  df-zrh 21514  df-chr 21516  df-zn 21517  df-assa 21873  df-asp 21874  df-ascl 21875  df-psr 21929  df-mvr 21930  df-mpl 21931  df-opsr 21933  df-evls 22098  df-evl 22099  df-psr1 22181  df-vr1 22182  df-ply1 22183  df-coe1 22184  df-evl1 22320  df-mdeg 26094  df-deg1 26095  df-mon1 26170  df-uc1p 26171  df-q1p 26172  df-r1p 26173  df-primroots 42093
This theorem is referenced by:  aks6d1c7lem2  42182
  Copyright terms: Public domain W3C validator