Theorem archirng

Description: Property of Archimedean ordered groups, framing positive Y between multiples of X . (Contributed by Thierry Arnoux, 12-Apr-2018)

	Ref	Expression
Hypotheses	archirng.b	$$⊢B={\mathrm{Base}}_W$$
	archirng.0	$$⊢\underset{\dot{}}{0}=0_W$$
	archirng.i	$$⊢\underset{\dot{}}{<}={<}_W$$
	archirng.l	$$⊢\underset{\dot{}}{\le }={\le }_W$$
	archirng.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	archirng.1	$$⊢\phi \to W\in \mathrm{oGrp}$$
	archirng.2	$$⊢\phi \to W\in \mathrm{Archi}$$
	archirng.3	$$⊢\phi \to X\in B$$
	archirng.4	$$⊢\phi \to Y\in B$$
	archirng.5	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}X$$
	archirng.6	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}Y$$
Assertion	archirng	$$⊢\phi \to \exists n\in {\mathbb{N}}_0\left(\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\wedge Y\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		archirng.b	$$⊢B={\mathrm{Base}}_W$$
2		archirng.0	$$⊢\underset{\dot{}}{0}=0_W$$
3		archirng.i	$$⊢\underset{\dot{}}{<}={<}_W$$
4		archirng.l	$$⊢\underset{\dot{}}{\le }={\le }_W$$
5		archirng.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		archirng.1	$$⊢\phi \to W\in \mathrm{oGrp}$$
7		archirng.2	$$⊢\phi \to W\in \mathrm{Archi}$$
8		archirng.3	$$⊢\phi \to X\in B$$
9		archirng.4	$$⊢\phi \to Y\in B$$
10		archirng.5	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}X$$
11		archirng.6	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{<}Y$$
12		oveq1	$$⊢m=0\to m\underset{\dot{}}{·}X=0\underset{\dot{}}{·}X$$
13	12	breq2d	$$⊢m=0\to \left(Y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\leftrightarrow Y\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}X\right)\right)$$
14		oveq1	$$⊢m=n\to m\underset{\dot{}}{·}X=n\underset{\dot{}}{·}X$$
15	14	breq2d	$$⊢m=n\to \left(Y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\leftrightarrow Y\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}X\right)\right)$$
16		oveq1	$$⊢m=n+1\to m\underset{\dot{}}{·}X=\left(n+1\right)\underset{\dot{}}{·}X$$
17	16	breq2d	$$⊢m=n+1\to \left(Y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\leftrightarrow Y\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}X\right)\right)$$
18		isogrp	$$⊢W\in \mathrm{oGrp}\leftrightarrow \left(W\in \mathrm{Grp}\wedge W\in \mathrm{oMnd}\right)$$
19	18	simprbi	$$⊢W\in \mathrm{oGrp}\to W\in \mathrm{oMnd}$$
20		omndtos	$$⊢W\in \mathrm{oMnd}\to W\in \mathrm{Toset}$$
21	6 19 20	3syl	$$⊢\phi \to W\in \mathrm{Toset}$$
22		ogrpgrp	$$⊢W\in \mathrm{oGrp}\to W\in \mathrm{Grp}$$
23	6 22	syl	$$⊢\phi \to W\in \mathrm{Grp}$$
24	1 2	grpidcl	$$⊢W\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
25	23 24	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
26	1 4 3	tltnle	$$⊢\left(W\in \mathrm{Toset}\wedge \underset{\dot{}}{0}\in B\wedge Y\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}Y\leftrightarrow \neg Y\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)$$
27	21 25 9 26	syl3anc	$$⊢\phi \to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}Y\leftrightarrow \neg Y\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)$$
28	11 27	mpbid	$$⊢\phi \to \neg Y\underset{\dot{}}{\le }\underset{\dot{}}{0}$$
29	1 2 5	mulg0	$$⊢X\in B\to 0\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
30	8 29	syl	$$⊢\phi \to 0\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
31	30	breq2d	$$⊢\phi \to \left(Y\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}X\right)\leftrightarrow Y\underset{\dot{}}{\le }\underset{\dot{}}{0}\right)$$
32	28 31	mtbird	$$⊢\phi \to \neg Y\underset{\dot{}}{\le }\left(0\underset{\dot{}}{·}X\right)$$
33	8 9	jca	$$⊢\phi \to \left(X\in B\wedge Y\in B\right)$$
34		omndmnd	$$⊢W\in \mathrm{oMnd}\to W\in \mathrm{Mnd}$$
35	6 19 34	3syl	$$⊢\phi \to W\in \mathrm{Mnd}$$
36	1 2 5 4 3	isarchi2	$$⊢\left(W\in \mathrm{Toset}\wedge W\in \mathrm{Mnd}\right)\to \left(W\in \mathrm{Archi}\leftrightarrow \forall x\in B\forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}x\right)\right)\right)$$
37	36	biimpa	$$⊢\left(\left(W\in \mathrm{Toset}\wedge W\in \mathrm{Mnd}\right)\wedge W\in \mathrm{Archi}\right)\to \forall x\in B\forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}x\right)\right)$$
38	21 35 7 37	syl21anc	$$⊢\phi \to \forall x\in B\forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}x\right)\right)$$
39		breq2	$$⊢x=X\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)$$
40		oveq2	$$⊢x=X\to m\underset{\dot{}}{·}x=m\underset{\dot{}}{·}X$$
41	40	breq2d	$$⊢x=X\to \left(y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}x\right)\leftrightarrow y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\right)$$
42	41	rexbidv	$$⊢x=X\to \left(\exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}x\right)\leftrightarrow \exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\right)$$
43	39 42	imbi12d	$$⊢x=X\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}x\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\right)\right)$$
44		breq1	$$⊢y=Y\to \left(y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\leftrightarrow Y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\right)$$
45	44	rexbidv	$$⊢y=Y\to \left(\exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\leftrightarrow \exists m\in \mathbb{N}Y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\right)$$
46	45	imbi2d	$$⊢y=Y\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists m\in \mathbb{N}Y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\right)\right)$$
47	43 46	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists m\in \mathbb{N}y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}x\right)\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists m\in \mathbb{N}Y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)\right)\right)$$
48	33 38 10 47	syl3c	$$⊢\phi \to \exists m\in \mathbb{N}Y\underset{\dot{}}{\le }\left(m\underset{\dot{}}{·}X\right)$$
49	13 15 17 32 48	nn0min	$$⊢\phi \to \exists n\in {\mathbb{N}}_0\left(\neg Y\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}X\right)\wedge Y\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}X\right)\right)$$
50	21	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to W\in \mathrm{Toset}$$
51	23	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to W\in \mathrm{Grp}$$
52		simpr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to n\in {\mathbb{N}}_0$$
53	52	nn0zd	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to n\in \mathbb{Z}$$
54	8	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to X\in B$$
55	1 5	mulgcl	$$⊢\left(W\in \mathrm{Grp}\wedge n\in \mathbb{Z}\wedge X\in B\right)\to n\underset{\dot{}}{·}X\in B$$
56	51 53 54 55	syl3anc	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to n\underset{\dot{}}{·}X\in B$$
57	9	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to Y\in B$$
58	1 4 3	tltnle	$$⊢\left(W\in \mathrm{Toset}\wedge n\underset{\dot{}}{·}X\in B\wedge Y\in B\right)\to \left(\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\leftrightarrow \neg Y\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}X\right)\right)$$
59	50 56 57 58	syl3anc	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\leftrightarrow \neg Y\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}X\right)\right)$$
60	59	anbi1d	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(\left(\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\wedge Y\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}X\right)\right)\leftrightarrow \left(\neg Y\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}X\right)\wedge Y\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}X\right)\right)\right)$$
61	60	rexbidva	$$⊢\phi \to \left(\exists n\in {\mathbb{N}}_0\left(\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\wedge Y\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}X\right)\right)\leftrightarrow \exists n\in {\mathbb{N}}_0\left(\neg Y\underset{\dot{}}{\le }\left(n\underset{\dot{}}{·}X\right)\wedge Y\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}X\right)\right)\right)$$
62	49 61	mpbird	$$⊢\phi \to \exists n\in {\mathbb{N}}_0\left(\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\wedge Y\underset{\dot{}}{\le }\left(\left(n+1\right)\underset{\dot{}}{·}X\right)\right)$$