:: REAL_1 semantic presentation

Show IDV graph for whole article

registration

cluster -> real Element of REAL ;
coherence

proof end;

end;

definition

mode Real is Element of REAL ;

end;

definition

let x be Real;
:: original: -
redefine func - x -> Real;
coherence by XREAL_0:def 1;
:: original: "
redefine func x " -> Real;
coherence by XREAL_0:def 1;

end;

definition

let x, y be Real;
:: original: +
redefine func x + y -> Real;
coherence by XREAL_0:def 1;
:: original: *
redefine func x * y -> Real;
coherence by XREAL_0:def 1;
:: original: -
redefine func x - y -> Real;
coherence by XREAL_0:def 1;
:: original: /
redefine func x / y -> Real;
coherence by XREAL_0:def 1;

end;

theorem :: REAL_1:1

Show IDV graph

canceled;

theorem :: REAL_1:2

Show IDV graph

canceled;

theorem :: REAL_1:3

Show IDV graph

canceled;

theorem :: REAL_1:4

Show IDV graph

canceled;

theorem :: REAL_1:5

Show IDV graph

canceled;

theorem :: REAL_1:6

Show IDV graph

canceled;

theorem :: REAL_1:7

Show IDV graph

canceled;

theorem :: REAL_1:8

Show IDV graph

canceled;

theorem :: REAL_1:9

Show IDV graph

canceled;

theorem :: REAL_1:10

Show IDV graph

canceled;

theorem :: REAL_1:11

Show IDV graph

canceled;

theorem :: REAL_1:12

Show IDV graph

canceled;

theorem :: REAL_1:13

Show IDV graph

canceled;

theorem :: REAL_1:14

Show IDV graph

canceled;

theorem :: REAL_1:15

Show IDV graph

canceled;

theorem :: REAL_1:16

Show IDV graph

canceled;

theorem :: REAL_1:17

Show IDV graph

canceled;

theorem :: REAL_1:18

Show IDV graph

canceled;

theorem :: REAL_1:19

Show IDV graph

canceled;

theorem :: REAL_1:20

Show IDV graph

canceled;

theorem :: REAL_1:21

Show IDV graph

canceled;

theorem :: REAL_1:22

Show IDV graph

canceled;

theorem :: REAL_1:23

Show IDV graph

canceled;

theorem :: REAL_1:24

Show IDV graph

canceled;

theorem :: REAL_1:25

Show IDV graph

for x being real number holds x - 0 = x ;

theorem :: REAL_1:26

Show IDV graph

- 0 = 0 ;

definition

let y, x be real number ;
canceled;
canceled;
canceled;
canceled;
redefine pred y <= x means :: REAL_1:def 5
( not x <= y or not x <> y );
compatibility by XREAL_1:1;

end;

:: deftheorem REAL_1:def 1 :

:: deftheorem REAL_1:def 2 :

:: deftheorem REAL_1:def 3 :

:: deftheorem REAL_1:def 4 :

:: deftheorem defines < REAL_1:def 5 :

theorem :: REAL_1:27

Show IDV graph

canceled;

theorem :: REAL_1:28

Show IDV graph

canceled;

theorem :: REAL_1:29

Show IDV graph

canceled;

theorem :: REAL_1:30

Show IDV graph

canceled;

theorem :: REAL_1:31

Show IDV graph

canceled;

theorem :: REAL_1:32

Show IDV graph

canceled;

theorem :: REAL_1:33

Show IDV graph

canceled;

theorem :: REAL_1:34

Show IDV graph

canceled;

theorem :: REAL_1:35

Show IDV graph

canceled;

theorem :: REAL_1:36

Show IDV graph

canceled;

theorem :: REAL_1:37

Show IDV graph

canceled;

theorem :: REAL_1:38

Show IDV graph

canceled;

theorem :: REAL_1:39

Show IDV graph

canceled;

theorem :: REAL_1:40

Show IDV graph

canceled;

theorem :: REAL_1:41

Show IDV graph

canceled;

theorem :: REAL_1:42

Show IDV graph

canceled;

theorem :: REAL_1:43

Show IDV graph

canceled;

theorem :: REAL_1:44

Show IDV graph

canceled;

theorem :: REAL_1:45

Show IDV graph

canceled;

theorem :: REAL_1:46

Show IDV graph

canceled;

theorem :: REAL_1:47

Show IDV graph

canceled;

theorem :: REAL_1:48

Show IDV graph

canceled;

theorem :: REAL_1:49

Show IDV graph

canceled;

theorem :: REAL_1:50

Show IDV graph

canceled;

theorem :: REAL_1:51

Show IDV graph

canceled;

theorem :: REAL_1:52

Show IDV graph

canceled;

theorem :: REAL_1:53

Show IDV graph

canceled;

theorem :: REAL_1:54

Show IDV graph

canceled;

theorem :: REAL_1:55

Show IDV graph

canceled;

theorem :: REAL_1:56

Show IDV graph

canceled;

theorem :: REAL_1:57

Show IDV graph

canceled;

theorem :: REAL_1:58

Show IDV graph

canceled;

theorem :: REAL_1:59

Show IDV graph

canceled;

theorem :: REAL_1:60

Show IDV graph

canceled;

theorem :: REAL_1:61

Show IDV graph

canceled;

theorem :: REAL_1:62

Show IDV graph

canceled;

theorem :: REAL_1:63

Show IDV graph

canceled;

theorem :: REAL_1:64

Show IDV graph

canceled;

theorem :: REAL_1:65

Show IDV graph

canceled;

theorem :: REAL_1:66

Show IDV graph

canceled;

theorem :: REAL_1:67

Show IDV graph

canceled;

theorem :: REAL_1:68

Show IDV graph

canceled;

theorem :: REAL_1:69

Show IDV graph

canceled;

theorem :: REAL_1:70

Show IDV graph

canceled;

theorem :: REAL_1:71

Show IDV graph

canceled;

theorem :: REAL_1:72

Show IDV graph

canceled;

theorem :: REAL_1:73

Show IDV graph

for z, x, y being real number st 0 < z holds
( x < y iff x / z < y / z ) by XREAL_1:74, XREAL_1:76;

theorem :: REAL_1:74

Show IDV graph

for z, x, y being real number st z < 0 holds
( x < y iff y / z < x / z ) by XREAL_1:75, XREAL_1:77;

scheme :: REAL_1:sch 1
SepReal{ P₁[ Real] } :

ex X being Subset of REAL st
for x being Real holds
( x in X iff P₁[x] )

proof end;

theorem :: REAL_1:75

Show IDV graph

canceled;

theorem :: REAL_1:76

Show IDV graph

canceled;

theorem :: REAL_1:77

Show IDV graph

canceled;

theorem :: REAL_1:78

Show IDV graph

canceled;

theorem :: REAL_1:79

Show IDV graph

canceled;

theorem :: REAL_1:80

Show IDV graph

canceled;

theorem :: REAL_1:81

Show IDV graph

canceled;

theorem :: REAL_1:82

Show IDV graph

canceled;

theorem :: REAL_1:83

Show IDV graph

canceled;

theorem :: REAL_1:84

Show IDV graph

canceled;

theorem :: REAL_1:85

Show IDV graph

canceled;

theorem :: REAL_1:86

Show IDV graph

canceled;

theorem :: REAL_1:87

Show IDV graph

canceled;

theorem :: REAL_1:88

Show IDV graph

canceled;

theorem :: REAL_1:89

Show IDV graph

canceled;

theorem :: REAL_1:90

Show IDV graph

canceled;

theorem :: REAL_1:91

Show IDV graph

canceled;

theorem :: REAL_1:92

Show IDV graph

for x, y, z, t being real number holds
( ( x <= y & z <= t implies x - t <= y - z ) & ( ( ( x < y & z <= t ) or ( x <= y & z < t ) ) implies x - t < y - z ) ) by XREAL_1:15, XREAL_1:16, XREAL_1:17;