Metamath Proof Explorer

Theorem archiabllem1a

Description: Lemma for archiabl : In case an archimedean group W admits a smallest positive element U , then any positive element X of W can be written as ( n .x. U ) with n e. NN . Since the reciprocal holds for negative elements, W is then isomorphic to ZZ . (Contributed by Thierry Arnoux, 12-Apr-2018)

Ref Expression
Hypotheses archiabllem.b 
|- B = ( Base ` W )
archiabllem.0 
|- .0. = ( 0g ` W )
archiabllem.e 
|- .<_ = ( le ` W )
archiabllem.t 
|- .< = ( lt ` W )
archiabllem.m 
|- .x. = ( .g ` W )
archiabllem.g 
|- ( ph -> W e. oGrp )
archiabllem.a 
|- ( ph -> W e. Archi )
archiabllem1.u 
|- ( ph -> U e. B )
archiabllem1.p 
|- ( ph -> .0. .< U )
archiabllem1.s 
|- ( ( ph /\ x e. B /\ .0. .< x ) -> U .<_ x )
archiabllem1a.x 
|- ( ph -> X e. B )
archiabllem1a.c 
|- ( ph -> .0. .< X )
Assertion archiabllem1a 
|- ( ph -> E. n e. NN X = ( n .x. U ) )

Proof

Step Hyp Ref Expression
1 archiabllem.b 
 |-  B = ( Base ` W )
2 archiabllem.0 
 |-  .0. = ( 0g ` W )
3 archiabllem.e 
 |-  .<_ = ( le ` W )
4 archiabllem.t 
 |-  .< = ( lt ` W )
5 archiabllem.m 
 |-  .x. = ( .g ` W )
6 archiabllem.g 
 |-  ( ph -> W e. oGrp )
7 archiabllem.a 
 |-  ( ph -> W e. Archi )
8 archiabllem1.u 
 |-  ( ph -> U e. B )
9 archiabllem1.p 
 |-  ( ph -> .0. .< U )
10 archiabllem1.s 
 |-  ( ( ph /\ x e. B /\ .0. .< x ) -> U .<_ x )
11 archiabllem1a.x 
 |-  ( ph -> X e. B )
12 archiabllem1a.c 
 |-  ( ph -> .0. .< X )
13 simplr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> m e. NN0 )
14 nn0p1nn 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN )
15 13 14 syl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( m + 1 ) e. NN )
16 8 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> U e. B )
17 1 5 mulg1 
 |-  ( U e. B -> ( 1 .x. U ) = U )
18 16 17 syl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( 1 .x. U ) = U )
19 18 oveq1d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( 1 .x. U ) ( +g ` W ) ( m .x. U ) ) = ( U ( +g ` W ) ( m .x. U ) ) )
20 6 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> W e. oGrp )
21 ogrpgrp 
 |-  ( W e. oGrp -> W e. Grp )
22 20 21 syl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> W e. Grp )
23 1zzd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> 1 e. ZZ )
24 13 nn0zd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> m e. ZZ )
25 eqid 
 |-  ( +g ` W ) = ( +g ` W )
26 1 5 25 mulgdir 
 |-  ( ( W e. Grp /\ ( 1 e. ZZ /\ m e. ZZ /\ U e. B ) ) -> ( ( 1 + m ) .x. U ) = ( ( 1 .x. U ) ( +g ` W ) ( m .x. U ) ) )
27 22 23 24 16 26 syl13anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( 1 + m ) .x. U ) = ( ( 1 .x. U ) ( +g ` W ) ( m .x. U ) ) )
28 isogrp 
 |-  ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) )
29 28 simprbi 
 |-  ( W e. oGrp -> W e. oMnd )
30 omndtos 
 |-  ( W e. oMnd -> W e. Toset )
31 tospos 
 |-  ( W e. Toset -> W e. Poset )
32 29 30 31 3syl 
 |-  ( W e. oGrp -> W e. Poset )
33 20 32 syl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> W e. Poset )
34 11 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> X e. B )
35 1 5 mulgcl 
 |-  ( ( W e. Grp /\ m e. ZZ /\ U e. B ) -> ( m .x. U ) e. B )
36 22 24 16 35 syl3anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( m .x. U ) e. B )
37 eqid 
 |-  ( -g ` W ) = ( -g ` W )
38 1 37 grpsubcl 
 |-  ( ( W e. Grp /\ X e. B /\ ( m .x. U ) e. B ) -> ( X ( -g ` W ) ( m .x. U ) ) e. B )
39 22 34 36 38 syl3anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( X ( -g ` W ) ( m .x. U ) ) e. B )
40 24 peano2zd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( m + 1 ) e. ZZ )
41 1 5 mulgcl 
 |-  ( ( W e. Grp /\ ( m + 1 ) e. ZZ /\ U e. B ) -> ( ( m + 1 ) .x. U ) e. B )
42 22 40 16 41 syl3anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( m + 1 ) .x. U ) e. B )
43 simprr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> X .<_ ( ( m + 1 ) .x. U ) )
44 1 3 37 ogrpsub 
 |-  ( ( W e. oGrp /\ ( X e. B /\ ( ( m + 1 ) .x. U ) e. B /\ ( m .x. U ) e. B ) /\ X .<_ ( ( m + 1 ) .x. U ) ) -> ( X ( -g ` W ) ( m .x. U ) ) .<_ ( ( ( m + 1 ) .x. U ) ( -g ` W ) ( m .x. U ) ) )
45 20 34 42 36 43 44 syl131anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( X ( -g ` W ) ( m .x. U ) ) .<_ ( ( ( m + 1 ) .x. U ) ( -g ` W ) ( m .x. U ) ) )
46 13 nn0cnd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> m e. CC )
47 1cnd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> 1 e. CC )
48 46 47 pncan2d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( m + 1 ) - m ) = 1 )
49 48 oveq1d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( ( m + 1 ) - m ) .x. U ) = ( 1 .x. U ) )
50 1 5 37 mulgsubdir 
 |-  ( ( W e. Grp /\ ( ( m + 1 ) e. ZZ /\ m e. ZZ /\ U e. B ) ) -> ( ( ( m + 1 ) - m ) .x. U ) = ( ( ( m + 1 ) .x. U ) ( -g ` W ) ( m .x. U ) ) )
51 22 40 24 16 50 syl13anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( ( m + 1 ) - m ) .x. U ) = ( ( ( m + 1 ) .x. U ) ( -g ` W ) ( m .x. U ) ) )
52 49 51 18 3eqtr3d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( ( m + 1 ) .x. U ) ( -g ` W ) ( m .x. U ) ) = U )
53 45 52 breqtrd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( X ( -g ` W ) ( m .x. U ) ) .<_ U )
54 10 3expia 
 |-  ( ( ph /\ x e. B ) -> ( .0. .< x -> U .<_ x ) )
55 54 ralrimiva 
 |-  ( ph -> A. x e. B ( .0. .< x -> U .<_ x ) )
56 55 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> A. x e. B ( .0. .< x -> U .<_ x ) )
57 1 2 37 grpsubid 
 |-  ( ( W e. Grp /\ ( m .x. U ) e. B ) -> ( ( m .x. U ) ( -g ` W ) ( m .x. U ) ) = .0. )
58 22 36 57 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( m .x. U ) ( -g ` W ) ( m .x. U ) ) = .0. )
59 simprl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( m .x. U ) .< X )
60 1 4 37 ogrpsublt 
 |-  ( ( W e. oGrp /\ ( ( m .x. U ) e. B /\ X e. B /\ ( m .x. U ) e. B ) /\ ( m .x. U ) .< X ) -> ( ( m .x. U ) ( -g ` W ) ( m .x. U ) ) .< ( X ( -g ` W ) ( m .x. U ) ) )
61 20 36 34 36 59 60 syl131anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( m .x. U ) ( -g ` W ) ( m .x. U ) ) .< ( X ( -g ` W ) ( m .x. U ) ) )
62 58 61 eqbrtrrd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> .0. .< ( X ( -g ` W ) ( m .x. U ) ) )
63 breq2 
 |-  ( x = ( X ( -g ` W ) ( m .x. U ) ) -> ( .0. .< x <-> .0. .< ( X ( -g ` W ) ( m .x. U ) ) ) )
64 breq2 
 |-  ( x = ( X ( -g ` W ) ( m .x. U ) ) -> ( U .<_ x <-> U .<_ ( X ( -g ` W ) ( m .x. U ) ) ) )
65 63 64 imbi12d 
 |-  ( x = ( X ( -g ` W ) ( m .x. U ) ) -> ( ( .0. .< x -> U .<_ x ) <-> ( .0. .< ( X ( -g ` W ) ( m .x. U ) ) -> U .<_ ( X ( -g ` W ) ( m .x. U ) ) ) ) )
66 65 rspcv 
 |-  ( ( X ( -g ` W ) ( m .x. U ) ) e. B -> ( A. x e. B ( .0. .< x -> U .<_ x ) -> ( .0. .< ( X ( -g ` W ) ( m .x. U ) ) -> U .<_ ( X ( -g ` W ) ( m .x. U ) ) ) ) )
67 39 56 62 66 syl3c 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> U .<_ ( X ( -g ` W ) ( m .x. U ) ) )
68 1 3 posasymb 
 |-  ( ( W e. Poset /\ ( X ( -g ` W ) ( m .x. U ) ) e. B /\ U e. B ) -> ( ( ( X ( -g ` W ) ( m .x. U ) ) .<_ U /\ U .<_ ( X ( -g ` W ) ( m .x. U ) ) ) <-> ( X ( -g ` W ) ( m .x. U ) ) = U ) )
69 68 biimpa 
 |-  ( ( ( W e. Poset /\ ( X ( -g ` W ) ( m .x. U ) ) e. B /\ U e. B ) /\ ( ( X ( -g ` W ) ( m .x. U ) ) .<_ U /\ U .<_ ( X ( -g ` W ) ( m .x. U ) ) ) ) -> ( X ( -g ` W ) ( m .x. U ) ) = U )
70 33 39 16 53 67 69 syl32anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( X ( -g ` W ) ( m .x. U ) ) = U )
71 70 oveq1d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( X ( -g ` W ) ( m .x. U ) ) ( +g ` W ) ( m .x. U ) ) = ( U ( +g ` W ) ( m .x. U ) ) )
72 19 27 71 3eqtr4rd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( X ( -g ` W ) ( m .x. U ) ) ( +g ` W ) ( m .x. U ) ) = ( ( 1 + m ) .x. U ) )
73 1 25 37 grpnpcan 
 |-  ( ( W e. Grp /\ X e. B /\ ( m .x. U ) e. B ) -> ( ( X ( -g ` W ) ( m .x. U ) ) ( +g ` W ) ( m .x. U ) ) = X )
74 22 34 36 73 syl3anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( X ( -g ` W ) ( m .x. U ) ) ( +g ` W ) ( m .x. U ) ) = X )
75 47 46 addcomd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( 1 + m ) = ( m + 1 ) )
76 75 oveq1d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( 1 + m ) .x. U ) = ( ( m + 1 ) .x. U ) )
77 72 74 76 3eqtr3d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> X = ( ( m + 1 ) .x. U ) )
78 oveq1 
 |-  ( n = ( m + 1 ) -> ( n .x. U ) = ( ( m + 1 ) .x. U ) )
79 78 rspceeqv 
 |-  ( ( ( m + 1 ) e. NN /\ X = ( ( m + 1 ) .x. U ) ) -> E. n e. NN X = ( n .x. U ) )
80 15 77 79 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> E. n e. NN X = ( n .x. U ) )
81 1 2 4 3 5 6 7 8 11 9 12 archirng 
 |-  ( ph -> E. m e. NN0 ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) )
82 80 81 r19.29a 
 |-  ( ph -> E. n e. NN X = ( n .x. U ) )