lcm_9_5_eq_45

formal source

  35  simpa [h] using this
  36
  37/-- lcm(9,5) = 45, characterizing the first simultaneous occurrence of 9- and 5-fold periodicities. -/
  38lemma lcm_9_5_eq_45 : Nat.lcm 9 5 = 45 := by
  39  have hg : Nat.gcd 9 5 = 1 := by decide
  40  have h := Nat.gcd_mul_lcm 9 5
  41  have h' : Nat.lcm 9 5 = 9 * 5 := by simpa [hg, Nat.one_mul] using h
  42  have hmul : 9 * 5 = 45 := by decide
  43  simpa [hmul] using h'
  44
  45/-- 9 ∣ 45. -/
  46@[simp] lemma nine_dvd_45 : 9 ∣ 45 := by exact ⟨5, by decide⟩
  47
  48/-- 5 ∣ 45. -/
  49@[simp] lemma five_dvd_45 : 5 ∣ 45 := by exact ⟨9, by decide⟩
  50
  51/-- 8 ∤ 45. -/
  52@[simp] lemma eight_not_dvd_45 : ¬ 8 ∣ 45 := by decide
  53
  54/-- No positive `n < 45` is simultaneously divisible by 9 and 5. -/
  55lemma no_smaller_multiple_9_5 (n : Nat) (hnpos : 0 < n) (hnlt : n < 45) :
  56  ¬ (9 ∣ n ∧ 5 ∣ n) := by
  57  intro h
  58  rcases h with ⟨h9, h5⟩
  59  have hmul : 9 * 5 ∣ n := coprime_9_5.mul_dvd_of_dvd_of_dvd h9 h5
  60  have h45 : 45 ∣ n := by simpa using hmul
  61  rcases h45 with ⟨k, hk⟩
  62  rcases (Nat.eq_zero_or_pos k) with rfl | hkpos
  63  · simp only [mul_zero] at hk
  64    omega
  65  · have : 45 ≤ 45 * k := Nat.mul_le_mul_left 45 hkpos
  66    have : 45 ≤ n := by simpa [hk] using this
  67    exact (not_le_of_gt hnlt) this
  68