![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fveecn | Structured version Visualization version GIF version |
Description: The function value of a point is a complex. (Contributed by Scott Fenton, 10-Jun-2013.) |
Ref | Expression |
---|---|
fveecn | ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveere 26779 | . 2 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℝ) | |
2 | 1 | recnd 10692 | 1 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐴‘𝐼) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 400 ∈ wcel 2112 ‘cfv 6328 (class class class)co 7143 ℂcc 10558 1c1 10561 ...cfz 12924 𝔼cee 26766 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-cnex 10616 ax-resscn 10617 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3an 1087 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-ral 3073 df-rex 3074 df-rab 3077 df-v 3409 df-sbc 3694 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-op 4522 df-uni 4792 df-br 5026 df-opab 5088 df-mpt 5106 df-id 5423 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-fv 6336 df-ov 7146 df-oprab 7147 df-mpo 7148 df-map 8411 df-ee 26769 |
This theorem is referenced by: brbtwn2 26783 colinearalglem2 26785 colinearalg 26788 axcgrrflx 26792 axcgrid 26794 axsegconlem1 26795 ax5seglem1 26806 ax5seglem2 26807 ax5seglem4 26810 ax5seglem5 26811 ax5seglem6 26812 ax5seglem9 26815 axbtwnid 26817 axpasch 26819 axlowdimlem16 26835 axlowdimlem17 26836 axeuclidlem 26840 axeuclid 26841 axcontlem2 26843 axcontlem4 26845 axcontlem7 26848 axcontlem8 26849 |
Copyright terms: Public domain | W3C validator |