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 | |
|
archirng.0 | |
||
archirng.i | |
||
archirng.l | |
||
archirng.x | |
||
archirng.1 | |
||
archirng.2 | |
||
archirng.3 | |
||
archirng.4 | |
||
archirng.5 | |
||
archirng.6 | |
||
Assertion | archirng | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | archirng.b | |
|
2 | archirng.0 | |
|
3 | archirng.i | |
|
4 | archirng.l | |
|
5 | archirng.x | |
|
6 | archirng.1 | |
|
7 | archirng.2 | |
|
8 | archirng.3 | |
|
9 | archirng.4 | |
|
10 | archirng.5 | |
|
11 | archirng.6 | |
|
12 | oveq1 | |
|
13 | 12 | breq2d | |
14 | oveq1 | |
|
15 | 14 | breq2d | |
16 | oveq1 | |
|
17 | 16 | breq2d | |
18 | isogrp | |
|
19 | 18 | simprbi | |
20 | omndtos | |
|
21 | 6 19 20 | 3syl | |
22 | ogrpgrp | |
|
23 | 6 22 | syl | |
24 | 1 2 | grpidcl | |
25 | 23 24 | syl | |
26 | 1 4 3 | tltnle | |
27 | 21 25 9 26 | syl3anc | |
28 | 11 27 | mpbid | |
29 | 1 2 5 | mulg0 | |
30 | 8 29 | syl | |
31 | 30 | breq2d | |
32 | 28 31 | mtbird | |
33 | 8 9 | jca | |
34 | omndmnd | |
|
35 | 6 19 34 | 3syl | |
36 | 1 2 5 4 3 | isarchi2 | |
37 | 36 | biimpa | |
38 | 21 35 7 37 | syl21anc | |
39 | breq2 | |
|
40 | oveq2 | |
|
41 | 40 | breq2d | |
42 | 41 | rexbidv | |
43 | 39 42 | imbi12d | |
44 | breq1 | |
|
45 | 44 | rexbidv | |
46 | 45 | imbi2d | |
47 | 43 46 | rspc2v | |
48 | 33 38 10 47 | syl3c | |
49 | 13 15 17 32 48 | nn0min | |
50 | 21 | adantr | |
51 | 23 | adantr | |
52 | simpr | |
|
53 | 52 | nn0zd | |
54 | 8 | adantr | |
55 | 1 5 | mulgcl | |
56 | 51 53 54 55 | syl3anc | |
57 | 9 | adantr | |
58 | 1 4 3 | tltnle | |
59 | 50 56 57 58 | syl3anc | |
60 | 59 | anbi1d | |
61 | 60 | rexbidva | |
62 | 49 61 | mpbird | |