PF000W · theorem body

pythagorean_primitive_hypotenuse_coprime_first_leg

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

In every primitive Pythagorean triple, the first leg and hypotenuse have no nonunit common divisor.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ x. ∀ y. ∀ z. PrimitivePythagorean(x,y,z) → Coprime(x,z)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

CF0013 PrimitivePythagorean PD0005 Coprime

In local proof propositions

PD0003 Dvd PD0005 Coprime
Exact expanded first-order statement
forall x y z. ((((x) * (x) + (y) * (y) = (z) * (z)) /\ (forall pff_divisor_pairwise_source. (exists pff_left_pairwise_source. (x) = pff_divisor_pairwise_source * pff_left_pairwise_source) -> (exists pff_right_pairwise_source. (y) = pff_divisor_pairwise_source * pff_right_pairwise_source) -> pff_divisor_pairwise_source = 1))) -> (forall pff_divisor_first_hypotenuse_result. (exists pff_left_first_hypotenuse_result. (x) = pff_divisor_first_hypotenuse_result * pff_left_first_hypotenuse_result) -> (exists pff_right_first_hypotenuse_result. (z) = pff_divisor_first_hypotenuse_result * pff_right_first_hypotenuse_result) -> pff_divisor_first_hypotenuse_result = 1)

Proof neighborhood

Direct theorem prerequisites

PF000O pythagorean_parameter_divisor_divides_square divides_remainder · Stable closed mul_one · Stable closed coprime_mul_right · Stable closed

Direct theorem dependents

PF000X pythagorean_primitive_hypotenuse_coprime_second_leg PF000Y pythagorean_primitive_pairwise_coprime PF001V pythagorean_odd_even_half_factors

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

42 script commands · 10 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
pythagorean parameter divisor divides square
01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro x
  2. L2
    intro y
  3. L3
    intro z
  4. L4
    intro hprimitive
02Separate the logical casesL5–5

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L5
    cases hprimitive
03Fix variables and assumptionsL6–8

Work with arbitrary variables or the premises of the current implication.

  1. L6
    intro divisor
  2. L7
    intro hx
  3. L8
    intro hz
04Establish hxsquareL9–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean parameter divisor divides square.

  1. L9
    have hxsquare : Dvd(divisor,x · x)Definitions: Dvd(divisor,x · x)Original native command in the exact edition
  2. L10
    specialize pythagorean_parameter_divisor_divides_square divisor
  3. L11
    specialize pythagorean_parameter_divisor_divides_square x
  4. L12
    apply pythagorean_parameter_divisor_divides_square
  5. L13
    exact hx
05Establish hzsquareL14–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean parameter divisor divides square.

  1. L14
    have hzsquare : Dvd(divisor,z · z)Definitions: Dvd(divisor,z · z)Original native command in the exact edition
  2. L15
    specialize pythagorean_parameter_divisor_divides_square divisor
  3. L16
    specialize pythagorean_parameter_divisor_divides_square z
  4. L17
    apply pythagorean_parameter_divisor_divides_square
  5. L18
    exact hz
06Establish hysquareL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divides remainder.

  1. L19
    have hysquare : Dvd(divisor,y · y)Definitions: Dvd(divisor,y · y)Original native command in the exact edition
  2. L20
    specialize divides_remainder divisor
  3. L21
    specialize divides_remainder (z * z)
  4. L22
    specialize divides_remainder (x * x)
  5. L23
    specialize divides_remainder 1
  6. L24
    specialize divides_remainder (y * y)
  7. L25
    apply divides_remainder
  8. L26
    exact hzsquare
  9. L27
    exact hxsquare
  10. L28
    specialize mul_one (x * x)
07Calculate and transport equalitiesL29–30

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L29
    rewrite mul_one
  2. L30
    symm
08Use earlier factsL31–31

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L31
    exact hprimitive_left
09Establish hsquarecopL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply coprime mul right.

  1. L32
    have hsquarecop : Coprime(x,y · y)Definitions: Coprime(x,y · y)Original native command in the exact edition
  2. L33
    specialize coprime_mul_right x
  3. L34
    specialize coprime_mul_right y
  4. L35
    specialize coprime_mul_right y
  5. L36
    apply coprime_mul_right
  6. L37
    exact hprimitive_right
  7. L38
    exact hprimitive_right
  8. L39
    specialize hsquarecop divisor
  9. L40
    apply hsquarecop
  10. L41
    exact hx
10Use earlier factsL42–42

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L42
    exact hysquare

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro x
  2. 0002intro y
  3. 0003intro z
  4. 0004intro hprimitive
  5. 0005cases hprimitive
  6. 0006intro divisor
  7. 0007intro hx
  8. 0008intro hz
  9. 0009have hxsquare : Dvd(divisor,x · x)
    Exact native replay linehave hxsquare : exists q. x * x = divisor * q
  10. 0010specialize pythagorean_parameter_divisor_divides_square divisor
  11. 0011specialize pythagorean_parameter_divisor_divides_square x
  12. 0012apply pythagorean_parameter_divisor_divides_square
  13. 0013exact hx
  14. 0014have hzsquare : Dvd(divisor,z · z)
    Exact native replay linehave hzsquare : exists q. z * z = divisor * q
  15. 0015specialize pythagorean_parameter_divisor_divides_square divisor
  16. 0016specialize pythagorean_parameter_divisor_divides_square z
  17. 0017apply pythagorean_parameter_divisor_divides_square
  18. 0018exact hz
  19. 0019have hysquare : Dvd(divisor,y · y)
    Exact native replay linehave hysquare : exists q. y * y = divisor * q
  20. 0020specialize divides_remainder divisor
  21. 0021specialize divides_remainder (z * z)
  22. 0022specialize divides_remainder (x * x)
  23. 0023specialize divides_remainder 1
  24. 0024specialize divides_remainder (y * y)
  25. 0025apply divides_remainder
  26. 0026exact hzsquare
  27. 0027exact hxsquare
  28. 0028specialize mul_one (x * x)
  29. 0029rewrite mul_one
  30. 0030symm
  31. 0031exact hprimitive_left
  32. 0032have hsquarecop : Coprime(x,y · y)
    Exact native replay linehave hsquarecop : forall pff_divisor_hypotenuse_first_square. (exists pff_left_hypotenuse_first_square. (x) = pff_divisor_hypotenuse_first_square * pff_left_hypotenuse_first_square) -> (exists pff_right_hypotenuse_first_square. (y * y) = pff_divisor_hypotenuse_first_square * pff_right_hypotenuse_first_square) -> pff_divisor_hypotenuse_first_square = 1
  33. 0033specialize coprime_mul_right x
  34. 0034specialize coprime_mul_right y
  35. 0035specialize coprime_mul_right y
  36. 0036apply coprime_mul_right
  37. 0037exact hprimitive_right
  38. 0038exact hprimitive_right
  39. 0039specialize hsquarecop divisor
  40. 0040apply hsquarecop
  41. 0041exact hx
  42. 0042exact hysquare