Description: 139 is a prime number. In contrast to 139prm , the proof of this theorem uses 3dvds2dec for checking the divisibility by 3. Although the proof using 3dvds2dec is longer (regarding size: 1849 characters compared with 1809 for 139prm ), the number of essential steps is smaller (301 compared with 327 for 139prm ). (Contributed by Mario Carneiro, 19-Feb-2014) (Revised by AV, 18-Aug-2021) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 139prmALT |