Theorem lterpq

Description: Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	lterpq	$$⊢A{<}_{\mathrm{𝑝𝑸}}B\leftrightarrow {/}_{𝑸}\left(A\right){<}_{𝑸}{/}_{𝑸}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ltpq	$$⊢{<}_{\mathrm{𝑝𝑸}}=\left\{⟨x,y⟩|\left(\left(x\in \left(𝑵\times 𝑵\right)\wedge y\in \left(𝑵\times 𝑵\right)\right)\wedge \left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){<}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right)\right)\right\}$$
2		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in \left(𝑵\times 𝑵\right)\wedge y\in \left(𝑵\times 𝑵\right)\right)\wedge \left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){<}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right)\right)\right\}\subseteq \left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)$$
3	1 2	eqsstri	$$⊢{<}_{\mathrm{𝑝𝑸}}\subseteq \left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)$$
4	3	brel	$$⊢A{<}_{\mathrm{𝑝𝑸}}B\to \left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)$$
5		ltrelnq	$$⊢{<}_{𝑸}\subseteq 𝑸\times 𝑸$$
6	5	brel	$$⊢{/}_{𝑸}\left(A\right){<}_{𝑸}{/}_{𝑸}\left(B\right)\to \left({/}_{𝑸}\left(A\right)\in 𝑸\wedge {/}_{𝑸}\left(B\right)\in 𝑸\right)$$
7		elpqn	$$⊢{/}_{𝑸}\left(A\right)\in 𝑸\to {/}_{𝑸}\left(A\right)\in \left(𝑵\times 𝑵\right)$$
8		elpqn	$$⊢{/}_{𝑸}\left(B\right)\in 𝑸\to {/}_{𝑸}\left(B\right)\in \left(𝑵\times 𝑵\right)$$
9		nqerf	$$⊢{/}_{𝑸}:𝑵\times 𝑵⟶𝑸$$
10	9	fdmi	$$⊢\mathrm{dom}{/}_{𝑸}=𝑵\times 𝑵$$
11		0nelxp	$$⊢\neg \varnothing \in \left(𝑵\times 𝑵\right)$$
12	10 11	ndmfvrcl	$$⊢{/}_{𝑸}\left(A\right)\in \left(𝑵\times 𝑵\right)\to A\in \left(𝑵\times 𝑵\right)$$
13	10 11	ndmfvrcl	$$⊢{/}_{𝑸}\left(B\right)\in \left(𝑵\times 𝑵\right)\to B\in \left(𝑵\times 𝑵\right)$$
14	12 13	anim12i	$$⊢\left({/}_{𝑸}\left(A\right)\in \left(𝑵\times 𝑵\right)\wedge {/}_{𝑸}\left(B\right)\in \left(𝑵\times 𝑵\right)\right)\to \left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)$$
15	7 8 14	syl2an	$$⊢\left({/}_{𝑸}\left(A\right)\in 𝑸\wedge {/}_{𝑸}\left(B\right)\in 𝑸\right)\to \left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)$$
16	6 15	syl	$$⊢{/}_{𝑸}\left(A\right){<}_{𝑸}{/}_{𝑸}\left(B\right)\to \left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)$$
17		xp1st	$$⊢A\in \left(𝑵\times 𝑵\right)\to 1^{st}\left(A\right)\in 𝑵$$
18		xp2nd	$$⊢B\in \left(𝑵\times 𝑵\right)\to 2^{nd}\left(B\right)\in 𝑵$$
19		mulclpi	$$⊢\left(1^{st}\left(A\right)\in 𝑵\wedge 2^{nd}\left(B\right)\in 𝑵\right)\to 1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\in 𝑵$$
20	17 18 19	syl2an	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to 1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\in 𝑵$$
21		ltmpi	$$⊢1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\in 𝑵\to \left(\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){<}_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)\leftrightarrow \left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)\right)\right)$$
22	20 21	syl	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){<}_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)\leftrightarrow \left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)\right)\right)$$
23		nqercl	$$⊢A\in \left(𝑵\times 𝑵\right)\to {/}_{𝑸}\left(A\right)\in 𝑸$$
24		nqercl	$$⊢B\in \left(𝑵\times 𝑵\right)\to {/}_{𝑸}\left(B\right)\in 𝑸$$
25		ordpinq	$$⊢\left({/}_{𝑸}\left(A\right)\in 𝑸\wedge {/}_{𝑸}\left(B\right)\in 𝑸\right)\to \left({/}_{𝑸}\left(A\right){<}_{𝑸}{/}_{𝑸}\left(B\right)\leftrightarrow \left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){<}_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)\right)$$
26	23 24 25	syl2an	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left({/}_{𝑸}\left(A\right){<}_{𝑸}{/}_{𝑸}\left(B\right)\leftrightarrow \left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){<}_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)\right)$$
27		1st2nd2	$$⊢A\in \left(𝑵\times 𝑵\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
28		1st2nd2	$$⊢B\in \left(𝑵\times 𝑵\right)\to B=⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩$$
29	27 28	breqan12d	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(A{<}_{\mathrm{𝑝𝑸}}B\leftrightarrow ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩{<}_{\mathrm{𝑝𝑸}}⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\right)$$
30		ordpipq	$$⊢⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩{<}_{\mathrm{𝑝𝑸}}⟨1^{st}\left(B\right),2^{nd}\left(B\right)⟩\leftrightarrow \left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){<}_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)$$
31	29 30	bitrdi	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(A{<}_{\mathrm{𝑝𝑸}}B\leftrightarrow \left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){<}_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\right)$$
32		xp1st	$$⊢{/}_{𝑸}\left(A\right)\in \left(𝑵\times 𝑵\right)\to 1^{st}\left({/}_{𝑸}\left(A\right)\right)\in 𝑵$$
33	23 7 32	3syl	$$⊢A\in \left(𝑵\times 𝑵\right)\to 1^{st}\left({/}_{𝑸}\left(A\right)\right)\in 𝑵$$
34		xp2nd	$$⊢{/}_{𝑸}\left(B\right)\in \left(𝑵\times 𝑵\right)\to 2^{nd}\left({/}_{𝑸}\left(B\right)\right)\in 𝑵$$
35	24 8 34	3syl	$$⊢B\in \left(𝑵\times 𝑵\right)\to 2^{nd}\left({/}_{𝑸}\left(B\right)\right)\in 𝑵$$
36		mulclpi	$$⊢\left(1^{st}\left({/}_{𝑸}\left(A\right)\right)\in 𝑵\wedge 2^{nd}\left({/}_{𝑸}\left(B\right)\right)\in 𝑵\right)\to 1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\in 𝑵$$
37	33 35 36	syl2an	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to 1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\in 𝑵$$
38		ltmpi	$$⊢1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\in 𝑵\to \left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){<}_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\leftrightarrow \left(\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)\right){<}_{𝑵}\left(\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\right)\right)$$
39	37 38	syl	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){<}_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\leftrightarrow \left(\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)\right){<}_{𝑵}\left(\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\right)\right)$$
40		mulcompi	$$⊢\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)=\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)$$
41	40	a1i	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)=\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)$$
42		nqerrel	$$⊢A\in \left(𝑵\times 𝑵\right)\to A{~}_{𝑸}{/}_{𝑸}\left(A\right)$$
43	23 7	syl	$$⊢A\in \left(𝑵\times 𝑵\right)\to {/}_{𝑸}\left(A\right)\in \left(𝑵\times 𝑵\right)$$
44		enqbreq2	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge {/}_{𝑸}\left(A\right)\in \left(𝑵\times 𝑵\right)\right)\to \left(A{~}_{𝑸}{/}_{𝑸}\left(A\right)\leftrightarrow 1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)=1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)$$
45	43 44	mpdan	$$⊢A\in \left(𝑵\times 𝑵\right)\to \left(A{~}_{𝑸}{/}_{𝑸}\left(A\right)\leftrightarrow 1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)=1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)$$
46	42 45	mpbid	$$⊢A\in \left(𝑵\times 𝑵\right)\to 1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)=1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)$$
47	46	eqcomd	$$⊢A\in \left(𝑵\times 𝑵\right)\to 1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)=1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)$$
48		nqerrel	$$⊢B\in \left(𝑵\times 𝑵\right)\to B{~}_{𝑸}{/}_{𝑸}\left(B\right)$$
49	24 8	syl	$$⊢B\in \left(𝑵\times 𝑵\right)\to {/}_{𝑸}\left(B\right)\in \left(𝑵\times 𝑵\right)$$
50		enqbreq2	$$⊢\left(B\in \left(𝑵\times 𝑵\right)\wedge {/}_{𝑸}\left(B\right)\in \left(𝑵\times 𝑵\right)\right)\to \left(B{~}_{𝑸}{/}_{𝑸}\left(B\right)\leftrightarrow 1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)=1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)$$
51	49 50	mpdan	$$⊢B\in \left(𝑵\times 𝑵\right)\to \left(B{~}_{𝑸}{/}_{𝑸}\left(B\right)\leftrightarrow 1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)=1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)$$
52	48 51	mpbid	$$⊢B\in \left(𝑵\times 𝑵\right)\to 1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)=1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)$$
53	47 52	oveqan12d	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){\cdot }_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)=\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)$$
54		mulcompi	$$⊢\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)=\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)$$
55		fvex	$$⊢1^{st}\left(B\right)\in \mathrm{V}$$
56		fvex	$$⊢2^{nd}\left(A\right)\in \mathrm{V}$$
57		fvex	$$⊢1^{st}\left({/}_{𝑸}\left(A\right)\right)\in \mathrm{V}$$
58		mulcompi	$$⊢x{\cdot }_{𝑵}y=y{\cdot }_{𝑵}x$$
59		mulasspi	$$⊢\left(x{\cdot }_{𝑵}y\right){\cdot }_{𝑵}z=x{\cdot }_{𝑵}\left(y{\cdot }_{𝑵}z\right)$$
60		fvex	$$⊢2^{nd}\left({/}_{𝑸}\left(B\right)\right)\in \mathrm{V}$$
61	55 56 57 58 59 60	caov411	$$⊢\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)=\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){\cdot }_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)$$
62	54 61	eqtri	$$⊢\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)=\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right){\cdot }_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)$$
63		mulcompi	$$⊢\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)=\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)$$
64		fvex	$$⊢1^{st}\left({/}_{𝑸}\left(B\right)\right)\in \mathrm{V}$$
65		fvex	$$⊢2^{nd}\left({/}_{𝑸}\left(A\right)\right)\in \mathrm{V}$$
66		fvex	$$⊢1^{st}\left(A\right)\in \mathrm{V}$$
67		fvex	$$⊢2^{nd}\left(B\right)\in \mathrm{V}$$
68	64 65 66 58 59 67	caov411	$$⊢\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)=\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)$$
69	63 68	eqtri	$$⊢\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)=\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)$$
70	53 62 69	3eqtr4g	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)=\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)$$
71	41 70	breq12d	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(\left(\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right)\right){<}_{𝑵}\left(\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right){\cdot }_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)\right)\leftrightarrow \left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)\right)\right)$$
72	31 39 71	3bitrd	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(A{<}_{\mathrm{𝑝𝑸}}B\leftrightarrow \left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(A\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(B\right)\right)\right)\right){<}_{𝑵}\left(\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){\cdot }_{𝑵}\left(1^{st}\left({/}_{𝑸}\left(B\right)\right){\cdot }_{𝑵}{2}^{nd}\left({/}_{𝑸}\left(A\right)\right)\right)\right)\right)$$
73	22 26 72	3bitr4rd	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to \left(A{<}_{\mathrm{𝑝𝑸}}B\leftrightarrow {/}_{𝑸}\left(A\right){<}_{𝑸}{/}_{𝑸}\left(B\right)\right)$$
74	4 16 73	pm5.21nii	$$⊢A{<}_{\mathrm{𝑝𝑸}}B\leftrightarrow {/}_{𝑸}\left(A\right){<}_{𝑸}{/}_{𝑸}\left(B\right)$$