Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  archirngz Structured version   Unicode version

Theorem archirngz 28498
Description: Property of Archimedean left and right ordered groups. (Contributed by Thierry Arnoux, 6-May-2018.)
Hypotheses
Ref Expression
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 )
archirngz.1  |-  ( ph  ->  (oppg
`  W )  e. oGrp
)
Assertion
Ref Expression
archirngz  |-  ( ph  ->  E. n  e.  ZZ  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
Distinct variable groups:    n, X    n, Y    ph, n    .0. , n    .<_ , n    .< , n    .x. , n
Allowed substitution hints:    B( n)    W( n)

Proof of Theorem archirngz
Dummy variable  m is distinct from all other variables.
StepHypRef Expression
1 neg1z 10973 . . 3  |-  -u 1  e.  ZZ
2 archirng.1 . . . . . . . . . 10  |-  ( ph  ->  W  e. oGrp )
3 ogrpgrp 28458 . . . . . . . . . 10  |-  ( W  e. oGrp  ->  W  e.  Grp )
42, 3syl 17 . . . . . . . . 9  |-  ( ph  ->  W  e.  Grp )
5 1zzd 10968 . . . . . . . . 9  |-  ( ph  ->  1  e.  ZZ )
6 archirng.3 . . . . . . . . 9  |-  ( ph  ->  X  e.  B )
7 archirng.b . . . . . . . . . 10  |-  B  =  ( Base `  W
)
8 archirng.x . . . . . . . . . 10  |-  .x.  =  (.g
`  W )
9 eqid 2422 . . . . . . . . . 10  |-  ( invg `  W )  =  ( invg `  W )
107, 8, 9mulgneg 16761 . . . . . . . . 9  |-  ( ( W  e.  Grp  /\  1  e.  ZZ  /\  X  e.  B )  ->  ( -u 1  .x.  X )  =  ( ( invg `  W ) `
 ( 1  .x. 
X ) ) )
114, 5, 6, 10syl3anc 1264 . . . . . . . 8  |-  ( ph  ->  ( -u 1  .x. 
X )  =  ( ( invg `  W ) `  (
1  .x.  X )
) )
127, 8mulg1 16750 . . . . . . . . . 10  |-  ( X  e.  B  ->  (
1  .x.  X )  =  X )
136, 12syl 17 . . . . . . . . 9  |-  ( ph  ->  ( 1  .x.  X
)  =  X )
1413fveq2d 5881 . . . . . . . 8  |-  ( ph  ->  ( ( invg `  W ) `  (
1  .x.  X )
)  =  ( ( invg `  W
) `  X )
)
1511, 14eqtrd 2463 . . . . . . 7  |-  ( ph  ->  ( -u 1  .x. 
X )  =  ( ( invg `  W ) `  X
) )
16 archirng.5 . . . . . . . 8  |-  ( ph  ->  .0.  .<  X )
17 archirng.i . . . . . . . . . 10  |-  .<  =  ( lt `  W )
18 archirng.0 . . . . . . . . . 10  |-  .0.  =  ( 0g `  W )
197, 17, 9, 18ogrpinv0lt 28478 . . . . . . . . 9  |-  ( ( W  e. oGrp  /\  X  e.  B )  ->  (  .0.  .<  X  <->  ( ( invg `  W ) `
 X )  .<  .0.  ) )
2019biimpa 486 . . . . . . . 8  |-  ( ( ( W  e. oGrp  /\  X  e.  B )  /\  .0.  .<  X )  ->  ( ( invg `  W ) `  X
)  .<  .0.  )
212, 6, 16, 20syl21anc 1263 . . . . . . 7  |-  ( ph  ->  ( ( invg `  W ) `  X
)  .<  .0.  )
2215, 21eqbrtrd 4441 . . . . . 6  |-  ( ph  ->  ( -u 1  .x. 
X )  .<  .0.  )
2322adantr 466 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( -u
1  .x.  X )  .<  .0.  )
24 simpr 462 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  Y  =  .0.  )
2523, 24breqtrrd 4447 . . . 4  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( -u
1  .x.  X )  .<  Y )
26 isogrp 28457 . . . . . . . . . 10  |-  ( W  e. oGrp 
<->  ( W  e.  Grp  /\  W  e. oMnd ) )
2726simprbi 465 . . . . . . . . 9  |-  ( W  e. oGrp  ->  W  e. oMnd )
28 omndtos 28460 . . . . . . . . 9  |-  ( W  e. oMnd  ->  W  e. Toset )
292, 27, 283syl 18 . . . . . . . 8  |-  ( ph  ->  W  e. Toset )
30 tospos 28411 . . . . . . . 8  |-  ( W  e. Toset  ->  W  e.  Poset )
3129, 30syl 17 . . . . . . 7  |-  ( ph  ->  W  e.  Poset )
327, 18grpidcl 16679 . . . . . . . 8  |-  ( W  e.  Grp  ->  .0.  e.  B )
332, 3, 323syl 18 . . . . . . 7  |-  ( ph  ->  .0.  e.  B )
34 archirng.l . . . . . . . 8  |-  .<_  =  ( le `  W )
357, 34posref 16181 . . . . . . 7  |-  ( ( W  e.  Poset  /\  .0.  e.  B )  ->  .0.  .<_  .0.  )
3631, 33, 35syl2anc 665 . . . . . 6  |-  ( ph  ->  .0.  .<_  .0.  )
3736adantr 466 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  .0.  .<_  .0.  )
38 1m1e0 10678 . . . . . . . . . 10  |-  ( 1  -  1 )  =  0
3938negeqi 9868 . . . . . . . . 9  |-  -u (
1  -  1 )  =  -u 0
40 ax-1cn 9597 . . . . . . . . . 10  |-  1  e.  CC
4140, 40negsubdii 9960 . . . . . . . . 9  |-  -u (
1  -  1 )  =  ( -u 1  +  1 )
42 neg0 9920 . . . . . . . . 9  |-  -u 0  =  0
4339, 41, 423eqtr3i 2459 . . . . . . . 8  |-  ( -u
1  +  1 )  =  0
4443oveq1i 6311 . . . . . . 7  |-  ( (
-u 1  +  1 )  .x.  X )  =  ( 0  .x. 
X )
457, 18, 8mulg0 16748 . . . . . . . 8  |-  ( X  e.  B  ->  (
0  .x.  X )  =  .0.  )
466, 45syl 17 . . . . . . 7  |-  ( ph  ->  ( 0  .x.  X
)  =  .0.  )
4744, 46syl5eq 2475 . . . . . 6  |-  ( ph  ->  ( ( -u 1  +  1 )  .x.  X )  =  .0.  )
4847adantr 466 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( (
-u 1  +  1 )  .x.  X )  =  .0.  )
4937, 24, 483brtr4d 4451 . . . 4  |-  ( (
ph  /\  Y  =  .0.  )  ->  Y  .<_  ( ( -u 1  +  1 )  .x.  X
) )
5025, 49jca 534 . . 3  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( (
-u 1  .x.  X
)  .<  Y  /\  Y  .<_  ( ( -u 1  +  1 )  .x.  X ) ) )
51 oveq1 6308 . . . . . 6  |-  ( n  =  -u 1  ->  (
n  .x.  X )  =  ( -u 1  .x.  X ) )
5251breq1d 4430 . . . . 5  |-  ( n  =  -u 1  ->  (
( n  .x.  X
)  .<  Y  <->  ( -u 1  .x.  X )  .<  Y ) )
53 oveq1 6308 . . . . . . 7  |-  ( n  =  -u 1  ->  (
n  +  1 )  =  ( -u 1  +  1 ) )
5453oveq1d 6316 . . . . . 6  |-  ( n  =  -u 1  ->  (
( n  +  1 )  .x.  X )  =  ( ( -u
1  +  1 ) 
.x.  X ) )
5554breq2d 4432 . . . . 5  |-  ( n  =  -u 1  ->  ( Y  .<_  ( ( n  +  1 )  .x.  X )  <->  Y  .<_  ( ( -u 1  +  1 )  .x.  X
) ) )
5652, 55anbi12d 715 . . . 4  |-  ( n  =  -u 1  ->  (
( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) )  <->  ( ( -u 1  .x.  X ) 
.<  Y  /\  Y  .<_  ( ( -u 1  +  1 )  .x.  X
) ) ) )
5756rspcev 3182 . . 3  |-  ( (
-u 1  e.  ZZ  /\  ( ( -u 1  .x.  X )  .<  Y  /\  Y  .<_  ( ( -u
1  +  1 ) 
.x.  X ) ) )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) )
581, 50, 57sylancr 667 . 2  |-  ( (
ph  /\  Y  =  .0.  )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) )
59 simpr 462 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  m  e.  NN0 )
6059nn0zd 11038 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  m  e.  ZZ )
6160ad2antrr 730 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  m  e.  ZZ )
6261znegcld 11042 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  -u m  e.  ZZ )
63 2z 10969 . . . . . . 7  |-  2  e.  ZZ
6463a1i 11 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  2  e.  ZZ )
6562, 64zsubcld 11045 . . . . 5  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( -u m  -  2 )  e.  ZZ )
66 nn0cn 10879 . . . . . . . . . . 11  |-  ( m  e.  NN0  ->  m  e.  CC )
6766adantl 467 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  m  e.  CC )
68 2cnd 10682 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  2  e.  CC )
6967, 68negdi2d 10000 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u (
m  +  2 )  =  ( -u m  -  2 ) )
7069oveq1d 6316 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  .x.  X )  =  ( ( -u m  -  2 ) 
.x.  X ) )
712ad2antrr 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e. oGrp )
72 archirngz.1 . . . . . . . . . . . 12  |-  ( ph  ->  (oppg
`  W )  e. oGrp
)
7372ad2antrr 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (oppg `  W
)  e. oGrp )
7471, 73jca 534 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( W  e. oGrp  /\  (oppg `  W
)  e. oGrp ) )
754ad2antrr 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e.  Grp )
7660peano2zd 11043 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  1 )  e.  ZZ )
776ad2antrr 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  X  e.  B )
787, 8mulgcl 16760 . . . . . . . . . . 11  |-  ( ( W  e.  Grp  /\  ( m  +  1
)  e.  ZZ  /\  X  e.  B )  ->  ( ( m  + 
1 )  .x.  X
)  e.  B )
7975, 76, 77, 78syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  1 )  .x.  X )  e.  B )
8063a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  2  e.  ZZ )
8160, 80zaddcld 11044 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  2 )  e.  ZZ )
827, 8mulgcl 16760 . . . . . . . . . . 11  |-  ( ( W  e.  Grp  /\  ( m  +  2
)  e.  ZZ  /\  X  e.  B )  ->  ( ( m  + 
2 )  .x.  X
)  e.  B )
8375, 81, 77, 82syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  2 )  .x.  X )  e.  B )
8475, 32syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  .0.  e.  B )
8516ad2antrr 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  .0.  .<  X )
86 eqid 2422 . . . . . . . . . . . . 13  |-  ( +g  `  W )  =  ( +g  `  W )
877, 17, 86ogrpaddlt 28473 . . . . . . . . . . . 12  |-  ( ( W  e. oGrp  /\  (  .0.  e.  B  /\  X  e.  B  /\  (
( m  +  1 )  .x.  X )  e.  B )  /\  .0.  .<  X )  -> 
(  .0.  ( +g  `  W ) ( ( m  +  1 ) 
.x.  X ) ) 
.<  ( X ( +g  `  W ) ( ( m  +  1 ) 
.x.  X ) ) )
8871, 84, 77, 79, 85, 87syl131anc 1277 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (  .0.  ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  .< 
( X ( +g  `  W ) ( ( m  +  1 ) 
.x.  X ) ) )
897, 86, 18grplid 16681 . . . . . . . . . . . 12  |-  ( ( W  e.  Grp  /\  ( ( m  + 
1 )  .x.  X
)  e.  B )  ->  (  .0.  ( +g  `  W ) ( ( m  +  1 )  .x.  X ) )  =  ( ( m  +  1 ) 
.x.  X ) )
9075, 79, 89syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (  .0.  ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  =  ( ( m  + 
1 )  .x.  X
) )
91 1cnd 9659 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  NN0  ->  1  e.  CC )
9266, 91, 91addassd 9665 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN0  ->  ( ( m  +  1 )  +  1 )  =  ( m  +  ( 1  +  1 ) ) )
93 1p1e2 10723 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  1 )  =  2
9493oveq2i 6312 . . . . . . . . . . . . . . . 16  |-  ( m  +  ( 1  +  1 ) )  =  ( m  +  2 )
9592, 94syl6eq 2479 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( ( m  +  1 )  +  1 )  =  ( m  +  2 ) )
9666, 91addcld 9662 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN0  ->  ( m  +  1 )  e.  CC )
9796, 91addcomd 9835 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( ( m  +  1 )  +  1 )  =  ( 1  +  ( m  +  1 ) ) )
9895, 97eqtr3d 2465 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( m  +  2 )  =  ( 1  +  ( m  +  1 ) ) )
9998oveq1d 6316 . . . . . . . . . . . . 13  |-  ( m  e.  NN0  ->  ( ( m  +  2 ) 
.x.  X )  =  ( ( 1  +  ( m  +  1 ) )  .x.  X
) )
10099adantl 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  2 )  .x.  X )  =  ( ( 1  +  ( m  + 
1 ) )  .x.  X ) )
101 1zzd 10968 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  1  e.  ZZ )
1027, 8, 86mulgdir 16768 . . . . . . . . . . . . 13  |-  ( ( W  e.  Grp  /\  ( 1  e.  ZZ  /\  ( m  +  1 )  e.  ZZ  /\  X  e.  B )
)  ->  ( (
1  +  ( m  +  1 ) ) 
.x.  X )  =  ( ( 1  .x. 
X ) ( +g  `  W ) ( ( m  +  1 ) 
.x.  X ) ) )
10375, 101, 76, 77, 102syl13anc 1266 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( 1  +  ( m  +  1 ) )  .x.  X )  =  ( ( 1 
.x.  X ) ( +g  `  W ) ( ( m  + 
1 )  .x.  X
) ) )
10477, 12syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
1  .x.  X )  =  X )
105104oveq1d 6316 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( 1  .x.  X
) ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  =  ( X ( +g  `  W ) ( ( m  +  1 ) 
.x.  X ) ) )
106100, 103, 1053eqtrrd 2468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( X ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  =  ( ( m  + 
2 )  .x.  X
) )
10788, 90, 1063brtr3d 4450 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  1 )  .x.  X ) 
.<  ( ( m  + 
2 )  .x.  X
) )
1087, 17, 9ogrpinvlt 28479 . . . . . . . . . . 11  |-  ( ( ( W  e. oGrp  /\  (oppg `  W )  e. oGrp )  /\  ( ( m  + 
1 )  .x.  X
)  e.  B  /\  ( ( m  + 
2 )  .x.  X
)  e.  B )  ->  ( ( ( m  +  1 ) 
.x.  X )  .< 
( ( m  + 
2 )  .x.  X
)  <->  ( ( invg `  W ) `
 ( ( m  +  2 )  .x.  X ) )  .< 
( ( invg `  W ) `  (
( m  +  1 )  .x.  X ) ) ) )
109108biimpa 486 . . . . . . . . . 10  |-  ( ( ( ( W  e. oGrp  /\  (oppg
`  W )  e. oGrp
)  /\  ( (
m  +  1 ) 
.x.  X )  e.  B  /\  ( ( m  +  2 ) 
.x.  X )  e.  B )  /\  (
( m  +  1 )  .x.  X ) 
.<  ( ( m  + 
2 )  .x.  X
) )  ->  (
( invg `  W ) `  (
( m  +  2 )  .x.  X ) )  .<  ( ( invg `  W ) `
 ( ( m  +  1 )  .x.  X ) ) )
11074, 79, 83, 107, 109syl31anc 1267 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( invg `  W ) `  (
( m  +  2 )  .x.  X ) )  .<  ( ( invg `  W ) `
 ( ( m  +  1 )  .x.  X ) ) )
1117, 8, 9mulgneg 16761 . . . . . . . . . 10  |-  ( ( W  e.  Grp  /\  ( m  +  2
)  e.  ZZ  /\  X  e.  B )  ->  ( -u ( m  +  2 )  .x.  X )  =  ( ( invg `  W ) `  (
( m  +  2 )  .x.  X ) ) )
11275, 81, 77, 111syl3anc 1264 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  .x.  X )  =  ( ( invg `  W ) `
 ( ( m  +  2 )  .x.  X ) ) )
1137, 8, 9mulgneg 16761 . . . . . . . . . 10  |-  ( ( W  e.  Grp  /\  ( m  +  1
)  e.  ZZ  /\  X  e.  B )  ->  ( -u ( m  +  1 )  .x.  X )  =  ( ( invg `  W ) `  (
( m  +  1 )  .x.  X ) ) )
11475, 76, 77, 113syl3anc 1264 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  1 )  .x.  X )  =  ( ( invg `  W ) `
 ( ( m  +  1 )  .x.  X ) ) )
115110, 112, 1143brtr4d 4451 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  .x.  X ) 
.<  ( -u ( m  +  1 )  .x.  X ) )
11670, 115eqbrtrrd 4443 . . . . . . 7  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u m  -  2 )  .x.  X ) 
.<  ( -u ( m  +  1 )  .x.  X ) )
117116ad2antrr 730 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( ( -u m  -  2 ) 
.x.  X )  .< 
( -u ( m  + 
1 )  .x.  X
) )
118114ad2antrr 730 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( -u (
m  +  1 ) 
.x.  X )  =  ( ( invg `  W ) `  (
( m  +  1 )  .x.  X ) ) )
11931ad4antr 736 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  W  e.  Poset )
120 archirng.4 . . . . . . . . . . . 12  |-  ( ph  ->  Y  e.  B )
1217, 9grpinvcl 16696 . . . . . . . . . . . 12  |-  ( ( W  e.  Grp  /\  Y  e.  B )  ->  ( ( invg `  W ) `  Y
)  e.  B )
1224, 120, 121syl2anc 665 . . . . . . . . . . 11  |-  ( ph  ->  ( ( invg `  W ) `  Y
)  e.  B )
123122ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( invg `  W ) `  Y
)  e.  B )
124123ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( ( invg `  W ) `
 Y )  e.  B )
12579ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( ( m  +  1 )  .x.  X )  e.  B
)
126 simplrr 769 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) )
127 simpr 462 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( ( m  +  1 )  .x.  X )  .<_  ( ( invg `  W
) `  Y )
)
1287, 34posasymb 16183 . . . . . . . . . 10  |-  ( ( W  e.  Poset  /\  (
( invg `  W ) `  Y
)  e.  B  /\  ( ( m  + 
1 )  .x.  X
)  e.  B )  ->  ( ( ( ( invg `  W ) `  Y
)  .<_  ( ( m  +  1 )  .x.  X )  /\  (
( m  +  1 )  .x.  X ) 
.<_  ( ( invg `  W ) `  Y
) )  <->  ( ( invg `  W ) `
 Y )  =  ( ( m  + 
1 )  .x.  X
) ) )
129128biimpa 486 . . . . . . . . 9  |-  ( ( ( W  e.  Poset  /\  ( ( invg `  W ) `  Y
)  e.  B  /\  ( ( m  + 
1 )  .x.  X
)  e.  B )  /\  ( ( ( invg `  W
) `  Y )  .<_  ( ( m  + 
1 )  .x.  X
)  /\  ( (
m  +  1 ) 
.x.  X )  .<_  ( ( invg `  W ) `  Y
) ) )  -> 
( ( invg `  W ) `  Y
)  =  ( ( m  +  1 ) 
.x.  X ) )
130119, 124, 125, 126, 127, 129syl32anc 1272 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( ( invg `  W ) `
 Y )  =  ( ( m  + 
1 )  .x.  X
) )
131130fveq2d 5881 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) )  =  ( ( invg `  W ) `
 ( ( m  +  1 )  .x.  X ) ) )
1327, 9grpinvinv 16706 . . . . . . . . 9  |-  ( ( W  e.  Grp  /\  Y  e.  B )  ->  ( ( invg `  W ) `  (
( invg `  W ) `  Y
) )  =  Y )
1334, 120, 132syl2anc 665 . . . . . . . 8  |-  ( ph  ->  ( ( invg `  W ) `  (
( invg `  W ) `  Y
) )  =  Y )
134133ad4antr 736 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) )  =  Y )
135118, 131, 1343eqtr2rd 2470 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  Y  =  (
-u ( m  + 
1 )  .x.  X
) )
136117, 135breqtrrd 4447 . . . . 5  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( ( -u m  -  2 ) 
.x.  X )  .<  Y )
137 1cnd 9659 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  1  e.  CC )
13867, 68, 137addsubassd 10006 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  2 )  -  1 )  =  ( m  +  ( 2  -  1 ) ) )
139 2m1e1 10724 . . . . . . . . . . . . 13  |-  ( 2  -  1 )  =  1
140139oveq2i 6312 . . . . . . . . . . . 12  |-  ( m  +  ( 2  -  1 ) )  =  ( m  +  1 )
141138, 140syl6req 2480 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  1 )  =  ( ( m  +  2 )  - 
1 ) )
142141negeqd 9869 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u (
m  +  1 )  =  -u ( ( m  +  2 )  - 
1 ) )
14367, 68addcld 9662 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  2 )  e.  CC )
144143, 137negsubdid 10001 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u (
( m  +  2 )  -  1 )  =  ( -u (
m  +  2 )  +  1 ) )
14569oveq1d 6316 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  +  1 )  =  ( ( -u m  -  2 )  +  1 ) )
146142, 144, 1453eqtrrd 2468 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u m  -  2 )  +  1 )  =  -u ( m  + 
1 ) )
147146oveq1d 6316 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  =  ( -u ( m  +  1
)  .x.  X )
)
14829ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e. Toset )
149148, 30syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e.  Poset )
15060znegcld 11042 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u m  e.  ZZ )
151150, 80zsubcld 11045 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u m  -  2 )  e.  ZZ )
152151peano2zd 11043 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u m  -  2 )  +  1 )  e.  ZZ )
1537, 8mulgcl 16760 . . . . . . . . . 10  |-  ( ( W  e.  Grp  /\  ( ( -u m  -  2 )  +  1 )  e.  ZZ  /\  X  e.  B )  ->  ( ( (
-u m  -  2 )  +  1 ) 
.x.  X )  e.  B )
15475, 152, 77, 153syl3anc 1264 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  e.  B )
1557, 34posref 16181 . . . . . . . . 9  |-  ( ( W  e.  Poset  /\  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  e.  B )  ->  ( ( (
-u m  -  2 )  +  1 ) 
.x.  X )  .<_  ( ( ( -u m  -  2 )  +  1 )  .x.  X ) )
156149, 154, 155syl2anc 665 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  .<_  ( ( (
-u m  -  2 )  +  1 ) 
.x.  X ) )
157147, 156eqbrtrrd 4443 . . . . . . 7  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  1 )  .x.  X ) 
.<_  ( ( ( -u m  -  2 )  +  1 )  .x.  X ) )
158157ad2antrr 730 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  ( -u (
m  +  1 ) 
.x.  X )  .<_  ( ( ( -u m  -  2 )  +  1 )  .x.  X ) )
159135, 158eqbrtrd 4441 . . . . 5  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  Y  .<_  ( ( ( -u m  - 
2 )  +  1 )  .x.  X ) )
160 oveq1 6308 . . . . . . . 8  |-  ( n  =  ( -u m  -  2 )  -> 
( n  .x.  X
)  =  ( (
-u m  -  2 )  .x.  X ) )
161160breq1d 4430 . . . . . . 7  |-  ( n  =  ( -u m  -  2 )  -> 
( ( n  .x.  X )  .<  Y  <->  ( ( -u m  -  2 ) 
.x.  X )  .<  Y ) )
162 oveq1 6308 . . . . . . . . 9  |-  ( n  =  ( -u m  -  2 )  -> 
( n  +  1 )  =  ( (
-u m  -  2 )  +  1 ) )
163162oveq1d 6316 . . . . . . . 8  |-  ( n  =  ( -u m  -  2 )  -> 
( ( n  + 
1 )  .x.  X
)  =  ( ( ( -u m  - 
2 )  +  1 )  .x.  X ) )
164163breq2d 4432 . . . . . . 7  |-  ( n  =  ( -u m  -  2 )  -> 
( Y  .<_  ( ( n  +  1 ) 
.x.  X )  <->  Y  .<_  ( ( ( -u m  -  2 )  +  1 )  .x.  X
) ) )
165161, 164anbi12d 715 . . . . . 6  |-  ( n  =  ( -u m  -  2 )  -> 
( ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) )  <-> 
( ( ( -u m  -  2 ) 
.x.  X )  .<  Y  /\  Y  .<_  ( ( ( -u m  - 
2 )  +  1 )  .x.  X ) ) ) )
166165rspcev 3182 . . . . 5  |-  ( ( ( -u m  - 
2 )  e.  ZZ  /\  ( ( ( -u m  -  2 ) 
.x.  X )  .<  Y  /\  Y  .<_  ( ( ( -u m  - 
2 )  +  1 )  .x.  X ) ) )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) )
16765, 136, 159, 166syl12anc 1262 . . . 4  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y ) )  ->  E. n  e.  ZZ  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
16876ad2antrr 730 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( m  +  1 )  e.  ZZ )
169168znegcld 11042 . . . . 5  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  ->  -u ( m  +  1 )  e.  ZZ )
1702ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  (
m  e.  NN0  /\  ( ( m  .x.  X )  .<  (
( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) )  /\  (
( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) ) )  ->  W  e. oGrp )
17172ad2antrr 730 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  (
m  e.  NN0  /\  ( ( m  .x.  X )  .<  (
( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) )  /\  (
( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) ) )  ->  (oppg
`  W )  e. oGrp
)
172170, 171jca 534 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  (
m  e.  NN0  /\  ( ( m  .x.  X )  .<  (
( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) )  /\  (
( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) ) )  ->  ( W  e. oGrp  /\  (oppg
`  W )  e. oGrp
) )
1731723anassrs 1228 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( W  e. oGrp  /\  (oppg `  W )  e. oGrp )
)
174123ad2antrr 730 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( invg `  W ) `  Y
)  e.  B )
17579ad2antrr 730 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( m  + 
1 )  .x.  X
)  e.  B )
176 simpr 462 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )
1777, 17, 9ogrpinvlt 28479 . . . . . . . 8  |-  ( ( ( W  e. oGrp  /\  (oppg `  W )  e. oGrp )  /\  ( ( invg `  W ) `  Y
)  e.  B  /\  ( ( m  + 
1 )  .x.  X
)  e.  B )  ->  ( ( ( invg `  W
) `  Y )  .<  ( ( m  + 
1 )  .x.  X
)  <->  ( ( invg `  W ) `
 ( ( m  +  1 )  .x.  X ) )  .< 
( ( invg `  W ) `  (
( invg `  W ) `  Y
) ) ) )
178177biimpa 486 . . . . . . 7  |-  ( ( ( ( W  e. oGrp  /\  (oppg
`  W )  e. oGrp
)  /\  ( ( invg `  W ) `
 Y )  e.  B  /\  ( ( m  +  1 ) 
.x.  X )  e.  B )  /\  (
( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( invg `  W ) `  (
( m  +  1 )  .x.  X ) )  .<  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) )
179173, 174, 175, 176, 178syl31anc 1267 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( invg `  W ) `  (
( m  +  1 )  .x.  X ) )  .<  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) )
180114ad2antrr 730 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( -u ( m  + 
1 )  .x.  X
)  =  ( ( invg `  W
) `  ( (
m  +  1 ) 
.x.  X ) ) )
181180eqcomd 2430 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( invg `  W ) `  (
( m  +  1 )  .x.  X ) )  =  ( -u ( m  +  1
)  .x.  X )
)
182133ad4antr 736 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( invg `  W ) `  (
( invg `  W ) `  Y
) )  =  Y )
183179, 181, 1823brtr3d 4450 . . . . 5  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( -u ( m  + 
1 )  .x.  X
)  .<  Y )
184 simp-4l 774 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  ->  ph )
1857, 8mulgcl 16760 . . . . . . . . . . . 12  |-  ( ( W  e.  Grp  /\  m  e.  ZZ  /\  X  e.  B )  ->  (
m  .x.  X )  e.  B )
18675, 60, 77, 185syl3anc 1264 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  .x.  X )  e.  B )
1877, 17, 9ogrpinvlt 28479 . . . . . . . . . . 11  |-  ( ( ( W  e. oGrp  /\  (oppg `  W )  e. oGrp )  /\  ( m  .x.  X
)  e.  B  /\  ( ( invg `  W ) `  Y
)  e.  B )  ->  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  ( ( invg `  W ) `  (
m  .x.  X )
) ) )
18874, 186, 123, 187syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  .x.  X
)  .<  ( ( invg `  W ) `
 Y )  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  ( ( invg `  W ) `  (
m  .x.  X )
) ) )
189188biimpa 486 . . . . . . . . 9  |-  ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( m  .x.  X ) 
.<  ( ( invg `  W ) `  Y
) )  ->  (
( invg `  W ) `  (
( invg `  W ) `  Y
) )  .<  (
( invg `  W ) `  (
m  .x.  X )
) )
190189adantrr 721 . . . . . . . 8  |-  ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m  .x.  X )  .<  (
( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  -> 
( ( invg `  W ) `  (
( invg `  W ) `  Y
) )  .<  (
( invg `  W ) `  (
m  .x.  X )
) )
191190adantr 466 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( invg `  W ) `  (
( invg `  W ) `  Y
) )  .<  (
( invg `  W ) `  (
m  .x.  X )
) )
192 negdi 9931 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  CC  /\  1  e.  CC )  -> 
-u ( m  + 
1 )  =  (
-u m  +  -u
1 ) )
19366, 40, 192sylancl 666 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  -u (
m  +  1 )  =  ( -u m  +  -u 1 ) )
194193oveq1d 6316 . . . . . . . . . . . . 13  |-  ( m  e.  NN0  ->  ( -u ( m  +  1
)  +  1 )  =  ( ( -u m  +  -u 1 )  +  1 ) )
19566negcld 9973 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  -u m  e.  CC )
19691negcld 9973 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  -u 1  e.  CC )
197195, 196, 91addassd 9665 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( (
-u m  +  -u
1 )  +  1 )  =  ( -u m  +  ( -u 1  +  1 ) ) )
19843oveq2i 6312 . . . . . . . . . . . . . . 15  |-  ( -u m  +  ( -u 1  +  1 ) )  =  ( -u m  +  0 )
199198a1i 11 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( -u m  +  ( -u 1  +  1 ) )  =  ( -u m  +  0 ) )
200195addid1d 9833 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( -u m  +  0 )  =  -u m )
201197, 199, 2003eqtrd 2467 . . . . . . . . . . . . 13  |-  ( m  e.  NN0  ->  ( (
-u m  +  -u
1 )  +  1 )  =  -u m
)
202194, 201eqtrd 2463 . . . . . . . . . . . 12  |-  ( m  e.  NN0  ->  ( -u ( m  +  1
)  +  1 )  =  -u m )
203202oveq1d 6316 . . . . . . . . . . 11  |-  ( m  e.  NN0  ->  ( (
-u ( m  + 
1 )  +  1 )  .x.  X )  =  ( -u m  .x.  X ) )
204203adantl 467 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  =  ( -u m  .x.  X ) )
2057, 8, 9mulgneg 16761 . . . . . . . . . . 11  |-  ( ( W  e.  Grp  /\  m  e.  ZZ  /\  X  e.  B )  ->  ( -u m  .x.  X )  =  ( ( invg `  W ) `
 ( m  .x.  X ) ) )
20675, 60, 77, 205syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u m  .x.  X )  =  ( ( invg `  W ) `
 ( m  .x.  X ) ) )
207204, 206eqtrd 2463 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  =  ( ( invg `  W ) `
 ( m  .x.  X ) ) )
208207ad2antrr 730 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( -u (
m  +  1 )  +  1 )  .x.  X )  =  ( ( invg `  W ) `  (
m  .x.  X )
) )
209208eqcomd 2430 . . . . . . 7  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  -> 
( ( invg `  W ) `  (
m  .x.  X )
)  =  ( (
-u ( m  + 
1 )  +  1 )  .x.  X ) )
210191, 182, 2093brtr3d 4450 . . . . . 6  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  ->  Y  .<  ( ( -u ( m  +  1
)  +  1 ) 
.x.  X ) )
211 ovex 6329 . . . . . . . 8  |-  ( (
-u ( m  + 
1 )  +  1 )  .x.  X )  e.  _V
212211a1i 11 . . . . . . 7  |-  ( ph  ->  ( ( -u (
m  +  1 )  +  1 )  .x.  X )  e.  _V )
21334, 17pltle 16192 . . . . . . 7  |-  ( ( W  e. oGrp  /\  Y  e.  B  /\  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  e.  _V )  -> 
( Y  .<  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  ->  Y  .<_  ( (
-u ( m  + 
1 )  +  1 )  .x.  X ) ) )
2142, 120, 212, 213syl3anc 1264 . . . . . 6  |-  ( ph  ->  ( Y  .<  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  ->  Y  .<_  ( (
-u ( m  + 
1 )  +  1 )  .x.  X ) ) )
215184, 210, 214sylc 62 . . . . 5  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  ->  Y  .<_  ( ( -u ( m  +  1
)  +  1 ) 
.x.  X ) )
216 oveq1 6308 . . . . . . . 8  |-  ( n  =  -u ( m  + 
1 )  ->  (
n  .x.  X )  =  ( -u (
m  +  1 ) 
.x.  X ) )
217216breq1d 4430 . . . . . . 7  |-  ( n  =  -u ( m  + 
1 )  ->  (
( n  .x.  X
)  .<  Y  <->  ( -u (
m  +  1 ) 
.x.  X )  .<  Y ) )
218 oveq1 6308 . . . . . . . . 9  |-  ( n  =  -u ( m  + 
1 )  ->  (
n  +  1 )  =  ( -u (
m  +  1 )  +  1 ) )
219218oveq1d 6316 . . . . . . . 8  |-  ( n  =  -u ( m  + 
1 )  ->  (
( n  +  1 )  .x.  X )  =  ( ( -u ( m  +  1
)  +  1 ) 
.x.  X ) )
220219breq2d 4432 . . . . . . 7  |-  ( n  =  -u ( m  + 
1 )  ->  ( Y  .<_  ( ( n  +  1 )  .x.  X )  <->  Y  .<_  ( ( -u ( m  +  1 )  +  1 )  .x.  X
) ) )
221217, 220anbi12d 715 . . . . . 6  |-  ( n  =  -u ( m  + 
1 )  ->  (
( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) )  <->  ( ( -u ( m  +  1 )  .x.  X ) 
.<  Y  /\  Y  .<_  ( ( -u ( m  +  1 )  +  1 )  .x.  X
) ) ) )
222221rspcev 3182 . . . . 5  |-  ( (
-u ( m  + 
1 )  e.  ZZ  /\  ( ( -u (
m  +  1 ) 
.x.  X )  .<  Y  /\  Y  .<_  ( (
-u ( m  + 
1 )  +  1 )  .x.  X ) ) )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) )
223169, 183, 215, 222syl12anc 1262 . . . 4  |-  ( ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  /\  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) )  ->  E. n  e.  ZZ  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
2247, 34, 17tlt2 28417 . . . . . 6  |-  ( ( W  e. Toset  /\  (
( m  +  1 )  .x.  X )  e.  B  /\  (
( invg `  W ) `  Y
)  e.  B )  ->  ( ( ( m  +  1 ) 
.x.  X )  .<_  ( ( invg `  W ) `  Y
)  \/  ( ( invg `  W
) `  Y )  .<  ( ( m  + 
1 )  .x.  X
) ) )
225148, 79, 123, 224syl3anc 1264 . . . . 5  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y )  \/  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) ) )
226225adantr 466 . . . 4  |-  ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m  .x.  X )  .<  (
( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  -> 
( ( ( m  +  1 )  .x.  X )  .<_  ( ( invg `  W
) `  Y )  \/  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) ) )
227167, 223, 226mpjaodan 793 . . 3  |-  ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( ( m  .x.  X )  .<  (
( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )  ->  E. n  e.  ZZ  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
2282adantr 466 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  W  e. oGrp )
229 archirng.2 . . . . 5  |-  ( ph  ->  W  e. Archi )
230229adantr 466 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  W  e. Archi )
2316adantr 466 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  X  e.  B )
232122adantr 466 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  ( ( invg `  W ) `
 Y )  e.  B )
23316adantr 466 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  .0.  .<  X )
234133breq1d 4430 . . . . . 6  |-  ( ph  ->  ( ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  <->  Y  .<  .0.  )
)
235234biimpar 487 . . . . 5  |-  ( (
ph  /\  Y  .<  .0.  )  ->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  )
2367, 17, 9, 18ogrpinv0lt 28478 . . . . . . 7  |-  ( ( W  e. oGrp  /\  (
( invg `  W ) `  Y
)  e.  B )  ->  (  .0.  .<  ( ( invg `  W ) `  Y
)  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  ) )
2372, 122, 236syl2anc 665 . . . . . 6  |-  ( ph  ->  (  .0.  .<  (
( invg `  W ) `  Y
)  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  ) )
238237biimpar 487 . . . . 5  |-  ( (
ph  /\  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  )  ->  .0.  .< 
( ( invg `  W ) `  Y
) )
239235, 238syldan 472 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  .0.  .<  (
( invg `  W ) `  Y
) )
2407, 18, 17, 34, 8, 228, 230, 231, 232, 233, 239archirng 28497 . . 3  |-  ( (
ph  /\  Y  .<  .0.  )  ->  E. m  e.  NN0  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )
241227, 240r19.29a 2970 . 2  |-  ( (
ph  /\  Y  .<  .0.  )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) )
242 nn0ssz 10958 . . 3  |-  NN0  C_  ZZ
2432adantr 466 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  W  e. oGrp )
244229adantr 466 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  W  e. Archi )
2456adantr 466 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  X  e.  B
)
246120adantr 466 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  Y  e.  B
)
24716adantr 466 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  .0.  .<  X )
248 simpr 462 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  .0.  .<  Y )
2497, 18, 17, 34, 8, 243, 244, 245, 246, 247, 248archirng 28497 . . 3  |-  ( (
ph  /\  .0.  .<  Y )  ->  E. n  e.  NN0  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
250 ssrexv 3526 . . 3  |-  ( NN0  C_  ZZ  ->  ( E. n  e.  NN0  ( ( n  .x.  X ) 
.<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) ) )
251242, 249, 250mpsyl 65 . 2  |-  ( (
ph  /\  .0.  .<  Y )  ->  E. n  e.  ZZ  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
2527, 17tlt3 28418 . . 3  |-  ( ( W  e. Toset  /\  Y  e.  B  /\  .0.  e.  B )  ->  ( Y  =  .0.  \/  Y  .<  .0.  \/  .0.  .<  Y ) )
25329, 120, 33, 252syl3anc 1264 . 2  |-  ( ph  ->  ( Y  =  .0. 
\/  Y  .<  .0.  \/  .0.  .<  Y ) )
25458, 241, 251, 253mpjao3dan 1331 1  |-  ( ph  ->  E. n  e.  ZZ  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    \/ w3o 981    /\ w3a 982    = wceq 1437    e. wcel 1868   E.wrex 2776   _Vcvv 3081    C_ wss 3436   class class class wbr 4420   ` cfv 5597  (class class class)co 6301   CCcc 9537   0cc0 9539   1c1 9540    + caddc 9542    - cmin 9860   -ucneg 9861   2c2 10659   NN0cn0 10869   ZZcz 10937   Basecbs 15106   +g cplusg 15175   lecple 15182   0gc0g 15323   Posetcpo 16170   ltcplt 16171  Tosetctos 16264   Grpcgrp 16654   invgcminusg 16655  .gcmg 16657  oppgcoppg 16981  oMndcomnd 28452  oGrpcogrp 28453  Archicarchi 28486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-1st 6803  df-2nd 6804  df-tpos 6977  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-uz 11160  df-fz 11785  df-seq 12213  df-ndx 15109  df-slot 15110  df-base 15111  df-sets 15112  df-plusg 15188  df-ple 15195  df-0g 15325  df-preset 16158  df-poset 16176  df-plt 16189  df-toset 16265  df-mgm 16473  df-sgrp 16512  df-mnd 16522  df-grp 16658  df-minusg 16659  df-mulg 16661  df-oppg 16982  df-omnd 28454  df-ogrp 28455  df-inftm 28487  df-archi 28488
This theorem is referenced by:  archiabllem2c  28504
  Copyright terms: Public domain W3C validator