PF001G · theorem body

square_divides_square_root

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

For all naturals, if a squared divisor divides a squared value, the unsquared divisor divides the unsquared value.

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. Dvd(a · a,b · b) → Dvd(a,b)

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

PD0003 Dvd

In local proof propositions

PD0003 Dvd PD0005 Coprime
Exact expanded first-order statement
forall a b. (exists q. b * b = (a * a) * q) -> exists k. b = a * k

Proof neighborhood

Direct theorem prerequisites

eq_decidable · Stable closed mul_zero_left · Stable closed PF001C square_zero_root canonical_gcd_exists · Alpha closed is_gcd_dvd_left · Stable closed is_gcd_dvd_right · Stable closed factor_nonzero_left · Stable closed is_gcd_quotients_coprime_nonzero · Stable closed PF001F square_divides_square_reduced_root

Direct theorem dependents

PF002F fermat_four_primitive_normalization

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

66 script commands · 17 reading checkpoints · 5 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 (2)
square zero rootsquare divides square reduced root
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hdiv
02Separate the logical casesL4–4

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

  1. L4
    cases hdiv
03Use earlier factsL5–6

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

  1. L5
    specialize eq_decidable a
  2. L6
    specialize eq_decidable 0
04Separate the logical casesL7–7

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

  1. L7
    cases eq_decidable
05Establish hbzeroL8–14

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

  1. L8
    have hbzero : b = 0
  2. L9
    specialize square_zero_root b
  3. L10
    apply square_zero_root
  4. L11
    trans (a * a) * x
  5. L12
    exact hdiv_witness
  6. L13
    rewrite eq_decidable_left
  7. L14
    simp [mul_zero_left]
06Construct an explicit witnessL15–15

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

  1. L15
    exists 0
07Calculate and transport equalitiesL16–17

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

  1. L16
    rewrite hbzero
  2. L17
    simp
08Use earlier factsL18–19

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

  1. L18
    specialize canonical_gcd_exists a
  2. L19
    specialize canonical_gcd_exists b
09Separate the logical casesL20–20

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

  1. L20
    cases canonical_gcd_exists
10Establish haquotL21–26

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

  1. L21
    have haquot : Dvd(x1,a)Definitions: Dvd(x1,a)Original native command in the exact edition
  2. L22
    specialize is_gcd_dvd_left x1
  3. L23
    specialize is_gcd_dvd_left a
  4. L24
    specialize is_gcd_dvd_left b
  5. L25
    apply is_gcd_dvd_left
  6. L26
    exact canonical_gcd_exists_witness
11Separate the logical casesL27–27

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

  1. L27
    cases haquot
12Establish hbquotL28–33

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

  1. L28
    have hbquot : Dvd(x1,b)Definitions: Dvd(x1,b)Original native command in the exact edition
  2. L29
    specialize is_gcd_dvd_right x1
  3. L30
    specialize is_gcd_dvd_right a
  4. L31
    specialize is_gcd_dvd_right b
  5. L32
    apply is_gcd_dvd_right
  6. L33
    exact canonical_gcd_exists_witness
13Separate the logical casesL34–34

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

  1. L34
    cases hbquot
14Establish hgnonzeroL35–43

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

  1. L35
    have hgnonzero : ~(x1 = 0)
  2. L36
    intro hzero
  3. L37
    specialize factor_nonzero_left a
  4. L38
    specialize factor_nonzero_left x1
  5. L39
    specialize factor_nonzero_left x2
  6. L40
    apply factor_nonzero_left
  7. L41
    exact eq_decidable_right
  8. L42
    exact haquot_witness
  9. L43
    exact hzero
15Establish hquotcopL44–53

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

  1. L44
    have hquotcop : Coprime(x2,x3)Definitions: Coprime(x2,x3)Original native command in the exact edition
  2. L45
    specialize is_gcd_quotients_coprime_nonzero x1
  3. L46
    specialize is_gcd_quotients_coprime_nonzero a
  4. L47
    specialize is_gcd_quotients_coprime_nonzero b
  5. L48
    specialize is_gcd_quotients_coprime_nonzero x2
  6. L49
    specialize is_gcd_quotients_coprime_nonzero x3
  7. L50
    apply is_gcd_quotients_coprime_nonzero
  8. L51
    exact canonical_gcd_exists_witness
  9. L52
    exact hgnonzero
  10. L53
    exact haquot_witness
16Use earlier factsL54–63

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

  1. L54
    exact hbquot_witness
  2. L55
    specialize square_divides_square_reduced_root a
  3. L56
    specialize square_divides_square_reduced_root b
  4. L57
    specialize square_divides_square_reduced_root x1
  5. L58
    specialize square_divides_square_reduced_root x2
  6. L59
    specialize square_divides_square_reduced_root x3
  7. L60
    specialize square_divides_square_reduced_root x
  8. L61
    apply square_divides_square_reduced_root
  9. L62
    exact hgnonzero
  10. L63
    exact haquot_witness
17Use earlier factsL64–66

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

  1. L64
    exact hbquot_witness
  2. L65
    exact hquotcop
  3. L66
    exact hdiv_witness

Library-wide reading audit

Original defined command ledger · 66 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hdiv
  4. 0004cases hdiv
  5. 0005specialize eq_decidable a
  6. 0006specialize eq_decidable 0
  7. 0007cases eq_decidable
  8. 0008have hbzero : b = 0
  9. 0009specialize square_zero_root b
  10. 0010apply square_zero_root
  11. 0011trans (a * a) * x
  12. 0012exact hdiv_witness
  13. 0013rewrite eq_decidable_left
  14. 0014simp [mul_zero_left]
  15. 0015exists 0
  16. 0016rewrite hbzero
  17. 0017simp
  18. 0018specialize canonical_gcd_exists a
  19. 0019specialize canonical_gcd_exists b
  20. 0020cases canonical_gcd_exists
  21. 0021have haquot : Dvd(x1,a)
    Exact native replay linehave haquot : exists A. a = x1 * A
  22. 0022specialize is_gcd_dvd_left x1
  23. 0023specialize is_gcd_dvd_left a
  24. 0024specialize is_gcd_dvd_left b
  25. 0025apply is_gcd_dvd_left
  26. 0026exact canonical_gcd_exists_witness
  27. 0027cases haquot
  28. 0028have hbquot : Dvd(x1,b)
    Exact native replay linehave hbquot : exists B. b = x1 * B
  29. 0029specialize is_gcd_dvd_right x1
  30. 0030specialize is_gcd_dvd_right a
  31. 0031specialize is_gcd_dvd_right b
  32. 0032apply is_gcd_dvd_right
  33. 0033exact canonical_gcd_exists_witness
  34. 0034cases hbquot
  35. 0035have hgnonzero : ~(x1 = 0)
  36. 0036intro hzero
  37. 0037specialize factor_nonzero_left a
  38. 0038specialize factor_nonzero_left x1
  39. 0039specialize factor_nonzero_left x2
  40. 0040apply factor_nonzero_left
  41. 0041exact eq_decidable_right
  42. 0042exact haquot_witness
  43. 0043exact hzero
  44. 0044have hquotcop : Coprime(x2,x3)
    Exact native replay linehave hquotcop : forall frp_divisor_csf_divisibility_quotients. (exists frp_left_factor_csf_divisibility_quotients. x2 = frp_divisor_csf_divisibility_quotients * frp_left_factor_csf_divisibility_quotients) -> (exists frp_right_factor_csf_divisibility_quotients. x3 = frp_divisor_csf_divisibility_quotients * frp_right_factor_csf_divisibility_quotients) -> frp_divisor_csf_divisibility_quotients = 1
  45. 0045specialize is_gcd_quotients_coprime_nonzero x1
  46. 0046specialize is_gcd_quotients_coprime_nonzero a
  47. 0047specialize is_gcd_quotients_coprime_nonzero b
  48. 0048specialize is_gcd_quotients_coprime_nonzero x2
  49. 0049specialize is_gcd_quotients_coprime_nonzero x3
  50. 0050apply is_gcd_quotients_coprime_nonzero
  51. 0051exact canonical_gcd_exists_witness
  52. 0052exact hgnonzero
  53. 0053exact haquot_witness
  54. 0054exact hbquot_witness
  55. 0055specialize square_divides_square_reduced_root a
  56. 0056specialize square_divides_square_reduced_root b
  57. 0057specialize square_divides_square_reduced_root x1
  58. 0058specialize square_divides_square_reduced_root x2
  59. 0059specialize square_divides_square_reduced_root x3
  60. 0060specialize square_divides_square_reduced_root x
  61. 0061apply square_divides_square_reduced_root
  62. 0062exact hgnonzero
  63. 0063exact haquot_witness
  64. 0064exact hbquot_witness
  65. 0065exact hquotcop
  66. 0066exact hdiv_witness