MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  divval Structured version   Visualization version   GIF version

Theorem divval 10969
Description: Value of division: if 𝐴 and 𝐵 are complex numbers with 𝐵 nonzero, then (𝐴 / 𝐵) is the (unique) complex number such that (𝐵 · 𝑥) = 𝐴. (Contributed by NM, 8-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.)
Assertion
Ref Expression
divval ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem divval
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifsn 4505 . . 3 (𝐵 ∈ (ℂ ∖ {0}) ↔ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
2 eqeq2 2816 . . . . 5 (𝑧 = 𝐴 → ((𝑦 · 𝑥) = 𝑧 ↔ (𝑦 · 𝑥) = 𝐴))
32riotabidv 6834 . . . 4 (𝑧 = 𝐴 → (𝑥 ∈ ℂ (𝑦 · 𝑥) = 𝑧) = (𝑥 ∈ ℂ (𝑦 · 𝑥) = 𝐴))
4 oveq1 6878 . . . . . 6 (𝑦 = 𝐵 → (𝑦 · 𝑥) = (𝐵 · 𝑥))
54eqeq1d 2807 . . . . 5 (𝑦 = 𝐵 → ((𝑦 · 𝑥) = 𝐴 ↔ (𝐵 · 𝑥) = 𝐴))
65riotabidv 6834 . . . 4 (𝑦 = 𝐵 → (𝑥 ∈ ℂ (𝑦 · 𝑥) = 𝐴) = (𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴))
7 df-div 10967 . . . 4 / = (𝑧 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 ∈ ℂ (𝑦 · 𝑥) = 𝑧))
8 riotaex 6836 . . . 4 (𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴) ∈ V
93, 6, 7, 8ovmpt2 7023 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ (ℂ ∖ {0})) → (𝐴 / 𝐵) = (𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴))
101, 9sylan2br 584 . 2 ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) = (𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴))
11103impb 1136 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2158  wne 2977  cdif 3763  {csn 4367  crio 6831  (class class class)co 6871  cc 10216  0cc0 10218   · cmul 10223   / cdiv 10966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pr 5093
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-rab 3104  df-v 3392  df-sbc 3631  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4627  df-br 4841  df-opab 4903  df-id 5216  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-iota 6061  df-fun 6100  df-fv 6106  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-div 10967
This theorem is referenced by:  divmul  10970  divcl  10973  cnflddiv  19980  divcn  22880  rexdiv  29956
  Copyright terms: Public domain W3C validator