CutLemma "Real(a1)&Zero < a1 -> Zero < Sup({x1 | Zero <x1 & x1*x1<a1})"; r(); l(); ThmCut "SUP2"; 
(* 5 *)  l(); UseThm "BDED" [1,2] [1]; 
(* 7 *)  ThmCut "SupLemma"; 
(* 8 *)  gl 2; gr 1; Done(); 
(* 11 *)  gl 3; gr 1; Done(); 
(* 14 *)  l(); l(); gl 2; l(); l(); r(); gl 4; gr 1; Done(); 
(* 23 *)  gl 5; l(); gl 3; l(); l(); NextGoal(); 
(* 29 *)  NextGoal(); 
(* 30 *)  NextGoal(); 
(* 31 *)  NextGoal(); 
(* 32 *)  ThmCut "TRANS"; 
(* 33 *)  l(); r(); gl 5; gr 1; Done(); 
(* 38 *)  Done(); 
(* 39 *)  Done(); 
(* 40 *)  l(); ThmCut "IPLUSa"; 
(* 42 *)  NextGoal(); 
(* 43 *)  NextGoal(); 
(* 44 *)  NextGoal(); 
(* 45 *)  NextGoal(); 
(* 46 *)  rwl [2]; gl 2; crwr [1]; gl 5; ThmCut "MPLUS"; 
(* 51 *)  l(); Done(); 
(* 53 *)  su 168 "Zero"; 
(* 54 *)  ThmCut "IPLUSa"; 
(* 55 *)  UseThm "RZERO" [] [1]; 
(* 56 *)  rwl [1]; gl 2; gr 1; Done(); 
(* 60 *)  UseThm "RSUP" [] [1]; 
(* 61 *)  NameSequent 367  "SUPPOS"; 
(* 62 *)  

(* 61

SUPPOS:



1:  Real(a1)

2:  Zero < a1

|-

1:  Zero < Sup({x77|Zero < x77 & x77 * x77 < a1})

*)


(* Sequent snapshot:


1:  Real(a1) & Zero < a1
      -> Zero < Sup({x77|Zero < x77 & 
     x77 * x77 < a1})

2:  (Ax77.Zero < x77
      & Real(x77) & x77 < Sup({x78|Zero < x78
      & x78 * x78 < a1})
      -> [a1
      + Minus(Sup({x79|
     Zero < x79 & x79 * x79 < a1})
      * Sup({x80|
     Zero < x80 & x80 * x80 < a1}))]
      * Inv(
     Three
      * Sup({x81|Zero < x81 & x81 * x81 < a1})) <= x77)

3:  (Ax77.
     x77 E {x78|Zero < x78 & x78 * x78 < a1}
      -> x77 <= Sup({x79|
     Zero < x79 & x79 * x79 < a1}))

4:  
     Sup({x77|Zero < x77 & x77 * x77 < a1})
      * Sup({x78|
     Zero < x78 & x78 * x78 < a1}) < a1

5:  Real(a1)

6:  Zero < a1

|-

1:  
     Sup({x77|Zero < x77 & x77 * x77 < a1})
      * Sup({x78|
     Zero < x78 & x78 * x78 < a1}) = a1

2:  (Ex77.x77 * x77 = a1)


*)

CutLemma "Real(a1) & Real(a2) & a1*a2 = Zero -> a1= Zero v a2 = Zero"; r(); r(); l(); gl 2; l(); ThmCut "TRI"; 
(* 69 *)  l(); ThmCut "EQUALITY"; 
(* 71 *)  Done(); 
(* 72 *)  gl 4; gr 1; Done(); 
(* 75 *)  UseThm "RZERO" [] [1]; 
(* 76 *)  Done(); 
(* 77 *)  l(); Cut "Inv(a1)*a1*a2 = Inv(a1) * Zero"; 
(* 79 *)  gl 3; rwr [1]; r(); ThmCut "ATIMES"; 
(* 83 *)  crwl [1]; pl 1; ThmCut "MZERO"; 
(* 86 *)  rwr [1]; rwl [1]; pl 1; ThmCut "INV"; 
(* 90 *)  l(); ThmCut "EQUALITY"; 
(* 92 *)  Done(); 
(* 93 *)  gl 6; gr 1; Done(); 
(* 96 *)  UseThm "RZERO" [] [1]; 
(* 97 *)  Done(); 
(* 98 *)  ThmCut "CTIMES"; 
(* 99 *)  rwl [1]; pl 1; rwl [1]; pl 1; ThmCut "ITIMES"; 
(* 104 *)  l(); gl 3; gr 1; Done(); 
(* 108 *)  ThmCut "CTIMES"; 
(* 109 *)  rwl [1]; pl 1; rwl [1]; gl 2; gr 2; Done(); 
(* 115 *)  Cut "Inv(a1) * a1 *a2 = Inv(a1) * Zero"; 
(* 116 *)  gl 3; rwr [1]; r(); ThmCut "ATIMES"; 
(* 120 *)  crwl [1]; pl 1; ThmCut "MZERO"; 
(* 123 *)  rwl [1]; pl 1; ThmCut "CTIMES"; 
(* 126 *)  rwl [2]; pl 1; ThmCut "INV"; 
(* 129 *)  l(); ThmCut "EQUALITY"; 
(* 131 *)  Done(); 
(* 132 *)  gl 6; gr 1; Done(); 
(* 135 *)  UseThm "RZERO" [] [1]; 
(* 136 *)  Done(); 
(* 137 *)  rwl [1]; pl 1; ThmCut "CTIMES"; 
(* 140 *)  rwl [1]; pl 1; ThmCut "ITIMES"; 
(* 143 *)  l(); gl 3; gr 1; Done(); 
(* 147 *)  rwl [1]; gl 2; gr 2; Done(); 

(* 151 *)  NameSequent 411 "ZPROD"; 
(* 152 *)  

(* 151

ZPROD:



1:  Real(a2)

2:  a1 * a2 = Zero

3:  Real(a1)

|-

1:  a1 = Zero

2:  a2 = Zero

*)


(* Sequent snapshot:


1:  Real(a1)
      & Real(a2) & a1 * a2 = Zero -> 
     a1 = Zero v a2 = Zero

2:  Real(a1) & Zero < a1
      -> Zero < Sup({x77|Zero < x77 & 
     x77 * x77 < a1})

3:  (Ax77.Zero < x77
      & Real(x77) & x77 < Sup({x78|Zero < x78
      & x78 * x78 < a1})
      -> [a1
      + Minus(Sup({x79|
     Zero < x79 & x79 * x79 < a1})
      * Sup({x80|
     Zero < x80 & x80 * x80 < a1}))]
      * Inv(
     Three
      * Sup({x81|Zero < x81 & x81 * x81 < a1})) <= x77)

4:  (Ax77.
     x77 E {x78|Zero < x78 & x78 * x78 < a1}
      -> x77 <= Sup({x79|
     Zero < x79 & x79 * x79 < a1}))

5:  
     Sup({x77|Zero < x77 & x77 * x77 < a1})
      * Sup({x78|
     Zero < x78 & x78 * x78 < a1}) < a1

6:  Real(a1)

7:  Zero < a1

|-

1:  
     Sup({x77|Zero < x77 & x77 * x77 < a1})
      * Sup({x78|
     Zero < x78 & x78 * x78 < a1}) = a1

2:  (Ex77.x77 * x77 = a1)


*)

CutLemma "Real(a1) & Zero < a1 & Zero =  [a1 + Minus(Sup({x13|Zero < x13 & x13 * x13 < a1})* Sup({x14|Zero < x14 & x14 * x14 < a1}))] * Inv(Three* Sup({x15|Zero < x15 & x15 * x15 < a1})) -> Zero = a1 + Minus(Sup({x13|Zero < x13 & x13 * x13 < a1})* Sup({x14|Zero < x14 & x14 * x14 < a1}))"; r(); l(); gl 2; l(); (* ThmCut "ZEROPROD"; *) 
(* 158 *)  

(* 157

No such theorem as ZEROPROD*)


(* Sequent snapshot:


1:  Zero < a1

2:  Zero = 
     [a1 + Minus(
     Sup({x13|Zero < x13 & x13 * x13 < a1})
      * Sup({x14|
     Zero < x14 & x14 * x14 < a1}))] * Inv(Three
      * Sup({x15|
     Zero < x15 & x15 * x15 < a1}))

3:  Real(a1)

|-

1:  Zero = a1 + Minus(
     Sup({x13|Zero < x13 & x13 * x13 < a1})
      * Sup({x14|
     Zero < x14 & x14 * x14 < a1}))


*)

ThmCut "ZPROD"; 
(* 159 *)  su 169 "Inv(Three* Sup({x15|Zero < x15 & x15 * x15 < a1}))"; 
(* 160 *)  UseThm "RINV" [] [1]; 
(* 161 *)  su 170 "[a1 + Minus(Sup({x13|Zero < x13 & x13 * x13 < a1})* Sup({x14|Zero < x14 & x14 * x14 < a1}))] "; 
(* 162 *)  gl 2; crwr [1]; r(); UseThm "RPLUS" [] [1]; 
(* 166 *)  crwr [1]; r(); Cut "[Three*Sup({x15|Zero < x15 & x15 * x15 < a1})]*[Inv(Three* Sup({x15|Zero < x15 & x15 * x15 < a1}))] = One"; 
(* 169 *)  ThmCut "INV"; 
(* 170 *)  l(); NextGoal(); 
(* 172 *)  NextGoal(); 
(* 173 *)  NextGoal(); 
(* 174 *)  NextGoal(); 
(* 175 *)  NextGoal(); 
(* 176 *)  NextGoal(); 
(* 177 *)  NextGoal(); 
(* 178 *)  NextGoal(); 
(* 179 *)  Done(); 
(* 180 *)  ThmCut "THREEPOS"; 
(* 181 *)  ThmCut "SUPPOS"; 
(* 182 *)  gl 6; gr 1; Done(); 
(* 185 *)  gl 4; gr 1; Done(); 
(* 188 *)  ThmCut "TIMESPOS"; 
(* 189 *)  gl 2; gr 1; Done(); 
(* 192 *)  Done(); 
(* 193 *)  UseThm "NOTBOTH3" [1,4] []; 
(* 194 *)  Cut "[Three*Sup({x15|Zero < x15 & x15 * x15 < a1})]*[Inv(Three* Sup({x15|Zero < x15 & x15 * x15 < a1}))] = Zero"; 
(* 195 *)  gl 2; rwr [1]; ThmCut "MZERO"; 
(* 198 *)  rwr [1]; r(); rwl [1]; ThmCut "NONTRIV"; 
(* 202 *)  l(); gl 2; rwr [1]; r(); r(); NameSequent 488 "ZFRAC"; 
(* 208 *)  

(* 207

ZFRAC:



1:  Zero < a1

2:  Zero = 
     [a1 + Minus(
     Sup({x78|Zero < x78 & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}))] * Inv(Three
      * Sup({x80|
     Zero < x80 & x80 * x80 < a1}))

3:  Real(a1)

|-

1:  Zero = a1 + Minus(
     Sup({x78|Zero < x78 & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}))

*)


(* Sequent snapshot:


1:  
     Real(a1)
      & Zero < a1
      & Zero = [a1
      + Minus(Sup({x78|Zero < x78
      & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}))]
      * Inv(
     Three
      * Sup({x80|Zero < x80 & x80 * x80 < a1})) -> Zero = a1
      + Minus(Sup({x81|
     Zero < x81 & x81 * x81 < a1})
      * Sup({x82|
     Zero < x82 & x82 * x82 < a1}))

2:  Real(a1)
      & Real(a2) & a1 * a2 = Zero -> 
     a1 = Zero v a2 = Zero

3:  Real(a1) & Zero < a1
      -> Zero < Sup({x78|Zero < x78 & 
     x78 * x78 < a1})

4:  (Ax78.Zero < x78
      & Real(x78) & x78 < Sup({x79|Zero < x79
      & x79 * x79 < a1})
      -> [a1
      + Minus(Sup({x80|
     Zero < x80 & x80 * x80 < a1})
      * Sup({x81|
     Zero < x81 & x81 * x81 < a1}))]
      * Inv(
     Three
      * Sup({x82|Zero < x82 & x82 * x82 < a1})) <= x78)

5:  (Ax78.
     x78 E {x79|Zero < x79 & x79 * x79 < a1}
      -> x78 <= Sup({x80|
     Zero < x80 & x80 * x80 < a1}))

6:  
     Sup({x78|Zero < x78 & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}) < a1

7:  Real(a1)

8:  Zero < a1

|-

1:  
     Sup({x78|Zero < x78 & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}) = a1

2:  (Ex78.x78 * x78 = a1)


*)

CutLemma "Real(a1) & Zero = a1 + Minus(Sup({x16|Zero < x16 & x16 * x16 < a1})* Sup({x17|Zero < x17 & x17 * x17 < a1})) -> a1 = Sup({x16|Zero < x16 & x16 * x16 < a1})* Sup({x17|Zero < x17 & x17 * x17 < a1})"; r(); l(); ThmCut "CPLUS"; 
(* 212 *)  gl2 3; rwl [1]; pl 1; ThmCut "UINV"; 
(* 216 *)  gl 2; gr 1; Done(); 
(* 219 *)  su 172 "Minus(Sup({x16|Zero < x16 & x16 * x16 < a1})* Sup({x17|Zero < x17 & x17 * x17 < a1}))"; 
(* 220 *)  crwr [1]; r(); ThmCut "DOUBLENEG"; 
(* 223 *)  su 172 "Sup({x16|Zero < x16 & x16 * x16 < a1})* Sup({x17|Zero < x17 & x17 * x17 < a1})"; 
(* 224 *)  UseThm "RTIMES" [] [1]; 
(* 225 *)  rwl [1]; gl 2; gr 1; Done(); 
(* 229 *)  NameSequent 528 "EQSUPa1"; 
(* 230 *)  

(* 229

EQSUPa1:



1:  Real(a1)

2:  Zero = a1 + Minus(
     Sup({x78|Zero < x78 & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}))

|-

1:  a1 = 
     Sup({x78|Zero < x78 & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1})

*)


(* Sequent snapshot:


1:  Real(a1)
      & Zero = a1 + Minus(
     Sup({x78|Zero < x78 & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}))
      -> a1 = Sup({x80|
     Zero < x80 & x80 * x80 < a1})
      * Sup({x81|
     Zero < x81 & x81 * x81 < a1})

2:  
     Real(a1)
      & Zero < a1
      & Zero = [a1
      + Minus(Sup({x78|Zero < x78
      & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}))]
      * Inv(
     Three
      * Sup({x80|Zero < x80 & x80 * x80 < a1})) -> Zero = a1
      + Minus(Sup({x81|
     Zero < x81 & x81 * x81 < a1})
      * Sup({x82|
     Zero < x82 & x82 * x82 < a1}))

3:  Real(a1)
      & Real(a2) & a1 * a2 = Zero -> 
     a1 = Zero v a2 = Zero

4:  Real(a1) & Zero < a1
      -> Zero < Sup({x78|Zero < x78 & 
     x78 * x78 < a1})

5:  (Ax78.Zero < x78
      & Real(x78) & x78 < Sup({x79|Zero < x79
      & x79 * x79 < a1})
      -> [a1
      + Minus(Sup({x80|
     Zero < x80 & x80 * x80 < a1})
      * Sup({x81|
     Zero < x81 & x81 * x81 < a1}))]
      * Inv(
     Three
      * Sup({x82|Zero < x82 & x82 * x82 < a1})) <= x78)

6:  (Ax78.
     x78 E {x79|Zero < x79 & x79 * x79 < a1}
      -> x78 <= Sup({x80|
     Zero < x80 & x80 * x80 < a1}))

7:  
     Sup({x78|Zero < x78 & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}) < a1

8:  Real(a1)

9:  Zero < a1

|-

1:  
     Sup({x78|Zero < x78 & x78 * x78 < a1})
      * Sup({x79|
     Zero < x79 & x79 * x79 < a1}) = a1

2:  (Ex78.x78 * x78 = a1)


*)