PROOF 189

Prove.

What each extension loses

On each number system.

What you may use

A1∅ ≠ S ⊆ ℕ ⟹ a least element exists
well-ordering (property of ℕ)
A20 < 1
1 is positive
A3a < b ⟹ a + c < b + c
order and addition
A4no integer n with 0 < n < 1
discreteness (property of ℤ)
A5a < b, 0 < c ⟹ ac < bc
order and multiplication by positives
A60 < a ⟹ 0 < 1/a
the reciprocal of a positive is positive
A7a<b, b<c ⟹ a<c
transitivity of order
A8exactly one of a<b, a=b, b<a
trichotomy of order
A90<a, 0<b ⟹ 0 < ab
order is compatible with multiplication (ordered field)
A10i × i = −1
definition of i (Proof 14)
A11(−a)(−b) = ab
product of negatives (Proof 01)
A12a × 0 = 0
lemma of Proof 01
Fthe computation rules of the four operations
field axioms — associativity, commutativity, distributivity, identities, inverses
Ea = b ⟹ apply the same operation to both sides
properties of equality

Nothing outside this list may be cited.

Theorem T1

In ℕ → ℤ, well-ordering is lost. ℤ has no least element.

Proof.

Related labs