PF001E · theorem body

coprime_square_product_factors

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

If two coprime naturals have square product, each has a constructed natural square root, including both zero boundary cases.

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

∀ a. ∀ b. ∀ z. Coprime(a,b) → a · b = z · z → ∃ x. ∃ y. a = x · x ∧ b = y · y

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

In local proof propositions

PD0003 Dvd PD0005 Coprime
Exact expanded first-order statement
forall a b z. (forall frp_divisor_csf_product. (exists frp_left_factor_csf_product. a = frp_divisor_csf_product * frp_left_factor_csf_product) -> (exists frp_right_factor_csf_product. b = frp_divisor_csf_product * frp_right_factor_csf_product) -> frp_divisor_csf_product = 1) -> a * b = z * z -> exists u v. a = u * u /\ b = v * v

Proof neighborhood

Direct theorem prerequisites

eq_decidable · Stable closed mul_eq_zero · Stable closed mul_one · Stable closed canonical_gcd_exists · Alpha closed is_gcd_dvd_left · Stable closed is_gcd_dvd_right · Stable closed factor_nonzero_left · Stable closed factor_nonzero_right · Alpha closed is_gcd_quotients_coprime_nonzero · Stable closed PF001D coprime_square_reduced_factors

Direct theorem dependents

PF001W pythagorean_half_factors_extract_parameters PF002E fermat_four_odd_double_square_factors PF002H fermat_four_second_parameter_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

114 script commands · 37 reading checkpoints · 9 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)
coprime square reduced factors
01Fix variables and assumptionsL1–5

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro z
  4. L4
    intro hcop
  5. L5
    intro heq
02Use earlier factsL6–7

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

  1. L6
    specialize eq_decidable z
  2. L7
    specialize eq_decidable 0
03Separate the logical casesL8–8

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

  1. L8
    cases eq_decidable
04Establish habzeroL9–14

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have habzero : a * b = 0
  2. L10
    trans z * z
  3. L11
    exact heq
  4. L12
    rewrite eq_decidable_left
  5. L13
    rewrite eq_decidable_left
  6. L14
    simp
05Establish hzeroL15–19

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

  1. L15
    have hzero : a = 0 \/ b = 0
  2. L16
    specialize mul_eq_zero a
  3. L17
    specialize mul_eq_zero b
  4. L18
    apply mul_eq_zero
  5. L19
    exact habzero
06Separate the logical casesL20–20

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

  1. L20
    cases hzero
07Establish hboneL21–23

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

  1. L21
    have hbone : b = 1
  2. L22
    specialize hcop b
  3. L23
    apply hcop
08Construct an explicit witnessL24–24

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

  1. L24
    exists 0
09Calculate and transport equalitiesL25–26

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

  1. L25
    rewrite hzero_left
  2. L26
    simp
10Construct an explicit witnessL27–27

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

  1. L27
    exists 1
11Calculate and transport equalitiesL28–28

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

  1. L28
    symm
12Use earlier factsL29–29

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

  1. L29
    apply mul_one
13Construct an explicit witnessL30–31

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

  1. L30
    exists 0
  2. L31
    exists 1
14Separate the logical casesL32–32

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

  1. L32
    split
15Calculate and transport equalitiesL33–36

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

  1. L33
    rewrite hzero_left
  2. L34
    simp
  3. L35
    rewrite hbone
  4. L36
    simp
16Establish haoneL37–39

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

  1. L37
    have haone : a = 1
  2. L38
    specialize hcop a
  3. L39
    apply hcop
17Construct an explicit witnessL40–40

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

  1. L40
    exists 1
18Calculate and transport equalitiesL41–41

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

  1. L41
    symm
19Use earlier factsL42–42

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

  1. L42
    apply mul_one
20Construct an explicit witnessL43–43

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

  1. L43
    exists 0
21Calculate and transport equalitiesL44–45

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

  1. L44
    rewrite hzero_right
  2. L45
    simp
22Construct an explicit witnessL46–47

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

  1. L46
    exists 1
  2. L47
    exists 0
23Separate the logical casesL48–48

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

  1. L48
    split
24Calculate and transport equalitiesL49–52

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

  1. L49
    rewrite haone
  2. L50
    simp
  3. L51
    rewrite hzero_right
  4. L52
    simp
25Use earlier factsL53–54

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

  1. L53
    specialize canonical_gcd_exists a
  2. L54
    specialize canonical_gcd_exists z
26Separate the logical casesL55–55

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

  1. L55
    cases canonical_gcd_exists
27Establish haquotL56–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply is gcd dvd left.

  1. L56
    have haquot : Dvd(x,a)Definitions: Dvd(x,a)Original native command in the exact edition
  2. L57
    specialize is_gcd_dvd_left x
  3. L58
    specialize is_gcd_dvd_left a
  4. L59
    specialize is_gcd_dvd_left z
  5. L60
    apply is_gcd_dvd_left
  6. L61
    exact canonical_gcd_exists_witness
28Separate the logical casesL62–62

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

  1. L62
    cases haquot
29Establish hzquotL63–68

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

  1. L63
    have hzquot : Dvd(x,z)Definitions: Dvd(x,z)Original native command in the exact edition
  2. L64
    specialize is_gcd_dvd_right x
  3. L65
    specialize is_gcd_dvd_right a
  4. L66
    specialize is_gcd_dvd_right z
  5. L67
    apply is_gcd_dvd_right
  6. L68
    exact canonical_gcd_exists_witness
30Separate the logical casesL69–69

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

  1. L69
    cases hzquot
31Establish hgnonzeroL70–78

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero left.

  1. L70
    have hgnonzero : ~(x = 0)
  2. L71
    intro hzero
  3. L72
    specialize factor_nonzero_left z
  4. L73
    specialize factor_nonzero_left x
  5. L74
    specialize factor_nonzero_left x2
  6. L75
    apply factor_nonzero_left
  7. L76
    exact eq_decidable_right
  8. L77
    exact hzquot_witness
  9. L78
    exact hzero
32Establish hZnonzeroL79–87

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

  1. L79
    have hZnonzero : ~(x2 = 0)
  2. L80
    intro hzero
  3. L81
    specialize factor_nonzero_right z
  4. L82
    specialize factor_nonzero_right x
  5. L83
    specialize factor_nonzero_right x2
  6. L84
    apply factor_nonzero_right
  7. L85
    exact eq_decidable_right
  8. L86
    exact hzquot_witness
  9. L87
    exact hzero
33Establish hquotcopL88–97

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

  1. L88
    have hquotcop : Coprime(x1,x2)Definitions: Coprime(x1,x2)Original native command in the exact edition
  2. L89
    specialize is_gcd_quotients_coprime_nonzero x
  3. L90
    specialize is_gcd_quotients_coprime_nonzero a
  4. L91
    specialize is_gcd_quotients_coprime_nonzero z
  5. L92
    specialize is_gcd_quotients_coprime_nonzero x1
  6. L93
    specialize is_gcd_quotients_coprime_nonzero x2
  7. L94
    apply is_gcd_quotients_coprime_nonzero
  8. L95
    exact canonical_gcd_exists_witness
  9. L96
    exact hgnonzero
  10. L97
    exact haquot_witness
34Use earlier factsL98–98

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

  1. L98
    exact hzquot_witness
35Construct an explicit witnessL99–100

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

  1. L99
    exists x1
  2. L100
    exists x2
36Use earlier factsL101–110

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

  1. L101
    specialize coprime_square_reduced_factors a
  2. L102
    specialize coprime_square_reduced_factors b
  3. L103
    specialize coprime_square_reduced_factors z
  4. L104
    specialize coprime_square_reduced_factors x
  5. L105
    specialize coprime_square_reduced_factors x1
  6. L106
    specialize coprime_square_reduced_factors x2
  7. L107
    apply coprime_square_reduced_factors
  8. L108
    exact hgnonzero
  9. L109
    exact hZnonzero
  10. L110
    exact haquot_witness
37Use earlier factsL111–114

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

  1. L111
    exact hzquot_witness
  2. L112
    exact heq
  3. L113
    exact hcop
  4. L114
    exact hquotcop

Library-wide reading audit

Original defined command ledger · 114 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro z
  4. 0004intro hcop
  5. 0005intro heq
  6. 0006specialize eq_decidable z
  7. 0007specialize eq_decidable 0
  8. 0008cases eq_decidable
  9. 0009have habzero : a * b = 0
  10. 0010trans z * z
  11. 0011exact heq
  12. 0012rewrite eq_decidable_left
  13. 0013rewrite eq_decidable_left
  14. 0014simp
  15. 0015have hzero : a = 0 \/ b = 0
  16. 0016specialize mul_eq_zero a
  17. 0017specialize mul_eq_zero b
  18. 0018apply mul_eq_zero
  19. 0019exact habzero
  20. 0020cases hzero
  21. 0021have hbone : b = 1
  22. 0022specialize hcop b
  23. 0023apply hcop
  24. 0024exists 0
  25. 0025rewrite hzero_left
  26. 0026simp
  27. 0027exists 1
  28. 0028symm
  29. 0029apply mul_one
  30. 0030exists 0
  31. 0031exists 1
  32. 0032split
  33. 0033rewrite hzero_left
  34. 0034simp
  35. 0035rewrite hbone
  36. 0036simp
  37. 0037have haone : a = 1
  38. 0038specialize hcop a
  39. 0039apply hcop
  40. 0040exists 1
  41. 0041symm
  42. 0042apply mul_one
  43. 0043exists 0
  44. 0044rewrite hzero_right
  45. 0045simp
  46. 0046exists 1
  47. 0047exists 0
  48. 0048split
  49. 0049rewrite haone
  50. 0050simp
  51. 0051rewrite hzero_right
  52. 0052simp
  53. 0053specialize canonical_gcd_exists a
  54. 0054specialize canonical_gcd_exists z
  55. 0055cases canonical_gcd_exists
  56. 0056have haquot : Dvd(x,a)
    Exact native replay linehave haquot : exists A. a = x * A
  57. 0057specialize is_gcd_dvd_left x
  58. 0058specialize is_gcd_dvd_left a
  59. 0059specialize is_gcd_dvd_left z
  60. 0060apply is_gcd_dvd_left
  61. 0061exact canonical_gcd_exists_witness
  62. 0062cases haquot
  63. 0063have hzquot : Dvd(x,z)
    Exact native replay linehave hzquot : exists Z. z = x * Z
  64. 0064specialize is_gcd_dvd_right x
  65. 0065specialize is_gcd_dvd_right a
  66. 0066specialize is_gcd_dvd_right z
  67. 0067apply is_gcd_dvd_right
  68. 0068exact canonical_gcd_exists_witness
  69. 0069cases hzquot
  70. 0070have hgnonzero : ~(x = 0)
  71. 0071intro hzero
  72. 0072specialize factor_nonzero_left z
  73. 0073specialize factor_nonzero_left x
  74. 0074specialize factor_nonzero_left x2
  75. 0075apply factor_nonzero_left
  76. 0076exact eq_decidable_right
  77. 0077exact hzquot_witness
  78. 0078exact hzero
  79. 0079have hZnonzero : ~(x2 = 0)
  80. 0080intro hzero
  81. 0081specialize factor_nonzero_right z
  82. 0082specialize factor_nonzero_right x
  83. 0083specialize factor_nonzero_right x2
  84. 0084apply factor_nonzero_right
  85. 0085exact eq_decidable_right
  86. 0086exact hzquot_witness
  87. 0087exact hzero
  88. 0088have hquotcop : Coprime(x1,x2)
    Exact native replay linehave hquotcop : forall frp_divisor_csf_product_reduced. (exists frp_left_factor_csf_product_reduced. x1 = frp_divisor_csf_product_reduced * frp_left_factor_csf_product_reduced) -> (exists frp_right_factor_csf_product_reduced. x2 = frp_divisor_csf_product_reduced * frp_right_factor_csf_product_reduced) -> frp_divisor_csf_product_reduced = 1
  89. 0089specialize is_gcd_quotients_coprime_nonzero x
  90. 0090specialize is_gcd_quotients_coprime_nonzero a
  91. 0091specialize is_gcd_quotients_coprime_nonzero z
  92. 0092specialize is_gcd_quotients_coprime_nonzero x1
  93. 0093specialize is_gcd_quotients_coprime_nonzero x2
  94. 0094apply is_gcd_quotients_coprime_nonzero
  95. 0095exact canonical_gcd_exists_witness
  96. 0096exact hgnonzero
  97. 0097exact haquot_witness
  98. 0098exact hzquot_witness
  99. 0099exists x1
  100. 0100exists x2
  101. 0101specialize coprime_square_reduced_factors a
  102. 0102specialize coprime_square_reduced_factors b
  103. 0103specialize coprime_square_reduced_factors z
  104. 0104specialize coprime_square_reduced_factors x
  105. 0105specialize coprime_square_reduced_factors x1
  106. 0106specialize coprime_square_reduced_factors x2
  107. 0107apply coprime_square_reduced_factors
  108. 0108exact hgnonzero
  109. 0109exact hZnonzero
  110. 0110exact haquot_witness
  111. 0111exact hzquot_witness
  112. 0112exact heq
  113. 0113exact hcop
  114. 0114exact hquotcop