lemma 7.65 The integer part

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

Rests on

depends_on axiom 3.33 Peano axioms ¶
depends_on corollary A.45 Archimedean property and density of $\Q$ ¶
- depends_on definition A.36 Cut ¶
- depends_on theorem A.40 Least-upper-bound property ¶
  - depends_on definition A.36 Cut ¶ ↺
  - depends_on definition A.38 Order on $\R$ ¶
    - depends_on definition A.36 Cut ¶ ↺
  - proves proof app:A-long-proofs@proof-29 ¶
- proves proof app:A-long-proofs@proof-32 ¶
depends_on lemma 7.64 Well-ordering of $\N$ ¶
- depends_on axiom 3.33 Peano axioms ¶ ↺
- depends_on axiom 3.34 Principle of induction ¶
- proves proof ch:05-real-analysis@proof-41 ¶
proves proof ch:05-real-analysis@proof-42 ¶

Supports

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 remark 7.88 $\pi$ elsewhere in this treatise ¶
    - depends_on proposition 7.83 Viète's product ¶
      - depends_on remark 7.84 One construction, two faces ¶
    - 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 ¶ ↺

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:1532
`depends_on`	→	Archimedean property and density of $\Q$	declared	parts/02-mathematical-methods/05-real-analysis.tex:1532
`depends_on`	→	Well-ordering of $\N$	declared	parts/02-mathematical-methods/05-real-analysis.tex:1532
`depends_on`	←	The limit over real exponents	declared	parts/02-mathematical-methods/05-real-analysis.tex:1563
`depends_on`	←	Special values, periodicity, and the kernel	declared	parts/02-mathematical-methods/05-real-analysis.tex:2077
`depends_on`	←	Irrationality of square roots	declared	parts/02-mathematical-methods/05-real-analysis.tex:2649
`proves`	←	ch:05-real-analysis@proof-42	declared	parts/02-mathematical-methods/05-real-analysis.tex:1535