Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > subf | Structured version Visualization version GIF version |
Description: Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
Ref | Expression |
---|---|
subf | ⊢ − :(ℂ × ℂ)⟶ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subval 11195 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 − 𝑦) = (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) | |
2 | subcl 11203 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 − 𝑦) ∈ ℂ) | |
3 | 1, 2 | eqeltrrd 2841 | . . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥) ∈ ℂ) |
4 | 3 | rgen2 3128 | . 2 ⊢ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥) ∈ ℂ |
5 | df-sub 11190 | . . 3 ⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) | |
6 | 5 | fmpo 7894 | . 2 ⊢ (∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥) ∈ ℂ ↔ − :(ℂ × ℂ)⟶ℂ) |
7 | 4, 6 | mpbi 229 | 1 ⊢ − :(ℂ × ℂ)⟶ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1541 ∈ wcel 2109 ∀wral 3065 × cxp 5586 ⟶wf 6426 ℩crio 7224 (class class class)co 7268 ℂcc 10853 + caddc 10858 − cmin 11188 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7579 ax-resscn 10912 ax-1cn 10913 ax-icn 10914 ax-addcl 10915 ax-addrcl 10916 ax-mulcl 10917 ax-mulrcl 10918 ax-mulcom 10919 ax-addass 10920 ax-mulass 10921 ax-distr 10922 ax-i2m1 10923 ax-1ne0 10924 ax-1rid 10925 ax-rnegex 10926 ax-rrecex 10927 ax-cnre 10928 ax-pre-lttri 10929 ax-pre-lttrn 10930 ax-pre-ltadd 10931 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3072 df-rab 3074 df-v 3432 df-sbc 3720 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4845 df-iun 4931 df-br 5079 df-opab 5141 df-mpt 5162 df-id 5488 df-po 5502 df-so 5503 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-res 5600 df-ima 5601 df-iota 6388 df-fun 6432 df-fn 6433 df-f 6434 df-f1 6435 df-fo 6436 df-f1o 6437 df-fv 6438 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-1st 7817 df-2nd 7818 df-er 8472 df-en 8708 df-dom 8709 df-sdom 8710 df-pnf 10995 df-mnf 10996 df-ltxr 10998 df-sub 11190 |
This theorem is referenced by: dfz2 12321 zexALT 12322 rlimsub 15335 znnen 15902 cnfldds 20588 cnfldfun 20590 cnfldfunOLD 20591 cnfldfunALT 20592 cnfldsub 20607 cnmetdval 23915 cnmet 23916 cnfldms 23920 subcn 24010 cnfldcusp 24502 ovolfsf 24616 ovolctb 24635 dvlip2 25140 cnnvm 29023 mblfinlem2 35794 sblpnf 41881 fourierdlem42 43644 ovolval2lem 44135 ovolval2 44136 ovolval3 44139 |
Copyright terms: Public domain | W3C validator |