:: JGRAPH_3 semantic presentation
Lemma1:
for b1 being real number holds (b1 ^2 ) + 1 > 0
Lemma2:
TOP-REAL 2 = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
Lemma3:
( dom proj1 = the carrier of (TOP-REAL 2) & dom proj2 = the carrier of (TOP-REAL 2) )
by FUNCT_2:def 1;
theorem Th1: :: JGRAPH_3:1
theorem Th2: :: JGRAPH_3:2
theorem Th3: :: JGRAPH_3:3
Lemma7:
for b1, b2 being real number st b1 >= 0 & (b2 - b1) * (b2 + b1) <= 0 holds
( - b1 <= b2 & b2 <= b1 )
by XREAL_1:95;
theorem Th4: :: JGRAPH_3:4
canceled;
theorem Th5: :: JGRAPH_3:5
theorem Th6: :: JGRAPH_3:6
for
b1,
b2,
b3 being
real number holds
( (
b1 < b2 &
b1 < b3 ) iff
b1 < min b2,
b3 )
theorem Th7: :: JGRAPH_3:7
theorem Th8: :: JGRAPH_3:8
theorem Th9: :: JGRAPH_3:9
theorem Th10: :: JGRAPH_3:10
theorem Th11: :: JGRAPH_3:11
theorem Th12: :: JGRAPH_3:12
theorem Th13: :: JGRAPH_3:13
definition
func Sq_Circ -> Function of the
carrier of
(TOP-REAL 2),the
carrier of
(TOP-REAL 2) means :
Def1:
:: JGRAPH_3:def 1
for
b1 being
Point of
(TOP-REAL 2) holds
( (
b1 = 0.REAL 2 implies
a1 . b1 = b1 ) & ( ( (
b1 `2 <= b1 `1 &
- (b1 `1 ) <= b1 `2 ) or (
b1 `2 >= b1 `1 &
b1 `2 <= - (b1 `1 ) ) ) &
b1 <> 0.REAL 2 implies
a1 . b1 = |[((b1 `1 ) / (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 )))),((b1 `2 ) / (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 ))))]| ) & ( (
b1 `2 <= b1 `1 &
- (b1 `1 ) <= b1 `2 ) or (
b1 `2 >= b1 `1 &
b1 `2 <= - (b1 `1 ) ) or not
b1 <> 0.REAL 2 or
a1 . b1 = |[((b1 `1 ) / (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 )))),((b1 `2 ) / (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 ))))]| ) );
existence
ex b1 being Function of the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2) st
for b2 being Point of (TOP-REAL 2) holds
( ( b2 = 0.REAL 2 implies b1 . b2 = b2 ) & ( ( ( b2 `2 <= b2 `1 & - (b2 `1 ) <= b2 `2 ) or ( b2 `2 >= b2 `1 & b2 `2 <= - (b2 `1 ) ) ) & b2 <> 0.REAL 2 implies b1 . b2 = |[((b2 `1 ) / (sqrt (1 + (((b2 `2 ) / (b2 `1 )) ^2 )))),((b2 `2 ) / (sqrt (1 + (((b2 `2 ) / (b2 `1 )) ^2 ))))]| ) & ( ( b2 `2 <= b2 `1 & - (b2 `1 ) <= b2 `2 ) or ( b2 `2 >= b2 `1 & b2 `2 <= - (b2 `1 ) ) or not b2 <> 0.REAL 2 or b1 . b2 = |[((b2 `1 ) / (sqrt (1 + (((b2 `1 ) / (b2 `2 )) ^2 )))),((b2 `2 ) / (sqrt (1 + (((b2 `1 ) / (b2 `2 )) ^2 ))))]| ) )
uniqueness
for b1, b2 being Function of the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2) st ( for b3 being Point of (TOP-REAL 2) holds
( ( b3 = 0.REAL 2 implies b1 . b3 = b3 ) & ( ( ( b3 `2 <= b3 `1 & - (b3 `1 ) <= b3 `2 ) or ( b3 `2 >= b3 `1 & b3 `2 <= - (b3 `1 ) ) ) & b3 <> 0.REAL 2 implies b1 . b3 = |[((b3 `1 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 )))),((b3 `2 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 ))))]| ) & ( ( b3 `2 <= b3 `1 & - (b3 `1 ) <= b3 `2 ) or ( b3 `2 >= b3 `1 & b3 `2 <= - (b3 `1 ) ) or not b3 <> 0.REAL 2 or b1 . b3 = |[((b3 `1 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 )))),((b3 `2 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 ))))]| ) ) ) & ( for b3 being Point of (TOP-REAL 2) holds
( ( b3 = 0.REAL 2 implies b2 . b3 = b3 ) & ( ( ( b3 `2 <= b3 `1 & - (b3 `1 ) <= b3 `2 ) or ( b3 `2 >= b3 `1 & b3 `2 <= - (b3 `1 ) ) ) & b3 <> 0.REAL 2 implies b2 . b3 = |[((b3 `1 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 )))),((b3 `2 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 ))))]| ) & ( ( b3 `2 <= b3 `1 & - (b3 `1 ) <= b3 `2 ) or ( b3 `2 >= b3 `1 & b3 `2 <= - (b3 `1 ) ) or not b3 <> 0.REAL 2 or b2 . b3 = |[((b3 `1 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 )))),((b3 `2 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 ))))]| ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Sq_Circ JGRAPH_3:def 1 :
theorem Th14: :: JGRAPH_3:14
theorem Th15: :: JGRAPH_3:15
theorem Th16: :: JGRAPH_3:16
theorem Th17: :: JGRAPH_3:17
theorem Th18: :: JGRAPH_3:18
theorem Th19: :: JGRAPH_3:19
theorem Th20: :: JGRAPH_3:20
Lemma23:
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Point of ((TOP-REAL 2) | b1) holds (proj2 | b1) . b2 = proj2 . b2
Lemma24:
for b1 being non empty Subset of (TOP-REAL 2) holds proj2 | b1 is continuous Function of ((TOP-REAL 2) | b1),R^1
Lemma25:
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Point of ((TOP-REAL 2) | b1) holds (proj1 | b1) . b2 = proj1 . b2
Lemma26:
for b1 being non empty Subset of (TOP-REAL 2) holds proj1 | b1 is continuous Function of ((TOP-REAL 2) | b1),R^1
theorem Th21: :: JGRAPH_3:21
theorem Th22: :: JGRAPH_3:22
theorem Th23: :: JGRAPH_3:23
theorem Th24: :: JGRAPH_3:24
Lemma31:
( ( ( (1.REAL 2) `2 <= (1.REAL 2) `1 & - ((1.REAL 2) `1 ) <= (1.REAL 2) `2 ) or ( (1.REAL 2) `2 >= (1.REAL 2) `1 & (1.REAL 2) `2 <= - ((1.REAL 2) `1 ) ) ) & 1.REAL 2 <> 0.REAL 2 )
by JGRAPH_2:13, REVROT_1:19;
Lemma32:
for b1 being non empty Subset of (TOP-REAL 2) holds dom (proj2 * (Sq_Circ | b1)) = the carrier of ((TOP-REAL 2) | b1)
Lemma33:
for b1 being non empty Subset of (TOP-REAL 2) holds dom (proj1 * (Sq_Circ | b1)) = the carrier of ((TOP-REAL 2) | b1)
Lemma34:
the carrier of (TOP-REAL 2) \ {(0.REAL 2)} <> {}
by JGRAPH_2:19;
theorem Th25: :: JGRAPH_3:25
Lemma36:
( ( ( (1.REAL 2) `1 <= (1.REAL 2) `2 & - ((1.REAL 2) `2 ) <= (1.REAL 2) `1 ) or ( (1.REAL 2) `1 >= (1.REAL 2) `2 & (1.REAL 2) `1 <= - ((1.REAL 2) `2 ) ) ) & 1.REAL 2 <> 0.REAL 2 )
by JGRAPH_2:13, REVROT_1:19;
theorem Th26: :: JGRAPH_3:26
theorem Th27: :: JGRAPH_3:27
theorem Th28: :: JGRAPH_3:28
theorem Th29: :: JGRAPH_3:29
theorem Th30: :: JGRAPH_3:30
theorem Th31: :: JGRAPH_3:31
theorem Th32: :: JGRAPH_3:32
theorem Th33: :: JGRAPH_3:33
theorem Th34: :: JGRAPH_3:34
theorem Th35: :: JGRAPH_3:35
theorem Th36: :: JGRAPH_3:36
theorem Th37: :: JGRAPH_3:37
theorem Th38: :: JGRAPH_3:38
theorem Th39: :: JGRAPH_3:39
theorem Th40: :: JGRAPH_3:40
theorem Th41: :: JGRAPH_3:41
theorem Th42: :: JGRAPH_3:42
theorem Th43: :: JGRAPH_3:43
theorem Th44: :: JGRAPH_3:44
theorem Th45: :: JGRAPH_3:45
theorem Th46: :: JGRAPH_3:46
Lemma56:
for b1 being non empty Subset of (TOP-REAL 2) holds proj2 * ((Sq_Circ " ) | b1) is Function of ((TOP-REAL 2) | b1),R^1
Lemma57:
for b1 being non empty Subset of (TOP-REAL 2) holds proj1 * ((Sq_Circ " ) | b1) is Function of ((TOP-REAL 2) | b1),R^1
theorem Th47: :: JGRAPH_3:47
theorem Th48: :: JGRAPH_3:48
theorem Th49: :: JGRAPH_3:49
theorem Th50: :: JGRAPH_3:50
theorem Th51: :: JGRAPH_3:51
theorem Th52: :: JGRAPH_3:52
Lemma64:
Sq_Circ " is one-to-one
by FUNCT_1:62;
theorem Th53: :: JGRAPH_3:53
canceled;
theorem Th54: :: JGRAPH_3:54
E67:
now
let c1 be
real number ;
assume
(c1 ^2 ) - 1
= 0
;
then
(c1 - 1) * (c1 + 1) = 0
;
then
(
c1 - 1
= 0 or
c1 + 1
= 0 )
by XCMPLX_1:6;
then
(
c1 = 0
+ 1 or
c1 + 1
= 0 )
;
then
(
c1 = 1 or
c1 = 0
- 1 )
;
hence
(
c1 = 1 or
c1 = - 1 )
;
end;
theorem Th55: :: JGRAPH_3:55