Selected Objects
| COM | simple_mul_factsVERSION
|
1 |
| THM | nat_prod_one_iff_factors_one
|
 x,y: . x y = 1   x = 1 & y = 1 |
| THM | prod_zero_iff_factor_zero
|
a,b: . ab = 0 a = 0  b = 0 |
| THM | mul_nat_com
|
a,b,c,d:. a = b  c = d ac = db  |
| THM | nat_factor_cancel_rw
|
a,b:, n: . na nb ab |
| THM | mul_cancel_in_eq1
|
a,b:, n:  . na = nb a = b |
| THM | mul_cancel_in_eq2
|
a,b:, m,n:. m = n (ma = nb a = b) |
| THM | le_mul_rt_by_pos
|
x,y:, z:. xy xyz |
| THM | factor_bound
|
k:, n:, x,y:. kx+n = ky xy |
| THM | lt_mul_rt_by_pos
|
x,y:, z:. x<y x<yz |
| THM | factors_bound
|
i,j:. iij & jij |
| THM | pos_mul_arg_boundsNat
|
a,b:. 0<ab 0<a & 0<b |
| THM | pos_mul_arg_boundsNat2
|
i,j:. 0<ij iij & jij |
| THM | factor_smaller
|
i:{2...}, j:{1...}. j<ij |
| THM | factor_smaller2
|
i:{2...}, j:. j<ij |
| THM | factors_smaller
|
i,j:{2...}. i<ij & j<ij |
| THM | factors_smaller2
|
k:, i:{2..k}, j:. ij = k 2 j < k & i<k |
| THM | mul_nat_plus
|
x,y:. xy |
| THM | divides_def_on_nat
|
a divides b (specialized to natural numbers)
a,b:. a | b ( c:. b = ac) |
| THM | only_one_nat_divs_one
|
b:. b | 1 b = 1 |
| THM | div_inverts_nat_mul
|
x,y:, z:. x = yz (x  z) = y |
| THM | div_inverts_nat_mul2
|
x:, y,z:. x = yz (x z) = y |
| THM | prime_nat
|
x:. prime(x) 2x &  (i:{2..x}. i | x) |
| def | prime_nats
|
Prime == {x:| prime(x) } |
| THM | natprimes_lb
|
x:. prime(x) 2x |
| THM | natprime_nondivs
|
x:. prime(x) (i:{2..x}. i | x) |
| THM | nonprime_nat
|
x:. prime(x) x<2 (i,j:{2..x}. x = ij) |
| THM | composite_with_prime_factor
|
x:{2...}. prime(x) (i,j:{2..x}. x = ij & prime(i)) |
| THM | prime_or_smaller_prime_factor2
|
x:{2...}. p:{2...}, c:{1...}. px & prime(p) & x = pc |
| THM | prime_or_smaller_prime_factor
|
A number bigger than 1 is divisible by a prime.
x:{2...}. p:{2...}. px & prime(p) & p | x |
| THM | prime_neg
|
y:. prime(-y) prime(y) |
| THM | decidable__prime
|
x:. Dec(prime(x)) |
| THM | prime_decider_exists
|
!{p:(   )| x:. p(x) prime(x) } |
| def | prime_decider
|
Boolean decider for primeness implicit in Thm* !{p:()| x:. p(x) prime(x) }
is_prime(x) == prime_decider_exists{1:l}(x) |
| THM | no_nat_prime_divs_one
|
b:. b | 1 prime(b) |
| THM | no_prime_divs_one
|
One has no prime divisors.
b:. b | 1 prime(b) |
| THM | no_prime_divs_one_b
|
One has no prime divisors.
b:. prime(b) b | 1 |
| THM | prime_nat_divby_self_only
|
x:{2...}, y:. prime(y) x | y x = y |
| THM | prime_among_factors
|
Factoring a prime always includes the prime itself.
a,b:. prime(ab) ab = a ab = b |