| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → ((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶)) |
| 2 | | simprl 771 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → 𝑏 < 𝑐) |
| 3 | 1, 2 | jca 511 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐)) |
| 4 | | simprr 773 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))) |
| 5 | 3, 4 | jca 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) |
| 9 | 8 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝐾 ∈ Field) |
| 10 | | aks6d1c2a.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 11 | 10 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑃 ∈ ℙ) |
| 12 | | aks6d1c2a.5 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ ℕ) |
| 13 | 12 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑅 ∈ ℕ) |
| 14 | | aks6d1c2a.6 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 15 | 14 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑁 ∈ ℕ) |
| 16 | | aks6d1c2a.7 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∥ 𝑁) |
| 17 | 16 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑃 ∥ 𝑁) |
| 18 | | aks6d1c2a.8 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) |
| 19 | 18 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (𝑁 gcd 𝑅) = 1) |
| 20 | | 0nn0 12541 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
| 21 | 20 | a1i 11 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) ∧ 𝑗 ∈ (0...𝐴)) → 0 ∈
ℕ0) |
| 22 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑗 ∈ (0...𝐴) ↦ 0) = (𝑗 ∈ (0...𝐴) ↦ 0) |
| 23 | 21, 22 | fmptd 7134 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (𝑗 ∈ (0...𝐴) ↦ 0):(0...𝐴)⟶ℕ0) |
| 24 | | aks6d1c2a.10 |
. . . . . . 7
⊢ 𝐺 = (𝑔 ∈ (ℕ0
↑m (0...𝐴))
↦ ((mulGrp‘(Poly1‘𝐾)) Σg (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖)(.g‘(mulGrp‘(Poly1‘𝐾)))((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑖))))))) |
| 25 | | aks6d1c2a.11 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℕ0) |
| 26 | 25 | ad5antr 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‘𝐾)‘𝑎)))) |
| 30 | 29 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → ∀𝑎 ∈ (1...𝐴)𝑁 ∼
((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) |
| 31 | | aks6d1c2a.15 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) |
| 32 | 31 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) |
| 33 | | aks6d1c2a.16 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) |
| 34 | 33 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) |
| 35 | | aks6d1c2a.17 |
. . . . . . 7
⊢ 𝐻 = (ℎ ∈ (ℕ0
↑m (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
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → 𝑐 = (𝑏 + (𝑑 · 𝑅))) |
| 46 | 6, 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, 45 | aks6d1c2lem4 42128 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) ∧ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴)))) ≤ (𝑁↑𝐵)) |
| 47 | 46 | ex 412 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ 𝑑 ∈ ℕ) → (𝑐 = (𝑏 + (𝑑 · 𝑅)) → (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴)))) ≤ (𝑁↑𝐵))) |
| 48 | 47 | rexlimdva 3155 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) → (∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)) → (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴)))) ≤ (𝑁↑𝐵))) |
| 49 | 48 | imp 406 |
. . 3
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ 𝑏 < 𝑐) ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))) → (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴)))) ≤ (𝑁↑𝐵)) |
| 50 | 5, 49 | syl 17 |
. 2
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) → (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴)))) ≤ (𝑁↑𝐵)) |
| 51 | | simprr 773 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑏 < 𝑐) |
| 52 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑠(𝐿‘𝑡) |
| 53 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡(𝐿‘𝑠) |
| 54 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → (𝐿‘𝑡) = (𝐿‘𝑠)) |
| 55 | 52, 53, 54 | cbvmpt 5253 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡)) = (𝑠 ∈ 𝐶 ↦ (𝐿‘𝑠)) |
| 56 | 55 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡)) = (𝑠 ∈ 𝐶 ↦ (𝐿‘𝑠))) |
| 57 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑏) → 𝑠 = 𝑏) |
| 58 | 57 | fveq2d 6910 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑏) → (𝐿‘𝑠) = (𝐿‘𝑏)) |
| 59 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑏 ∈ 𝐶) |
| 60 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿‘𝑏) ∈ V) |
| 61 | 56, 58, 59, 60 | fvmptd 7023 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = (𝐿‘𝑏)) |
| 62 | 61 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏)) |
| 63 | | simprl 771 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐)) |
| 64 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑐) → 𝑠 = 𝑐) |
| 65 | 64 | fveq2d 6910 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ 𝑠 = 𝑐) → (𝐿‘𝑠) = (𝐿‘𝑐)) |
| 66 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑐 ∈ 𝐶) |
| 67 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿‘𝑐) ∈ V) |
| 68 | 56, 65, 66, 67 | fvmptd 7023 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) = (𝐿‘𝑐)) |
| 69 | 63, 68 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = (𝐿‘𝑐)) |
| 70 | 62, 69 | eqtrd 2777 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿‘𝑏) = (𝐿‘𝑐)) |
| 71 | 70 | eqcomd 2743 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝐿‘𝑐) = (𝐿‘𝑏)) |
| 72 | 12 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈
ℕ0) |
| 73 | 72 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐶) → 𝑅 ∈
ℕ0) |
| 74 | 73 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) → 𝑅 ∈
ℕ0) |
| 75 | 74 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∈
ℕ0) |
| 76 | | fz0ssnn0 13662 |
. . . . . . . . . . . . . . . . . 18
⊢
(0...𝐵) ⊆
ℕ0 |
| 77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0...𝐵) ⊆
ℕ0) |
| 78 | 77, 77 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((0...𝐵) ⊆ ℕ0 ∧
(0...𝐵) ⊆
ℕ0)) |
| 79 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅) |
| 80 | 14, 10, 16, 12, 18, 27, 28, 79 | hashscontpowcl 42121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ0) |
| 81 | 80 | nn0red 12588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℝ) |
| 82 | 80 | nn0ge0d 12590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 0 ≤
(♯‘(𝐿 “
(𝐸 “
(ℕ0 × ℕ0))))) |
| 83 | 81, 82 | resqrtcld 15456 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℝ) |
| 84 | 83 | flcld 13838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 →
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℤ) |
| 85 | 81, 82 | sqrtge0d 15459 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ≤
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 86 | | 0zd 12625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 0 ∈
ℤ) |
| 87 | | flge 13845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ↔ 0 ≤
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 88 | 83, 86, 87 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (0 ≤
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ↔ 0 ≤
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 89 | 85, 88 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 0 ≤
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 90 | 84, 89 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 →
((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℤ ∧ 0 ≤
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 91 | | elnn0z 12626 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℕ0 ↔
((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℤ ∧ 0 ≤
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 92 | 90, 91 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 →
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℕ0) |
| 93 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐵 =
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 94 | 93 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐵 ∈ ℕ0 ↔
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℕ0)) |
| 95 | 92, 94 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
| 96 | 95 | nn0ge0d 12590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ≤ 𝐵) |
| 97 | 95 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐵 ∈ ℤ) |
| 98 | | eluz 12892 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ ℤ ∧ 𝐵
∈ ℤ) → (𝐵
∈ (ℤ≥‘0) ↔ 0 ≤ 𝐵)) |
| 99 | 86, 97, 98 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐵 ∈ (ℤ≥‘0)
↔ 0 ≤ 𝐵)) |
| 100 | 96, 99 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐵 ∈
(ℤ≥‘0)) |
| 101 | | fzn0 13578 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((0...𝐵) ≠
∅ ↔ 𝐵 ∈
(ℤ≥‘0)) |
| 102 | 100, 101 | sylibr 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (0...𝐵) ≠ ∅) |
| 103 | 102, 102 | jca 511 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((0...𝐵) ≠ ∅ ∧ (0...𝐵) ≠ ∅)) |
| 104 | | xpnz 6179 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((0...𝐵) ≠
∅ ∧ (0...𝐵) ≠
∅) ↔ ((0...𝐵)
× (0...𝐵)) ≠
∅) |
| 105 | 104 | biimpi 216 |
. . . . . . . . . . . . . . . . . 18
⊢
(((0...𝐵) ≠
∅ ∧ (0...𝐵) ≠
∅) → ((0...𝐵)
× (0...𝐵)) ≠
∅) |
| 106 | 103, 105 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...𝐵) × (0...𝐵)) ≠ ∅) |
| 107 | | ssxpb 6194 |
. . . . . . . . . . . . . . . . 17
⊢
(((0...𝐵) ×
(0...𝐵)) ≠ ∅
→ (((0...𝐵) ×
(0...𝐵)) ⊆
(ℕ0 × ℕ0) ↔ ((0...𝐵) ⊆ ℕ0
∧ (0...𝐵) ⊆
ℕ0))) |
| 108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((0...𝐵) × (0...𝐵)) ⊆ (ℕ0 ×
ℕ0) ↔ ((0...𝐵) ⊆ ℕ0 ∧
(0...𝐵) ⊆
ℕ0))) |
| 109 | 78, 108 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((0...𝐵) × (0...𝐵)) ⊆ (ℕ0 ×
ℕ0)) |
| 110 | | imass2 6120 |
. . . . . . . . . . . . . . 15
⊢
(((0...𝐵) ×
(0...𝐵)) ⊆
(ℕ0 × ℕ0) → (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ (𝐸 “ (ℕ0 ×
ℕ0))) |
| 111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ (𝐸 “ (ℕ0 ×
ℕ0))) |
| 112 | | nfv 1914 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑜𝜑 |
| 113 | | aks6d1c2a.20 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁 ∧ 𝑃 ≠ 𝑄)) |
| 114 | 113 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑄 ∈ ℙ) |
| 115 | 113 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑄 ∥ 𝑁) |
| 116 | 113 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
| 117 | 14, 10, 16, 27, 114, 115, 116 | aks6d1c2p2 42120 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐸:(ℕ0 ×
ℕ0)–1-1→ℕ) |
| 118 | | f1f 6804 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸:(ℕ0 ×
ℕ0)–1-1→ℕ → 𝐸:(ℕ0 ×
ℕ0)⟶ℕ) |
| 119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸:(ℕ0 ×
ℕ0)⟶ℕ) |
| 120 | 119 | ffnd 6737 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 Fn (ℕ0 ×
ℕ0)) |
| 121 | 120 | fnfund 6669 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun 𝐸) |
| 122 | 119 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑜 ∈ (ℕ0 ×
ℕ0)) → (𝐸‘𝑜) ∈ ℕ) |
| 123 | 112, 121,
122 | funimassd 6975 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ℕ) |
| 124 | 111, 123 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ ℕ) |
| 125 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 = (𝐸 “ ((0...𝐵) × (0...𝐵)))) |
| 126 | 125 | sseq1d 4015 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 ⊆ ℕ ↔ (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ ℕ)) |
| 127 | 124, 126 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ⊆ ℕ) |
| 128 | 127 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) → 𝐶 ⊆ ℕ) |
| 129 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) → 𝑐 ∈ 𝐶) |
| 130 | 128, 129 | sseldd 3984 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) → 𝑐 ∈ ℕ) |
| 131 | 130 | nnzd 12640 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) → 𝑐 ∈ ℤ) |
| 132 | 131 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑐 ∈ ℤ) |
| 133 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) → 𝑏 ∈ 𝐶) |
| 134 | 128, 133 | sseldd 3984 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) → 𝑏 ∈ ℕ) |
| 135 | 134 | nnzd 12640 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) → 𝑏 ∈ ℤ) |
| 136 | 135 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑏 ∈ ℤ) |
| 137 | 79, 28 | zndvds 21568 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℕ0
∧ 𝑐 ∈ ℤ
∧ 𝑏 ∈ ℤ)
→ ((𝐿‘𝑐) = (𝐿‘𝑏) ↔ 𝑅 ∥ (𝑐 − 𝑏))) |
| 138 | 75, 132, 136, 137 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ((𝐿‘𝑐) = (𝐿‘𝑏) ↔ 𝑅 ∥ (𝑐 − 𝑏))) |
| 139 | 71, 138 | mpbid 232 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∥ (𝑐 − 𝑏)) |
| 140 | 75 | nn0zd 12639 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∈ ℤ) |
| 141 | 132, 136 | zsubcld 12727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑐 − 𝑏) ∈ ℤ) |
| 142 | | divides 16292 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℤ ∧ (𝑐 − 𝑏) ∈ ℤ) → (𝑅 ∥ (𝑐 − 𝑏) ↔ ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐 − 𝑏))) |
| 143 | 140, 141,
142 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑅 ∥ (𝑐 − 𝑏) ↔ ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐 − 𝑏))) |
| 144 | 143 | biimpd 229 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑅 ∥ (𝑐 − 𝑏) → ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐 − 𝑏))) |
| 145 | 139, 144 | mpd 15 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ∃𝑑 ∈ ℤ (𝑑 · 𝑅) = (𝑐 − 𝑏)) |
| 146 | | simprl 771 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑑 ∈ ℤ) |
| 147 | 130 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑐 ∈ ℕ) |
| 148 | 147 | nnred 12281 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑐 ∈ ℝ) |
| 149 | 134 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑏 ∈ ℕ) |
| 150 | 149 | nnred 12281 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑏 ∈ ℝ) |
| 151 | 148, 150 | resubcld 11691 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑐 − 𝑏) ∈ ℝ) |
| 152 | 12 | nnrpd 13075 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
| 153 | 152 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐶) → 𝑅 ∈
ℝ+) |
| 154 | 153 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) → 𝑅 ∈
ℝ+) |
| 155 | 154 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → 𝑅 ∈
ℝ+) |
| 156 | 155 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑅 ∈
ℝ+) |
| 157 | 156 | rpred 13077 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑅 ∈ ℝ) |
| 158 | 51 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑏 < 𝑐) |
| 159 | 150, 148 | posdifd 11850 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑏 < 𝑐 ↔ 0 < (𝑐 − 𝑏))) |
| 160 | 158, 159 | mpbid 232 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 0 < (𝑐 − 𝑏)) |
| 161 | 156 | rpgt0d 13080 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 0 < 𝑅) |
| 162 | 151, 157,
160, 161 | divgt0d 12203 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 0 < ((𝑐 − 𝑏) / 𝑅)) |
| 163 | 157 | recnd 11289 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑅 ∈ ℂ) |
| 164 | 146 | zred 12722 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑑 ∈ ℝ) |
| 165 | 164 | recnd 11289 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑑 ∈ ℂ) |
| 166 | 163, 165 | mulcomd 11282 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑅 · 𝑑) = (𝑑 · 𝑅)) |
| 167 | | simprr 773 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑑 · 𝑅) = (𝑐 − 𝑏)) |
| 168 | 166, 167 | eqtrd 2777 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑅 · 𝑑) = (𝑐 − 𝑏)) |
| 169 | 151 | recnd 11289 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑐 − 𝑏) ∈ ℂ) |
| 170 | 161 | gt0ne0d 11827 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑅 ≠ 0) |
| 171 | 169, 163,
165, 170 | divmuld 12065 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (((𝑐 − 𝑏) / 𝑅) = 𝑑 ↔ (𝑅 · 𝑑) = (𝑐 − 𝑏))) |
| 172 | 168, 171 | mpbird 257 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → ((𝑐 − 𝑏) / 𝑅) = 𝑑) |
| 173 | 162, 172 | breqtrd 5169 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 0 < 𝑑) |
| 174 | 146, 173 | jca 511 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑑 ∈ ℤ ∧ 0 < 𝑑)) |
| 175 | | elnnz 12623 |
. . . . . 6
⊢ (𝑑 ∈ ℕ ↔ (𝑑 ∈ ℤ ∧ 0 <
𝑑)) |
| 176 | 174, 175 | sylibr 234 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑑 ∈ ℕ) |
| 177 | 167 | eqcomd 2743 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑐 − 𝑏) = (𝑑 · 𝑅)) |
| 178 | 148 | recnd 11289 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑐 ∈ ℂ) |
| 179 | 150 | recnd 11289 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑏 ∈ ℂ) |
| 180 | 167, 169 | eqeltrd 2841 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑑 · 𝑅) ∈ ℂ) |
| 181 | 178, 179,
180 | subaddd 11638 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → ((𝑐 − 𝑏) = (𝑑 · 𝑅) ↔ (𝑏 + (𝑑 · 𝑅)) = 𝑐)) |
| 182 | 177, 181 | mpbid 232 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → (𝑏 + (𝑑 · 𝑅)) = 𝑐) |
| 183 | 182 | eqcomd 2743 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) ∧ (𝑑 ∈ ℤ ∧ (𝑑 · 𝑅) = (𝑐 − 𝑏))) → 𝑐 = (𝑏 + (𝑑 · 𝑅))) |
| 184 | 145, 176,
183 | reximssdv 3173 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅))) |
| 185 | 51, 184 | jca 511 |
. . 3
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐶) ∧ 𝑐 ∈ 𝐶) ∧ (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) → (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) |
| 186 | | fzfid 14014 |
. . . . . . 7
⊢ (𝜑 → (0...𝐵) ∈ Fin) |
| 187 | | xpfi 9358 |
. . . . . . 7
⊢
(((0...𝐵) ∈ Fin
∧ (0...𝐵) ∈ Fin)
→ ((0...𝐵) ×
(0...𝐵)) ∈
Fin) |
| 188 | 186, 186,
187 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((0...𝐵) × (0...𝐵)) ∈ Fin) |
| 189 | | imafi 9353 |
. . . . . 6
⊢ ((Fun
𝐸 ∧ ((0...𝐵) × (0...𝐵)) ∈ Fin) → (𝐸 “ ((0...𝐵) × (0...𝐵))) ∈ Fin) |
| 190 | 121, 188,
189 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) ∈ Fin) |
| 191 | 125 | eleq1d 2826 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ Fin ↔ (𝐸 “ ((0...𝐵) × (0...𝐵))) ∈ Fin)) |
| 192 | 190, 191 | mpbird 257 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Fin) |
| 193 | 79 | zncrng 21563 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℕ0
→ (ℤ/nℤ‘𝑅) ∈ CRing) |
| 194 | 72, 193 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(ℤ/nℤ‘𝑅) ∈ CRing) |
| 195 | | crngring 20242 |
. . . . . . . . 9
⊢
((ℤ/nℤ‘𝑅) ∈ CRing →
(ℤ/nℤ‘𝑅) ∈ Ring) |
| 196 | 194, 195 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ/nℤ‘𝑅) ∈ Ring) |
| 197 | 28 | zrhrhm 21522 |
. . . . . . . 8
⊢
((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤring RingHom
(ℤ/nℤ‘𝑅))) |
| 198 | 196, 197 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (ℤring RingHom
(ℤ/nℤ‘𝑅))) |
| 199 | 198 | imaexd 7938 |
. . . . . 6
⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ V) |
| 200 | | hashclb 14397 |
. . . . . 6
⊢ ((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ V → ((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ Fin ↔ (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ0)) |
| 201 | 199, 200 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ Fin ↔ (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ0)) |
| 202 | 80, 201 | mpbird 257 |
. . . 4
⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ Fin) |
| 203 | | hashcl 14395 |
. . . . . . . . . . . . 13
⊢ ((𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ Fin → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ0) |
| 204 | 202, 203 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ0) |
| 205 | 204 | nn0red 12588 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℝ) |
| 206 | 204 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤
(♯‘(𝐿 “
(𝐸 “
(ℕ0 × ℕ0))))) |
| 207 | | sqrtmsq 15309 |
. . . . . . . . . . 11
⊢
(((♯‘(𝐿
“ (𝐸 “
(ℕ0 × ℕ0)))) ∈ ℝ ∧ 0
≤ (♯‘(𝐿
“ (𝐸 “
(ℕ0 × ℕ0))))) →
(√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) = (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) |
| 208 | 205, 206,
207 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 →
(√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) = (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) |
| 209 | 208 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) = (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 210 | 205, 206 | jca 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))))))) |
| 212 | 210, 210,
211 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 →
(√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) = ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 213 | 205, 206 | resqrtcld 15456 |
. . . . . . . . . . 11
⊢ (𝜑 →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℝ) |
| 214 | 213 | flcld 13838 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℤ) |
| 215 | 205, 206 | sqrtge0d 15459 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ≤
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 216 | 213, 86, 87 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0 ≤
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ↔ 0 ≤
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 217 | 215, 216 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 218 | 214, 217 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℤ ∧ 0 ≤
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 219 | 218, 91 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℕ0) |
| 220 | 219, 94 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
| 221 | 220 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 222 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
| 223 | 221, 222 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 + 1) ∈ ℝ) |
| 224 | | flltp1 13840 |
. . . . . . . . . . . . 13
⊢
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℝ →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) <
((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) + 1)) |
| 225 | 213, 224 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) <
((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) + 1)) |
| 226 | 93 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 + 1) =
((⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) + 1)) |
| 227 | 225, 226 | breqtrrd 5171 |
. . . . . . . . . . 11
⊢ (𝜑 →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) < (𝐵 + 1)) |
| 228 | 213, 223,
213, 223, 215, 227, 215, 227 | ltmul12ad 12209 |
. . . . . . . . . 10
⊢ (𝜑 →
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) < ((𝐵 + 1) · (𝐵 + 1))) |
| 229 | 212, 228 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ (𝜑 →
(√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) < ((𝐵 + 1) · (𝐵 + 1))) |
| 230 | 209, 229 | eqbrtrd 5165 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) < ((𝐵 + 1) · (𝐵 + 1))) |
| 231 | | hashfz0 14471 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℕ0
→ (♯‘(0...𝐵)) = (𝐵 + 1)) |
| 232 | 220, 231 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(0...𝐵)) = (𝐵 + 1)) |
| 233 | 232, 232 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(0...𝐵)) ·
(♯‘(0...𝐵))) =
((𝐵 + 1) · (𝐵 + 1))) |
| 234 | 230, 233 | breqtrrd 5171 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) < ((♯‘(0...𝐵)) · (♯‘(0...𝐵)))) |
| 235 | 186, 186 | jca 511 |
. . . . . . . 8
⊢ (𝜑 → ((0...𝐵) ∈ Fin ∧ (0...𝐵) ∈ Fin)) |
| 236 | | hashxp 14473 |
. . . . . . . 8
⊢
(((0...𝐵) ∈ Fin
∧ (0...𝐵) ∈ Fin)
→ (♯‘((0...𝐵) × (0...𝐵))) = ((♯‘(0...𝐵)) · (♯‘(0...𝐵)))) |
| 237 | 235, 236 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘((0...𝐵) × (0...𝐵))) = ((♯‘(0...𝐵)) · (♯‘(0...𝐵)))) |
| 238 | 234, 237 | breqtrrd 5171 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) < (♯‘((0...𝐵) × (0...𝐵)))) |
| 239 | | ovexd 7466 |
. . . . . . . . . . 11
⊢ (𝜑 → (0...𝐵) ∈ V) |
| 240 | 239, 239 | jca 511 |
. . . . . . . . . 10
⊢ (𝜑 → ((0...𝐵) ∈ V ∧ (0...𝐵) ∈ V)) |
| 241 | | xpexg 7770 |
. . . . . . . . . 10
⊢
(((0...𝐵) ∈ V
∧ (0...𝐵) ∈ V)
→ ((0...𝐵) ×
(0...𝐵)) ∈
V) |
| 242 | 240, 241 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((0...𝐵) × (0...𝐵)) ∈ V) |
| 243 | 242 | mptexd 7244 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤)) ∈ V) |
| 244 | 120 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ((0...𝐵) × (0...𝐵))) → 𝐸 Fn (ℕ0 ×
ℕ0)) |
| 245 | 109 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ((0...𝐵) × (0...𝐵))) → 𝑤 ∈ (ℕ0 ×
ℕ0)) |
| 246 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ((0...𝐵) × (0...𝐵))) → 𝑤 ∈ ((0...𝐵) × (0...𝐵))) |
| 247 | 244, 245,
246 | fnfvimad 7254 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ ((0...𝐵) × (0...𝐵))) → (𝐸‘𝑤) ∈ (𝐸 “ ((0...𝐵) × (0...𝐵)))) |
| 248 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤)) = (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤)) |
| 249 | 247, 248 | fmptd 7134 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤)):((0...𝐵) × (0...𝐵))⟶(𝐸 “ ((0...𝐵) × (0...𝐵)))) |
| 250 | 119, 109 | feqresmpt 6978 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸 ↾ ((0...𝐵) × (0...𝐵))) = (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤))) |
| 251 | 250 | feq1d 6720 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸 ↾ ((0...𝐵) × (0...𝐵))):((0...𝐵) × (0...𝐵))⟶(𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤)):((0...𝐵) × (0...𝐵))⟶(𝐸 “ ((0...𝐵) × (0...𝐵))))) |
| 252 | 249, 251 | mpbird 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...𝐵)))) |
| 254 | 117, 109,
252, 253 | syl3anc 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...𝐵)))) |
| 257 | 250, 255,
256 | f1eq123d 6840 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 ↾ ((0...𝐵) × (0...𝐵))):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵))) ↔ (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤)):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵))))) |
| 258 | 254, 257 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤)):((0...𝐵) × (0...𝐵))–1-1→(𝐸 “ ((0...𝐵) × (0...𝐵)))) |
| 259 | | df-ima 5698 |
. . . . . . . . . . . 12
⊢ (𝐸 “ ((0...𝐵) × (0...𝐵))) = ran (𝐸 ↾ ((0...𝐵) × (0...𝐵))) |
| 260 | 259 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 “ ((0...𝐵) × (0...𝐵))) = ran (𝐸 ↾ ((0...𝐵) × (0...𝐵)))) |
| 261 | 250 | rneqd 5949 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝐸 ↾ ((0...𝐵) × (0...𝐵))) = ran (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤))) |
| 262 | 260, 261 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑤 ∈ ((0...𝐵) × (0...𝐵)) ↦ (𝐸‘𝑤)) = (𝐸 “ ((0...𝐵) × (0...𝐵)))) |
| 263 | 258, 262 | jca 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...𝐵))))) |
| 265 | 263, 264 | sylibr 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...𝐵))))) |
| 267 | 243, 265,
266 | spcedv 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...𝐵)))))) |
| 269 | 242, 268 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∃𝑢 𝑢:((0...𝐵) × (0...𝐵))–1-1-onto→(𝐸 “ ((0...𝐵) × (0...𝐵))) → (♯‘((0...𝐵) × (0...𝐵))) = (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵)))))) |
| 270 | 267, 269 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (♯‘((0...𝐵) × (0...𝐵))) = (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵))))) |
| 271 | 238, 270 | breqtrd 5169 |
. . . . 5
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) < (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵))))) |
| 272 | 125 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (♯‘𝐶) = (♯‘(𝐸 “ ((0...𝐵) × (0...𝐵))))) |
| 273 | 271, 272 | breqtrrd 5171 |
. . . 4
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) < (♯‘𝐶)) |
| 274 | | zringbas 21464 |
. . . . . . . . . 10
⊢ ℤ =
(Base‘ℤring) |
| 275 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(ℤ/nℤ‘𝑅)) =
(Base‘(ℤ/nℤ‘𝑅)) |
| 276 | 274, 275 | rhmf 20485 |
. . . . . . . . 9
⊢ (𝐿 ∈ (ℤring
RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅))) |
| 277 | 198, 276 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅))) |
| 278 | 277 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝐿 Fn ℤ) |
| 279 | 278 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐶) → 𝐿 Fn ℤ) |
| 280 | | resss 6019 |
. . . . . . . . . . . 12
⊢ (𝐸 ↾ (ℕ0
× ℕ0)) ⊆ 𝐸 |
| 281 | 280 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ↾ (ℕ0 ×
ℕ0)) ⊆ 𝐸) |
| 282 | | rnss 5950 |
. . . . . . . . . . 11
⊢ ((𝐸 ↾ (ℕ0
× ℕ0)) ⊆ 𝐸 → ran (𝐸 ↾ (ℕ0 ×
ℕ0)) ⊆ ran 𝐸) |
| 283 | 281, 282 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝐸 ↾ (ℕ0 ×
ℕ0)) ⊆ ran 𝐸) |
| 284 | | df-ima 5698 |
. . . . . . . . . . . 12
⊢ (𝐸 “ (ℕ0
× ℕ0)) = ran (𝐸 ↾ (ℕ0 ×
ℕ0)) |
| 285 | 284 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) = ran (𝐸 ↾ (ℕ0 ×
ℕ0))) |
| 286 | 285 | sseq1d 4015 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ran 𝐸 ↔ ran (𝐸 ↾ (ℕ0 ×
ℕ0)) ⊆ ran 𝐸)) |
| 287 | 283, 286 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ran 𝐸) |
| 288 | | frn 6743 |
. . . . . . . . . 10
⊢ (𝐸:(ℕ0 ×
ℕ0)⟶ℕ → ran 𝐸 ⊆ ℕ) |
| 289 | 119, 288 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐸 ⊆ ℕ) |
| 290 | 287, 289 | sstrd 3994 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ℕ) |
| 291 | | nnssz 12635 |
. . . . . . . . 9
⊢ ℕ
⊆ ℤ |
| 292 | 291 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℕ ⊆
ℤ) |
| 293 | 290, 292 | sstrd 3994 |
. . . . . . 7
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ℤ) |
| 294 | 293 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐶) → (𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ℤ) |
| 295 | 125 | sseq1d 4015 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ⊆ (𝐸 “ (ℕ0 ×
ℕ0)) ↔ (𝐸 “ ((0...𝐵) × (0...𝐵))) ⊆ (𝐸 “ (ℕ0 ×
ℕ0)))) |
| 296 | 111, 295 | mpbird 257 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ⊆ (𝐸 “ (ℕ0 ×
ℕ0))) |
| 297 | 296 | sseld 3982 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ 𝐶 → 𝑡 ∈ (𝐸 “ (ℕ0 ×
ℕ0)))) |
| 298 | 297 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐶) → 𝑡 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) |
| 299 | | fnfvima 7253 |
. . . . . 6
⊢ ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ0
× ℕ0)) ⊆ ℤ ∧ 𝑡 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → (𝐿‘𝑡) ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) |
| 300 | 279, 294,
298, 299 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐶) → (𝐿‘𝑡) ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) |
| 301 | | eqid 2737 |
. . . . 5
⊢ (𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡)) = (𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡)) |
| 302 | 300, 301 | fmptd 7134 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡)):𝐶⟶(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) |
| 303 | | nnssre 12270 |
. . . . . 6
⊢ ℕ
⊆ ℝ |
| 304 | 303 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℕ ⊆
ℝ) |
| 305 | 127, 304 | sstrd 3994 |
. . . 4
⊢ (𝜑 → 𝐶 ⊆ ℝ) |
| 306 | 192, 202,
273, 302, 305 | hashnexinjle 42130 |
. . 3
⊢ (𝜑 → ∃𝑏 ∈ 𝐶 ∃𝑐 ∈ 𝐶 (((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑏) = ((𝑡 ∈ 𝐶 ↦ (𝐿‘𝑡))‘𝑐) ∧ 𝑏 < 𝑐)) |
| 307 | 185, 306 | reximddv2 3215 |
. 2
⊢ (𝜑 → ∃𝑏 ∈ 𝐶 ∃𝑐 ∈ 𝐶 (𝑏 < 𝑐 ∧ ∃𝑑 ∈ ℕ 𝑐 = (𝑏 + (𝑑 · 𝑅)))) |
| 308 | 50, 307 | r19.29vva 3216 |
1
⊢ (𝜑 → (♯‘(𝐻 “ (ℕ0
↑m (0...𝐴)))) ≤ (𝑁↑𝐵)) |