Definition D1
An ordered field is a number system satisfying A1–A8, with a relation < on it satisfying A11–A14.
Proof.
ℚ and ℝ are ordered fields.convention
∎
Definition D2
i is the number satisfying i × i = −1, and ℂ is obtained by adjoining i to ℝ.
Proof.
i is not a number that was found, but a number fixed by this equation.convention
∎
Lemma L1
If a ≠ 0, then 0 < a × a
Proof.
(1)Since a ≠ 0, either 0 < a or a < 0.assumption, A11
(2)If 0 < a, then 0 < a × a.(1), A13
(3)If a < 0, then a + (−a) < 0 + (−a), that is, 0 < −a.(1), A12, A2, A1
(4)Then 0 < (−a)(−a).(3), A13
(5)(−a)(−a) = a × aA10
(6)In either case, 0 < a × a.(2), (4), (5), E
∎
(1)1 ≠ 0A8
(2)0 < 1 × 1(1), L1
(3)1 × 1 = 1A3
(4)0 < 1(2), (3), E
∎
Theorem T1
An ordered field with additive inverses has no least element.
Proof.
(1)Suppose there is a least element m.assumption
(2)0 < 1L2
(3)0 + (−1) < 1 + (−1), that is, −1 < 0(2), A12, A2, A1
(4)m + (−1) < m + 0 = m(3), A12, A1
(5)m + (−1) is also an element of this field.A2, D1
(6)There is an element smaller than m, contradicting (1).(1), (4), (5)
(7)There is no least element. Therefore A15 fails.(6), A15
∎
Theorem T2
An ordered field with multiplicative inverses contains an x with 0 < x < 1.
Proof.
(1)Set 2 = 1 + 1.convention
(2)0 < 1L2
(3)0 + 1 < 1 + 1, that is, 1 < 2(1), (2), A12, A1
(4)0 < 2(2), (3), A14
(5)Since 2 ≠ 0, there is a 2⁻¹ with 2 × 2⁻¹ = 1.(4), A11, A4
(6)If 2⁻¹ = 0, then 1 = 2 × 0 = 0, contradicting A8.(5), A9, A8
(7)0 < 2⁻¹ × 2⁻¹(6), L1
(8)2(2⁻¹ × 2⁻¹) = (2 × 2⁻¹)2⁻¹ = 2⁻¹A5, (5), A3, A6
(9)0 < 2⁻¹(4), (7), (8), A13, E
(10)2⁻¹ + 2⁻¹ = 2⁻¹(1 + 1) = 2⁻¹ × 2 = 1A3, A7, (1), A6, (5)
(11)0 + 2⁻¹ < 2⁻¹ + 2⁻¹, that is, 2⁻¹ < 1(9), (10), A12, A1
(12)0 < 2⁻¹ < 1(9), (11)
∎
Theorem T3
ℂ cannot be an ordered field.
Proof.
(1)Suppose ℂ is an ordered field.assumption, D1
(2)0 < 1L2
(3)0 + (−1) < 1 + (−1), that is, −1 < 0(2), A12, A2, A1
(4)Therefore −1 ≠ 0(3), A11
(5)If i = 0, then i × i = 0, contradicting (4). Therefore i ≠ 0.(4), A9, D2
(6)0 < i × i(5), L1
(7)i × i = −1D2
(8)0 < −1(6), (7), E
(9)(3) and (8) violate A11.(3), (8), A11
(10)ℂ is not an ordered field.(9)
∎