Underlying Axioms

• 692: 1.1: Straight Line Determined by Two Distinct Points
• 694: 1.2: Circle Determined by its Center and its Radius
• 734: 1.3: Segment Extension
• 939: 1.5: Parallel Postulate
• 1339: Archimedean Axiom
• 682: Axiom of Distributivity
• 666: Axiom of Empty Set
• 551: Axiom of Extensionality
• 717: Axiom of Foundation
• 678: Axiom of Infinity
• 716: Axiom of Power Set
• 675: Axiom of Separation (Restricted Principle of Comprehension)
• 705: Bivalence of Truth
• 504: Peano Axioms
• 1427: Zermelo-Fraenkel Axioms

Logical Predecessors

• (used in the Proof)
  • Definitions:
    • 8116: Möbius Function, Square-free
    • 261: Sums
  • Theorems:
    • 1105: Definition of Real Numbers
    • 8107: Number of Multiples of a Given Number Less Than Another Number
    • 8142: Sum of Möbius Function Over Divisors

Logical Successors

• Theorems:
  • 8147: Upper Bound of Harmonic Series Times Möbius Function