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

Metamath Proof Explorer

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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
archirng.0 ⊢ 0 = ( 0g ‘ 𝑊 )
archirng.i ⊢ < = ( lt ‘ 𝑊 )
archirng.l ⊢ ≤ = ( le ‘ 𝑊 )
archirng.x ⊢ · = ( .g ‘ 𝑊 )
archirng.1 ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
archirng.2 ⊢ ( 𝜑 → 𝑊 ∈ Archi )
archirng.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
archirng.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
archirng.5 ⊢ ( 𝜑 → 0 < 𝑋 )
archirng.6 ⊢ ( 𝜑 → 0 < 𝑌 )
Assertion archirng ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( ( 𝑛 · 𝑋 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 archirng.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 archirng.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 archirng.i ⊢ < = ( lt ‘ 𝑊 )
4 archirng.l ⊢ ≤ = ( le ‘ 𝑊 )
5 archirng.x ⊢ · = ( .g ‘ 𝑊 )
6 archirng.1 ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
7 archirng.2 ⊢ ( 𝜑 → 𝑊 ∈ Archi )
8 archirng.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9 archirng.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10 archirng.5 ⊢ ( 𝜑 → 0 < 𝑋 )
11 archirng.6 ⊢ ( 𝜑 → 0 < 𝑌 )
12 oveq1 ⊢ ( 𝑚 = 0 → ( 𝑚 · 𝑋 ) = ( 0 · 𝑋 ) )
13 12 breq2d ⊢ ( 𝑚 = 0 → ( 𝑌 ≤ ( 𝑚 · 𝑋 ) ↔ 𝑌 ≤ ( 0 · 𝑋 ) ) )
14 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 · 𝑋 ) = ( 𝑛 · 𝑋 ) )
15 14 breq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑌 ≤ ( 𝑚 · 𝑋 ) ↔ 𝑌 ≤ ( 𝑛 · 𝑋 ) ) )
16 oveq1 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 · 𝑋 ) = ( ( 𝑛 + 1 ) · 𝑋 ) )
17 16 breq2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑌 ≤ ( 𝑚 · 𝑋 ) ↔ 𝑌 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) )
18 isogrp ⊢ ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
19 18 simprbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
20 omndtos ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
21 6 19 20 3syl ⊢ ( 𝜑 → 𝑊 ∈ Toset )
22 ogrpgrp ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
23 6 22 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
24 1 2 grpidcl ⊢ ( 𝑊 ∈ Grp → 0 ∈ 𝐵 )
25 23 24 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
26 1 4 3 tltnle ⊢ ( ( 𝑊 ∈ Toset ∧ 0 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 0 < 𝑌 ↔ ¬ 𝑌 ≤ 0 ) )
27 21 25 9 26 syl3anc ⊢ ( 𝜑 → ( 0 < 𝑌 ↔ ¬ 𝑌 ≤ 0 ) )
28 11 27 mpbid ⊢ ( 𝜑 → ¬ 𝑌 ≤ 0 )
29 1 2 5 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = 0 )
30 8 29 syl ⊢ ( 𝜑 → ( 0 · 𝑋 ) = 0 )
31 30 breq2d ⊢ ( 𝜑 → ( 𝑌 ≤ ( 0 · 𝑋 ) ↔ 𝑌 ≤ 0 ) )
32 28 31 mtbird ⊢ ( 𝜑 → ¬ 𝑌 ≤ ( 0 · 𝑋 ) )
33 8 9 jca ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
34 omndmnd ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Mnd )
35 6 19 34 3syl ⊢ ( 𝜑 → 𝑊 ∈ Mnd )
36 1 2 5 4 3 isarchi2 ⊢ ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) → ( 𝑊 ∈ Archi ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑥 ) ) ) )
37 36 biimpa ⊢ ( ( ( 𝑊 ∈ Toset ∧ 𝑊 ∈ Mnd ) ∧ 𝑊 ∈ Archi ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑥 ) ) )
38 21 35 7 37 syl21anc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑥 ) ) )
39 breq2 ⊢ ( 𝑥 = 𝑋 → ( 0 < 𝑥 ↔ 0 < 𝑋 ) )
40 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑚 · 𝑥 ) = ( 𝑚 · 𝑋 ) )
41 40 breq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ≤ ( 𝑚 · 𝑥 ) ↔ 𝑦 ≤ ( 𝑚 · 𝑋 ) ) )
42 41 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑥 ) ↔ ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑋 ) ) )
43 39 42 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 0 < 𝑥 → ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑥 ) ) ↔ ( 0 < 𝑋 → ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑋 ) ) ) )
44 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ≤ ( 𝑚 · 𝑋 ) ↔ 𝑌 ≤ ( 𝑚 · 𝑋 ) ) )
45 44 rexbidv ⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑋 ) ↔ ∃ 𝑚 ∈ ℕ 𝑌 ≤ ( 𝑚 · 𝑋 ) ) )
46 45 imbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 0 < 𝑋 → ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑋 ) ) ↔ ( 0 < 𝑋 → ∃ 𝑚 ∈ ℕ 𝑌 ≤ ( 𝑚 · 𝑋 ) ) ) )
47 43 46 rspc2v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 0 < 𝑥 → ∃ 𝑚 ∈ ℕ 𝑦 ≤ ( 𝑚 · 𝑥 ) ) → ( 0 < 𝑋 → ∃ 𝑚 ∈ ℕ 𝑌 ≤ ( 𝑚 · 𝑋 ) ) ) )
48 33 38 10 47 syl3c ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ 𝑌 ≤ ( 𝑚 · 𝑋 ) )
49 13 15 17 32 48 nn0min ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( ¬ 𝑌 ≤ ( 𝑛 · 𝑋 ) ∧ 𝑌 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) )
50 21 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑊 ∈ Toset )
51 23 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑊 ∈ Grp )
52 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
53 52 nn0zd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℤ )
54 8 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
55 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
56 51 53 54 55 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
57 9 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑌 ∈ 𝐵 )
58 1 4 3 tltnle ⊢ ( ( 𝑊 ∈ Toset ∧ ( 𝑛 · 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑛 · 𝑋 ) < 𝑌 ↔ ¬ 𝑌 ≤ ( 𝑛 · 𝑋 ) ) )
59 50 56 57 58 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 · 𝑋 ) < 𝑌 ↔ ¬ 𝑌 ≤ ( 𝑛 · 𝑋 ) ) )
60 59 anbi1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑛 · 𝑋 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) ↔ ( ¬ 𝑌 ≤ ( 𝑛 · 𝑋 ) ∧ 𝑌 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) ) )
61 60 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ0 ( ( 𝑛 · 𝑋 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) ↔ ∃ 𝑛 ∈ ℕ0 ( ¬ 𝑌 ≤ ( 𝑛 · 𝑋 ) ∧ 𝑌 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) ) )
62 49 61 mpbird ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( ( 𝑛 · 𝑋 ) < 𝑌 ∧ 𝑌 ≤ ( ( 𝑛 + 1 ) · 𝑋 ) ) )