# Metamath Proof Explorer

## Theorem cnfldstr

Description: The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion cnfldstr ${⊢}{ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,13⟩$

### Proof

Step Hyp Ref Expression
1 df-cnfld ${⊢}{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$
2 eqid ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}$
3 2 srngstr ${⊢}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\right)\mathrm{Struct}⟨1,4⟩$
4 9nn ${⊢}9\in ℕ$
5 tsetndx ${⊢}\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$
6 9lt10 ${⊢}9<10$
7 10nn ${⊢}10\in ℕ$
8 plendx ${⊢}{\le }_{\mathrm{ndx}}=10$
9 1nn0 ${⊢}1\in {ℕ}_{0}$
10 0nn0 ${⊢}0\in {ℕ}_{0}$
11 2nn ${⊢}2\in ℕ$
12 2pos ${⊢}0<2$
13 9 10 11 12 declt ${⊢}10<12$
14 9 11 decnncl ${⊢}12\in ℕ$
15 dsndx ${⊢}\mathrm{dist}\left(\mathrm{ndx}\right)=12$
16 4 5 6 7 8 13 14 15 strle3 ${⊢}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\mathrm{Struct}⟨9,12⟩$
17 3nn ${⊢}3\in ℕ$
18 9 17 decnncl ${⊢}13\in ℕ$
19 unifndx ${⊢}\mathrm{UnifSet}\left(\mathrm{ndx}\right)=13$
20 18 19 strle1 ${⊢}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\mathrm{Struct}⟨13,13⟩$
21 2nn0 ${⊢}2\in {ℕ}_{0}$
22 2lt3 ${⊢}2<3$
23 9 21 17 22 declt ${⊢}12<13$
24 16 20 23 strleun ${⊢}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\mathrm{Struct}⟨9,13⟩$
25 4lt9 ${⊢}4<9$
26 3 24 25 strleun ${⊢}\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)\mathrm{Struct}⟨1,13⟩$
27 1 26 eqbrtri ${⊢}{ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,13⟩$