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

Definition df-ap 7573
 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 7658 which says that a number apart from zero has a reciprocal). The defining characteristics of an apartness are irreflexivity (apirr 7596), symmetry (apsym 7597), and cotransitivity (apcotr 7598). Apartness implies negated equality, as seen at apne 7614, 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 7613). (Contributed by Jim Kingdon, 26-Jan-2020.)
Assertion
Ref Expression
df-ap # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))}
Distinct variable group:   𝑠,𝑟,𝑡,𝑢,𝑥,𝑦

Detailed syntax breakdown of Definition df-ap
StepHypRef Expression
1 cap 7572 . 2 class #
2 vx . . . . . . . . . . 11 setvar 𝑥
32cv 1242 . . . . . . . . . 10 class 𝑥
4 vr . . . . . . . . . . . 12 setvar 𝑟
54cv 1242 . . . . . . . . . . 11 class 𝑟
6 ci 6891 . . . . . . . . . . . 12 class i
7 vs . . . . . . . . . . . . 13 setvar 𝑠
87cv 1242 . . . . . . . . . . . 12 class 𝑠
9 cmul 6894 . . . . . . . . . . . 12 class ·
106, 8, 9co 5512 . . . . . . . . . . 11 class (i · 𝑠)
11 caddc 6892 . . . . . . . . . . 11 class +
125, 10, 11co 5512 . . . . . . . . . 10 class (𝑟 + (i · 𝑠))
133, 12wceq 1243 . . . . . . . . 9 wff 𝑥 = (𝑟 + (i · 𝑠))
14 vy . . . . . . . . . . 11 setvar 𝑦
1514cv 1242 . . . . . . . . . 10 class 𝑦
16 vt . . . . . . . . . . . 12 setvar 𝑡
1716cv 1242 . . . . . . . . . . 11 class 𝑡
18 vu . . . . . . . . . . . . 13 setvar 𝑢
1918cv 1242 . . . . . . . . . . . 12 class 𝑢
206, 19, 9co 5512 . . . . . . . . . . 11 class (i · 𝑢)
2117, 20, 11co 5512 . . . . . . . . . 10 class (𝑡 + (i · 𝑢))
2215, 21wceq 1243 . . . . . . . . 9 wff 𝑦 = (𝑡 + (i · 𝑢))
2313, 22wa 97 . . . . . . . 8 wff (𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢)))
24 creap 7565 . . . . . . . . . 10 class #
255, 17, 24wbr 3764 . . . . . . . . 9 wff 𝑟 # 𝑡
268, 19, 24wbr 3764 . . . . . . . . 9 wff 𝑠 # 𝑢
2725, 26wo 629 . . . . . . . 8 wff (𝑟 # 𝑡𝑠 # 𝑢)
2823, 27wa 97 . . . . . . 7 wff ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))
29 cr 6888 . . . . . . 7 class
3028, 18, 29wrex 2307 . . . . . 6 wff 𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))
3130, 16, 29wrex 2307 . . . . 5 wff 𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))
3231, 7, 29wrex 2307 . . . 4 wff 𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))
3332, 4, 29wrex 2307 . . 3 wff 𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))
3433, 2, 14copab 3817 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))}
351, 34wceq 1243 1 wff # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))}
 Colors of variables: wff set class This definition is referenced by:  apreap  7578  apreim  7594
 Copyright terms: Public domain W3C validator