a:
. prime(a) 
(
p:, q:
. p
p = aqq)P:(
Prop). (x:. P(x) (x':. x'<x & P(x'))) (x:. P(x))a:.
Thm* prime(a)
(p:, q:. pp = aqq (p':. p'<p & qq = ap'p'))| Rank | Theorem | Name |
| 12 | a:. prime(a) (p:, q:. pp = aqq) | [primes_sqr_roots] |
| cites the following: | ||
| 0 | P:(Prop). (x:. P(x) (x':. x'<x & P(x'))) (x:. P(x)) | [nat_descent] |
| 11 | a:.
Thm* prime(a) (p:, q:. pp = aqq (p':. p'<p & qq = ap'p')) | [primes_sqr_roots_LEMMA1] |