(=>
(and
(equal
(GreatestCommonDivisorFn @ROW) ?NUMBER)
(not
(equal ?NUMBER 0)))
(forall (?ELEMENT)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER) 0)))) |
Merge.kif 4973-4984 |
If equal the greatest common divisor of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Z mod Y and 0 |
(=>
(and
(equal
(GreatestCommonDivisorFn @ROW) ?NUMBER)
(not
(equal ?NUMBER 0)))
(not
(exists (?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall (?ELEMENT)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER) 0))))))) |
Merge.kif 4986-5000 |
If equal the greatest common divisor of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is greater than Y and W W is a member of (@ROW)equal W mod Z and 0 |
(=>
(and
(equal
(LeastCommonMultipleFn @ROW) ?NUMBER)
(not
(equal ?NUMBER 0)))
(forall (?ELEMENT)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT) 0)))) |
Merge.kif 5058-5068 |
If equal the least common multiple of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Y mod Z and 0 |
(=>
(and
(equal
(LeastCommonMultipleFn @ROW) ?NUMBER)
(not
(equal ?NUMBER 0)))
(not
(exists (?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall (?ELEMENT)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT) 0))))))) |
Merge.kif 5070-5084 |
If equal the least common multiple of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is less than Y and W W is a member of (@ROW)equal Z mod W and 0 |
(=>
(and
(not
(equal ?NUMBER2 0))
(equal
(AdditionFn
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
(equal
(RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)) |
Merge.kif 5229-5240 |
If equal X and 0 and equal (the largest integer less than or equal to Y and X and X and Z) and Y, then equal Y mod X and Z |
(=>
(instance ?NUMBER EvenInteger)
(equal
(RemainderFn ?NUMBER 2) 0)) |
Merge.kif 5256-5259 |
If X is an instance of even integer, then equal X mod 2 and 0 |
(=>
(instance ?NUMBER OddInteger)
(equal
(RemainderFn ?NUMBER 2) 1)) |
Merge.kif 5261-5264 |
If X is an instance of odd integer, then equal X mod 2 and 1 |
(=>
(instance ?PRIME PrimeNumber)
(forall (?NUMBER)
(=>
(and
(equal
(RemainderFn ?PRIME ?NUMBER) 0)
(not
(equal ?NUMBER 0)))
(or
(equal ?NUMBER 1)
(equal ?NUMBER ?PRIME))))) |
Merge.kif 5266-5277 |
If X is an instance of prime number, then For all Integer Y: if equal X mod Y and 0 and equal Y and 0, then equal Y and 1 or equal Y and X |
(=>
(and
(instance ?LEAP LeapYear)
(instance ?LEAP
(YearFn ?NUMBER)))
(or
(and
(equal
(RemainderFn ?NUMBER 4) 0)
(not
(equal
(RemainderFn ?NUMBER 100) 0)))
(equal
(RemainderFn ?NUMBER 400) 0))) |
Merge.kif 9203-9211 |
If X is an instance of leap year and X is an instance of the year Y, then equal Y mod 4 and 0 and equal Y mod 100 and 0 or equal Y mod 400 and 0 |
Jaw