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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	archiexdiv.0	⊢ 0 = ( 0g ‘ 𝑊 )
	archiexdiv.i	⊢ < = ( lt ‘ 𝑊 )
	archiexdiv.x	⊢ · = ( .g ‘ 𝑊 )
Assertion	archiexdiv	⊢ ( ( ( 𝑊 ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ∃ 𝑛 ∈ ℕ 𝑌 < ( 𝑛 · 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		archiexdiv.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		archiexdiv.0	⊢ 0 = ( 0g ‘ 𝑊 )
3		archiexdiv.i	⊢ < = ( lt ‘ 𝑊 )
4		archiexdiv.x	⊢ · = ( .g ‘ 𝑊 )
5	1 2 3 4	isarchi3	⊢ ( 𝑊 ∈ oGrp → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) ) )
6	5	biimpa	⊢ ( ( 𝑊 ∈ oGrp ∧ 𝑊 ∈ Archi ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) )
7	6	3ad2ant1	⊢ ( ( ( 𝑊 ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) )
8		simp3	⊢ ( ( ( 𝑊 ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → 0 < 𝑋 )
9		breq2	⊢ ( 𝑥 = 𝑋 → ( 0 < 𝑥 ↔ 0 < 𝑋 ) )
10		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑛 · 𝑥 ) = ( 𝑛 · 𝑋 ) )
11	10	breq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑦 < ( 𝑛 · 𝑥 ) ↔ 𝑦 < ( 𝑛 · 𝑋 ) ) )
12	11	rexbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑋 ) ) )
13	9 12	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) ↔ ( 0 < 𝑋 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑋 ) ) ) )
14		breq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 < ( 𝑛 · 𝑋 ) ↔ 𝑌 < ( 𝑛 · 𝑋 ) ) )
15	14	rexbidv	⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑋 ) ↔ ∃ 𝑛 ∈ ℕ 𝑌 < ( 𝑛 · 𝑋 ) ) )
16	15	imbi2d	⊢ ( 𝑦 = 𝑌 → ( ( 0 < 𝑋 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑋 ) ) ↔ ( 0 < 𝑋 → ∃ 𝑛 ∈ ℕ 𝑌 < ( 𝑛 · 𝑋 ) ) ) )
17	13 16	rspc2v	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) → ( 0 < 𝑋 → ∃ 𝑛 ∈ ℕ 𝑌 < ( 𝑛 · 𝑋 ) ) ) )
18	17	3ad2ant2	⊢ ( ( ( 𝑊 ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑛 ∈ ℕ 𝑦 < ( 𝑛 · 𝑥 ) ) → ( 0 < 𝑋 → ∃ 𝑛 ∈ ℕ 𝑌 < ( 𝑛 · 𝑋 ) ) ) )
19	7 8 18	mp2d	⊢ ( ( ( 𝑊 ∈ oGrp ∧ 𝑊 ∈ Archi ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 < 𝑋 ) → ∃ 𝑛 ∈ ℕ 𝑌 < ( 𝑛 · 𝑋 ) )