Nuprl - Proof: primes sqr roots LEMMA1 1 2 1 a 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: primes sqr roots LEMMA1 1 2 1 a 1

1. a :

2. prime(a)
3. p :

4. q :

5. p

p = a

q
6. p' :

7. p = a

p'
8.

, b:

. a

b>0

a>0 & b>0

a>0 & p>0 & p'>0

By:	a>0 By Analyze2 THEN aqq>0 By Repeat BackThru: Hyp:8 THEN p>0 By FwdThru: Hyp:8 on [ pp>0 ] THEN p'>0 By Sel 2 FwdThru: Hyp:8 on [ ap'>0 ]

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html