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
• 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:
    • 8093: Co-prime Numbers
    • 700: Divisor, Complementary Divisor, Multiple
    • 7990: Equivalence Class
    • 574: Equivalence Relation
    • 8117: Euler function
    • 718: Set-theoretic Definitions of Natural Numbers
  • Theorems:
    • 1289: Generating Co-Prime Numbers Knowing the Greatest Common Divisor
    • 1291: Generating the Greatest Common Divisor Knowing Co-Prime Numbers
    • 1280: Greatest Common Divisor

Logical Successors

• Theorems:
  • 2790: Explicit Formula for the Euler Function