let m be Nat; :: thesis: ( m satisfies_Sierpinski_problem_76b & m <= 62 implies m in {20,32,51,53,62} )
assume A1: m satisfies_Sierpinski_problem_76b ; :: thesis: ( not m <= 62 or m in {20,32,51,53,62} )
assume m <= 62 ; :: thesis: m in {20,32,51,53,62}
then not not m = 0 & ... & not m = 62 ;
then ( m = 20 or m = 32 or m = 51 or m = 53 or m = 62 ) by A1, XPRIMES1:2, XPRIMES1:13, XPRIMES1:23, XPRIMES1:31, XPRIMES1:41, XPRIMES1:53, XPRIMES1:61, XPRIMES1:71, XPRIMES1:83, XPRIMES1:97, XPRIMES1:101, XPRIMES1:113, XPRIMES1:127, XPRIMES1:131, XPRIMES1:149, XPRIMES1:151, XPRIMES1:163, XPRIMES1:173, XPRIMES1:181, XPRIMES1:191, XPRIMES1:211, XPRIMES1:223, XPRIMES1:233, XPRIMES1:241, XPRIMES1:251, XPRIMES1:263, XPRIMES1:271, XPRIMES1:281, XPRIMES1:293, XPRIMES1:307, XPRIMES1:311, XPRIMES1:331, XPRIMES1:347, XPRIMES1:353, XPRIMES1:367, XPRIMES1:373, XPRIMES1:383, XPRIMES1:397, XPRIMES1:401, XPRIMES1:419, XPRIMES1:421, XPRIMES1:431, XPRIMES1:443, XPRIMES1:457, XPRIMES1:461, XPRIMES1:479, XPRIMES1:487, XPRIMES1:491, XPRIMES1:503, XPRIMES1:521, XPRIMES1:541, XPRIMES1:557, XPRIMES1:563, XPRIMES1:571, XPRIMES1:587, XPRIMES1:593, XPRIMES1:601, XPRIMES1:613;
hence m in {20,32,51,53,62} by ENUMSET1:def 3; :: thesis: verum