`minimal_sync_360_divides`

proved

show as: view math explainer →

module: IndisputableMonolith.Gap45
domain: Gap45
line: 109 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45 on GitHub at line 109.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 106  simpa [beats] using Nat.lcm_dvd h8 h45
 107
 108/-- Convenience form of minimality with 360 on the left. -/
 109lemma minimal_sync_360_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : 360 ∣ t := by
 110  simpa [beats_eq_360] using minimal_sync_divides (t:=t) h8 h45
 111
 112/-- No positive `n < 360` can be simultaneously divisible by 8 and 45. -/
 113lemma no_smaller_multiple_8_45 {n : Nat} (hnpos : 0 < n) (hnlt : n < 360) :
 114  ¬ (8 ∣ n ∧ 45 ∣ n) := by
 115  intro h
 116  rcases h with ⟨h8, h45⟩
 117  have h360 : 360 ∣ n := minimal_sync_360_divides (t:=n) h8 h45
 118  rcases h360 with ⟨k, hk⟩
 119  rcases Nat.eq_zero_or_pos k with rfl | hkpos
 120  · simp only [mul_zero] at hk
 121    omega
 122  · have : 360 ≤ 360 * k := Nat.mul_le_mul_left 360 hkpos
 123    have : 360 ≤ n := by simpa [hk] using this
 124    exact (not_le_of_gt hnlt) this
 125
 126end Beat
 127
 128-- (Moved to IndisputableMonolith/Gap45/TimeLag.lean)
 129
 130-- (Moved to IndisputableMonolith/Gap45/RecognitionBarrier.lean)
 131
 132-- (Moved to IndisputableMonolith/Gap45/GroupView.lean)
 133
 134-- (Moved to IndisputableMonolith/Gap45/AddGroupView.lean)
 135
 136end Gap45
 137end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.