p:
, q:
. p
p = 2qq 
(
p':. p'<p & qq = 2p'p')x:
. Dec(prime(x))a:. prime(a) (x:. a | xx 
a | x)a,b:. ab>0 a>0 & b>0 
a<0 & b<0a,b:, n:
. na = nb a = b| Rank | Theorem | Name |
| 12 | p:, q:. pp = 2qq (p':. p'<p & qq = 2p'p') | [two_sqr_roots_LEMMA1] |
| cites the following: | ||
| 11 | x:. Dec(prime(x)) | [decidable__prime] |
| 1 | a:. prime(a) (x:. a | xx a | x) | [prime_divides_square] |
| 3 | a,b:. ab>0 a>0 & b>0 a<0 & b<0 | [pos_mul_arg_bounds] |
| 3 | a,b:, n:. na = nb a = b | [mul_cancel_in_eq] |