lemma A.44 $\R$ is an ordered field

open in the book · appendices/A-long-proofs.tex:3049 · p. 2811

Rests on

depends_on definition 4.32 Field ¶
- depends_on definition 4.11 Inverse element ¶
  - depends_on definition 4.9 Neutral element ¶
    - depends_on definition 4.3 Algebraic structure ¶
      - depends_on definition 4.2 Binary operation ¶
- depends_on definition 4.20 Monoid ¶
  - depends_on definition 4.9 Neutral element ¶ ↺
  - depends_on definition 4.18 Semigroup ¶
    - depends_on definition 4.6 Associativity ¶
      - depends_on definition 4.3 Algebraic structure ¶ ↺
    - depends_on definition 4.4 Internal binary operation; magma ¶
      - depends_on definition 4.3 Algebraic structure ¶ ↺
      - depends_on definition 4.2 Binary operation ¶ ↺
- depends_on definition 4.30 Ring ¶
  - depends_on definition 4.8 Commutativity; abelian structure ¶
    - depends_on definition 4.4 Internal binary operation; magma ¶ ↺
  - depends_on definition 4.28 Distributivity ¶
    - depends_on definition 4.3 Algebraic structure ¶ ↺
  - depends_on definition 4.21 Group ¶
    - depends_on definition 4.11 Inverse element ¶ ↺
    - depends_on definition 4.20 Monoid ¶ ↺
  - depends_on definition 4.18 Semigroup ¶ ↺
depends_on definition A.41 Addition ¶
- depends_on definition A.36 Cut ¶
depends_on definition A.43 Multiplication ¶
- depends_on definition A.41 Addition ¶ ↺
- depends_on definition A.36 Cut ¶ ↺
depends_on lemma A.42 $(\R, +)$ is an ordered abelian group ¶
- depends_on definition A.41 Addition ¶ ↺
- depends_on definition A.38 Order on $\R$ ¶
  - depends_on definition A.36 Cut ¶ ↺
- depends_on lemma A.37 Elementary properties of cuts ¶
  - depends_on definition A.36 Cut ¶ ↺
  - proves proof app:A-long-proofs@proof-27 ¶
- proves proof app:A-long-proofs@proof-30 ¶
proves proof app:A-long-proofs@proof-31 ¶

Supports

Nothing declares a dependency on this node yet.

Neighborhood

Every logical edge within two steps of this node.

declared and complete
partly declared
a check failed
not graded
declared in the source
inferred from structure

Edges

type	direction	node	provenance	where
`depends_on`	→	Field	declared	appendices/A-long-proofs.tex:3053
`depends_on`	→	Addition	declared	appendices/A-long-proofs.tex:3053
`depends_on`	→	Multiplication	declared	appendices/A-long-proofs.tex:3053
`depends_on`	→	$(\R, +)$ is an ordered abelian group	declared	appendices/A-long-proofs.tex:3053
`proves`	←	app:A-long-proofs@proof-31	declared	appendices/A-long-proofs.tex:3056