![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-ap | Unicode version |
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 8667 which says that a number apart from zero has a reciprocal). The defining characteristics of an apartness are irreflexivity (apirr 8593), symmetry (apsym 8594), and cotransitivity (apcotr 8595). Apartness implies negated equality, as seen at apne 8611, 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 8610). (Contributed by Jim Kingdon, 26-Jan-2020.) |
Ref | Expression |
---|---|
df-ap |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cap 8569 |
. 2
![]() | |
2 | vx |
. . . . . . . . . . 11
![]() ![]() | |
3 | 2 | cv 1363 |
. . . . . . . . . 10
![]() ![]() |
4 | vr |
. . . . . . . . . . . 12
![]() ![]() | |
5 | 4 | cv 1363 |
. . . . . . . . . . 11
![]() ![]() |
6 | ci 7844 |
. . . . . . . . . . . 12
![]() ![]() | |
7 | vs |
. . . . . . . . . . . . 13
![]() ![]() | |
8 | 7 | cv 1363 |
. . . . . . . . . . . 12
![]() ![]() |
9 | cmul 7847 |
. . . . . . . . . . . 12
![]() ![]() | |
10 | 6, 8, 9 | co 5897 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() |
11 | caddc 7845 |
. . . . . . . . . . 11
![]() ![]() | |
12 | 5, 10, 11 | co 5897 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 3, 12 | wceq 1364 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | vy |
. . . . . . . . . . 11
![]() ![]() | |
15 | 14 | cv 1363 |
. . . . . . . . . 10
![]() ![]() |
16 | vt |
. . . . . . . . . . . 12
![]() ![]() | |
17 | 16 | cv 1363 |
. . . . . . . . . . 11
![]() ![]() |
18 | vu |
. . . . . . . . . . . . 13
![]() ![]() | |
19 | 18 | cv 1363 |
. . . . . . . . . . . 12
![]() ![]() |
20 | 6, 19, 9 | co 5897 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() |
21 | 17, 20, 11 | co 5897 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | 15, 21 | wceq 1364 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
23 | 13, 22 | wa 104 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | creap 8562 |
. . . . . . . . . 10
![]() | |
25 | 5, 17, 24 | wbr 4018 |
. . . . . . . . 9
![]() ![]() ![]() |
26 | 8, 19, 24 | wbr 4018 |
. . . . . . . . 9
![]() ![]() ![]() |
27 | 25, 26 | wo 709 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
28 | 23, 27 | wa 104 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | cr 7841 |
. . . . . . 7
![]() ![]() | |
30 | 28, 18, 29 | wrex 2469 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 30, 16, 29 | wrex 2469 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | 31, 7, 29 | wrex 2469 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 32, 4, 29 | wrex 2469 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 33, 2, 14 | copab 4078 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | 1, 34 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: apreap 8575 apreim 8591 aprcl 8634 aptap 8638 |
Copyright terms: Public domain | W3C validator |