Metamath Proof Explorer

Theorem isarchi3

Description: This is the usual definition of the Archimedean property for an ordered group. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses isarchi3.b 
|- B = ( Base ` W )
isarchi3.0 
|- .0. = ( 0g ` W )
isarchi3.i 
|- .< = ( lt ` W )
isarchi3.x 
|- .x. = ( .g ` W )
Assertion isarchi3 
|- ( W e. oGrp -> ( W e. Archi <-> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) ) )

Proof

Step Hyp Ref Expression
1 isarchi3.b 
 |-  B = ( Base ` W )
2 isarchi3.0 
 |-  .0. = ( 0g ` W )
3 isarchi3.i 
 |-  .< = ( lt ` W )
4 isarchi3.x 
 |-  .x. = ( .g ` W )
5 isogrp 
 |-  ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) )
6 5 simprbi 
 |-  ( W e. oGrp -> W e. oMnd )
7 omndtos 
 |-  ( W e. oMnd -> W e. Toset )
8 6 7 syl 
 |-  ( W e. oGrp -> W e. Toset )
9 grpmnd 
 |-  ( W e. Grp -> W e. Mnd )
10 9 adantr 
 |-  ( ( W e. Grp /\ W e. oMnd ) -> W e. Mnd )
11 5 10 sylbi 
 |-  ( W e. oGrp -> W e. Mnd )
12 eqid 
 |-  ( le ` W ) = ( le ` W )
13 1 2 4 12 3 isarchi2 
 |-  ( ( W e. Toset /\ W e. Mnd ) -> ( W e. Archi <-> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y ( le ` W ) ( n .x. x ) ) ) )
14 8 11 13 syl2anc 
 |-  ( W e. oGrp -> ( W e. Archi <-> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y ( le ` W ) ( n .x. x ) ) ) )
15 simpr 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> n e. NN )
16 15 adantr 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> n e. NN )
17 16 peano2nnd 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( n + 1 ) e. NN )
18 simp-4l 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> W e. oGrp )
19 18 adantr 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> W e. oGrp )
20 ogrpgrp 
 |-  ( W e. oGrp -> W e. Grp )
21 1 2 grpidcl 
 |-  ( W e. Grp -> .0. e. B )
22 19 20 21 3syl 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> .0. e. B )
23 simp-4r 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> x e. B )
24 23 adantr 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> x e. B )
25 20 ad4antr 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> W e. Grp )
26 15 nnzd 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> n e. ZZ )
27 1 4 mulgcl 
 |-  ( ( W e. Grp /\ n e. ZZ /\ x e. B ) -> ( n .x. x ) e. B )
28 25 26 23 27 syl3anc 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> ( n .x. x ) e. B )
29 28 adantr 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( n .x. x ) e. B )
30 simpllr 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> .0. .< x )
31 eqid 
 |-  ( +g ` W ) = ( +g ` W )
32 1 3 31 ogrpaddlt 
 |-  ( ( W e. oGrp /\ ( .0. e. B /\ x e. B /\ ( n .x. x ) e. B ) /\ .0. .< x ) -> ( .0. ( +g ` W ) ( n .x. x ) ) .< ( x ( +g ` W ) ( n .x. x ) ) )
33 19 22 24 29 30 32 syl131anc 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( .0. ( +g ` W ) ( n .x. x ) ) .< ( x ( +g ` W ) ( n .x. x ) ) )
34 19 20 syl 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> W e. Grp )
35 1 31 2 grplid 
 |-  ( ( W e. Grp /\ ( n .x. x ) e. B ) -> ( .0. ( +g ` W ) ( n .x. x ) ) = ( n .x. x ) )
36 34 29 35 syl2anc 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( .0. ( +g ` W ) ( n .x. x ) ) = ( n .x. x ) )
37 nncn 
 |-  ( n e. NN -> n e. CC )
38 ax-1cn 
 |-  1 e. CC
39 addcom 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( n + 1 ) = ( 1 + n ) )
40 37 38 39 sylancl 
 |-  ( n e. NN -> ( n + 1 ) = ( 1 + n ) )
41 40 oveq1d 
 |-  ( n e. NN -> ( ( n + 1 ) .x. x ) = ( ( 1 + n ) .x. x ) )
42 16 41 syl 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( ( n + 1 ) .x. x ) = ( ( 1 + n ) .x. x ) )
43 grpsgrp 
 |-  ( W e. Grp -> W e. Smgrp )
44 19 20 43 3syl 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> W e. Smgrp )
45 1nn 
 |-  1 e. NN
46 45 a1i 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> 1 e. NN )
47 1 4 31 mulgnndir 
 |-  ( ( W e. Smgrp /\ ( 1 e. NN /\ n e. NN /\ x e. B ) ) -> ( ( 1 + n ) .x. x ) = ( ( 1 .x. x ) ( +g ` W ) ( n .x. x ) ) )
48 44 46 16 24 47 syl13anc 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( ( 1 + n ) .x. x ) = ( ( 1 .x. x ) ( +g ` W ) ( n .x. x ) ) )
49 1 4 mulg1 
 |-  ( x e. B -> ( 1 .x. x ) = x )
50 24 49 syl 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( 1 .x. x ) = x )
51 50 oveq1d 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( ( 1 .x. x ) ( +g ` W ) ( n .x. x ) ) = ( x ( +g ` W ) ( n .x. x ) ) )
52 42 48 51 3eqtrrd 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( x ( +g ` W ) ( n .x. x ) ) = ( ( n + 1 ) .x. x ) )
53 33 36 52 3brtr3d 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> ( n .x. x ) .< ( ( n + 1 ) .x. x ) )
54 tospos 
 |-  ( W e. Toset -> W e. Poset )
55 18 8 54 3syl 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> W e. Poset )
56 simpllr 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> y e. B )
57 26 peano2zd 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> ( n + 1 ) e. ZZ )
58 1 4 mulgcl 
 |-  ( ( W e. Grp /\ ( n + 1 ) e. ZZ /\ x e. B ) -> ( ( n + 1 ) .x. x ) e. B )
59 25 57 23 58 syl3anc 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> ( ( n + 1 ) .x. x ) e. B )
60 1 12 3 plelttr 
 |-  ( ( W e. Poset /\ ( y e. B /\ ( n .x. x ) e. B /\ ( ( n + 1 ) .x. x ) e. B ) ) -> ( ( y ( le ` W ) ( n .x. x ) /\ ( n .x. x ) .< ( ( n + 1 ) .x. x ) ) -> y .< ( ( n + 1 ) .x. x ) ) )
61 55 56 28 59 60 syl13anc 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> ( ( y ( le ` W ) ( n .x. x ) /\ ( n .x. x ) .< ( ( n + 1 ) .x. x ) ) -> y .< ( ( n + 1 ) .x. x ) ) )
62 61 impl 
 |-  ( ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) /\ ( n .x. x ) .< ( ( n + 1 ) .x. x ) ) -> y .< ( ( n + 1 ) .x. x ) )
63 53 62 mpdan 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> y .< ( ( n + 1 ) .x. x ) )
64 oveq1 
 |-  ( m = ( n + 1 ) -> ( m .x. x ) = ( ( n + 1 ) .x. x ) )
65 64 breq2d 
 |-  ( m = ( n + 1 ) -> ( y .< ( m .x. x ) <-> y .< ( ( n + 1 ) .x. x ) ) )
66 65 rspcev 
 |-  ( ( ( n + 1 ) e. NN /\ y .< ( ( n + 1 ) .x. x ) ) -> E. m e. NN y .< ( m .x. x ) )
67 17 63 66 syl2anc 
 |-  ( ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) /\ y ( le ` W ) ( n .x. x ) ) -> E. m e. NN y .< ( m .x. x ) )
68 67 r19.29an 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ E. n e. NN y ( le ` W ) ( n .x. x ) ) -> E. m e. NN y .< ( m .x. x ) )
69 oveq1 
 |-  ( m = n -> ( m .x. x ) = ( n .x. x ) )
70 69 breq2d 
 |-  ( m = n -> ( y .< ( m .x. x ) <-> y .< ( n .x. x ) ) )
71 70 cbvrexvw 
 |-  ( E. m e. NN y .< ( m .x. x ) <-> E. n e. NN y .< ( n .x. x ) )
72 68 71 sylib 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ E. n e. NN y ( le ` W ) ( n .x. x ) ) -> E. n e. NN y .< ( n .x. x ) )
73 12 3 pltle 
 |-  ( ( W e. oGrp /\ y e. B /\ ( n .x. x ) e. B ) -> ( y .< ( n .x. x ) -> y ( le ` W ) ( n .x. x ) ) )
74 18 56 28 73 syl3anc 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ n e. NN ) -> ( y .< ( n .x. x ) -> y ( le ` W ) ( n .x. x ) ) )
75 74 reximdva 
 |-  ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) -> ( E. n e. NN y .< ( n .x. x ) -> E. n e. NN y ( le ` W ) ( n .x. x ) ) )
76 75 imp 
 |-  ( ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) /\ E. n e. NN y .< ( n .x. x ) ) -> E. n e. NN y ( le ` W ) ( n .x. x ) )
77 72 76 impbida 
 |-  ( ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) /\ .0. .< x ) -> ( E. n e. NN y ( le ` W ) ( n .x. x ) <-> E. n e. NN y .< ( n .x. x ) ) )
78 77 pm5.74da 
 |-  ( ( ( W e. oGrp /\ x e. B ) /\ y e. B ) -> ( ( .0. .< x -> E. n e. NN y ( le ` W ) ( n .x. x ) ) <-> ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) ) )
79 78 ralbidva 
 |-  ( ( W e. oGrp /\ x e. B ) -> ( A. y e. B ( .0. .< x -> E. n e. NN y ( le ` W ) ( n .x. x ) ) <-> A. y e. B ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) ) )
80 79 ralbidva 
 |-  ( W e. oGrp -> ( A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y ( le ` W ) ( n .x. x ) ) <-> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) ) )
81 14 80 bitrd 
 |-  ( W e. oGrp -> ( W e. Archi <-> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .< ( n .x. x ) ) ) )