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. = ( 0g ` W )
archirng.i 
|- .< = ( lt ` W )
archirng.l 
|- .<_ = ( le ` W )
archirng.x 
|- .x. = ( .g ` W )
archirng.1 
|- ( ph -> W e. oGrp )
archirng.2 
|- ( ph -> W e. Archi )
archirng.3 
|- ( ph -> X e. B )
archirng.4 
|- ( ph -> Y e. B )
archirng.5 
|- ( ph -> .0. .< X )
archirng.6 
|- ( ph -> .0. .< Y )
Assertion archirng 
|- ( ph -> E. n e. NN0 ( ( n .x. X ) .< Y /\ Y .<_ ( ( n + 1 ) .x. X ) ) )

Proof

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