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 ) · 𝑋 ) ) )