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

• Definitions:
  • 571: Relation
• Theorems:
  • 844: Definition of Integers

Logical Successors

• Definitions:
  • 703: 7.03: Proper Divisor
  • 2323: 7.04: Aliquant Part, a Number Being Not a Divisor of Another Number
  • 1275: 7.05: Multiple, Number Multiplying another Number
  • 704: 7.11: Prime Number
  • 2330: 7.22: Perfect Number
  • 8153: Congruent, Residue
  • 6406: Divisor-Closed Sets
  • 8130: Even and Odd Numbers
  • 8257: Generalization of Divisor and Multiple
  • 8115: Number of Divisors
  • 8131: Perfect Number
  • 473: Prime Numbers
  • 6404: Subsets of Prime Numbers Not Dividing a Natural Number
  • 8127: Sum of Divisors
• Theorems:
  • 8191: A Necessary Condition for an Integer to be Prime
  • 8128: Calculating the Sum of Divisors
  • 8182: Chinese Remainder Theorem
  • 8273: Classification of Finite Groups with the Order of a Prime Number
  • 8100: Co-prime Primes
  • 8185: Complete and Reduced Residue Systems (Revised)
  • 8154: Congruence Classes
  • 8171: Congruence Modulo a Divisor
  • 8176: Coprimality and Congruence Classes
  • 508: Divisibility Laws
  • 1293: Divisors of a Product Of Two Factors, Co-Prime to One Factor Divide the Other Factor
  • 8134: Even Perfect Numbers
  • 8178: Existence and Number of Solutions of Congruence With One Variable
  • 8179: Existence of Solutions of an LDE With More Variables
  • 2483: Factorization of Greatest Common Divisor and Least Common Multiple
  • 1278: Finite Number of Divisors
  • 8208: Gaussian Lemma (Number Theory)
  • 1298: Generalized Euclidean Lemma
  • 1280: Greatest Common Divisor
  • 8122: Greatest Common Divisor of More Than Two Numbers
  • 1296: Greatest Common Divisors Of Integers and Prime Numbers
  • 8099: Infinite Set of Prime Numbers
  • 1276: Least Common Multiple
  • 8124: Least Common Multiple of More Than Two Numbers
  • 8199: Legendre Symbols of Equal Residues
  • 8149: Möbius Inversion Formula
  • 8202: Multiplicativity of the Legendre Symbol
  • 8118: Natural Logarithm Sum of von Mangoldt Function Over Divisors
  • 8107: Number of Multiples of a Given Number Less Than Another Number
  • 8111: Number of Multiples of a Prime Number Less Than Factorial
  • 8136: Numbers Being the Product of Their Divisors
  • 808: Order of Cyclic Group (Fermat's Little Theorem)
  • 1300: Prime Dividing Product of Primes Implies Prime Divisor
  • 8168: Product of an Even and an Odd Number
  • 8167: Product of Two Even Numbers
  • 8169: Product of Two Odd Numbers
  • 8216: Properties of the Jacobi Symbol
  • 8210: Reciprocity Law for Floor Functions
  • 1273: Sign of Divisors of Integers
  • 825: Subgroups of Finite Cyclic Groups
  • 6196: Sum of Euler Function
  • 8142: Sum of Möbius Function Over Divisors
  • 3247: Sum of Möbius Function Over Divisors With Division
  • 8193: Wilson's Condition for an Integer to be Prime