Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-divc Structured version   Visualization version   GIF version

Definition df-bj-divc 35438
Description: Definition of the divisibility relation (compare df-dvds 15964).

Since 0 is absorbing, (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 0)) and ((0 ∥ 𝐴) ↔ 𝐴 = 0).

(Contributed by BJ, 28-Jul-2023.)

Assertion
Ref Expression
df-bj-divc = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
Distinct variable group:   𝑥,𝑛,𝑦

Detailed syntax breakdown of Definition df-bj-divc
StepHypRef Expression
1 cdivc 35437 . 2 class
2 vx . . . . . . 7 setvar 𝑥
32cv 1538 . . . . . 6 class 𝑥
4 vy . . . . . . 7 setvar 𝑦
54cv 1538 . . . . . 6 class 𝑦
63, 5cop 4567 . . . . 5 class 𝑥, 𝑦
7 cccbar 35386 . . . . . . 7 class ℂ̅
87, 7cxp 5587 . . . . . 6 class (ℂ̅ × ℂ̅)
9 ccchat 35403 . . . . . . 7 class ℂ̂
109, 9cxp 5587 . . . . . 6 class (ℂ̂ × ℂ̂)
118, 10cun 3885 . . . . 5 class ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
126, 11wcel 2106 . . . 4 wff 𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂))
13 vn . . . . . . . 8 setvar 𝑛
1413cv 1538 . . . . . . 7 class 𝑛
15 cmulc 35416 . . . . . . 7 class ·ℂ̅
1614, 3, 15co 7275 . . . . . 6 class (𝑛 ·ℂ̅ 𝑥)
1716, 5wceq 1539 . . . . 5 wff (𝑛 ·ℂ̅ 𝑥) = 𝑦
18 czzbar 35433 . . . . . 6 class ℤ̅
19 czzhat 35435 . . . . . 6 class ℤ̂
2018, 19cun 3885 . . . . 5 class (ℤ̅ ∪ ℤ̂)
2117, 13, 20wrex 3065 . . . 4 wff 𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦
2212, 21wa 396 . . 3 wff (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)
2322, 2, 4copab 5136 . 2 class {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
241, 23wceq 1539 1 wff = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator