Theorem zringfrac

Description: The field of fractions of the ring of integers is isomorphic to the field of the rational numbers. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	zringfrac.1	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
	zringfrac.2	No typesetting found for |- .~ = ( ZZring ~RL ( ZZ \ { 0 } ) ) with typecode |-
	zringfrac.3	$$⊢F=\left(q\in \mathbb{Q}⟼\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }\right)$$
Assertion	zringfrac	Could not format assertion : No typesetting found for |- F e. ( Q RingIso ( Frac ` ZZring ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		zringfrac.1	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		zringfrac.2	Could not format .~ = ( ZZring ~RL ( ZZ \ { 0 } ) ) : No typesetting found for |- .~ = ( ZZring ~RL ( ZZ \ { 0 } ) ) with typecode |-
3		zringfrac.3	$$⊢F=\left(q\in \mathbb{Q}⟼\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }\right)$$
4	1	qdrng	$$⊢Q\in \mathrm{DivRing}$$
5		drngring	$$⊢Q\in \mathrm{DivRing}\to Q\in \mathrm{Ring}$$
6	4 5	ax-mp	$$⊢Q\in \mathrm{Ring}$$
7		zringidom	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}$$
8		id	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}$$
9	8	fracfld	Could not format ( ZZring e. IDomn -> ( Frac ` ZZring ) e. Field ) : No typesetting found for |- ( ZZring e. IDomn -> ( Frac ` ZZring ) e. Field ) with typecode |-
10	9	fldcrngd	Could not format ( ZZring e. IDomn -> ( Frac ` ZZring ) e. CRing ) : No typesetting found for |- ( ZZring e. IDomn -> ( Frac ` ZZring ) e. CRing ) with typecode |-
11	10	crngringd	Could not format ( ZZring e. IDomn -> ( Frac ` ZZring ) e. Ring ) : No typesetting found for |- ( ZZring e. IDomn -> ( Frac ` ZZring ) e. Ring ) with typecode |-
12	7 11	ax-mp	Could not format ( Frac ` ZZring ) e. Ring : No typesetting found for |- ( Frac ` ZZring ) e. Ring with typecode |-
13	6 12	pm3.2i	Could not format ( Q e. Ring /\ ( Frac ` ZZring ) e. Ring ) : No typesetting found for |- ( Q e. Ring /\ ( Frac ` ZZring ) e. Ring ) with typecode |-
14		ringgrp	$$⊢Q\in \mathrm{Ring}\to Q\in \mathrm{Grp}$$
15	6 14	ax-mp	$$⊢Q\in \mathrm{Grp}$$
16		ringgrp	Could not format ( ( Frac ` ZZring ) e. Ring -> ( Frac ` ZZring ) e. Grp ) : No typesetting found for |- ( ( Frac ` ZZring ) e. Ring -> ( Frac ` ZZring ) e. Grp ) with typecode |-
17	12 16	ax-mp	Could not format ( Frac ` ZZring ) e. Grp : No typesetting found for |- ( Frac ` ZZring ) e. Grp with typecode |-
18	15 17	pm3.2i	Could not format ( Q e. Grp /\ ( Frac ` ZZring ) e. Grp ) : No typesetting found for |- ( Q e. Grp /\ ( Frac ` ZZring ) e. Grp ) with typecode |-
19		qnumcl	$$⊢q\in \mathbb{Q}\to \mathrm{numer}\left(q\right)\in \mathbb{Z}$$
20		qdencl	$$⊢q\in \mathbb{Q}\to \mathrm{denom}\left(q\right)\in \mathbb{N}$$
21	20	nnzd	$$⊢q\in \mathbb{Q}\to \mathrm{denom}\left(q\right)\in \mathbb{Z}$$
22	20	nnne0d	$$⊢q\in \mathbb{Q}\to \mathrm{denom}\left(q\right)\ne 0$$
23	21 22	eldifsnd	$$⊢q\in \mathbb{Q}\to \mathrm{denom}\left(q\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
24	19 23	opelxpd	$$⊢q\in \mathbb{Q}\to ⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\in \left(\mathbb{Z}\times \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)$$
25	2	ovexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
26	25	ecelqsi	$$⊢⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\in \left(\mathbb{Z}\times \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }\in \left(\left(\mathbb{Z}\times \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)/\underset{\dot{}}{\sim }\right)$$
27	24 26	syl	$$⊢q\in \mathbb{Q}\to \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }\in \left(\left(\mathbb{Z}\times \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)/\underset{\dot{}}{\sim }\right)$$
28		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
29		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
30		zringmulr	$$⊢\times ={\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}$$
31		eqid	$$⊢{-}_{{\mathbb{Z}}_{\mathrm{ring}}}={-}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
32		eqid	$$⊢\mathbb{Z}\times \left(\mathbb{Z}\setminus \left\{0\right\}\right)=\mathbb{Z}\times \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
33		fracval	Could not format ( Frac ` ZZring ) = ( ZZring RLocal ( RLReg ` ZZring ) ) : No typesetting found for |- ( Frac ` ZZring ) = ( ZZring RLocal ( RLReg ` ZZring ) ) with typecode |-
34	8	idomdomd	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Domn}$$
35	7 34	ax-mp	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Domn}$$
36		eqid	$$⊢\mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
37	28 36 29	isdomn6	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Domn}\leftrightarrow \left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{NzRing}\wedge \mathbb{Z}\setminus \left\{0\right\}=\mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)$$
38	35 37	mpbi	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{NzRing}\wedge \mathbb{Z}\setminus \left\{0\right\}=\mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)$$
39	38	simpri	$$⊢\mathbb{Z}\setminus \left\{0\right\}=\mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
40	39	oveq2i	Could not format ( ZZring RLocal ( ZZ \ { 0 } ) ) = ( ZZring RLocal ( RLReg ` ZZring ) ) : No typesetting found for |- ( ZZring RLocal ( ZZ \ { 0 } ) ) = ( ZZring RLocal ( RLReg ` ZZring ) ) with typecode |-
41	33 40	eqtr4i	Could not format ( Frac ` ZZring ) = ( ZZring RLocal ( ZZ \ { 0 } ) ) : No typesetting found for |- ( Frac ` ZZring ) = ( ZZring RLocal ( ZZ \ { 0 } ) ) with typecode |-
42	7	a1i	$$⊢\top \to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}$$
43		difssd	$$⊢\top \to \mathbb{Z}\setminus \left\{0\right\}\subseteq \mathbb{Z}$$
44	28 29 30 31 32 41 2 42 43	rlocbas	Could not format ( T. -> ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) = ( Base ` ( Frac ` ZZring ) ) ) : No typesetting found for |- ( T. -> ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) = ( Base ` ( Frac ` ZZring ) ) ) with typecode |-
45	44	mptru	Could not format ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) = ( Base ` ( Frac ` ZZring ) ) : No typesetting found for |- ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) = ( Base ` ( Frac ` ZZring ) ) with typecode |-
46	27 45	eleqtrdi	Could not format ( q e. QQ -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) ) : No typesetting found for |- ( q e. QQ -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) ) with typecode |-
47	3 46	fmpti	Could not format F : QQ --> ( Base ` ( Frac ` ZZring ) ) : No typesetting found for |- F : QQ --> ( Base ` ( Frac ` ZZring ) ) with typecode |-
48		ecexg	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}\to \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
49	25 48	ax-mp	$$⊢\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
50	3	fvmpt2	$$⊢\left(q\in \mathbb{Q}\wedge \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }\in \mathrm{V}\right)\to F\left(q\right)=\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }$$
51	49 50	mpan2	$$⊢q\in \mathbb{Q}\to F\left(q\right)=\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }$$
52	51	adantr	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to F\left(q\right)=\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }$$
53		fveq2	$$⊢q=p\to \mathrm{numer}\left(q\right)=\mathrm{numer}\left(p\right)$$
54		fveq2	$$⊢q=p\to \mathrm{denom}\left(q\right)=\mathrm{denom}\left(p\right)$$
55	53 54	opeq12d	$$⊢q=p\to ⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩=⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩$$
56	55	eceq1d	$$⊢q=p\to \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }$$
57	56 3 27	fvmpt3	$$⊢p\in \mathbb{Q}\to F\left(p\right)=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }$$
58	57	adantl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to F\left(p\right)=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }$$
59	52 58	oveq12d	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( ( F ` q ) ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ( F ` p ) ) = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( ( F ` q ) ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ( F ` p ) ) = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) ) with typecode |-
60	41	fveq2i	Could not format ( +g ` ( Frac ` ZZring ) ) = ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) : No typesetting found for |- ( +g ` ( Frac ` ZZring ) ) = ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) with typecode |-
61	60	oveqi	Could not format ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) = ( ( F ` q ) ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ( F ` p ) ) : No typesetting found for |- ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) = ( ( F ` q ) ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ( F ` p ) ) with typecode |-
62	61	a1i	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) = ( ( F ` q ) ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ( F ` p ) ) ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) = ( ( F ` q ) ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ( F ` p ) ) ) with typecode |-
63		fveq2	$$⊢q=u\to \mathrm{numer}\left(q\right)=\mathrm{numer}\left(u\right)$$
64		fveq2	$$⊢q=u\to \mathrm{denom}\left(q\right)=\mathrm{denom}\left(u\right)$$
65	63 64	opeq12d	$$⊢q=u\to ⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩=⟨\mathrm{numer}\left(u\right),\mathrm{denom}\left(u\right)⟩$$
66	65	eceq1d	$$⊢q=u\to \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(u\right),\mathrm{denom}\left(u\right)⟩\right]\underset{\dot{}}{\sim }$$
67	66	cbvmptv	$$⊢\left(q\in \mathbb{Q}⟼\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }\right)=\left(u\in \mathbb{Q}⟼\left[⟨\mathrm{numer}\left(u\right),\mathrm{denom}\left(u\right)⟩\right]\underset{\dot{}}{\sim }\right)$$
68	3 67	eqtri	$$⊢F=\left(u\in \mathbb{Q}⟼\left[⟨\mathrm{numer}\left(u\right),\mathrm{denom}\left(u\right)⟩\right]\underset{\dot{}}{\sim }\right)$$
69		zring1	$$⊢1=1_{{\mathbb{Z}}_{\mathrm{ring}}}$$
70	7	a1i	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}$$
71	70	idomcringd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}$$
72	35	a1i	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Domn}$$
73		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}={\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
74	28 29 73	isdomn3	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Domn}\leftrightarrow \left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge \mathbb{Z}\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\right)$$
75	72 74	sylib	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge \mathbb{Z}\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\right)$$
76	75	simprd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathbb{Z}\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)$$
77	28 29 69 30 31 32 2 71 76	erler	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \underset{\dot{}}{\sim }\mathrm{Er}\left(\mathbb{Z}\times \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)$$
78		qcn	$$⊢q\in \mathbb{Q}\to q\in ℂ$$
79	78	adantr	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q\in ℂ$$
80		qcn	$$⊢p\in \mathbb{Q}\to p\in ℂ$$
81	80	adantl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to p\in ℂ$$
82	79 81	addcld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q+p\in ℂ$$
83		qaddcl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q+p\in \mathbb{Q}$$
84		qdencl	$$⊢q+p\in \mathbb{Q}\to \mathrm{denom}\left(q+p\right)\in \mathbb{N}$$
85	83 84	syl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q+p\right)\in \mathbb{N}$$
86	85	nncnd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q+p\right)\in ℂ$$
87	20	adantr	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\in \mathbb{N}$$
88	87	nncnd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\in ℂ$$
89		qdencl	$$⊢p\in \mathbb{Q}\to \mathrm{denom}\left(p\right)\in \mathbb{N}$$
90	89	adantl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(p\right)\in \mathbb{N}$$
91	90	nncnd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(p\right)\in ℂ$$
92	88 91	mulcld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\in ℂ$$
93	82 86 92	mul32d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(q+p\right)\mathrm{denom}\left(q+p\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\left(q+p\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\mathrm{denom}\left(q+p\right)$$
94		qmuldeneqnum	$$⊢q+p\in \mathbb{Q}\to \left(q+p\right)\mathrm{denom}\left(q+p\right)=\mathrm{numer}\left(q+p\right)$$
95	83 94	syl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(q+p\right)\mathrm{denom}\left(q+p\right)=\mathrm{numer}\left(q+p\right)$$
96	95	oveq1d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(q+p\right)\mathrm{denom}\left(q+p\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\mathrm{numer}\left(q+p\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)$$
97	79 88 91	mulassd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=q\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)$$
98		qmuldeneqnum	$$⊢q\in \mathbb{Q}\to q\mathrm{denom}\left(q\right)=\mathrm{numer}\left(q\right)$$
99	98	adantr	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q\mathrm{denom}\left(q\right)=\mathrm{numer}\left(q\right)$$
100	99	oveq1d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)$$
101	97 100	eqtr3d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)$$
102	81 91 88	mulassd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to p\mathrm{denom}\left(p\right)\mathrm{denom}\left(q\right)=p\mathrm{denom}\left(p\right)\mathrm{denom}\left(q\right)$$
103		qmuldeneqnum	$$⊢p\in \mathbb{Q}\to p\mathrm{denom}\left(p\right)=\mathrm{numer}\left(p\right)$$
104	103	adantl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to p\mathrm{denom}\left(p\right)=\mathrm{numer}\left(p\right)$$
105	104	oveq1d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to p\mathrm{denom}\left(p\right)\mathrm{denom}\left(q\right)=\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)$$
106	91 88	mulcomd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(p\right)\mathrm{denom}\left(q\right)=\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)$$
107	106	oveq2d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to p\mathrm{denom}\left(p\right)\mathrm{denom}\left(q\right)=p\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)$$
108	102 105 107	3eqtr3rd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to p\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)$$
109	101 108	oveq12d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)+p\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)$$
110	79 92 81 109	joinlmuladdmuld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(q+p\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)$$
111	110	oveq1d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(q+p\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\mathrm{denom}\left(q+p\right)=\left(\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)\right)\mathrm{denom}\left(q+p\right)$$
112	93 96 111	3eqtr3d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(q+p\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\left(\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)\right)\mathrm{denom}\left(q+p\right)$$
113	39	oveq2i	Could not format ( ZZring ~RL ( ZZ \ { 0 } ) ) = ( ZZring ~RL ( RLReg ` ZZring ) ) : No typesetting found for |- ( ZZring ~RL ( ZZ \ { 0 } ) ) = ( ZZring ~RL ( RLReg ` ZZring ) ) with typecode |-
114	2 113	eqtri	Could not format .~ = ( ZZring ~RL ( RLReg ` ZZring ) ) : No typesetting found for |- .~ = ( ZZring ~RL ( RLReg ` ZZring ) ) with typecode |-
115		qnumcl	$$⊢q+p\in \mathbb{Q}\to \mathrm{numer}\left(q+p\right)\in \mathbb{Z}$$
116	83 115	syl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(q+p\right)\in \mathbb{Z}$$
117	19	adantr	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(q\right)\in \mathbb{Z}$$
118	89	nnzd	$$⊢p\in \mathbb{Q}\to \mathrm{denom}\left(p\right)\in \mathbb{Z}$$
119	118	adantl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(p\right)\in \mathbb{Z}$$
120	117 119	zmulcld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)\in \mathbb{Z}$$
121		qnumcl	$$⊢p\in \mathbb{Q}\to \mathrm{numer}\left(p\right)\in \mathbb{Z}$$
122	121	adantl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(p\right)\in \mathbb{Z}$$
123	21	adantr	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\in \mathbb{Z}$$
124	122 123	zmulcld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)\in \mathbb{Z}$$
125	120 124	zaddcld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)\in \mathbb{Z}$$
126	85	nnzd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q+p\right)\in \mathbb{Z}$$
127	85	nnne0d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q+p\right)\ne 0$$
128	126 127	eldifsnd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q+p\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
129	128 39	eleqtrdi	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q+p\right)\in \mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
130	123 119	zmulcld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\in \mathbb{Z}$$
131	87 90	nnmulcld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\in \mathbb{N}$$
132	131	nnne0d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\ne 0$$
133	130 132	eldifsnd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
134	133 39	eleqtrdi	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\in \mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
135	28 30 114 71 116 125 129 134	fracerl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(⟨\mathrm{numer}\left(q+p\right),\mathrm{denom}\left(q+p\right)⟩\underset{\dot{}}{\sim }⟨\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right),\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)⟩\leftrightarrow \mathrm{numer}\left(q+p\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\left(\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)\right)\mathrm{denom}\left(q+p\right)\right)$$
136	112 135	mpbird	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to ⟨\mathrm{numer}\left(q+p\right),\mathrm{denom}\left(q+p\right)⟩\underset{\dot{}}{\sim }⟨\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right),\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)⟩$$
137	77 136	erthi	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left[⟨\mathrm{numer}\left(q+p\right),\mathrm{denom}\left(q+p\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right),\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }$$
138	137	adantr	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge u=q+p\right)\to \left[⟨\mathrm{numer}\left(q+p\right),\mathrm{denom}\left(q+p\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)+\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right),\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }$$
139		fveq2	$$⊢u=q+p\to \mathrm{numer}\left(u\right)=\mathrm{numer}\left(q+p\right)$$
140		fveq2	$$⊢u=q+p\to \mathrm{denom}\left(u\right)=\mathrm{denom}\left(q+p\right)$$
141	139 140	opeq12d	$$⊢u=q+p\to ⟨\mathrm{numer}\left(u\right),\mathrm{denom}\left(u\right)⟩=⟨\mathrm{numer}\left(q+p\right),\mathrm{denom}\left(q+p\right)⟩$$
142	141	adantl	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge u=q+p\right)\to ⟨\mathrm{numer}\left(u\right),\mathrm{denom}\left(u\right)⟩=⟨\mathrm{numer}\left(q+p\right),\mathrm{denom}\left(q+p\right)⟩$$
143	142	eceq1d	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge u=q+p\right)\to \left[⟨\mathrm{numer}\left(u\right),\mathrm{denom}\left(u\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(q+p\right),\mathrm{denom}\left(q+p\right)⟩\right]\underset{\dot{}}{\sim }$$
144		zringplusg	$$⊢+={+}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
145		eqid	Could not format ( ZZring RLocal ( ZZ \ { 0 } ) ) = ( ZZring RLocal ( ZZ \ { 0 } ) ) : No typesetting found for |- ( ZZring RLocal ( ZZ \ { 0 } ) ) = ( ZZring RLocal ( ZZ \ { 0 } ) ) with typecode |-
146		zringcrng	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}$$
147	146	a1i	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge u=q+p\right)\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}$$
148	35 74	mpbi	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge \mathbb{Z}\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\right)$$
149	148	simpri	$$⊢\mathbb{Z}\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)$$
150	149	a1i	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge u=q+p\right)\to \mathbb{Z}\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)$$
151	117	adantr	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge u=q+p\right)\to \mathrm{numer}\left(q\right)\in \mathbb{Z}$$
152	122	adantr	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge u=q+p\right)\to \mathrm{numer}\left(p\right)\in \mathbb{Z}$$
153	23	adantr	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
154	153	adantr	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge u=q+p\right)\to \mathrm{denom}\left(q\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
155	89	nnne0d	$$⊢p\in \mathbb{Q}\to \mathrm{denom}\left(p\right)\ne 0$$
156	118 155	eldifsnd	$$⊢p\in \mathbb{Q}\to \mathrm{denom}\left(p\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
157	156	adantl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(p\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
158	157	adantr	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge u=q+p\right)\to \mathrm{denom}\left(p\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
159		eqid	Could not format ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) = ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) : No typesetting found for |- ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) = ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) with typecode |-
160	28 30 144 145 2 147 150 151 152 154 158 159	rlocaddval	Could not format ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) = [ <. ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. ] .~ ) : No typesetting found for |- ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) = [ <. ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. ] .~ ) with typecode |-
161	138 143 160	3eqtr4d	Could not format ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> [ <. ( numer ` u ) , ( denom ` u ) >. ] .~ = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) ) : No typesetting found for |- ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> [ <. ( numer ` u ) , ( denom ` u ) >. ] .~ = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) ) with typecode |-
162		ovexd	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) e. _V ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) e. _V ) with typecode |-
163	68 161 83 162	fvmptd2	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q + p ) ) = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q + p ) ) = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) ) with typecode |-
164	59 62 163	3eqtr4rd	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) ) with typecode |-
165	164	rgen2	Could not format A. q e. QQ A. p e. QQ ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) : No typesetting found for |- A. q e. QQ A. p e. QQ ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) with typecode |-
166	47 165	pm3.2i	Could not format ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) ) : No typesetting found for |- ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) ) with typecode |-
167	1	qrngbas	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$
168		eqid	Could not format ( Base ` ( Frac ` ZZring ) ) = ( Base ` ( Frac ` ZZring ) ) : No typesetting found for |- ( Base ` ( Frac ` ZZring ) ) = ( Base ` ( Frac ` ZZring ) ) with typecode |-
169		qex	$$⊢\mathbb{Q}\in \mathrm{V}$$
170		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
171	1 170	ressplusg	$$⊢\mathbb{Q}\in \mathrm{V}\to +={+}_Q$$
172	169 171	ax-mp	$$⊢+={+}_Q$$
173		eqid	Could not format ( +g ` ( Frac ` ZZring ) ) = ( +g ` ( Frac ` ZZring ) ) : No typesetting found for |- ( +g ` ( Frac ` ZZring ) ) = ( +g ` ( Frac ` ZZring ) ) with typecode |-
174	167 168 172 173	isghm	Could not format ( F e. ( Q GrpHom ( Frac ` ZZring ) ) <-> ( ( Q e. Grp /\ ( Frac ` ZZring ) e. Grp ) /\ ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) ) ) ) : No typesetting found for |- ( F e. ( Q GrpHom ( Frac ` ZZring ) ) <-> ( ( Q e. Grp /\ ( Frac ` ZZring ) e. Grp ) /\ ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) ) ) ) with typecode |-
175	18 166 174	mpbir2an	Could not format F e. ( Q GrpHom ( Frac ` ZZring ) ) : No typesetting found for |- F e. ( Q GrpHom ( Frac ` ZZring ) ) with typecode |-
176		eqid	$$⊢{\mathrm{mulGrp}}_Q={\mathrm{mulGrp}}_Q$$
177	176	ringmgp	$$⊢Q\in \mathrm{Ring}\to {\mathrm{mulGrp}}_Q\in \mathrm{Mnd}$$
178	6 177	ax-mp	$$⊢{\mathrm{mulGrp}}_Q\in \mathrm{Mnd}$$
179		eqid	Could not format ( mulGrp ` ( Frac ` ZZring ) ) = ( mulGrp ` ( Frac ` ZZring ) ) : No typesetting found for |- ( mulGrp ` ( Frac ` ZZring ) ) = ( mulGrp ` ( Frac ` ZZring ) ) with typecode |-
180	179	ringmgp	Could not format ( ( Frac ` ZZring ) e. Ring -> ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd ) : No typesetting found for |- ( ( Frac ` ZZring ) e. Ring -> ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd ) with typecode |-
181	12 180	ax-mp	Could not format ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd : No typesetting found for |- ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd with typecode |-
182	178 181	pm3.2i	Could not format ( ( mulGrp ` Q ) e. Mnd /\ ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd ) : No typesetting found for |- ( ( mulGrp ` Q ) e. Mnd /\ ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd ) with typecode |-
183		eqid	Could not format ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) = ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) : No typesetting found for |- ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) = ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) with typecode |-
184	28 30 144 145 2 71 76 117 122 153 157 183	rlocmulval	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) = [ <. ( ( numer ` q ) x. ( numer ` p ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. ] .~ ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) = [ <. ( ( numer ` q ) x. ( numer ` p ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. ] .~ ) with typecode |-
185	79 81	mulcld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to qp\in ℂ$$
186		qmulcl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to qp\in \mathbb{Q}$$
187		qdencl	$$⊢qp\in \mathbb{Q}\to \mathrm{denom}\left(qp\right)\in \mathbb{N}$$
188	186 187	syl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(qp\right)\in \mathbb{N}$$
189	188	nncnd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(qp\right)\in ℂ$$
190	185 189 92	mul32d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to qp\mathrm{denom}\left(qp\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=qp\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\mathrm{denom}\left(qp\right)$$
191	79 81 88 91	mul4d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to qp\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=q\mathrm{denom}\left(q\right)p\mathrm{denom}\left(p\right)$$
192	191	oveq1d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to qp\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\mathrm{denom}\left(qp\right)=q\mathrm{denom}\left(q\right)p\mathrm{denom}\left(p\right)\mathrm{denom}\left(qp\right)$$
193	190 192	eqtrd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to qp\mathrm{denom}\left(qp\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=q\mathrm{denom}\left(q\right)p\mathrm{denom}\left(p\right)\mathrm{denom}\left(qp\right)$$
194		qmuldeneqnum	$$⊢qp\in \mathbb{Q}\to qp\mathrm{denom}\left(qp\right)=\mathrm{numer}\left(qp\right)$$
195	186 194	syl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to qp\mathrm{denom}\left(qp\right)=\mathrm{numer}\left(qp\right)$$
196	195	oveq1d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to qp\mathrm{denom}\left(qp\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)=\mathrm{numer}\left(qp\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)$$
197	99 104	oveq12d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q\mathrm{denom}\left(q\right)p\mathrm{denom}\left(p\right)=\mathrm{numer}\left(q\right)\mathrm{numer}\left(p\right)$$
198	197	oveq1d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to q\mathrm{denom}\left(q\right)p\mathrm{denom}\left(p\right)\mathrm{denom}\left(qp\right)=\mathrm{numer}\left(q\right)\mathrm{numer}\left(p\right)\mathrm{denom}\left(qp\right)$$
199	193 196 198	3eqtr3rd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(q\right)\mathrm{numer}\left(p\right)\mathrm{denom}\left(qp\right)=\mathrm{numer}\left(qp\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)$$
200	117 122	zmulcld	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(q\right)\mathrm{numer}\left(p\right)\in \mathbb{Z}$$
201		qnumcl	$$⊢qp\in \mathbb{Q}\to \mathrm{numer}\left(qp\right)\in \mathbb{Z}$$
202	186 201	syl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(qp\right)\in \mathbb{Z}$$
203	188	nnzd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(qp\right)\in \mathbb{Z}$$
204	188	nnne0d	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(qp\right)\ne 0$$
205	203 204	eldifsnd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(qp\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
206	205 39	eleqtrdi	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(qp\right)\in \mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
207	28 30 114 71 200 202 134 206	fracerl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(⟨\mathrm{numer}\left(q\right)\mathrm{numer}\left(p\right),\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)⟩\underset{\dot{}}{\sim }⟨\mathrm{numer}\left(qp\right),\mathrm{denom}\left(qp\right)⟩\leftrightarrow \mathrm{numer}\left(q\right)\mathrm{numer}\left(p\right)\mathrm{denom}\left(qp\right)=\mathrm{numer}\left(qp\right)\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)\right)$$
208	199 207	mpbird	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to ⟨\mathrm{numer}\left(q\right)\mathrm{numer}\left(p\right),\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)⟩\underset{\dot{}}{\sim }⟨\mathrm{numer}\left(qp\right),\mathrm{denom}\left(qp\right)⟩$$
209	77 208	erthi	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left[⟨\mathrm{numer}\left(q\right)\mathrm{numer}\left(p\right),\mathrm{denom}\left(q\right)\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(qp\right),\mathrm{denom}\left(qp\right)⟩\right]\underset{\dot{}}{\sim }$$
210	184 209	eqtrd	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) = [ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. ] .~ ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) = [ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. ] .~ ) with typecode |-
211	41	fveq2i	Could not format ( .r ` ( Frac ` ZZring ) ) = ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) : No typesetting found for |- ( .r ` ( Frac ` ZZring ) ) = ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) with typecode |-
212	211	a1i	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( .r ` ( Frac ` ZZring ) ) = ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( .r ` ( Frac ` ZZring ) ) = ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ) with typecode |-
213	212 52 58	oveq123d	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) ) with typecode |-
214		fveq2	$$⊢u=qp\to \mathrm{numer}\left(u\right)=\mathrm{numer}\left(qp\right)$$
215		fveq2	$$⊢u=qp\to \mathrm{denom}\left(u\right)=\mathrm{denom}\left(qp\right)$$
216	214 215	opeq12d	$$⊢u=qp\to ⟨\mathrm{numer}\left(u\right),\mathrm{denom}\left(u\right)⟩=⟨\mathrm{numer}\left(qp\right),\mathrm{denom}\left(qp\right)⟩$$
217	216	eceq1d	$$⊢u=qp\to \left[⟨\mathrm{numer}\left(u\right),\mathrm{denom}\left(u\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(qp\right),\mathrm{denom}\left(qp\right)⟩\right]\underset{\dot{}}{\sim }$$
218		ecexg	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}\to \left[⟨\mathrm{numer}\left(qp\right),\mathrm{denom}\left(qp\right)⟩\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
219	25 218	mp1i	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left[⟨\mathrm{numer}\left(qp\right),\mathrm{denom}\left(qp\right)⟩\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
220	68 217 186 219	fvmptd3	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to F\left(qp\right)=\left[⟨\mathrm{numer}\left(qp\right),\mathrm{denom}\left(qp\right)⟩\right]\underset{\dot{}}{\sim }$$
221	210 213 220	3eqtr4rd	Could not format ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) ) : No typesetting found for |- ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) ) with typecode |-
222	221	rgen2	Could not format A. q e. QQ A. p e. QQ ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) : No typesetting found for |- A. q e. QQ A. p e. QQ ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) with typecode |-
223		zssq	$$⊢\mathbb{Z}\subseteq \mathbb{Q}$$
224		1z	$$⊢1\in \mathbb{Z}$$
225	223 224	sselii	$$⊢1\in \mathbb{Q}$$
226		fveq2	$$⊢q=1\to \mathrm{numer}\left(q\right)=\mathrm{numer}\left(1\right)$$
227		1zzd	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}\to 1\in \mathbb{Z}$$
228	227	znumd	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}\to \mathrm{numer}\left(1\right)=1$$
229	7 228	ax-mp	$$⊢\mathrm{numer}\left(1\right)=1$$
230	226 229	eqtrdi	$$⊢q=1\to \mathrm{numer}\left(q\right)=1$$
231		fveq2	$$⊢q=1\to \mathrm{denom}\left(q\right)=\mathrm{denom}\left(1\right)$$
232	227	zdend	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}\to \mathrm{denom}\left(1\right)=1$$
233	7 232	ax-mp	$$⊢\mathrm{denom}\left(1\right)=1$$
234	231 233	eqtrdi	$$⊢q=1\to \mathrm{denom}\left(q\right)=1$$
235	230 234	opeq12d	$$⊢q=1\to ⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩=⟨1,1⟩$$
236	235	eceq1d	$$⊢q=1\to \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨1,1⟩\right]\underset{\dot{}}{\sim }$$
237	236 3 49	fvmpt3i	$$⊢1\in \mathbb{Q}\to F\left(1\right)=\left[⟨1,1⟩\right]\underset{\dot{}}{\sim }$$
238	225 237	ax-mp	$$⊢F\left(1\right)=\left[⟨1,1⟩\right]\underset{\dot{}}{\sim }$$
239	47 222 238	3pm3.2i	Could not format ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) /\ ( F ` 1 ) = [ <. 1 , 1 >. ] .~ ) : No typesetting found for |- ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) /\ ( F ` 1 ) = [ <. 1 , 1 >. ] .~ ) with typecode |-
240	176 167	mgpbas	$$⊢\mathbb{Q}={\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}$$
241	179 168	mgpbas	Could not format ( Base ` ( Frac ` ZZring ) ) = ( Base ` ( mulGrp ` ( Frac ` ZZring ) ) ) : No typesetting found for |- ( Base ` ( Frac ` ZZring ) ) = ( Base ` ( mulGrp ` ( Frac ` ZZring ) ) ) with typecode |-
242		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
243	1 242	ressmulr	$$⊢\mathbb{Q}\in \mathrm{V}\to \times ={\cdot }_Q$$
244	169 243	ax-mp	$$⊢\times ={\cdot }_Q$$
245	176 244	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_Q}$$
246		eqid	Could not format ( .r ` ( Frac ` ZZring ) ) = ( .r ` ( Frac ` ZZring ) ) : No typesetting found for |- ( .r ` ( Frac ` ZZring ) ) = ( .r ` ( Frac ` ZZring ) ) with typecode |-
247	179 246	mgpplusg	Could not format ( .r ` ( Frac ` ZZring ) ) = ( +g ` ( mulGrp ` ( Frac ` ZZring ) ) ) : No typesetting found for |- ( .r ` ( Frac ` ZZring ) ) = ( +g ` ( mulGrp ` ( Frac ` ZZring ) ) ) with typecode |-
248	1	qrng1	$$⊢1=1_Q$$
249	176 248	ringidval	$$⊢1=0_{{\mathrm{mulGrp}}_Q}$$
250	146	a1i	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}$$
251	149	a1i	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{IDomn}\to \mathbb{Z}\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)$$
252		eqid	$$⊢\left[⟨1,1⟩\right]\underset{\dot{}}{\sim }=\left[⟨1,1⟩\right]\underset{\dot{}}{\sim }$$
253	29 69 41 2 250 251 252	rloc1r	Could not format ( ZZring e. IDomn -> [ <. 1 , 1 >. ] .~ = ( 1r ` ( Frac ` ZZring ) ) ) : No typesetting found for |- ( ZZring e. IDomn -> [ <. 1 , 1 >. ] .~ = ( 1r ` ( Frac ` ZZring ) ) ) with typecode |-
254	7 253	ax-mp	Could not format [ <. 1 , 1 >. ] .~ = ( 1r ` ( Frac ` ZZring ) ) : No typesetting found for |- [ <. 1 , 1 >. ] .~ = ( 1r ` ( Frac ` ZZring ) ) with typecode |-
255	179 254	ringidval	Could not format [ <. 1 , 1 >. ] .~ = ( 0g ` ( mulGrp ` ( Frac ` ZZring ) ) ) : No typesetting found for |- [ <. 1 , 1 >. ] .~ = ( 0g ` ( mulGrp ` ( Frac ` ZZring ) ) ) with typecode |-
256	240 241 245 247 249 255	ismhm	Could not format ( F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) <-> ( ( ( mulGrp ` Q ) e. Mnd /\ ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd ) /\ ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) /\ ( F ` 1 ) = [ <. 1 , 1 >. ] .~ ) ) ) : No typesetting found for |- ( F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) <-> ( ( ( mulGrp ` Q ) e. Mnd /\ ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd ) /\ ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) /\ ( F ` 1 ) = [ <. 1 , 1 >. ] .~ ) ) ) with typecode |-
257	182 239 256	mpbir2an	Could not format F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) : No typesetting found for |- F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) with typecode |-
258	175 257	pm3.2i	Could not format ( F e. ( Q GrpHom ( Frac ` ZZring ) ) /\ F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) ) : No typesetting found for |- ( F e. ( Q GrpHom ( Frac ` ZZring ) ) /\ F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) ) with typecode |-
259	176 179	isrhm	Could not format ( F e. ( Q RingHom ( Frac ` ZZring ) ) <-> ( ( Q e. Ring /\ ( Frac ` ZZring ) e. Ring ) /\ ( F e. ( Q GrpHom ( Frac ` ZZring ) ) /\ F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) ) ) ) : No typesetting found for |- ( F e. ( Q RingHom ( Frac ` ZZring ) ) <-> ( ( Q e. Ring /\ ( Frac ` ZZring ) e. Ring ) /\ ( F e. ( Q GrpHom ( Frac ` ZZring ) ) /\ F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) ) ) ) with typecode |-
260	13 258 259	mpbir2an	Could not format F e. ( Q RingHom ( Frac ` ZZring ) ) : No typesetting found for |- F e. ( Q RingHom ( Frac ` ZZring ) ) with typecode |-
261	46	rgen	Could not format A. q e. QQ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) : No typesetting found for |- A. q e. QQ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) with typecode |-
262	117	zcnd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(q\right)\in ℂ$$
263	122	zcnd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{numer}\left(p\right)\in ℂ$$
264	22	adantr	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\ne 0$$
265	155	adantl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(p\right)\ne 0$$
266	262 88 263 91 264 265	divmuleqd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(\frac{\mathrm{numer}\left(q\right)}{\mathrm{denom}\left(q\right)}=\frac{\mathrm{numer}\left(p\right)}{\mathrm{denom}\left(p\right)}\leftrightarrow \mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)=\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)\right)$$
267	153 39	eleqtrdi	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(q\right)\in \mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
268	157 39	eleqtrdi	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \mathrm{denom}\left(p\right)\in \mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
269	28 30 114 71 117 122 267 268	fracerl	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\underset{\dot{}}{\sim }⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\leftrightarrow \mathrm{numer}\left(q\right)\mathrm{denom}\left(p\right)=\mathrm{numer}\left(p\right)\mathrm{denom}\left(q\right)\right)$$
270	24	adantr	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to ⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\in \left(\mathbb{Z}\times \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)$$
271	77 270	erth	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\underset{\dot{}}{\sim }⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\leftrightarrow \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }\right)$$
272	266 269 271	3bitr2rd	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }\leftrightarrow \frac{\mathrm{numer}\left(q\right)}{\mathrm{denom}\left(q\right)}=\frac{\mathrm{numer}\left(p\right)}{\mathrm{denom}\left(p\right)}\right)$$
273	272	biimpa	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }\right)\to \frac{\mathrm{numer}\left(q\right)}{\mathrm{denom}\left(q\right)}=\frac{\mathrm{numer}\left(p\right)}{\mathrm{denom}\left(p\right)}$$
274		qeqnumdivden	$$⊢q\in \mathbb{Q}\to q=\frac{\mathrm{numer}\left(q\right)}{\mathrm{denom}\left(q\right)}$$
275	274	ad2antrr	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }\right)\to q=\frac{\mathrm{numer}\left(q\right)}{\mathrm{denom}\left(q\right)}$$
276		qeqnumdivden	$$⊢p\in \mathbb{Q}\to p=\frac{\mathrm{numer}\left(p\right)}{\mathrm{denom}\left(p\right)}$$
277	276	ad2antlr	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }\right)\to p=\frac{\mathrm{numer}\left(p\right)}{\mathrm{denom}\left(p\right)}$$
278	273 275 277	3eqtr4d	$$⊢\left(\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\wedge \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }\right)\to q=p$$
279	278	ex	$$⊢\left(q\in \mathbb{Q}\wedge p\in \mathbb{Q}\right)\to \left(\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }\to q=p\right)$$
280	279	rgen2	$$⊢\forall q\in \mathbb{Q}\forall p\in \mathbb{Q}\left(\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(p\right),\mathrm{denom}\left(p\right)⟩\right]\underset{\dot{}}{\sim }\to q=p\right)$$
281	3 56	f1mpt	Could not format ( F : QQ -1-1-> ( Base ` ( Frac ` ZZring ) ) <-> ( A. q e. QQ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ -> q = p ) ) ) : No typesetting found for |- ( F : QQ -1-1-> ( Base ` ( Frac ` ZZring ) ) <-> ( A. q e. QQ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ -> q = p ) ) ) with typecode |-
282	261 280 281	mpbir2an	Could not format F : QQ -1-1-> ( Base ` ( Frac ` ZZring ) ) : No typesetting found for |- F : QQ -1-1-> ( Base ` ( Frac ` ZZring ) ) with typecode |-
283		fveq2	$$⊢q=\frac{a}{b}\to \mathrm{numer}\left(q\right)=\mathrm{numer}\left(\frac{a}{b}\right)$$
284		fveq2	$$⊢q=\frac{a}{b}\to \mathrm{denom}\left(q\right)=\mathrm{denom}\left(\frac{a}{b}\right)$$
285	283 284	opeq12d	$$⊢q=\frac{a}{b}\to ⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩=⟨\mathrm{numer}\left(\frac{a}{b}\right),\mathrm{denom}\left(\frac{a}{b}\right)⟩$$
286	285	eceq1d	$$⊢q=\frac{a}{b}\to \left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }=\left[⟨\mathrm{numer}\left(\frac{a}{b}\right),\mathrm{denom}\left(\frac{a}{b}\right)⟩\right]\underset{\dot{}}{\sim }$$
287	286	eqeq2d	$$⊢q=\frac{a}{b}\to \left(z=\left[⟨\mathrm{numer}\left(q\right),\mathrm{denom}\left(q\right)⟩\right]\underset{\dot{}}{\sim }\leftrightarrow z=\left[⟨\mathrm{numer}\left(\frac{a}{b}\right),\mathrm{denom}\left(\frac{a}{b}\right)⟩\right]\underset{\dot{}}{\sim }\right)$$
288		simpllr	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> a e. ZZ ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> a e. ZZ ) with typecode |-
289	223 288	sselid	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> a e. QQ ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> a e. QQ ) with typecode |-
290		simplr	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b e. ( ZZ \ { 0 } ) ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b e. ( ZZ \ { 0 } ) ) with typecode |-
291	290	eldifad	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b e. ZZ ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b e. ZZ ) with typecode |-
292	223 291	sselid	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b e. QQ ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b e. QQ ) with typecode |-
293		eldifsni	$$⊢b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\to b\ne 0$$
294	290 293	syl	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b =/= 0 ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b =/= 0 ) with typecode |-
295		qdivcl	$$⊢\left(a\in \mathbb{Q}\wedge b\in \mathbb{Q}\wedge b\ne 0\right)\to \frac{a}{b}\in \mathbb{Q}$$
296	289 292 294 295	syl3anc	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> ( a / b ) e. QQ ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> ( a / b ) e. QQ ) with typecode |-
297		simpr	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> z = [ <. a , b >. ] .~ ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> z = [ <. a , b >. ] .~ ) with typecode |-
298	146	a1i	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> ZZring e. CRing ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> ZZring e. CRing ) with typecode |-
299	149	a1i	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) ) ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) ) ) with typecode |-
300	28 29 69 30 31 32 2 298 299	erler	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> .~ Er ( ZZ X. ( ZZ \ { 0 } ) ) ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> .~ Er ( ZZ X. ( ZZ \ { 0 } ) ) ) with typecode |-
301		simpl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to a\in \mathbb{Z}$$
302	301	zcnd	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to a\in ℂ$$
303		eldifi	$$⊢b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\to b\in \mathbb{Z}$$
304	303	adantl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to b\in \mathbb{Z}$$
305	304	zcnd	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to b\in ℂ$$
306	293	adantl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to b\ne 0$$
307	302 305 306	divcld	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \frac{a}{b}\in ℂ$$
308	223 301	sselid	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to a\in \mathbb{Q}$$
309	223 304	sselid	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to b\in \mathbb{Q}$$
310	308 309 306 295	syl3anc	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \frac{a}{b}\in \mathbb{Q}$$
311		qdencl	$$⊢\frac{a}{b}\in \mathbb{Q}\to \mathrm{denom}\left(\frac{a}{b}\right)\in \mathbb{N}$$
312	310 311	syl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \mathrm{denom}\left(\frac{a}{b}\right)\in \mathbb{N}$$
313	312	nncnd	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \mathrm{denom}\left(\frac{a}{b}\right)\in ℂ$$
314	307 313 305	mul32d	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \left(\frac{a}{b}\right)\mathrm{denom}\left(\frac{a}{b}\right)b=\left(\frac{a}{b}\right)b\mathrm{denom}\left(\frac{a}{b}\right)$$
315		qmuldeneqnum	$$⊢\frac{a}{b}\in \mathbb{Q}\to \left(\frac{a}{b}\right)\mathrm{denom}\left(\frac{a}{b}\right)=\mathrm{numer}\left(\frac{a}{b}\right)$$
316	310 315	syl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \left(\frac{a}{b}\right)\mathrm{denom}\left(\frac{a}{b}\right)=\mathrm{numer}\left(\frac{a}{b}\right)$$
317	316	oveq1d	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \left(\frac{a}{b}\right)\mathrm{denom}\left(\frac{a}{b}\right)b=\mathrm{numer}\left(\frac{a}{b}\right)b$$
318	302 305 306	divcan1d	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \left(\frac{a}{b}\right)b=a$$
319	318	oveq1d	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \left(\frac{a}{b}\right)b\mathrm{denom}\left(\frac{a}{b}\right)=a\mathrm{denom}\left(\frac{a}{b}\right)$$
320	314 317 319	3eqtr3rd	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to a\mathrm{denom}\left(\frac{a}{b}\right)=\mathrm{numer}\left(\frac{a}{b}\right)b$$
321	146	a1i	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}$$
322		qnumcl	$$⊢\frac{a}{b}\in \mathbb{Q}\to \mathrm{numer}\left(\frac{a}{b}\right)\in \mathbb{Z}$$
323	310 322	syl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \mathrm{numer}\left(\frac{a}{b}\right)\in \mathbb{Z}$$
324		simpr	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
325	324 39	eleqtrdi	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to b\in \mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
326	312	nnzd	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \mathrm{denom}\left(\frac{a}{b}\right)\in \mathbb{Z}$$
327	312	nnne0d	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \mathrm{denom}\left(\frac{a}{b}\right)\ne 0$$
328	326 327	eldifsnd	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \mathrm{denom}\left(\frac{a}{b}\right)\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
329	328 39	eleqtrdi	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \mathrm{denom}\left(\frac{a}{b}\right)\in \mathrm{RLReg}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
330	28 30 114 321 301 323 325 329	fracerl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to \left(⟨a,b⟩\underset{\dot{}}{\sim }⟨\mathrm{numer}\left(\frac{a}{b}\right),\mathrm{denom}\left(\frac{a}{b}\right)⟩\leftrightarrow a\mathrm{denom}\left(\frac{a}{b}\right)=\mathrm{numer}\left(\frac{a}{b}\right)b\right)$$
331	320 330	mpbird	$$⊢\left(a\in \mathbb{Z}\wedge b\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\right)\to ⟨a,b⟩\underset{\dot{}}{\sim }⟨\mathrm{numer}\left(\frac{a}{b}\right),\mathrm{denom}\left(\frac{a}{b}\right)⟩$$
332	331	ad4ant23	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> <. a , b >. .~ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> <. a , b >. .~ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ) with typecode |-
333	300 332	erthi	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> [ <. a , b >. ] .~ = [ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ] .~ ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> [ <. a , b >. ] .~ = [ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ] .~ ) with typecode |-
334	297 333	eqtrd	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> z = [ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ] .~ ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> z = [ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ] .~ ) with typecode |-
335	287 296 334	rspcedvdw	Could not format ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ) : No typesetting found for |- ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ) with typecode |-
336	45	eleq2i	Could not format ( z e. ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) <-> z e. ( Base ` ( Frac ` ZZring ) ) ) : No typesetting found for |- ( z e. ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) <-> z e. ( Base ` ( Frac ` ZZring ) ) ) with typecode |-
337	336	biimpri	Could not format ( z e. ( Base ` ( Frac ` ZZring ) ) -> z e. ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) ) : No typesetting found for |- ( z e. ( Base ` ( Frac ` ZZring ) ) -> z e. ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) ) with typecode |-
338	337	elrlocbasi	Could not format ( z e. ( Base ` ( Frac ` ZZring ) ) -> E. a e. ZZ E. b e. ( ZZ \ { 0 } ) z = [ <. a , b >. ] .~ ) : No typesetting found for |- ( z e. ( Base ` ( Frac ` ZZring ) ) -> E. a e. ZZ E. b e. ( ZZ \ { 0 } ) z = [ <. a , b >. ] .~ ) with typecode |-
339	335 338	r19.29vva	Could not format ( z e. ( Base ` ( Frac ` ZZring ) ) -> E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ) : No typesetting found for |- ( z e. ( Base ` ( Frac ` ZZring ) ) -> E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ) with typecode |-
340	339	rgen	Could not format A. z e. ( Base ` ( Frac ` ZZring ) ) E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ : No typesetting found for |- A. z e. ( Base ` ( Frac ` ZZring ) ) E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ with typecode |-
341	3	fompt	Could not format ( F : QQ -onto-> ( Base ` ( Frac ` ZZring ) ) <-> ( A. q e. QQ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) /\ A. z e. ( Base ` ( Frac ` ZZring ) ) E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ) ) : No typesetting found for |- ( F : QQ -onto-> ( Base ` ( Frac ` ZZring ) ) <-> ( A. q e. QQ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) /\ A. z e. ( Base ` ( Frac ` ZZring ) ) E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ) ) with typecode |-
342	261 340 341	mpbir2an	Could not format F : QQ -onto-> ( Base ` ( Frac ` ZZring ) ) : No typesetting found for |- F : QQ -onto-> ( Base ` ( Frac ` ZZring ) ) with typecode |-
343		df-f1o	Could not format ( F : QQ -1-1-onto-> ( Base ` ( Frac ` ZZring ) ) <-> ( F : QQ -1-1-> ( Base ` ( Frac ` ZZring ) ) /\ F : QQ -onto-> ( Base ` ( Frac ` ZZring ) ) ) ) : No typesetting found for |- ( F : QQ -1-1-onto-> ( Base ` ( Frac ` ZZring ) ) <-> ( F : QQ -1-1-> ( Base ` ( Frac ` ZZring ) ) /\ F : QQ -onto-> ( Base ` ( Frac ` ZZring ) ) ) ) with typecode |-
344	282 342 343	mpbir2an	Could not format F : QQ -1-1-onto-> ( Base ` ( Frac ` ZZring ) ) : No typesetting found for |- F : QQ -1-1-onto-> ( Base ` ( Frac ` ZZring ) ) with typecode |-
345	167 168	isrim	Could not format ( F e. ( Q RingIso ( Frac ` ZZring ) ) <-> ( F e. ( Q RingHom ( Frac ` ZZring ) ) /\ F : QQ -1-1-onto-> ( Base ` ( Frac ` ZZring ) ) ) ) : No typesetting found for |- ( F e. ( Q RingIso ( Frac ` ZZring ) ) <-> ( F e. ( Q RingHom ( Frac ` ZZring ) ) /\ F : QQ -1-1-onto-> ( Base ` ( Frac ` ZZring ) ) ) ) with typecode |-
346	260 344 345	mpbir2an	Could not format F e. ( Q RingIso ( Frac ` ZZring ) ) : No typesetting found for |- F e. ( Q RingIso ( Frac ` ZZring ) ) with typecode |-