English
For every element a of the quadratic integers Z√d, there exists a natural number n such that a ≤ n. In other words, Z√d is Archimedean with respect to its natural order.
Русский
Для каждого элемента a в Z√d существует натуральное число n, такое что a ≤ n. Иными словами, Z√d является Архимедовым по своему естественному порядку.
LaTeX
$$$$\forall a \in \mathbb{Z}\sqrt{d}, \exists n \in \mathbb{N}, a \le n.$$$$
Lean4
theorem le_arch (a : ℤ√d) : ∃ n : ℕ, a ≤ n :=
by
obtain ⟨x, y, (h : a ≤ ⟨x, y⟩)⟩ : ∃ x y : ℕ, Nonneg (⟨x, y⟩ + -a) :=
match -a with
| ⟨Int.ofNat x, Int.ofNat y⟩ => ⟨0, 0, by trivial⟩
| ⟨Int.ofNat x, -[y+1]⟩ => ⟨0, y + 1, by simp [add_def, Int.negSucc_eq, add_assoc]; trivial⟩
| ⟨-[x+1], Int.ofNat y⟩ => ⟨x + 1, 0, by simp [Int.negSucc_eq, add_assoc]; trivial⟩
| ⟨-[x+1], -[y+1]⟩ => ⟨x + 1, y + 1, by simp [Int.negSucc_eq, add_assoc]; trivial⟩
refine ⟨x + d * y, h.trans ?_⟩
change Nonneg ⟨↑x + d * y - ↑x, 0 - ↑y⟩
rcases y with - | y
· simp
trivial
have h : ∀ y, SqLe y d (d * y) 1 := fun y => by
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)
rw [show (x : ℤ) + d * Nat.succ y - x = d * Nat.succ y by simp]
exact h (y + 1)
