ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ap Unicode version

Definition df-ap 7646
Description: Define complex apartness. Definition 6.1 of [Geuvers], p. 17.

Two numbers are considered apart if it is possible to separate them. One common usage is that we can divide by a number if it is apart from zero (see for example recclap 7731 which says that a number apart from zero has a reciprocal).

The defining characteristics of an apartness are irreflexivity (apirr 7669), symmetry (apsym 7670), and cotransitivity (apcotr 7671). Apartness implies negated equality, as seen at apne 7687, and the converse would also follow if we assumed excluded middle.

In addition, apartness of complex numbers is tight, which means that two numbers which are not apart are equal (apti 7686).

(Contributed by Jim Kingdon, 26-Jan-2020.)

Assertion
Ref Expression
df-ap  |- #  =  { <. x ,  y >.  |  E. r  e.  RR  E. s  e.  RR  E. t  e.  RR  E. u  e.  RR  ( ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )  /\  ( r #  t  \/  s #  u
) ) }
Distinct variable group:    s, r, t, u, x, y

Detailed syntax breakdown of Definition df-ap
StepHypRef Expression
1 cap 7645 . 2  class #
2 vx . . . . . . . . . . 11  setvar  x
32cv 1258 . . . . . . . . . 10  class  x
4 vr . . . . . . . . . . . 12  setvar  r
54cv 1258 . . . . . . . . . . 11  class  r
6 ci 6948 . . . . . . . . . . . 12  class  _i
7 vs . . . . . . . . . . . . 13  setvar  s
87cv 1258 . . . . . . . . . . . 12  class  s
9 cmul 6951 . . . . . . . . . . . 12  class  x.
106, 8, 9co 5539 . . . . . . . . . . 11  class  ( _i  x.  s )
11 caddc 6949 . . . . . . . . . . 11  class  +
125, 10, 11co 5539 . . . . . . . . . 10  class  ( r  +  ( _i  x.  s ) )
133, 12wceq 1259 . . . . . . . . 9  wff  x  =  ( r  +  ( _i  x.  s ) )
14 vy . . . . . . . . . . 11  setvar  y
1514cv 1258 . . . . . . . . . 10  class  y
16 vt . . . . . . . . . . . 12  setvar  t
1716cv 1258 . . . . . . . . . . 11  class  t
18 vu . . . . . . . . . . . . 13  setvar  u
1918cv 1258 . . . . . . . . . . . 12  class  u
206, 19, 9co 5539 . . . . . . . . . . 11  class  ( _i  x.  u )
2117, 20, 11co 5539 . . . . . . . . . 10  class  ( t  +  ( _i  x.  u ) )
2215, 21wceq 1259 . . . . . . . . 9  wff  y  =  ( t  +  ( _i  x.  u ) )
2313, 22wa 101 . . . . . . . 8  wff  ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )
24 creap 7638 . . . . . . . . . 10  class #
255, 17, 24wbr 3791 . . . . . . . . 9  wff  r #  t
268, 19, 24wbr 3791 . . . . . . . . 9  wff  s #  u
2725, 26wo 639 . . . . . . . 8  wff  ( r #  t  \/  s #  u )
2823, 27wa 101 . . . . . . 7  wff  ( ( x  =  ( r  +  ( _i  x.  s ) )  /\  y  =  ( t  +  ( _i  x.  u ) ) )  /\  ( r #  t  \/  s #  u ) )
29 cr 6945 . . . . . . 7  class  RR
3028, 18, 29wrex 2324 . . . . . 6  wff  E. u  e.  RR  ( ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )  /\  ( r #  t  \/  s #  u
) )
3130, 16, 29wrex 2324 . . . . 5  wff  E. t  e.  RR  E. u  e.  RR  ( ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )  /\  ( r #  t  \/  s #  u
) )
3231, 7, 29wrex 2324 . . . 4  wff  E. s  e.  RR  E. t  e.  RR  E. u  e.  RR  ( ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )  /\  ( r #  t  \/  s #  u
) )
3332, 4, 29wrex 2324 . . 3  wff  E. r  e.  RR  E. s  e.  RR  E. t  e.  RR  E. u  e.  RR  ( ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )  /\  ( r #  t  \/  s #  u
) )
3433, 2, 14copab 3844 . 2  class  { <. x ,  y >.  |  E. r  e.  RR  E. s  e.  RR  E. t  e.  RR  E. u  e.  RR  ( ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )  /\  ( r #  t  \/  s #  u
) ) }
351, 34wceq 1259 1  wff #  =  { <. x ,  y >.  |  E. r  e.  RR  E. s  e.  RR  E. t  e.  RR  E. u  e.  RR  ( ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )  /\  ( r #  t  \/  s #  u
) ) }
Colors of variables: wff set class
This definition is referenced by:  apreap  7651  apreim  7667
  Copyright terms: Public domain W3C validator