This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 < 𝑋 ) → ∃ 𝑛 ∈ ℕ 𝑌 < ( 𝑛 · 𝑋 ) )