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

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

1. prime(2)
2. p :

3. q :

4. p

p = 2

q
5. p' :

6. p = 2

p'
7.

, b:

. a

b>0

a>0 & b>0

2>0 & p>0 & p'>0

By:	2>0 By Analyze1 THEN 2qq>0 By Repeat BackThru: Hyp:7 THEN p>0 By FwdThru: Hyp:7 on [ pp>0 ] THEN p'>0 By Sel 2 FwdThru: Hyp:7 on [ 2p'>0 ]

Generated subgoals:

None

About:

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