Theorem archiexdiv

Description: In an Archimedean group, given two positive elements, there exists a "divisor" n . (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	archiexdiv.b	$$⊢B={\mathrm{Base}}_W$$
	archiexdiv.0	$$⊢\underset{\dot{}}{0}=0_W$$
	archiexdiv.i	$$⊢\underset{\dot{}}{<}={<}_W$$
	archiexdiv.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
Assertion	archiexdiv	$$⊢\left(\left(W\in \mathrm{oGrp}\wedge W\in \mathrm{Archi}\right)\wedge \left(X\in B\wedge Y\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to \exists n\in \mathbb{N}Y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		archiexdiv.b	$$⊢B={\mathrm{Base}}_W$$
2		archiexdiv.0	$$⊢\underset{\dot{}}{0}=0_W$$
3		archiexdiv.i	$$⊢\underset{\dot{}}{<}={<}_W$$
4		archiexdiv.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5	1 2 3 4	isarchi3	$$⊢W\in \mathrm{oGrp}\to \left(W\in \mathrm{Archi}\leftrightarrow \forall x\in B\forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}x\right)\right)\right)$$
6	5	biimpa	$$⊢\left(W\in \mathrm{oGrp}\wedge W\in \mathrm{Archi}\right)\to \forall x\in B\forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}x\right)\right)$$
7	6	3ad2ant1	$$⊢\left(\left(W\in \mathrm{oGrp}\wedge W\in \mathrm{Archi}\right)\wedge \left(X\in B\wedge Y\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to \forall x\in B\forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}x\right)\right)$$
8		simp3	$$⊢\left(\left(W\in \mathrm{oGrp}\wedge W\in \mathrm{Archi}\right)\wedge \left(X\in B\wedge Y\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}X$$
9		breq2	$$⊢x=X\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)$$
10		oveq2	$$⊢x=X\to n\underset{\dot{}}{·}x=n\underset{\dot{}}{·}X$$
11	10	breq2d	$$⊢x=X\to \left(y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}x\right)\leftrightarrow y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\right)$$
12	11	rexbidv	$$⊢x=X\to \left(\exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}x\right)\leftrightarrow \exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\right)$$
13	9 12	imbi12d	$$⊢x=X\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}x\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\right)\right)$$
14		breq1	$$⊢y=Y\to \left(y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\leftrightarrow Y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\right)$$
15	14	rexbidv	$$⊢y=Y\to \left(\exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\leftrightarrow \exists n\in \mathbb{N}Y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\right)$$
16	15	imbi2d	$$⊢y=Y\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists n\in \mathbb{N}Y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\right)\right)$$
17	13 16	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 n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}x\right)\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists n\in \mathbb{N}Y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\right)\right)$$
18	17	3ad2ant2	$$⊢\left(\left(W\in \mathrm{oGrp}\wedge W\in \mathrm{Archi}\right)\wedge \left(X\in B\wedge Y\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to \left(\forall x\in B\forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\to \exists n\in \mathbb{N}y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}x\right)\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\to \exists n\in \mathbb{N}Y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)\right)\right)$$
19	7 8 18	mp2d	$$⊢\left(\left(W\in \mathrm{oGrp}\wedge W\in \mathrm{Archi}\right)\wedge \left(X\in B\wedge Y\in B\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to \exists n\in \mathbb{N}Y\underset{\dot{}}{<}\left(n\underset{\dot{}}{·}X\right)$$