PF002E · theorem body

fermat_four_odd_double_square_factors

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

A square twice a coprime product with odd first factor supplies an actual square first factor and twice-square second factor.

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

∀ m. ∀ n. ∀ y. Coprime(m,n) → Odd(m) → y · y = 2 · (m · n) → ∃ x. ∃ z. m = x · x ∧ n = 2 · (z · 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

PD0005 Coprime PD0010 Odd

In local proof propositions

PD0005 Coprime PD0009 Even
Exact expanded first-order statement
forall m n y. (forall pff_divisor_ffd_double_source. (exists pff_left_ffd_double_source. (m) = pff_divisor_ffd_double_source * pff_left_ffd_double_source) -> (exists pff_right_ffd_double_source. (n) = pff_divisor_ffd_double_source * pff_right_ffd_double_source) -> pff_divisor_ffd_double_source = 1) -> (exists k. m = 2 * k + 1) -> y * y = 2 * (m * n) -> exists u v. (m = u * u /\ n = 2 * (v * v))

Proof neighborhood

Direct theorem prerequisites

PF000N pythagorean_odd_coordinate_coprime_two coprime_mul_right · Stable closed PF001E coprime_square_product_factors PF002D fermat_four_double_product_commute PF002C fermat_four_even_square_root mul_left_cancel_nonzero · Stable closed four_square_product_square · Alpha closed mul_assoc · Stable closed succ_ne_zero · Stable closed

Direct theorem dependents

PF002K fermat_four_primitive_odd_even_descent

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

54 script commands · 19 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 (4)
pythagorean odd coordinate coprime twocoprime square product factorsfermat four double product commutefermat four even square root
01Fix variables and assumptionsL1–6

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro y
  4. L4
    intro hcoprime
  5. L5
    intro hm
  6. L6
    intro hequation
02Establish hm2L7–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean odd coordinate coprime two.

  1. L7
  2. L8
    apply pythagorean_odd_coordinate_coprime_two
  3. L9
    exact hm
03Establish hm2nL10–16

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

  1. L10
    have hm2n : Coprime(m,2 · n)Definitions: Coprime(m,2 · n)Original native command in the exact edition
  2. L11
    specialize coprime_mul_right (m)
  3. L12
    specialize coprime_mul_right (2)
  4. L13
    specialize coprime_mul_right (n)
  5. L14
    apply coprime_mul_right
  6. L15
    exact hm2
  7. L16
    exact hcoprime
04Establish hpartsL17–26

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

  1. L17
    have hparts : exists u v. (m = u * u /\ 2 * n = v * v)
  2. L18
    specialize coprime_square_product_factors (m)
  3. L19
    specialize coprime_square_product_factors (2 * n)
  4. L20
    specialize coprime_square_product_factors (y)
  5. L21
    apply coprime_square_product_factors
  6. L22
    exact hm2n
  7. L23
    trans 2 * (m * n)
  8. L24
    apply fermat_four_double_product_commute
  9. L25
    symm
  10. L26
    exact hequation
05Separate the logical casesL27–29

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

  1. L27
    cases hparts
  2. L28
    cases hparts_witness
  3. L29
    cases hparts_witness_witness
06Establish hhalfL30–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat four even square root.

  1. L30
  2. L31
    apply fermat_four_even_square_root
07Construct an explicit witnessL32–32

Supply the displayed value, then prove that it has the required property.

  1. L32
    exists n
08Calculate and transport equalitiesL33–33

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

  1. L33
    symm
09Use earlier factsL34–34

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

  1. L34
    exact hparts_witness_witness_right
10Separate the logical casesL35–35

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

  1. L35
    cases hhalf
11Construct an explicit witnessL36–37

Supply the displayed value, then prove that it has the required property.

  1. L36
    exists x
  2. L37
    exists x2
12Separate the logical casesL38–38

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

  1. L38
    split
13Use earlier factsL39–43

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

  1. L39
    exact hparts_witness_witness_left
  2. L40
    specialize mul_left_cancel_nonzero (2)
  3. L41
    specialize mul_left_cancel_nonzero (n)
  4. L42
    specialize mul_left_cancel_nonzero (2 * (x2 * x2))
  5. L43
    apply mul_left_cancel_nonzero
14Fix variables and assumptionsL44–44

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

  1. L44
    intro hzero
15Use earlier factsL45–47

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

  1. L45
    specialize succ_ne_zero 1
  2. L46
    apply succ_ne_zero
  3. L47
    exact hzero
16Calculate and transport equalitiesL48–48

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

  1. L48
    trans x1 * x1
17Use earlier factsL49–49

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

  1. L49
    exact hparts_witness_witness_right
18Calculate and transport equalitiesL50–52

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

  1. L50
    rewrite hhalf_witness
  2. L51
    rewrite hhalf_witness
  3. L52
    trans (2 * 2) * (x2 * x2)
19Use earlier factsL53–54

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

  1. L53
    apply four_square_product_square
  2. L54
    apply mul_assoc

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro y
  4. 0004intro hcoprime
  5. 0005intro hm
  6. 0006intro hequation
  7. 0007have hm2 : Coprime(m,2)
    Exact native replay linehave hm2 : forall pff_divisor_ffd_double_two. (exists pff_left_ffd_double_two. (m) = pff_divisor_ffd_double_two * pff_left_ffd_double_two) -> (exists pff_right_ffd_double_two. (2) = pff_divisor_ffd_double_two * pff_right_ffd_double_two) -> pff_divisor_ffd_double_two = 1
  8. 0008apply pythagorean_odd_coordinate_coprime_two
  9. 0009exact hm
  10. 0010have hm2n : Coprime(m,2 · n)
    Exact native replay linehave hm2n : forall pff_divisor_ffd_double_product. (exists pff_left_ffd_double_product. (m) = pff_divisor_ffd_double_product * pff_left_ffd_double_product) -> (exists pff_right_ffd_double_product. (2 * n) = pff_divisor_ffd_double_product * pff_right_ffd_double_product) -> pff_divisor_ffd_double_product = 1
  11. 0011specialize coprime_mul_right (m)
  12. 0012specialize coprime_mul_right (2)
  13. 0013specialize coprime_mul_right (n)
  14. 0014apply coprime_mul_right
  15. 0015exact hm2
  16. 0016exact hcoprime
  17. 0017have hparts : exists u v. (m = u * u /\ 2 * n = v * v)
  18. 0018specialize coprime_square_product_factors (m)
  19. 0019specialize coprime_square_product_factors (2 * n)
  20. 0020specialize coprime_square_product_factors (y)
  21. 0021apply coprime_square_product_factors
  22. 0022exact hm2n
  23. 0023trans 2 * (m * n)
  24. 0024apply fermat_four_double_product_commute
  25. 0025symm
  26. 0026exact hequation
  27. 0027cases hparts
  28. 0028cases hparts_witness
  29. 0029cases hparts_witness_witness
  30. 0030have hhalf : Even(x1)
    Exact native replay linehave hhalf : exists k. x1 = 2 * k
  31. 0031apply fermat_four_even_square_root
  32. 0032exists n
  33. 0033symm
  34. 0034exact hparts_witness_witness_right
  35. 0035cases hhalf
  36. 0036exists x
  37. 0037exists x2
  38. 0038split
  39. 0039exact hparts_witness_witness_left
  40. 0040specialize mul_left_cancel_nonzero (2)
  41. 0041specialize mul_left_cancel_nonzero (n)
  42. 0042specialize mul_left_cancel_nonzero (2 * (x2 * x2))
  43. 0043apply mul_left_cancel_nonzero
  44. 0044intro hzero
  45. 0045specialize succ_ne_zero 1
  46. 0046apply succ_ne_zero
  47. 0047exact hzero
  48. 0048trans x1 * x1
  49. 0049exact hparts_witness_witness_right
  50. 0050rewrite hhalf_witness
  51. 0051rewrite hhalf_witness
  52. 0052trans (2 * 2) * (x2 * x2)
  53. 0053apply four_square_product_square
  54. 0054apply mul_assoc