Definition df-ap 8873

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 8970 which says that a number apart from zero has a reciprocal).

The defining characteristics of an apartness are irreflexivity (apirr 8896), symmetry (apsym 8897), and cotransitivity (apcotr 8898). Apartness implies negated equality, as seen at apne 8914, 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 8913).

(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

Step	Hyp	Ref	Expression
1		cap 8872	. 2 class #
2		vx	. . . . . . . . . . 11 setvar x
3	2	cv 1397	. . . . . . . . . 10 class x
4		vr	. . . . . . . . . . . 12 setvar r
5	4	cv 1397	. . . . . . . . . . 11 class r
6		ci 8145	. . . . . . . . . . . 12 class _i
7		vs	. . . . . . . . . . . . 13 setvar s
8	7	cv 1397	. . . . . . . . . . . 12 class s
9		cmul 8148	. . . . . . . . . . . 12 class x.
10	6, 8, 9	co 6058	. . . . . . . . . . 11 class ( _i x. s )
11		caddc 8146	. . . . . . . . . . 11 class +
12	5, 10, 11	co 6058	. . . . . . . . . 10 class ( r + ( _i x. s ) )
13	3, 12	wceq 1398	. . . . . . . . 9 wff x = ( r + ( _i x. s ) )
14		vy	. . . . . . . . . . 11 setvar y
15	14	cv 1397	. . . . . . . . . 10 class y
16		vt	. . . . . . . . . . . 12 setvar t
17	16	cv 1397	. . . . . . . . . . 11 class t
18		vu	. . . . . . . . . . . . 13 setvar u
19	18	cv 1397	. . . . . . . . . . . 12 class u
20	6, 19, 9	co 6058	. . . . . . . . . . 11 class ( _i x. u )
21	17, 20, 11	co 6058	. . . . . . . . . 10 class ( t + ( _i x. u ) )
22	15, 21	wceq 1398	. . . . . . . . 9 wff y = ( t + ( _i x. u ) )
23	13, 22	wa 104	. . . . . . . 8 wff ( x = ( r + ( _i x. s ) ) /\ y = ( t + ( _i x. u ) ) )
24		creap 8865	. . . . . . . . . 10 class #ℝ
25	5, 17, 24	wbr 4114	. . . . . . . . 9 wff r #ℝ t
26	8, 19, 24	wbr 4114	. . . . . . . . 9 wff s #ℝ u
27	25, 26	wo 716	. . . . . . . 8 wff ( r #ℝ t \/ s #ℝ u )
28	23, 27	wa 104	. . . . . . 7 wff ( ( x = ( r + ( _i x. s ) ) /\ y = ( t + ( _i x. u ) ) ) /\ ( r #ℝ t \/ s #ℝ u ) )
29		cr 8142	. . . . . . 7 class RR
30	28, 18, 29	wrex 2523	. . . . . 6 wff E. u e. RR ( ( x = ( r + ( _i x. s ) ) /\ y = ( t + ( _i x. u ) ) ) /\ ( r #ℝ t \/ s #ℝ u ) )
31	30, 16, 29	wrex 2523	. . . . 5 wff E. t e. RR E. u e. RR ( ( x = ( r + ( _i x. s ) ) /\ y = ( t + ( _i x. u ) ) ) /\ ( r #ℝ t \/ s #ℝ u ) )
32	31, 7, 29	wrex 2523	. . . 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 ) )
33	32, 4, 29	wrex 2523	. . 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 ) )
34	33, 2, 14	copab 4175	. 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 ) ) }
35	1, 34	wceq 1398	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 ) ) }

This definition is referenced by:  apreap  8878  apreim  8894  aprcl  8937  aptap  8941