prove flt4lem5e [skip ci]

I think minimizing flt4lem5e is prohibitively long because, despite only being 27 lines long, there are 71 Zs, so there are 46140 steps when expanded+syntax. (Relevant: metamath#3180) I used theorems in Scott's mathbox without even realizing, so they're moved now I renamed dvdspw to reduce confusion with dvdsexp Fix comment of ncoprmgcdne1bgd
icecream17 · Aug 24, 2024 · 0925e6c · 0925e6c
1 parent c5a3626
commit 0925e6c
Show file tree

Hide file tree

Showing 2 changed files with 135 additions and 119 deletions.
diff --git a/changes-set.txt b/changes-set.txt
@@ -99,6 +99,8 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+24-Aug-24 dvdspw    dvdsexp2im  moved from SF's mathbox to main set.mm
+24-Aug-24 pdivsq    prmdvdssq   moved from SF's mathbox to main set.mm
 24-Aug-24 dvdstrd   [same]      moved from MKU's mathbox to main set.mm
 23-Aug-24 qred      [same]      moved from GS's mathbox to main set.mm
 20-Aug-24 uzssre    [same]      moved from GS's mathbox to main set.mm