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 20 29 30 31 4syl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> W e. Poset )
33 11 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> X e. B )
34 1 5 mulgcl 
 |-  ( ( W e. Grp /\ m e. ZZ /\ U e. B ) -> ( m .x. U ) e. B )
35 22 24 16 34 syl3anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( m .x. U ) e. B )
36 eqid 
 |-  ( -g ` W ) = ( -g ` W )
37 1 36 grpsubcl 
 |-  ( ( W e. Grp /\ X e. B /\ ( m .x. U ) e. B ) -> ( X ( -g ` W ) ( m .x. U ) ) e. B )
38 22 33 35 37 syl3anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( X ( -g ` W ) ( m .x. U ) ) e. B )
39 24 peano2zd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( m + 1 ) e. ZZ )
40 1 5 mulgcl 
 |-  ( ( W e. Grp /\ ( m + 1 ) e. ZZ /\ U e. B ) -> ( ( m + 1 ) .x. U ) e. B )
41 22 39 16 40 syl3anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( m + 1 ) .x. U ) e. B )
42 simprr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> X .<_ ( ( m + 1 ) .x. U ) )
43 1 3 36 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 ) ) )
44 20 33 41 35 42 43 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 ) ) )
45 13 nn0cnd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> m e. CC )
46 1cnd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> 1 e. CC )
47 45 46 pncan2d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( m + 1 ) - m ) = 1 )
48 47 oveq1d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( ( m + 1 ) - m ) .x. U ) = ( 1 .x. U ) )
49 1 5 36 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 ) ) )
50 22 39 24 16 49 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 ) ) )
51 48 50 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 )
52 44 51 breqtrd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( X ( -g ` W ) ( m .x. U ) ) .<_ U )
53 10 3expia 
 |-  ( ( ph /\ x e. B ) -> ( .0. .< x -> U .<_ x ) )
54 53 ralrimiva 
 |-  ( ph -> A. x e. B ( .0. .< x -> U .<_ x ) )
55 54 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> A. x e. B ( .0. .< x -> U .<_ x ) )
56 1 2 36 grpsubid 
 |-  ( ( W e. Grp /\ ( m .x. U ) e. B ) -> ( ( m .x. U ) ( -g ` W ) ( m .x. U ) ) = .0. )
57 22 35 56 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( m .x. U ) ( -g ` W ) ( m .x. U ) ) = .0. )
58 simprl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( m .x. U ) .< X )
59 1 4 36 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 ) ) )
60 20 35 33 35 58 59 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 ) ) )
61 57 60 eqbrtrrd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> .0. .< ( X ( -g ` W ) ( m .x. U ) ) )
62 breq2 
 |-  ( x = ( X ( -g ` W ) ( m .x. U ) ) -> ( .0. .< x <-> .0. .< ( X ( -g ` W ) ( m .x. U ) ) ) )
63 breq2 
 |-  ( x = ( X ( -g ` W ) ( m .x. U ) ) -> ( U .<_ x <-> U .<_ ( X ( -g ` W ) ( m .x. U ) ) ) )
64 62 63 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 ) ) ) ) )
65 64 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 ) ) ) ) )
66 38 55 61 65 syl3c 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> U .<_ ( X ( -g ` W ) ( m .x. U ) ) )
67 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 ) )
68 67 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 )
69 32 38 16 52 66 68 syl32anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( X ( -g ` W ) ( m .x. U ) ) = U )
70 69 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 ) ) )
71 19 27 70 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 ) )
72 1 25 36 grpnpcan 
 |-  ( ( W e. Grp /\ X e. B /\ ( m .x. U ) e. B ) -> ( ( X ( -g ` W ) ( m .x. U ) ) ( +g ` W ) ( m .x. U ) ) = X )
73 22 33 35 72 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 )
74 46 45 addcomd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( 1 + m ) = ( m + 1 ) )
75 74 oveq1d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> ( ( 1 + m ) .x. U ) = ( ( m + 1 ) .x. U ) )
76 71 73 75 3eqtr3d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> X = ( ( m + 1 ) .x. U ) )
77 oveq1 
 |-  ( n = ( m + 1 ) -> ( n .x. U ) = ( ( m + 1 ) .x. U ) )
78 77 rspceeqv 
 |-  ( ( ( m + 1 ) e. NN /\ X = ( ( m + 1 ) .x. U ) ) -> E. n e. NN X = ( n .x. U ) )
79 15 76 78 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( ( m .x. U ) .< X /\ X .<_ ( ( m + 1 ) .x. U ) ) ) -> E. n e. NN X = ( n .x. U ) )
80 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 ) ) )
81 79 80 r19.29a 
 |-  ( ph -> E. n e. NN X = ( n .x. U ) )