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 = Base W
archirng.0 0 ˙ = 0 W
archirng.i < ˙ = < W
archirng.l ˙ = W
archirng.x · ˙ = W
archirng.1 φ W oGrp
archirng.2 φ W Archi
archirng.3 φ X B
archirng.4 φ Y B
archirng.5 φ 0 ˙ < ˙ X
archirng.6 φ 0 ˙ < ˙ Y
Assertion archirng φ n 0 n · ˙ X < ˙ Y Y ˙ n + 1 · ˙ X

Proof

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