Theorem 1fldgenq

Description: The field of rational numbers QQ is generated by 1 in CCfld , that is, QQ is the prime field of CCfld . (Contributed by Thierry Arnoux, 15-Jan-2025)

	Ref	Expression
Assertion	1fldgenq	Could not format assertion : No typesetting found for |- ( CCfld fldGen { 1 } ) = QQ with typecode |-

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
2		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
3	2	a1i	$$⊢\top \to {ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
4		qsscn	$$⊢\mathbb{Q}\subseteq ℂ$$
5	4	a1i	$$⊢\top \to \mathbb{Q}\subseteq ℂ$$
6		1z	$$⊢1\in \mathbb{Z}$$
7		snssi	$$⊢1\in \mathbb{Z}\to \left\{1\right\}\subseteq \mathbb{Z}$$
8	6 7	ax-mp	$$⊢\left\{1\right\}\subseteq \mathbb{Z}$$
9		zssq	$$⊢\mathbb{Z}\subseteq \mathbb{Q}$$
10	8 9	sstri	$$⊢\left\{1\right\}\subseteq \mathbb{Q}$$
11	10	a1i	$$⊢\top \to \left\{1\right\}\subseteq \mathbb{Q}$$
12	1 3 5 11	fldgenss	Could not format ( T. -> ( CCfld fldGen { 1 } ) C_ ( CCfld fldGen QQ ) ) : No typesetting found for |- ( T. -> ( CCfld fldGen { 1 } ) C_ ( CCfld fldGen QQ ) ) with typecode |-
13		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
14	13	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
15	13	simpri	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}$$
16		issdrg	$$⊢\mathbb{Q}\in \mathrm{SubDRing}\left({ℂ}_{\mathrm{fld}}\right)\leftrightarrow \left({ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge \mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
17	2 14 15 16	mpbir3an	$$⊢\mathbb{Q}\in \mathrm{SubDRing}\left({ℂ}_{\mathrm{fld}}\right)$$
18	17	a1i	$$⊢\top \to \mathbb{Q}\in \mathrm{SubDRing}\left({ℂ}_{\mathrm{fld}}\right)$$
19	1 3 18	fldgenidfld	Could not format ( T. -> ( CCfld fldGen QQ ) = QQ ) : No typesetting found for |- ( T. -> ( CCfld fldGen QQ ) = QQ ) with typecode |-
20	12 19	sseqtrd	Could not format ( T. -> ( CCfld fldGen { 1 } ) C_ QQ ) : No typesetting found for |- ( T. -> ( CCfld fldGen { 1 } ) C_ QQ ) with typecode |-
21		elq	$$⊢z\in \mathbb{Q}\leftrightarrow \exists p\in \mathbb{Z}\exists q\in \mathbb{N}z=\frac{p}{q}$$
22		cnflddiv	$$⊢÷={/}_r\left({ℂ}_{\mathrm{fld}}\right)$$
23		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
24	11 4	sstrdi	$$⊢\top \to \left\{1\right\}\subseteq ℂ$$
25	1 3 24	fldgensdrg	Could not format ( T. -> ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) ) : No typesetting found for |- ( T. -> ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) ) with typecode |-
26	25	mptru	Could not format ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) : No typesetting found for |- ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) with typecode |-
27	26	a1i	Could not format ( ( p e. ZZ /\ q e. NN ) -> ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) ) : No typesetting found for |- ( ( p e. ZZ /\ q e. NN ) -> ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) ) with typecode |-
28		ax-1cn	$$⊢1\in ℂ$$
29		cnfldmulg	$$⊢\left(p\in \mathbb{Z}\wedge 1\in ℂ\right)\to p{\cdot }_{{ℂ}_{\mathrm{fld}}}1=p\cdot 1$$
30	28 29	mpan2	$$⊢p\in \mathbb{Z}\to p{\cdot }_{{ℂ}_{\mathrm{fld}}}1=p\cdot 1$$
31		zre	$$⊢p\in \mathbb{Z}\to p\in ℝ$$
32		ax-1rid	$$⊢p\in ℝ\to p\cdot 1=p$$
33	31 32	syl	$$⊢p\in \mathbb{Z}\to p\cdot 1=p$$
34	30 33	eqtrd	$$⊢p\in \mathbb{Z}\to p{\cdot }_{{ℂ}_{\mathrm{fld}}}1=p$$
35		issdrg	Could not format ( ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) /\ ( CCfld |`s ( CCfld fldGen { 1 } ) ) e. DivRing ) ) : No typesetting found for |- ( ( CCfld fldGen { 1 } ) e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) /\ ( CCfld |`s ( CCfld fldGen { 1 } ) ) e. DivRing ) ) with typecode |-
36	26 35	mpbi	Could not format ( CCfld e. DivRing /\ ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) /\ ( CCfld |`s ( CCfld fldGen { 1 } ) ) e. DivRing ) : No typesetting found for |- ( CCfld e. DivRing /\ ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) /\ ( CCfld |`s ( CCfld fldGen { 1 } ) ) e. DivRing ) with typecode |-
37	36	simp2i	Could not format ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) : No typesetting found for |- ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) with typecode |-
38		subrgsubg	Could not format ( ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) -> ( CCfld fldGen { 1 } ) e. ( SubGrp ` CCfld ) ) : No typesetting found for |- ( ( CCfld fldGen { 1 } ) e. ( SubRing ` CCfld ) -> ( CCfld fldGen { 1 } ) e. ( SubGrp ` CCfld ) ) with typecode |-
39	37 38	ax-mp	Could not format ( CCfld fldGen { 1 } ) e. ( SubGrp ` CCfld ) : No typesetting found for |- ( CCfld fldGen { 1 } ) e. ( SubGrp ` CCfld ) with typecode |-
40	1 3 24	fldgenssid	Could not format ( T. -> { 1 } C_ ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( T. -> { 1 } C_ ( CCfld fldGen { 1 } ) ) with typecode |-
41		1ex	$$⊢1\in \mathrm{V}$$
42	41	snss	Could not format ( 1 e. ( CCfld fldGen { 1 } ) <-> { 1 } C_ ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( 1 e. ( CCfld fldGen { 1 } ) <-> { 1 } C_ ( CCfld fldGen { 1 } ) ) with typecode |-
43	40 42	sylibr	Could not format ( T. -> 1 e. ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( T. -> 1 e. ( CCfld fldGen { 1 } ) ) with typecode |-
44	43	mptru	Could not format 1 e. ( CCfld fldGen { 1 } ) : No typesetting found for |- 1 e. ( CCfld fldGen { 1 } ) with typecode |-
45		eqid	$$⊢{\cdot }_{{ℂ}_{\mathrm{fld}}}={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
46	45	subgmulgcl	Could not format ( ( ( CCfld fldGen { 1 } ) e. ( SubGrp ` CCfld ) /\ p e. ZZ /\ 1 e. ( CCfld fldGen { 1 } ) ) -> ( p ( .g ` CCfld ) 1 ) e. ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( ( ( CCfld fldGen { 1 } ) e. ( SubGrp ` CCfld ) /\ p e. ZZ /\ 1 e. ( CCfld fldGen { 1 } ) ) -> ( p ( .g ` CCfld ) 1 ) e. ( CCfld fldGen { 1 } ) ) with typecode |-
47	39 44 46	mp3an13	Could not format ( p e. ZZ -> ( p ( .g ` CCfld ) 1 ) e. ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( p e. ZZ -> ( p ( .g ` CCfld ) 1 ) e. ( CCfld fldGen { 1 } ) ) with typecode |-
48	34 47	eqeltrrd	Could not format ( p e. ZZ -> p e. ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( p e. ZZ -> p e. ( CCfld fldGen { 1 } ) ) with typecode |-
49	48	adantr	Could not format ( ( p e. ZZ /\ q e. NN ) -> p e. ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( ( p e. ZZ /\ q e. NN ) -> p e. ( CCfld fldGen { 1 } ) ) with typecode |-
50	48	ssriv	Could not format ZZ C_ ( CCfld fldGen { 1 } ) : No typesetting found for |- ZZ C_ ( CCfld fldGen { 1 } ) with typecode |-
51		nnz	$$⊢q\in \mathbb{N}\to q\in \mathbb{Z}$$
52	51	adantl	$$⊢\left(p\in \mathbb{Z}\wedge q\in \mathbb{N}\right)\to q\in \mathbb{Z}$$
53	50 52	sselid	Could not format ( ( p e. ZZ /\ q e. NN ) -> q e. ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( ( p e. ZZ /\ q e. NN ) -> q e. ( CCfld fldGen { 1 } ) ) with typecode |-
54		nnne0	$$⊢q\in \mathbb{N}\to q\ne 0$$
55	54	adantl	$$⊢\left(p\in \mathbb{Z}\wedge q\in \mathbb{N}\right)\to q\ne 0$$
56	22 23 27 49 53 55	sdrgdvcl	Could not format ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. ( CCfld fldGen { 1 } ) ) with typecode |-
57		eleq1	Could not format ( z = ( p / q ) -> ( z e. ( CCfld fldGen { 1 } ) <-> ( p / q ) e. ( CCfld fldGen { 1 } ) ) ) : No typesetting found for |- ( z = ( p / q ) -> ( z e. ( CCfld fldGen { 1 } ) <-> ( p / q ) e. ( CCfld fldGen { 1 } ) ) ) with typecode |-
58	56 57	syl5ibrcom	Could not format ( ( p e. ZZ /\ q e. NN ) -> ( z = ( p / q ) -> z e. ( CCfld fldGen { 1 } ) ) ) : No typesetting found for |- ( ( p e. ZZ /\ q e. NN ) -> ( z = ( p / q ) -> z e. ( CCfld fldGen { 1 } ) ) ) with typecode |-
59	58	rexlimivv	Could not format ( E. p e. ZZ E. q e. NN z = ( p / q ) -> z e. ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( E. p e. ZZ E. q e. NN z = ( p / q ) -> z e. ( CCfld fldGen { 1 } ) ) with typecode |-
60	21 59	sylbi	Could not format ( z e. QQ -> z e. ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( z e. QQ -> z e. ( CCfld fldGen { 1 } ) ) with typecode |-
61	60	ssriv	Could not format QQ C_ ( CCfld fldGen { 1 } ) : No typesetting found for |- QQ C_ ( CCfld fldGen { 1 } ) with typecode |-
62	61	a1i	Could not format ( T. -> QQ C_ ( CCfld fldGen { 1 } ) ) : No typesetting found for |- ( T. -> QQ C_ ( CCfld fldGen { 1 } ) ) with typecode |-
63	20 62	eqssd	Could not format ( T. -> ( CCfld fldGen { 1 } ) = QQ ) : No typesetting found for |- ( T. -> ( CCfld fldGen { 1 } ) = QQ ) with typecode |-
64	63	mptru	Could not format ( CCfld fldGen { 1 } ) = QQ : No typesetting found for |- ( CCfld fldGen { 1 } ) = QQ with typecode |-