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 B=BaseW
archirng.0 0˙=0W
archirng.i <˙=<W
archirng.l ˙=W
archirng.x ·˙=W
archirng.1 φWoGrp
archirng.2 φWArchi
archirng.3 φXB
archirng.4 φYB
archirng.5 φ0˙<˙X
archirng.6 φ0˙<˙Y
Assertion archirng φn0n·˙X<˙YY˙n+1·˙X

Proof

Step Hyp Ref Expression
1 archirng.b B=BaseW
2 archirng.0 0˙=0W
3 archirng.i <˙=<W
4 archirng.l ˙=W
5 archirng.x ·˙=W
6 archirng.1 φWoGrp
7 archirng.2 φWArchi
8 archirng.3 φXB
9 archirng.4 φYB
10 archirng.5 φ0˙<˙X
11 archirng.6 φ0˙<˙Y
12 oveq1 m=0m·˙X=0·˙X
13 12 breq2d m=0Y˙m·˙XY˙0·˙X
14 oveq1 m=nm·˙X=n·˙X
15 14 breq2d m=nY˙m·˙XY˙n·˙X
16 oveq1 m=n+1m·˙X=n+1·˙X
17 16 breq2d m=n+1Y˙m·˙XY˙n+1·˙X
18 isogrp WoGrpWGrpWoMnd
19 18 simprbi WoGrpWoMnd
20 omndtos WoMndWToset
21 6 19 20 3syl φWToset
22 ogrpgrp WoGrpWGrp
23 6 22 syl φWGrp
24 1 2 grpidcl WGrp0˙B
25 23 24 syl φ0˙B
26 1 4 3 tltnle WToset0˙BYB0˙<˙Y¬Y˙0˙
27 21 25 9 26 syl3anc φ0˙<˙Y¬Y˙0˙
28 11 27 mpbid φ¬Y˙0˙
29 1 2 5 mulg0 XB0·˙X=0˙
30 8 29 syl φ0·˙X=0˙
31 30 breq2d φY˙0·˙XY˙0˙
32 28 31 mtbird φ¬Y˙0·˙X
33 8 9 jca φXBYB
34 omndmnd WoMndWMnd
35 6 19 34 3syl φWMnd
36 1 2 5 4 3 isarchi2 WTosetWMndWArchixByB0˙<˙xmy˙m·˙x
37 36 biimpa WTosetWMndWArchixByB0˙<˙xmy˙m·˙x
38 21 35 7 37 syl21anc φxByB0˙<˙xmy˙m·˙x
39 breq2 x=X0˙<˙x0˙<˙X
40 oveq2 x=Xm·˙x=m·˙X
41 40 breq2d x=Xy˙m·˙xy˙m·˙X
42 41 rexbidv x=Xmy˙m·˙xmy˙m·˙X
43 39 42 imbi12d x=X0˙<˙xmy˙m·˙x0˙<˙Xmy˙m·˙X
44 breq1 y=Yy˙m·˙XY˙m·˙X
45 44 rexbidv y=Ymy˙m·˙XmY˙m·˙X
46 45 imbi2d y=Y0˙<˙Xmy˙m·˙X0˙<˙XmY˙m·˙X
47 43 46 rspc2v XBYBxByB0˙<˙xmy˙m·˙x0˙<˙XmY˙m·˙X
48 33 38 10 47 syl3c φmY˙m·˙X
49 13 15 17 32 48 nn0min φn0¬Y˙n·˙XY˙n+1·˙X
50 21 adantr φn0WToset
51 23 adantr φn0WGrp
52 simpr φn0n0
53 52 nn0zd φn0n
54 8 adantr φn0XB
55 1 5 mulgcl WGrpnXBn·˙XB
56 51 53 54 55 syl3anc φn0n·˙XB
57 9 adantr φn0YB
58 1 4 3 tltnle WTosetn·˙XBYBn·˙X<˙Y¬Y˙n·˙X
59 50 56 57 58 syl3anc φn0n·˙X<˙Y¬Y˙n·˙X
60 59 anbi1d φn0n·˙X<˙YY˙n+1·˙X¬Y˙n·˙XY˙n+1·˙X
61 60 rexbidva φn0n·˙X<˙YY˙n+1·˙Xn0¬Y˙n·˙XY˙n+1·˙X
62 49 61 mpbird φn0n·˙X<˙YY˙n+1·˙X