lemma 7.64 Well-ordering of $\N$

open in the book · parts/02-mathematical-methods/05-real-analysis.tex:1513 · p. 225

Rests on

depends_on axiom 3.33 Peano axioms ¶
depends_on axiom 3.34 Principle of induction ¶
proves proof ch:05-real-analysis@proof-41 ¶

Supports

depends_on lemma 7.65 The integer part ¶
- depends_on lemma 7.67 The limit over real exponents ¶
  - depends_on proposition 7.68 The natural base ¶
    - depends_on remark 7.70 What the condition says ¶
- depends_on proposition 7.77 Special values, periodicity, and the kernel ¶
  - depends_on lemma 7.78 Chord, arc, tangent ¶
    - depends_on proposition 7.79 The polygon recursion ¶
      - depends_on corollary 7.81 The decimal expansion of $\pi$ ¶
      - depends_on proposition 7.83 Viète's product ¶
      - depends_on remark 7.82 What Archimedes proved ¶
      - depends_on remark 7.80 Why these are the polygon perimeters ¶
      - depends_on remark 7.84 One construction, two faces ¶
  - depends_on proposition 7.85 Irrationality of $\pi$ ¶
    - depends_on remark 7.94 Three numbers, two kinds ¶
    - depends_on remark 7.87 Priority, and what irrationality does not give ¶
  - depends_on proposition 7.79 The polygon recursion ¶ ↺
  - depends_on proposition 7.83 Viète's product ¶ ↺
  - depends_on proposition 125.2 Crystallographic restriction ¶
    - depends_on remark 125.3 What the theorem does and does not forbid ¶
  - depends_on remark 7.88 $\pi$ elsewhere in this treatise ¶
- depends_on proposition 7.89 Irrationality of square roots ¶
  - depends_on proposition 7.91 The golden ratio ¶
    - depends_on proposition 7.92 Continued fraction and the Fibonacci ratios ¶
      - depends_on remark 7.95 Where $\varphi$ is used ¶
    - depends_on proposition 125.2 Crystallographic restriction ¶ ↺
    - depends_on remark 7.95 Where $\varphi$ is used ¶ ↺
    - depends_on remark 7.94 Three numbers, two kinds ¶ ↺
depends_on proposition 7.89 Irrationality of square roots ¶ ↺

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`	→	Peano axioms	declared	parts/02-mathematical-methods/05-real-analysis.tex:1515
`depends_on`	→	Principle of induction	declared	parts/02-mathematical-methods/05-real-analysis.tex:1515
`depends_on`	←	The integer part	declared	parts/02-mathematical-methods/05-real-analysis.tex:1532
`depends_on`	←	Irrationality of square roots	declared	parts/02-mathematical-methods/05-real-analysis.tex:2649
`proves`	←	ch:05-real-analysis@proof-41	declared	parts/02-mathematical-methods/05-real-analysis.tex:1518