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
• 8041: Axiom of Choice
• 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:
    • 8112: Arithmetic Function
    • 8153: Congruent, Residue
    • 700: Divisor, Complementary Divisor, Multiple
    • 8130: Even and Odd Numbers
    • 8198: Legendre Symbol
    • 505: Multiplicative Functions
    • 473: Prime Numbers
    • 1585: Subtraction of Integers
  • Theorems:
    • 844: Definition of Integers
    • 8201: Euler's Criterion For Quadratic Residues
    • 8157: Sums, Products, and Powers Of Congruences
    • 657: The Proving Principle of Complete Induction

Logical Successors

• Theorems:
  • 8216: Properties of the Jacobi Symbol