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 "ZPROD"; 
(* 158 *)  su 169 "Inv(Three* Sup({x15|Zero < x15 & x15 * x15 < a1}))"; 
(* 159 *)  UseThm "RINV" [] [1]; 
(* 160 *)  su 170 "[a1 + Minus(Sup({x13|Zero < x13 & x13 * x13 < a1})* Sup({x14|Zero < x14 & x14 * x14 < a1}))] "; 
(* 161 *)  gl 2; crwr [1]; r(); UseThm "RPLUS" [] [1]; 
(* 165 *)  crwr [1]; r(); Cut "[Three*Sup({x15|Zero < x15 & x15 * x15 < a1})]*[Inv(Three* Sup({x15|Zero < x15 & x15 * x15 < a1}))] = One"; 
(* 168 *)  ThmCut "INV"; 
(* 169 *)  l(); NextGoal(); 
(* 171 *)  NextGoal(); 
(* 172 *)  NextGoal(); 
(* 173 *)  NextGoal(); 
(* 174 *)  NextGoal(); 
(* 175 *)  NextGoal(); 
(* 176 *)  NextGoal(); 
(* 177 *)  NextGoal(); 
(* 178 *)  Done(); 
(* 179 *)  ThmCut "THREEPOS"; 
(* 180 *)  ThmCut "SUPPOS"; 
(* 181 *)  gl 6; gr 1; Done(); 
(* 184 *)  gl 4; gr 1; Done(); 
(* 187 *)  ThmCut "TIMESPOS"; 
(* 188 *)  gl 2; gr 1; Done(); 
(* 191 *)  Done(); 
(* 192 *)  UseThm "NOTBOTH3" [1,4] []; 
(* 193 *)  Cut "[Three*Sup({x15|Zero < x15 & x15 * x15 < a1})]*[Inv(Three* Sup({x15|Zero < x15 & x15 * x15 < a1}))] = Zero"; 
(* 194 *)  gl 2; rwr [1]; ThmCut "MZERO"; 
(* 197 *)  rwr [1]; r(); rwl [1]; ThmCut "NONTRIV"; 
(* 201 *)  l(); gl 2; rwr [1]; r(); r(); NameSequent 488 "ZFRAC"; 
(* 207 *)  

(* 206

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"; 
(* 211 *)  gl2 3; rwl [1]; pl 1; ThmCut "UINV"; 
(* 215 *)  gl 2; gr 1; Done(); 
(* 218 *)  su 172 "Minus(Sup({x16|Zero < x16 & x16 * x16 < a1})* Sup({x17|Zero < x17 & x17 * x17 < a1}))"; 
(* 219 *)  crwr [1]; r(); ThmCut "DOUBLENEG"; 
(* 222 *)  su 172 "Sup({x16|Zero < x16 & x16 * x16 < a1})* Sup({x17|Zero < x17 & x17 * x17 < a1})"; 
(* 223 *)  UseThm "RTIMES" [] [1]; 
(* 224 *)  rwl [1]; gl 2; gr 1; Done(); 
(* 228 *)  NameSequent 528 "EQSUPa1"; 
(* 229 *)  

(* 228

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)


*)

gl 4; l(); r(); gl 4; gr 1; Done(); 
(* 235 *)  gl 5; gr 1; Done(); 
(* 238 *)  Cut2 "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}))"; 
(* 239 *)  ThmCut "EPSLEMMA"; 
(* 240 *)  su 172 " [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}))"; 
(* 241 *)  r(); r(); crwr [1]; r(); r(); UseThm "RTIMES" [] [1]; 
(* 251 *)  gl 2; gr 1; Done(); 
(* 254 *)  UseThm "RSUP" [] [1]; 
(* 255 *)  r(); r(); gl 2; crwr [1]; gl 11; l(); gl 2; l(); r(); r(); gl 1; gr 2; Done(); 
(* 278 *)  pl 1; 

(* 278 *)

hardcomment "frac = zero";


(* Sequent snapshot:


1:  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}))

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

3:  (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)

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

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

6:  Real(a1)

7:  Zero < a1

8:  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})

9:  
     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}))

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

|-

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

2:  (Ex78.x78 * x78 = a1)


*)

gl 9; l(); r(); gl 7; gr 1; Done(); 
(* 285 *)  r(); gl 8; gr 1; Done(); 
(* 289 *)  gl 2; gr 1; Done(); 
(* 292 *)  gl 10; l(); r(); gl 8; gr 1; Done(); 
(* 298 *)  Done(); 
(* 299 *)  crwr [1]; r(); 

(* 300 *)

hardcomment "now proving the cut was legal!";


(* Sequent snapshot:


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

2:  (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)

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

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

5:  Real(a1)

6:  Zero < a1

7:  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})

8:  
     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}))

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

|-

1:  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}))

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

3:  (Ex78.x78 * x78 = a1)


*)

ThmCut "EPSLEMMA"; 
(* 302 *)  su 174 "[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}))"; 
(* 303 *)  ThmCut "MPLUS"; 
(* 304 *)  l(); gl 4; gr 1; Done(); 
(* 308 *)  su 178 "Minus(Sup({x78|Zero < x78 & x78 * x78 < a1})* Sup({x79|Zero < x79 & x79 * x79 < a1}))"; 
(* 309 *)  ThmCut "MINUS"; 
(* 310 *)  su 178 "Sup({x78|Zero < x78 & x78 * x78 < a1})* Sup({x79|Zero < x79 & x79 * x79 < a1})"; 
(* 311 *)  rwl [1]; pl 1; ThmCut "THREEPOS"; 
(* 314 *)  ThmCut "TIMESPOS"; 
(* 315 *)  Done(); 
(* 316 *)  gl 3; gr 1; Done(); 
(* 319 *)  ThmCut "POSINV"; 
(* 320 *)  Done(); 
(* 321 *)  pl 2; pl 1; ThmCut "TIMESPOS"; 
(* 324 *)  Done(); 
(* 325 *)  gl 11; gr 1; Done(); 
(* 328 *)  r(); r(); gl 1; gr 2; Done(); 
(* 333 *)  UseThm "RTIMES" [] [1]; 
(* 349 *)  

(* 348 *)  Done(); 
(* 350 *)  UseThm "RSUP" [] [1]; 
(* 351 *)  r(); r(); gl 3; l(); l(); r(); gl 9; l(); gl 2; l(); Done(); 
(* 362 *)  r(); gl 9; l(); Done(); 
(* 366 *)  gl 9; l(); gl 2; l(); gl 2; gr 1; Done(); 
(* 373 *)  Done(); 
(* 374 *)  Done(); 
(* 375 *)  

(* 374 *)





Cut "(Ax2.Zero<x2 & Real(x2) & x2<Sup({x3|Zero < x3 & x3 * x3<a1})->[Sup({x70|Zero < x70 & x70 * x70 < a1})* Sup({x71|Zero < x71 &x71 * x71 < a1})+Minus(a1)] * Inv(Two* Sup({x72|Zero < x72 & x72 *x72 < a1}))<=x2)"; 
(* 2 *)  r(); r(); l(); gl 2; l(); CutLemma "Zero<a181 -> Minus(a181) < Zero"; r(); ThmCut "MPLUS"; 
(* 10 *)  l(); Done(); 
(* 12 *)  su 184 "Minus(a181)"; 
(* 13 *)  ThmCut "IPLUSb"; 
(* 14 *)  NextGoal(); 
(* 15 *)  NextGoal(); 
(* 16 *)  NextGoal(); 
(* 17 *)  NextGoal(); 
(* 18 *)  rwl [1]; pl 1; ThmCut "MINUS"; 
(* 21 *)  rwl [1]; pl 1; Done(); 
(* 24 *)  UseThm "RMINUS" [] [1]; 
(* 25 *)  NameSequent 627 "NEGINEQ2"; 
(* 26 *)  

(* 25

NEGINEQ2:



1:  Zero < a181

|-

1:  Minus(a181) < Zero

*)


(* Sequent snapshot:


1:  Zero < a181 -> Minus(a181) < Zero

2:  Real(a181)

3:  a181 < Sup({x80|Zero < x80 & x80 * x80 < a1})

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

5:  Real(a1)

6:  Zero < a1

7:  Zero < a181

|-

1:  [
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      * Sup({x82|
     Zero < x82 & x82 * x82 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x83|Zero < x83 & 
     x83 * x83 < a1})) <= a181

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)


*)

l(); gl 6; gr 1; Done(); 
(* 30 *)  ThmCut "MPLUS"; 
(* 31 *)  l(); Done(); 
(* 33 *)  su 186 "Sup({x80|Zero<x80 & x80*x80 < a1})"; 
(* 34 *)  ThmCut "IPLUSb"; 
(* 35 *)  NextGoal(); 
(* 36 *)  NextGoal(); 
(* 37 *)  rwl [1]; pl 1; ThmCut "CPLUS"; 
(* 40 *)  rwl [1]; pl 1; ThmCut "SquareOrder1"; 
(* 43 *)  Done(); 
(* 44 *)  CutLemma "a181 < Sup({x80|Zero<x80 & x80*x80 < a1}) -> Zero < Sup({x80|Zero<x80 & x80*x80 < a1})+ Minus(a181)"; r(); ThmCut "MPLUS"; 
(* 47 *)  l(); Done(); 
(* 49 *)  su 188 "Minus(a181)"; 
(* 50 *)  ThmCut "MINUS"; 
(* 51 *)  rwl [1]; pl 1; Done(); 
(* 54 *)  NameSequent 659 "SUPMINUSPOS"; 
(* 55 *)  

(* 54

SUPMINUSPOS:



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

|-

1:  Zero < 
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      + Minus(a181)

*)


(* Sequent snapshot:


1:  Minus(a181)
      + Sup({x80|Zero < x80 & x80 * x80 < a1}) < Zero
      + Sup({x81|
     Zero < x81 & x81 * x81 < a1})

2:  Minus(a181) < Zero

3:  Real(a181)

4:  a181 < Sup({x80|Zero < x80 & x80 * x80 < a1})

5:  a1 < 
     Sup({x80|Zero < x80 & x80 * x80 < a1})
      * Sup({x81|
     Zero < x81 & x81 * x81 < a1})

6:  Real(a1)

7:  Zero < a1

8:  Zero < a181

|-

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

2:  [
     Sup({x80|Zero < x80 & x80 * x80 < a1})
      * Sup({x81|
     Zero < x81 & x81 * x81 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x82|Zero < x82 & 
     x82 * x82 < a1})) <= a181

3:  
     Sup({x80|Zero < x80 & x80 * x80 < a1})
      * Sup({x81|
     Zero < x81 & x81 * x81 < a1}) = a1

4:  (Ex80.x80 * x80 = a1)


*)

UseThm "RSUP" [] [1]; 
(* 56 *)  UseThm "SUPMINUSPOS" [5] [1]; 
(* 57 *)  UseThm "SUPPOS" [6,7] [1]; 
(* 58 *)  ThmCut "TRI"; 
(* 59 *)  l(); su 188 "a1"; 
(* 61 *)  su 189 "[Sup({x3|Zero < x3 & x3 * x3 < a1})+Minus(a181)]*[Sup({x3|Zero < x3 & x3 * x3 < a1})+Minus(a181)]"; 
(* 62 *)  ThmCut "EQUALITY"; 
(* 63 *)  Done(); 
(* 64 *)  gl 8; gr 1; Done(); 
(* 67 *)  UseThm "RTIMES" [] [1]; 
(* 68 *)  

(* 67 *)

hardcomment "going for contra";


(* Sequent snapshot:


1:  a1 = [
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      + Minus(a181)] * [
     Sup({x82|Zero < x82 & 
     x82 * x82 < a1}) + Minus(a181)]

2:  a1 Equal [
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      + Minus(a181)] * [
     Sup({x82|Zero < x82 & 
     x82 * x82 < a1}) + Minus(a181)]

3:  [
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      + Minus(a181)] * [
     Sup({x82|Zero < x82 & 
     x82 * x82 < a1}) + Minus(a181)] < Sup({x83|
     Zero < x83 & x83 * x83 < a1})
      * Sup({x84|
     Zero < x84 & x84 * x84 < a1})

4:  
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      + Minus(a181) < Sup({x82|Zero < x82
      & x82 * x82 < a1})

5:  Minus(a181) < Zero

6:  Real(a181)

7:  a181 < Sup({x81|Zero < x81 & x81 * x81 < a1})

8:  a1 < 
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      * Sup({x82|
     Zero < x82 & x82 * x82 < a1})

9:  Real(a1)

10:  Zero < a1

11:  Zero < a181

|-

1:  [
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      * Sup({x82|
     Zero < x82 & x82 * x82 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x83|Zero < x83 & 
     x83 * x83 < a1})) <= a181

2:  
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      * Sup({x82|
     Zero < x82 & x82 * x82 < a1}) = a1

3:  (Ex81.x81 * x81 = a1)


*)

NextGoal(); 
(* 69 *)  NextGoal(); 
(* 70 *)  l(); ThmCut "SUP1"; 
(* 72 *)  l(); r(); ThmCut "SupLemma"; 
(* 75 *)  gl 8; gr 1; Done(); 
(* 78 *)  gl 9; gr 1; Done(); 
(* 81 *)  Done(); 
(* 82 *)  r(); r(); l(); l(); 

(* 85 *)





ThmCut "TRANS"; 
(* 87 *)  l(); r(); gl 2; gr 1; Done(); 
(* 92 *)  gl 3; gr 1; Done(); 
(* 95 *)  ThmCut "SquareOrder2"; 
(* 96 *)  Done(); 
(* 97 *)  gl 2; gr 1; Done(); 
(* 100 *)  UseThm "SUPMINUSPOS" [9] [1]; 
(* 101 *)  r(); r(); gl 1; gr 2; Done(); 
(* 106 *)  l(); l(); UseThm "NOTBOTH3" [4,1] []; 
(* 109 *)  UseThm "NOTBOTH" [1,4] []; 
(* 110 *)  

(* 109 *)



ThmCut "FOIL"; 
(* 111 *)  rwl [1]; pl 1; ThmCut "TIMESDOUBNEG"; 
(* 114 *)  rwl [1]; pl 1; ThmCut "NEGCOMM"; 
(* 117 *)  rwl [1]; pl 1; ThmCut "NEGCOMM"; 
(* 120 *)  rwl [1]; pl 1; ThmCut "MPLUS"; 
(* 123 *)  l(); Done(); 
(* 125 *)  su 196 "Two * Sup({x3|Zero < x3 & x3 * x3 < a1})*a181"; 
(* 126 *)  ThmCut "APLUS"; 
(* 127 *)  rwl [1]; pl 1; ThmCut "APLUS"; 
(* 130 *)  rwl [1]; pl 1; ThmCut "CPLUS"; 
(* 133 *)  rwl [3]; pl 1; ThmCut "APLUS"; 
(* 136 *)  crwl [2]; pl 1; ThmCut "MINUS"; 
(* 139 *)  ThmCut "CPLUS"; 
(* 140 *)  rwl [1]; pl 1; rwl [1]; pl 1; ThmCut "IPLUSb"; 
(* 145 *)  NextGoal(); 
(* 146 *)  NextGoal(); 
(* 147 *)  NextGoal(); 
(* 148 *)  NextGoal(); 
(* 149 *)  rwl [1]; pl 1; ThmCut "MPLUS"; 
(* 152 *)  l(); Done(); 
(* 154 *)  su 198 "Minus(a181*a181)"; 
(* 155 *)  pl 2; pl 2; ThmCut "APLUS"; 
(* 158 *)  gl2 10; rwl []; pl 1; ThmCut "APLUS"; 
(* 162 *)  rwl [1]; pl 1; ThmCut "MINUS"; 
(* 165 *)  rwl [1]; pl 1; ThmCut "IPLUSa"; 
(* 168 *)  NextGoal(); 
(* 169 *)  NextGoal(); 
(* 170 *)  NextGoal(); 
(* 171 *)  NextGoal(); 
(* 172 *)  UseThm "RTIMES" [] [1]; 
(* 173 *)  rwl [1]; pl 1; ThmCut "MPLUS"; 
(* 176 *)  l(); Done(); 
(* 178 *)  su 200 "Minus(a1)"; 
(* 179 *)  ThmCut "CPLUS"; 
(* 180 *)  rwl [2]; pl 1; pl 2; pl 1; ThmCut "APLUS"; 
(* 185 *)  gl2 10; crwl [1]; pl 1; ThmCut "MINUS"; 
(* 189 *)  ThmCut "CPLUS"; 
(* 190 *)  rwl [1]; pl 1; rwl [1]; pl 1; ThmCut "IPLUSb"; 
(* 195 *)  NextGoal(); 
(* 196 *)  NextGoal(); 
(* 197 *)  NextGoal(); 
(* 198 *)  NextGoal(); 
(* 199 *)  UseThm "RTIMES" [] [1]; 
(* 200 *)  rwl [1]; pl 1; CutLemma "Zero < a181 * a181 -> Two*Sup({x3|Zero < x3 & x3 * x3 < a1})*a181 + Minus(a181*a181) < Two *Sup({x3|Zero < x3 & x3 * x3 < a1})*a181"; r(); ThmCut "MPLUS"; 
(* 205 *)  l(); Done(); 
(* 207 *)  su 202 "Minus(a181*a181)"; 
(* 208 *)  ThmCut "MINUS"; 
(* 209 *)  rwl [1]; pl 1; ThmCut "IPLUSb"; 
(* 212 *)  NextGoal(); 
(* 213 *)  NextGoal(); 
(* 214 *)  NextGoal(); 
(* 215 *)  NextGoal(); 
(* 216 *)  UseThm "RPLUS" [] [1]; 
(* 217 *)  NextGoal(); 
(* 218 *)  NextGoal(); 
(* 219 *)  NextGoal(); 
(* 220 *)  NextGoal(); 
(* 221 *)  rwl [1]; pl 1; ThmCut "MPLUS"; 
(* 224 *)  l(); Done(); 
(* 226 *)  su 204 "Two *Sup({x3|Zero < x3 & x3 * x3 < a1})*a181"; 
(* 227 *)  ThmCut "IPLUSb"; 
(* 228 *)  NextGoal(); 
(* 229 *)  NextGoal(); 
(* 230 *)  NextGoal(); 
(* 231 *)  NextGoal(); 
(* 232 *)  NextGoal(); 
(* 233 *)  NextGoal(); 
(* 234 *)  NextGoal(); 
(* 235 *)  NextGoal(); 
(* 236 *)  UseThm "RMINUS" [] [1]; 
(* 237 *)  rwl [1]; pl 1; ThmCut "CPLUS"; 
(* 240 *)  rwl [1]; pl 1; Done(); 
(* 243 *)  UseThm "RTIMES" [] [1]; 
(* 244 *)  NameSequent 785 "SUBLESS"; 
(* 245 *)  

(* 244

SUBLESS:



1:  Zero < a181 * a181

|-

1:  Two * 
     Sup({x106|Zero < x106 & x106 * x106 < a1})
      * a181
      + Minus(a181 * a181) < Two * 
     Sup({x107|Zero < x107 & x107
      * x107 < a1}) * a181

*)


(* Sequent snapshot:


1:  a1 = [
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      + Minus(a181)] * [
     Sup({x82|Zero < x82 & 
     x82 * x82 < a1}) + Minus(a181)]

2:  a1 Equal [
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      + Minus(a181)] * [
     Sup({x82|Zero < x82 & 
     x82 * x82 < a1}) + Minus(a181)]

3:  [
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      + Minus(a181)] * [
     Sup({x82|Zero < x82 & 
     x82 * x82 < a1}) + Minus(a181)] < Sup({x83|
     Zero < x83 & x83 * x83 < a1})
      * Sup({x84|
     Zero < x84 & x84 * x84 < a1})

4:  
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      + Minus(a181) < Sup({x82|Zero < x82
      & x82 * x82 < a1})

5:  Minus(a181) < Zero

6:  Real(a181)

7:  a181 < Sup({x81|Zero < x81 & x81 * x81 < a1})

8:  a1 < 
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      * Sup({x82|
     Zero < x82 & x82 * x82 < a1})

9:  Real(a1)

10:  Zero < a1

11:  Zero < a181

|-

1:  [
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      * Sup({x82|
     Zero < x82 & x82 * x82 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x83|Zero < x83 & 
     x83 * x83 < a1})) <= a181

2:  
     Sup({x81|Zero < x81 & x81 * x81 < a1})
      * Sup({x82|
     Zero < x82 & x82 * x82 < a1}) = a1

3:  (Ex81.x81 * x81 = a1)


*)

NextGoal(); 
(* 246 *)  NextGoal(); 
(* 247 *)  l(); UseThm "SQPOS" [9] [1]; 
(* 249 *)  ThmCut "TRANS"; 
(* 250 *)  l(); r(); gl 2; gr 1; Done(); 
(* 255 *)  Done(); 
(* 256 *)  Cut2 "Zero<Two*Sup({x3|Zero < x3 & x3 * x3 < a1})"; 
(* 257 *)  ThmCut "MTIMES"; 
(* 258 *)  l(); r(); UseThm "POSINV" [1] [1]; 
(* 261 *)  gl 2; gr 1; Done(); 
(* 264 *)  pl 5; pl 12; ThmCut "CTIMES"; 
(* 267 *)  gl2 10; rwl [4]; pl 1; ThmCut "ATIMES"; 
(* 271 *)  crwl [4]; crwl [3]; crwl [2]; pl 1; ThmCut "ATIMES"; 
(* 276 *)  crwl [1]; pl 1; ThmCut "INV"; 
(* 279 *)  l(); NextGoal(); 
(* 281 *)  NextGoal(); 
(* 282 *)  NextGoal(); 
(* 283 *)  NextGoal(); 
(* 284 *)  NextGoal(); 
(* 285 *)  NextGoal(); 
(* 286 *)  NextGoal(); 
(* 287 *)  NextGoal(); 
(* 288 *)  ThmCut "CTIMES"; 
(* 289 *)  rwl [1]; pl 1; rwl [1]; pl 1; ThmCut "ITIMES"; 
(* 294 *)  l(); NextGoal(); 
(* 296 *)  NextGoal(); 
(* 297 *)  NextGoal(); 
(* 298 *)  NextGoal(); 
(* 299 *)  NextGoal(); 
(* 300 *)  NextGoal(); 
(* 301 *)  NextGoal(); 
(* 302 *)  NextGoal(); 
(* 303 *)  NextGoal(); 
(* 304 *)  NextGoal(); 
(* 305 *)  NextGoal(); 
(* 306 *)  NextGoal(); 
(* 307 *)  NextGoal(); 
(* 308 *)  NextGoal(); 
(* 309 *)  NextGoal(); 
(* 310 *)  NextGoal(); 
(* 311 *)  ThmCut "CTIMES"; 
(* 312 *)  rwl [1]; pl 1; rwl [1]; pl 1; r(); r(); gl 1; gr 2; Done(); 
(* 321 *)  gl 6; gr 1; Done(); 
(* 324 *)  UseThm "NOTBOTH3" [3,1] []; 
(* 325 *)  ThmCut "TWOPOS"; 
(* 326 *)  ThmCut "SUPPOS"; 
(* 327 *)  gl 10; gr 1; Done(); 
(* 330 *)  gl 11; gr 1; Done(); 
(* 333 *)  UseThm "TIMESPOS" [2,1] [1]; 
(* 334 *)  ThmCut "FOIL"; 
(* 335 *)  rwl [1]; pl 1; ThmCut "TIMESDOUBNEG"; 
(* 338 *)  rwl [1]; pl 1; ThmCut "NEGCOMM"; 
(* 341 *)  rwl [1]; pl 1; ThmCut "NEGCOMM"; 
(* 344 *)  rwl [1]; pl 1; CutLemma "a1 = a2 -> a1+a3 = a2+a3"; r(); rwr [1]; r(); NameSequent 873 "ADDEQ"; 
(* 351 *)  

(* 350

ADDEQ:



1:  a1 = a2

|-

1:  a1 + a3 = a2 + a3

*)


(* Sequent snapshot:


1:  a1 = a2 -> a1 + a3 = a2 + a3

2:  a1 = 
     Sup({x115|Zero < x115 & x115 * x115 < a1})
      * Sup({x116|
     Zero < x116 & x116 * x116 < a1}) + Minus(
     Two * 
     Sup({x117|Zero < x117 & x117 * x117 < a1})
      * a181)
      + a181 * a181

3:  a1 Equal [
     Sup({x115|Zero < x115 & x115 * x115 < a1})
      + Minus(a181)] * [
     Sup({x116|Zero < x116 & 
     x116 * x116 < a1}) + Minus(a181)]

4:  [
     Sup({x115|Zero < x115 & x115 * x115 < a1})
      + Minus(a181)] * [
     Sup({x116|Zero < x116 & 
     x116 * x116 < a1}) + Minus(a181)] < 
     Sup({x117|
     Zero < x117 & x117 * x117 < a1})
      * Sup({x118|Zero < x118 & 
     x118 * x118 < a1})

5:  
     Sup({x115|Zero < x115 & x115 * x115 < a1})
      + Minus(a181) < Sup({x116|Zero < x116
      & x116 * x116 < a1})

6:  Minus(a181) < Zero

7:  Real(a181)

8:  a181 < Sup({x115|Zero < x115 & x115 * x115 < a1})

9:  a1 < 
     Sup({x115|Zero < x115 & x115 * x115 < a1})
      * Sup({x116|
     Zero < x116 & x116 * x116 < a1})

10:  Real(a1)

11:  Zero < a1

12:  Zero < a181

|-

1:  [
     Sup({x115|Zero < x115 & x115 * x115 < a1})
      * Sup({x116|
     Zero < x116 & x116 * x116 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x117|Zero < x117 & 
     x117 * x117 < a1})) <= a181

2:  
     Sup({x115|Zero < x115 & x115 * x115 < a1})
      * Sup({x116|
     Zero < x116 & x116 * x116 < a1}) = a1

3:  (Ex115.x115 * x115 = a1)


*)

pl 1; ThmCut "ADDEQ"; 
(* 353 *)  Done(); 
(* 354 *)  su 209 "Minus(a1)"; 
(* 355 *)  ThmCut "MINUS"; 
(* 356 *)  rwl [1]; pl 1; ThmCut "ADDEQ"; 
(* 359 *)  Done(); 
(* 360 *)  su 211 "Two*Sup({x81|Zero < x81 & x81 * x81 < a1})*a181"; 
(* 361 *)  pl 2; pl 1; pl 1; gl 10; ThmCut "IPLUSb"; 
(* 366 *)  NextGoal(); 
(* 367 *)  NextGoal(); 
(* 368 *)  rwl [1]; pl 1; ThmCut "CPLUS"; 
(* 374 *)  rwl [1]; pl 1; ThmCut "APLUS"; 
(* 377 *)  rwl [1]; pl 1; ThmCut "APLUS"; 
(* 380 *)  rwl [1]; pl 1; ThmCut "APLUS"; 
(* 383 *)  crwl [1]; pl 1; ThmCut "CPLUS"; 
(* 386 *)  rwl [2]; pl 1; ThmCut "APLUS"; 
(* 397 *)  rwl [1]; pl 1; ThmCut "APLUS"; 
(* 400 *)  crwl [2]; pl 1; ThmCut "MINUS"; 
(* 403 *)  rwl [1]; pl 1; ThmCut "IPLUSb"; 
(* 406 *)  NextGoal(); 
(* 407 *)  NextGoal(); 
(* 408 *)  UseThm "RTIMES" [] [1]; 
(* 409 *)  rwl [1]; pl 1; ThmCut "ADDEQ"; 
(* 412 *)  Done(); 
(* 413 *)  su 213 "Minus(a181*a181)"; 
(* 414 *)  ThmCut "APLUS"; 
(* 415 *)  rwl [1]; pl 1; ThmCut "APLUS"; 
(* 418 *)  rwl [1]; pl 1; ThmCut "CPLUS"; 
(* 421 *)  rwl [4]; pl 1; ThmCut "APLUS"; 
(* 424 *)  crwl [2]; pl 1; ThmCut "MINUS"; 
(* 427 *)  rwl [1]; pl 1; ThmCut "IPLUSb"; 
(* 430 *)  NextGoal(); 
(* 431 *)  NextGoal(); 
(* 432 *)  UseThm "RPLUS" [] [1]; 
(* 433 *)  rwl [1]; pl 1; pl 2; pl 1; gl 9; ThmCut "SUBLESS"; 
(* 439 *)  UseThm "SQPOS" [9] [1]; 
(* 440 *)  gl 2; gl2 10; rwl [1]; pl 1; ThmCut "ATIMES"; 
(* 445 *)  crwl [1]; pl 1; ; Cut2 "Zero < Two * Sup({x115|Zero < x115 & x115 * x115 < a1})"; 
(* 450 *)  ThmCut "MTIMES"; 
(* 451 *)  l(); r(); UseThm "POSINV" [1] [1]; 
(* 454 *)  gl 2; gr 1; Done(); 
(* 457 *)  ThmCut "CTIMES"; 
(* 458 *)  rwl [4]; pl 1; ThmCut "ATIMES"; 
(* 498 *)  crwl [2]; crwl [1]; pl 1; ThmCut "INV"; 
(* 502 *)  l(); NextGoal(); 
(* 504 *)  NextGoal(); 
(* 505 *)  UseThm "RMINUS" [] [1]; 
(* 506 *)  NextGoal(); 
(* 507 *)  NextGoal(); 
(* 508 *)  ThmCut "CTIMES"; 
(* 509 *)  rwl [1]; pl 1; rwl [1]; pl 1; ThmCut "ITIMES"; 
(* 514 *)  l(); NextGoal(); 
(* 516 *)  NextGoal(); 
(* 517 *)  NextGoal(); 
(* 518 *)  NextGoal(); 
(* 519 *)  NextGoal(); 
(* 520 *)  NextGoal(); 
(* 521 *)  NextGoal(); 
(* 522 *)  NextGoal(); 
(* 523 *)  ThmCut "CTIMES"; 
(* 524 *)  rwl [1]; pl 1; rwl [1]; pl 1; r(); r(); gl 1; gr 2; Done(); 
(* 533 *)  gl 6; gr 1; Done(); 
(* 536 *)  UseThm "NOTBOTH3" [3,1] []; 
(* 537 *)  ThmCut "TWOPOS"; 
(* 538 *)  ThmCut "SUPPOS"; 
(* 539 *)  gl 8; gr 1; Done(); 
(* 542 *)  gl 9; gr 1; Done(); 
(* 545 *)  UseThm "TIMESPOS" [2,1] [1]; 
(* 577 *)  Cut2 "Zero = [Sup({x70|Zero < x70 & x70 * x70 < a1})* Sup({x71|Zero < x71 &x71 * x71 < a1})+Minus(a1)] * Inv(Two* Sup({x72|Zero < x72 & x72 *x72 < a1}))"; 
(* 578 *)  ThmCut "EPSLEMMA"; 
(* 579 *)  su 215 "[Sup({x70|Zero < x70 & x70 * x70 < a1})* Sup({x71|Zero < x71 &x71 * x71 < a1})+Minus(a1)] * Inv(Two* Sup({x72|Zero < x72 & x72 *x72 < a1}))"; 
(* 580 *)  r(); r(); crwr [1]; r(); r(); UseThm "RTIMES" [] [1]; 
(* 590 *)  UseThm "SUPPOS" [4,5] [1]; 
(* 591 *)  UseThm "RSUP" [] [1]; 
(* 592 *)  r(); r(); gl 3; l(); l(); gl 5; l(); r(); gl 2; l(); Done(); 
(* 603 *)  r(); Done(); 
(* 605 *)  gl 2; l(); gl 2; gr 1; Done(); 
(* 610 *)  Done(); 
(* 611 *)  pl 1; 

(* 611 *)

hardcomment "Need new zfrac, etc, then SO CLOSE to being DONE!!!!!";


(* Sequent snapshot:


1:  Zero = [
     Sup({x146|Zero < x146 & x146 * x146 < a1})
      * Sup({x147|
     Zero < x147 & x147 * x147 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x148|Zero < x148 & 
     x148 * x148 < a1}))

2:  (Ax146.
     Zero < x146 & Real(x146)
      & x146 < Sup({x147|Zero < x147
      & x147 * x147 < a1})
      -> [
     Sup({x148|Zero < x148
      & x148 * x148 < a1})
      * Sup({x149|
     Zero < x149 & x149 * x149 < a1}) + Minus(a1)]
      * Inv(
     Two
      * Sup({x150|Zero < x150 & x150 * x150 < a1})) <= x146)

3:  a1 < 
     Sup({x146|Zero < x146 & x146 * x146 < a1})
      * Sup({x147|
     Zero < x147 & x147 * x147 < a1})

4:  Real(a1)

5:  Zero < a1

|-

1:  
     Sup({x146|Zero < x146 & x146 * x146 < a1})
      * Sup({x147|
     Zero < x147 & x147 * x147 < a1}) = a1

2:  (Ex146.x146 * x146 = a1)


*)
 CutLemma "Real(a1) & Zero < a1 & Zero =  [Sup({x148|Zero < x148& x148 * x148 < a1})* Sup({x149|Zero < x149 & x149 * x149 < a1}) + Minus(a1)]* Inv(Two* Sup({x150|Zero < x150 & x150 * x150 < a1})) -> Zero = Sup({x148|Zero < x148& x148 * x148 < a1})* Sup({x149|Zero < x149 & x149 * x149 < a1}) + Minus(a1)"; r(); l(); gl 2; l(); ThmCut "ZPROD"; 
(* 634 *)  su 217 "Inv(Two* Sup({x15|Zero < x15 & x15 * x15 < a1}))"; 
(* 635 *)  UseThm "RINV" [] [1]; 
(* 636 *)  su 218 "[Sup({x148|Zero < x148& x148 * x148 < a1})* Sup({x149|Zero < x149 & x149 * x149 < a1}) + Minus(a1)] "; 
(* 637 *)  gl 2; crwr [1]; r(); UseThm "RPLUS" [] [1]; 
(* 641 *)  rwr [1]; r(); Cut "[Two*Sup({x15|Zero < x15 & x15 * x15 < a1})]*[Inv(Two* Sup({x15|Zero < x15 & x15 * x15 < a1}))] = One"; 
(* 646 *)  ThmCut "INV"; 
(* 647 *)  l(); NextGoal(); 
(* 649 *)  NextGoal(); 
(* 650 *)  NextGoal(); 
(* 651 *)  NextGoal(); 
(* 652 *)  NextGoal(); 
(* 653 *)  NextGoal(); 
(* 654 *)  NextGoal(); 
(* 655 *)  NextGoal(); 
(* 656 *)  Done(); 
(* 657 *)  ThmCut "TWOPOS"; 
(* 658 *)  ThmCut "SUPPOS"; 
(* 659 *)  gl 6; gr 1; Done(); 
(* 662 *)  gl 4; gr 1; Done(); 
(* 665 *)  ThmCut "TIMESPOS"; 
(* 666 *)  gl 2; gr 1; Done(); 
(* 669 *)  Done(); 
(* 670 *)  UseThm "NOTBOTH3" [1,4] []; 
(* 671 *)  Cut "[Two*Sup({x15|Zero < x15 & x15 * x15 < a1})]*[Inv(Two* Sup({x15|Zero < x15 & x15 * x15 < a1}))] = Zero"; 
(* 672 *)  gl 2; rwr [1]; ThmCut "MZERO"; 
(* 675 *)  rwr [1]; r(); rwr [1]; rwl [1]; ThmCut "NONTRIV"; 
(* 680 *)  l(); gl 2; rwr [1]; r(); r(); NameSequent 1013 "ZFRAC2"; 
(* 686 *)  

(* 685

ZFRAC2:



1:  Zero < a1

2:  Zero = [
     Sup({x151|Zero < x151 & x151 * x151 < a1})
      * Sup({x152|
     Zero < x152 & x152 * x152 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x153|Zero < x153 & 
     x153 * x153 < a1}))

3:  Real(a1)

|-

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

*)


(* Sequent snapshot:


1:  
     Real(a1)
      & Zero < a1
      & Zero = [
     Sup({x148|Zero < x148
      & x148 * x148 < a1})
      * Sup({x149|
     Zero < x149 & x149 * x149 < a1}) + Minus(a1)]
      * Inv(
     Two
      * Sup({x150|Zero < x150 & x150 * x150 < a1})) -> Zero = 
     Sup({x148|
     Zero < x148 & x148 * x148 < a1})
      * Sup({x149|Zero < x149 & 
     x149 * x149 < a1})
      + Minus(a1)

2:  Zero = [
     Sup({x146|Zero < x146 & x146 * x146 < a1})
      * Sup({x147|
     Zero < x147 & x147 * x147 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x148|Zero < x148 & 
     x148 * x148 < a1}))

3:  (Ax146.
     Zero < x146 & Real(x146)
      & x146 < Sup({x147|Zero < x147
      & x147 * x147 < a1})
      -> [
     Sup({x148|Zero < x148
      & x148 * x148 < a1})
      * Sup({x149|
     Zero < x149 & x149 * x149 < a1}) + Minus(a1)]
      * Inv(
     Two
      * Sup({x150|Zero < x150 & x150 * x150 < a1})) <= x146)

4:  a1 < 
     Sup({x146|Zero < x146 & x146 * x146 < a1})
      * Sup({x147|
     Zero < x147 & x147 * x147 < a1})

5:  Real(a1)

6:  Zero < a1

|-

1:  
     Sup({x146|Zero < x146 & x146 * x146 < a1})
      * Sup({x147|
     Zero < x147 & x147 * x147 < a1}) = a1

2:  (Ex146.x146 * x146 = a1)


*)

l(); r(); gl 4; gr 1; Done(); 
(* 691 *)  r(); gl 5; gr 1; Done(); 
(* 695 *)  Done(); 
(* 696 *)  CutLemma "Real(a1) & Zero = Sup({x148|Zero < x148& x148 * x148 < a1})* Sup({x149|Zero < x149 & x149 * x149 < a1}) + Minus(a1) ->  Sup({x16|Zero < x16 & x16 * x16 < a1})* Sup({x17|Zero < x17 & x17 * x17 < a1})=a1"; r(); l(); ThmCut "UINV"; 
(* 700 *)  NextGoal(); 
(* 701 *)  NextGoal(); 
(* 702 *)  NextGoal(); 
(* 703 *)  NextGoal();  NextGoal(); 
(* 710 *)  NextGoal(); 
(* 711 *)  NextGoal(); 
(* 712 *)  NextGoal(); 
(* 713 *)  su 220 "Minus(a1)"; 
(* 714 *)  su 219 "Sup({x148|Zero < x148& x148 * x148 < a1})* Sup({x149|Zero < x149 & x149 * x149 < a1})"; 
(* 715 *)  NextGoal(); 
(* 716 *)  NextGoal(); 
(* 717 *)  NextGoal(); 
(* 718 *)  NextGoal(); 
(* 719 *)  UseThm "RTIMES" [] [1]; 
(* 720 *)  gl 2; ThmCut "CPLUS"; 
(* 722 *)  rwl [1]; pl 1; crwr [1]; r(); 
ThmCut "DOUBLENEG"; 
(* 732 *)  NextGoal(); 
(* 733 *)  NextGoal(); 
(* 734 *)  NextGoal(); 
(* 735 *)  NextGoal(); 
(* 736 *)  rwl [1]; gl 2; gr 1; Done(); 
(* 740 *)  gl 2; gr 1; Done(); 
(* 743 *)  NameSequent 1060 "EQSUPa12"; 
(* 744 *)  

(* 743

EQSUPa12:



1:  Real(a1)

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

|-

1:  
     Sup({x151|Zero < x151 & x151 * x151 < a1})
      * Sup({x152|
     Zero < x152 & x152 * x152 < a1}) = a1

*)


(* Sequent snapshot:


1:  
     Real(a1) & Zero = 
     Sup({x148|Zero < x148 & x148 * x148 < a1})
      * Sup({x149|
     Zero < x149 & x149 * x149 < a1})
      + Minus(a1)
      -> Sup({x16|Zero < x16
      & x16 * x16 < a1})
      * Sup({x17|
     Zero < x17 & x17 * x17 < a1}) = a1

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

3:  Zero = [
     Sup({x146|Zero < x146 & x146 * x146 < a1})
      * Sup({x147|
     Zero < x147 & x147 * x147 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x148|Zero < x148 & 
     x148 * x148 < a1}))

4:  (Ax146.
     Zero < x146 & Real(x146)
      & x146 < Sup({x147|Zero < x147
      & x147 * x147 < a1})
      -> [
     Sup({x148|Zero < x148
      & x148 * x148 < a1})
      * Sup({x149|
     Zero < x149 & x149 * x149 < a1}) + Minus(a1)]
      * Inv(
     Two
      * Sup({x150|Zero < x150 & x150 * x150 < a1})) <= x146)

5:  a1 < 
     Sup({x146|Zero < x146 & x146 * x146 < a1})
      * Sup({x147|
     Zero < x147 & x147 * x147 < a1})

6:  Real(a1)

7:  Zero < a1

|-

1:  
     Sup({x146|Zero < x146 & x146 * x146 < a1})
      * Sup({x147|
     Zero < x147 & x147 * x147 < a1}) = a1

2:  (Ex146.x146 * x146 = a1)


*)

l(); r(); gl 5; gr 1; Done(); 
(* 749 *)  Done(); 
(* 750 *)  Done(); 
(* 751 *)  ThmCut "EPSLEMMA"; 
(* 752 *)  su 219 "[Sup({x148|Zero < x148& x148 * x148 < a1})* Sup({x149|Zero < x149 & x149 * x149 < a1}) + Minus(a1)]* Inv(Two* Sup({x150|Zero < x150 & x150 * x150 < a1})) "; 
(* 753 *)  

(* 752 *)




r(); r(); 

(* 757 *)

hardcomment "supminuspos won't work b/c no epsilon here";


(* Sequent snapshot:


1:  (Ax153.
     Zero < x153 & Real(x153)
      & x153 < Sup({x154|Zero < x154
      & x154 * x154 < a1})
      -> [
     Sup({x155|Zero < x155
      & x155 * x155 < a1})
      * Sup({x156|
     Zero < x156 & x156 * x156 < a1}) + Minus(a1)]
      * Inv(
     Two
      * Sup({x157|Zero < x157 & x157 * x157 < a1})) <= x153)

2:  a1 < 
     Sup({x153|Zero < x153 & x153 * x153 < a1})
      * Sup({x154|
     Zero < x154 & x154 * x154 < a1})

3:  Real(a1)

4:  Zero < a1

|-

1:  Zero Equal [
     Sup({x148|Zero < x148 & x148 * x148 < a1})
      * Sup({x149|
     Zero < x149 & x149 * x149 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x150|Zero < x150 & 
     x150 * x150 < a1}))

2:  Zero < [
     Sup({x148|Zero < x148 & x148 * x148 < a1})
      * Sup({x149|
     Zero < x149 & x149 * x149 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x150|Zero < x150 & 
     x150 * x150 < a1}))

3:  Zero = [
     Sup({x153|Zero < x153 & x153 * x153 < a1})
      * Sup({x154|
     Zero < x154 & x154 * x154 < a1})
      + Minus(a1)] * Inv(Two
      * Sup({x155|Zero < x155 & 
     x155 * x155 < a1}))

4:  
     Sup({x153|Zero < x153 & x153 * x153 < a1})
      * Sup({x154|
     Zero < x154 & x154 * x154 < a1}) = a1

5:  (Ex153.x153 * x153 = a1)


*)

gl 2; ThmCut "MPLUS"; 
(* 760 *)  l(); Done(); 
(* 762 *)  su 223 "Minus(a1)"; 
(* 763 *)  ThmCut "MINUS"; 
(* 764 *)  rwl [1]; pl 1; ThmCut "TWOPOS"; 
(* 767 *)  ThmCut "SUPPOS"; 
(* 768 *)  gl 4; gr 1; Done(); 
(* 771 *)  gl 5; gr 1; Done(); 
(* 774 *)  ThmCut "TIMESPOS"; 
(* 775 *)  gl 2; gr 1; Done(); 
(* 778 *)  Done(); 
(* 779 *)  pl 2; pl 1; ThmCut "POSINV"; 
(* 782 *)  gl 6; gr 1; Done(); 
(* 785 *)  ThmCut "TIMESPOS"; 
(* 786 *)  gl 2; gr 1; Done(); 
(* 789 *)  Done(); 
(* 790 *)  gl 1; gr 2; Done(); 
(* 793 *)  UseThm "RTIMES" [] [1]; 
(* 794 *)  ThmCut "SUPPOS"; 
(* 795 *)  gl 3; gr 1; Done(); 
(* 798 *)  gl 4; gr 1; Done(); 
(* 801 *)  Done(); 
(* 802 *)  UseThm "RSUP" [] [1]; 
(* 803 *)  r(); l(); r(); l(); gl 3; l(); r(); gl 6; l(); Done(); 
(* 813 *)  r(); gl 5; gr 1; Done(); 
(* 817 *)  gl 6; l(); gl 2; gr 1; Done(); 
(* 822 *)  Done(); 
(* 823 *)  Done(); 
(* 824 *)