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

Theorem archirngz 28557
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 11007 . . 3  |-  -u 1  e.  ZZ
2 archirng.1 . . . . . . . . . 10  |-  ( ph  ->  W  e. oGrp )
3 ogrpgrp 28517 . . . . . . . . . 10  |-  ( W  e. oGrp  ->  W  e.  Grp )
42, 3syl 17 . . . . . . . . 9  |-  ( ph  ->  W  e.  Grp )
5 1zzd 11002 . . . . . . . . 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 2462 . . . . . . . . . 10  |-  ( invg `  W )  =  ( invg `  W )
107, 8, 9mulgneg 16831 . . . . . . . . 9  |-  ( ( W  e.  Grp  /\  1  e.  ZZ  /\  X  e.  B )  ->  ( -u 1  .x.  X )  =  ( ( invg `  W ) `
 ( 1  .x. 
X ) ) )
114, 5, 6, 10syl3anc 1276 . . . . . . . 8  |-  ( ph  ->  ( -u 1  .x. 
X )  =  ( ( invg `  W ) `  (
1  .x.  X )
) )
127, 8mulg1 16820 . . . . . . . . . 10  |-  ( X  e.  B  ->  (
1  .x.  X )  =  X )
136, 12syl 17 . . . . . . . . 9  |-  ( ph  ->  ( 1  .x.  X
)  =  X )
1413fveq2d 5896 . . . . . . . 8  |-  ( ph  ->  ( ( invg `  W ) `  (
1  .x.  X )
)  =  ( ( invg `  W
) `  X )
)
1511, 14eqtrd 2496 . . . . . . 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 28537 . . . . . . . . 9  |-  ( ( W  e. oGrp  /\  X  e.  B )  ->  (  .0.  .<  X  <->  ( ( invg `  W ) `
 X )  .<  .0.  ) )
2019biimpa 491 . . . . . . . 8  |-  ( ( ( W  e. oGrp  /\  X  e.  B )  /\  .0.  .<  X )  ->  ( ( invg `  W ) `  X
)  .<  .0.  )
212, 6, 16, 20syl21anc 1275 . . . . . . 7  |-  ( ph  ->  ( ( invg `  W ) `  X
)  .<  .0.  )
2215, 21eqbrtrd 4439 . . . . . 6  |-  ( ph  ->  ( -u 1  .x. 
X )  .<  .0.  )
2322adantr 471 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( -u
1  .x.  X )  .<  .0.  )
24 simpr 467 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  Y  =  .0.  )
2523, 24breqtrrd 4445 . . . 4  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( -u
1  .x.  X )  .<  Y )
26 isogrp 28516 . . . . . . . . . 10  |-  ( W  e. oGrp 
<->  ( W  e.  Grp  /\  W  e. oMnd ) )
2726simprbi 470 . . . . . . . . 9  |-  ( W  e. oGrp  ->  W  e. oMnd )
28 omndtos 28519 . . . . . . . . 9  |-  ( W  e. oMnd  ->  W  e. Toset )
292, 27, 283syl 18 . . . . . . . 8  |-  ( ph  ->  W  e. Toset )
30 tospos 28471 . . . . . . . 8  |-  ( W  e. Toset  ->  W  e.  Poset )
3129, 30syl 17 . . . . . . 7  |-  ( ph  ->  W  e.  Poset )
327, 18grpidcl 16749 . . . . . . . 8  |-  ( W  e.  Grp  ->  .0.  e.  B )
332, 3, 323syl 18 . . . . . . 7  |-  ( ph  ->  .0.  e.  B )
34 archirng.l . . . . . . . 8  |-  .<_  =  ( le `  W )
357, 34posref 16251 . . . . . . 7  |-  ( ( W  e.  Poset  /\  .0.  e.  B )  ->  .0.  .<_  .0.  )
3631, 33, 35syl2anc 671 . . . . . 6  |-  ( ph  ->  .0.  .<_  .0.  )
3736adantr 471 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  .0.  .<_  .0.  )
38 1m1e0 10711 . . . . . . . . . 10  |-  ( 1  -  1 )  =  0
3938negeqi 9899 . . . . . . . . 9  |-  -u (
1  -  1 )  =  -u 0
40 ax-1cn 9628 . . . . . . . . . 10  |-  1  e.  CC
4140, 40negsubdii 9991 . . . . . . . . 9  |-  -u (
1  -  1 )  =  ( -u 1  +  1 )
42 neg0 9951 . . . . . . . . 9  |-  -u 0  =  0
4339, 41, 423eqtr3i 2492 . . . . . . . 8  |-  ( -u
1  +  1 )  =  0
4443oveq1i 6330 . . . . . . 7  |-  ( (
-u 1  +  1 )  .x.  X )  =  ( 0  .x. 
X )
457, 18, 8mulg0 16818 . . . . . . . 8  |-  ( X  e.  B  ->  (
0  .x.  X )  =  .0.  )
466, 45syl 17 . . . . . . 7  |-  ( ph  ->  ( 0  .x.  X
)  =  .0.  )
4744, 46syl5eq 2508 . . . . . 6  |-  ( ph  ->  ( ( -u 1  +  1 )  .x.  X )  =  .0.  )
4847adantr 471 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( (
-u 1  +  1 )  .x.  X )  =  .0.  )
4937, 24, 483brtr4d 4449 . . . 4  |-  ( (
ph  /\  Y  =  .0.  )  ->  Y  .<_  ( ( -u 1  +  1 )  .x.  X
) )
5025, 49jca 539 . . 3  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( (
-u 1  .x.  X
)  .<  Y  /\  Y  .<_  ( ( -u 1  +  1 )  .x.  X ) ) )
51 oveq1 6327 . . . . . 6  |-  ( n  =  -u 1  ->  (
n  .x.  X )  =  ( -u 1  .x.  X ) )
5251breq1d 4428 . . . . 5  |-  ( n  =  -u 1  ->  (
( n  .x.  X
)  .<  Y  <->  ( -u 1  .x.  X )  .<  Y ) )
53 oveq1 6327 . . . . . . 7  |-  ( n  =  -u 1  ->  (
n  +  1 )  =  ( -u 1  +  1 ) )
5453oveq1d 6335 . . . . . 6  |-  ( n  =  -u 1  ->  (
( n  +  1 )  .x.  X )  =  ( ( -u
1  +  1 ) 
.x.  X ) )
5554breq2d 4430 . . . . 5  |-  ( n  =  -u 1  ->  ( Y  .<_  ( ( n  +  1 )  .x.  X )  <->  Y  .<_  ( ( -u 1  +  1 )  .x.  X
) ) )
5652, 55anbi12d 722 . . . 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 3162 . . 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 674 . 2  |-  ( (
ph  /\  Y  =  .0.  )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) )
59 simpr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  m  e.  NN0 )
6059nn0zd 11072 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  m  e.  ZZ )
6160ad2antrr 737 . . . . . . 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 11076 . . . . . 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 11003 . . . . . . 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 11079 . . . . 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 10913 . . . . . . . . . . 11  |-  ( m  e.  NN0  ->  m  e.  CC )
6766adantl 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  m  e.  CC )
68 2cnd 10715 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  2  e.  CC )
6967, 68negdi2d 10031 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u (
m  +  2 )  =  ( -u m  -  2 ) )
7069oveq1d 6335 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  .x.  X )  =  ( ( -u m  -  2 ) 
.x.  X ) )
712ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e. oGrp )
72 archirngz.1 . . . . . . . . . . . 12  |-  ( ph  ->  (oppg
`  W )  e. oGrp
)
7372ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (oppg `  W
)  e. oGrp )
7471, 73jca 539 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( W  e. oGrp  /\  (oppg `  W
)  e. oGrp ) )
754ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e.  Grp )
7660peano2zd 11077 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  1 )  e.  ZZ )
776ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  X  e.  B )
787, 8mulgcl 16830 . . . . . . . . . . 11  |-  ( ( W  e.  Grp  /\  ( m  +  1
)  e.  ZZ  /\  X  e.  B )  ->  ( ( m  + 
1 )  .x.  X
)  e.  B )
7975, 76, 77, 78syl3anc 1276 . . . . . . . . . 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 11078 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  2 )  e.  ZZ )
827, 8mulgcl 16830 . . . . . . . . . . 11  |-  ( ( W  e.  Grp  /\  ( m  +  2
)  e.  ZZ  /\  X  e.  B )  ->  ( ( m  + 
2 )  .x.  X
)  e.  B )
8375, 81, 77, 82syl3anc 1276 . . . . . . . . . 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 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  .0.  .<  X )
86 eqid 2462 . . . . . . . . . . . . 13  |-  ( +g  `  W )  =  ( +g  `  W )
877, 17, 86ogrpaddlt 28532 . . . . . . . . . . . 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 1289 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (  .0.  ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  .< 
( X ( +g  `  W ) ( ( m  +  1 ) 
.x.  X ) ) )
897, 86, 18grplid 16751 . . . . . . . . . . . 12  |-  ( ( W  e.  Grp  /\  ( ( m  + 
1 )  .x.  X
)  e.  B )  ->  (  .0.  ( +g  `  W ) ( ( m  +  1 )  .x.  X ) )  =  ( ( m  +  1 ) 
.x.  X ) )
9075, 79, 89syl2anc 671 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (  .0.  ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  =  ( ( m  + 
1 )  .x.  X
) )
91 1cnd 9690 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  NN0  ->  1  e.  CC )
9266, 91, 91addassd 9696 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN0  ->  ( ( m  +  1 )  +  1 )  =  ( m  +  ( 1  +  1 ) ) )
93 1p1e2 10756 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  1 )  =  2
9493oveq2i 6331 . . . . . . . . . . . . . . . 16  |-  ( m  +  ( 1  +  1 ) )  =  ( m  +  2 )
9592, 94syl6eq 2512 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( ( m  +  1 )  +  1 )  =  ( m  +  2 ) )
9666, 91addcld 9693 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN0  ->  ( m  +  1 )  e.  CC )
9796, 91addcomd 9866 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( ( m  +  1 )  +  1 )  =  ( 1  +  ( m  +  1 ) ) )
9895, 97eqtr3d 2498 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( m  +  2 )  =  ( 1  +  ( m  +  1 ) ) )
9998oveq1d 6335 . . . . . . . . . . . . 13  |-  ( m  e.  NN0  ->  ( ( m  +  2 ) 
.x.  X )  =  ( ( 1  +  ( m  +  1 ) )  .x.  X
) )
10099adantl 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  2 )  .x.  X )  =  ( ( 1  +  ( m  + 
1 ) )  .x.  X ) )
101 1zzd 11002 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  1  e.  ZZ )
1027, 8, 86mulgdir 16838 . . . . . . . . . . . . 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 1278 . . . . . . . . . . . 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 6335 . . . . . . . . . . . 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 2501 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( X ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  =  ( ( m  + 
2 )  .x.  X
) )
10788, 90, 1063brtr3d 4448 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  1 )  .x.  X ) 
.<  ( ( m  + 
2 )  .x.  X
) )
1087, 17, 9ogrpinvlt 28538 . . . . . . . . . . 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 491 . . . . . . . . . 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 1279 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( invg `  W ) `  (
( m  +  2 )  .x.  X ) )  .<  ( ( invg `  W ) `
 ( ( m  +  1 )  .x.  X ) ) )
1117, 8, 9mulgneg 16831 . . . . . . . . . 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 1276 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  .x.  X )  =  ( ( invg `  W ) `
 ( ( m  +  2 )  .x.  X ) ) )
1137, 8, 9mulgneg 16831 . . . . . . . . . 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 1276 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  1 )  .x.  X )  =  ( ( invg `  W ) `
 ( ( m  +  1 )  .x.  X ) ) )
115110, 112, 1143brtr4d 4449 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  .x.  X ) 
.<  ( -u ( m  +  1 )  .x.  X ) )
11670, 115eqbrtrrd 4441 . . . . . . 7  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u m  -  2 )  .x.  X ) 
.<  ( -u ( m  +  1 )  .x.  X ) )
117116ad2antrr 737 . . . . . 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 737 . . . . . . 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 743 . . . . . . . . 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 16766 . . . . . . . . . . . 12  |-  ( ( W  e.  Grp  /\  Y  e.  B )  ->  ( ( invg `  W ) `  Y
)  e.  B )
1224, 120, 121syl2anc 671 . . . . . . . . . . 11  |-  ( ph  ->  ( ( invg `  W ) `  Y
)  e.  B )
123122ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( invg `  W ) `  Y
)  e.  B )
124123ad2antrr 737 . . . . . . . . 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 737 . . . . . . . . 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 776 . . . . . . . . 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 467 . . . . . . . . 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 16253 . . . . . . . . . 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 491 . . . . . . . . 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 1284 . . . . . . . 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 5896 . . . . . . 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 16776 . . . . . . . . 9  |-  ( ( W  e.  Grp  /\  Y  e.  B )  ->  ( ( invg `  W ) `  (
( invg `  W ) `  Y
) )  =  Y )
1334, 120, 132syl2anc 671 . . . . . . . 8  |-  ( ph  ->  ( ( invg `  W ) `  (
( invg `  W ) `  Y
) )  =  Y )
134133ad4antr 743 . . . . . . 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 2503 . . . . . 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 4445 . . . . 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 9690 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  1  e.  CC )
13867, 68, 137addsubassd 10037 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  2 )  -  1 )  =  ( m  +  ( 2  -  1 ) ) )
139 2m1e1 10757 . . . . . . . . . . . . 13  |-  ( 2  -  1 )  =  1
140139oveq2i 6331 . . . . . . . . . . . 12  |-  ( m  +  ( 2  -  1 ) )  =  ( m  +  1 )
141138, 140syl6req 2513 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  1 )  =  ( ( m  +  2 )  - 
1 ) )
142141negeqd 9900 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u (
m  +  1 )  =  -u ( ( m  +  2 )  - 
1 ) )
14367, 68addcld 9693 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  2 )  e.  CC )
144143, 137negsubdid 10032 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u (
( m  +  2 )  -  1 )  =  ( -u (
m  +  2 )  +  1 ) )
14569oveq1d 6335 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  +  1 )  =  ( ( -u m  -  2 )  +  1 ) )
146142, 144, 1453eqtrrd 2501 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u m  -  2 )  +  1 )  =  -u ( m  + 
1 ) )
147146oveq1d 6335 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  =  ( -u ( m  +  1
)  .x.  X )
)
14829ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e. Toset )
149148, 30syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e.  Poset )
15060znegcld 11076 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u m  e.  ZZ )
151150, 80zsubcld 11079 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u m  -  2 )  e.  ZZ )
152151peano2zd 11077 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u m  -  2 )  +  1 )  e.  ZZ )
1537, 8mulgcl 16830 . . . . . . . . . 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 1276 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  e.  B )
1557, 34posref 16251 . . . . . . . . 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 671 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  .<_  ( ( (
-u m  -  2 )  +  1 ) 
.x.  X ) )
157147, 156eqbrtrrd 4441 . . . . . . 7  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  1 )  .x.  X ) 
.<_  ( ( ( -u m  -  2 )  +  1 )  .x.  X ) )
158157ad2antrr 737 . . . . . 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 4439 . . . . 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 6327 . . . . . . . 8  |-  ( n  =  ( -u m  -  2 )  -> 
( n  .x.  X
)  =  ( (
-u m  -  2 )  .x.  X ) )
161160breq1d 4428 . . . . . . 7  |-  ( n  =  ( -u m  -  2 )  -> 
( ( n  .x.  X )  .<  Y  <->  ( ( -u m  -  2 ) 
.x.  X )  .<  Y ) )
162 oveq1 6327 . . . . . . . . 9  |-  ( n  =  ( -u m  -  2 )  -> 
( n  +  1 )  =  ( (
-u m  -  2 )  +  1 ) )
163162oveq1d 6335 . . . . . . . 8  |-  ( n  =  ( -u m  -  2 )  -> 
( ( n  + 
1 )  .x.  X
)  =  ( ( ( -u m  - 
2 )  +  1 )  .x.  X ) )
164163breq2d 4430 . . . . . . 7  |-  ( n  =  ( -u m  -  2 )  -> 
( Y  .<_  ( ( n  +  1 ) 
.x.  X )  <->  Y  .<_  ( ( ( -u m  -  2 )  +  1 )  .x.  X
) ) )
165161, 164anbi12d 722 . . . . . 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 3162 . . . . 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 1274 . . . 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 737 . . . . . 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 11076 . . . . 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 737 . . . . . . . . 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 737 . . . . . . . . 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 539 . . . . . . . 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 1240 . . . . . . 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 737 . . . . . . 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 737 . . . . . . 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 467 . . . . . . 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 28538 . . . . . . . 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 491 . . . . . . 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 1279 . . . . . 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 737 . . . . . . 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 2468 . . . . . 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 743 . . . . . 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 4448 . . . . 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 781 . . . . . 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 16830 . . . . . . . . . . . 12  |-  ( ( W  e.  Grp  /\  m  e.  ZZ  /\  X  e.  B )  ->  (
m  .x.  X )  e.  B )
18675, 60, 77, 185syl3anc 1276 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  .x.  X )  e.  B )
1877, 17, 9ogrpinvlt 28538 . . . . . . . . . . 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 1276 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  .x.  X
)  .<  ( ( invg `  W ) `
 Y )  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  ( ( invg `  W ) `  (
m  .x.  X )
) ) )
189188biimpa 491 . . . . . . . . 9  |-  ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( m  .x.  X ) 
.<  ( ( invg `  W ) `  Y
) )  ->  (
( invg `  W ) `  (
( invg `  W ) `  Y
) )  .<  (
( invg `  W ) `  (
m  .x.  X )
) )
190189adantrr 728 . . . . . . . 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 471 . . . . . . 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 9962 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  CC  /\  1  e.  CC )  -> 
-u ( m  + 
1 )  =  (
-u m  +  -u
1 ) )
19366, 40, 192sylancl 673 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  -u (
m  +  1 )  =  ( -u m  +  -u 1 ) )
194193oveq1d 6335 . . . . . . . . . . . . 13  |-  ( m  e.  NN0  ->  ( -u ( m  +  1
)  +  1 )  =  ( ( -u m  +  -u 1 )  +  1 ) )
19566negcld 10004 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  -u m  e.  CC )
19691negcld 10004 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  -u 1  e.  CC )
197195, 196, 91addassd 9696 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( (
-u m  +  -u
1 )  +  1 )  =  ( -u m  +  ( -u 1  +  1 ) ) )
19843oveq2i 6331 . . . . . . . . . . . . . . 15  |-  ( -u m  +  ( -u 1  +  1 ) )  =  ( -u m  +  0 )
199198a1i 11 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( -u m  +  ( -u 1  +  1 ) )  =  ( -u m  +  0 ) )
200195addid1d 9864 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( -u m  +  0 )  =  -u m )
201197, 199, 2003eqtrd 2500 . . . . . . . . . . . . 13  |-  ( m  e.  NN0  ->  ( (
-u m  +  -u
1 )  +  1 )  =  -u m
)
202194, 201eqtrd 2496 . . . . . . . . . . . 12  |-  ( m  e.  NN0  ->  ( -u ( m  +  1
)  +  1 )  =  -u m )
203202oveq1d 6335 . . . . . . . . . . 11  |-  ( m  e.  NN0  ->  ( (
-u ( m  + 
1 )  +  1 )  .x.  X )  =  ( -u m  .x.  X ) )
204203adantl 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  =  ( -u m  .x.  X ) )
2057, 8, 9mulgneg 16831 . . . . . . . . . . 11  |-  ( ( W  e.  Grp  /\  m  e.  ZZ  /\  X  e.  B )  ->  ( -u m  .x.  X )  =  ( ( invg `  W ) `
 ( m  .x.  X ) ) )
20675, 60, 77, 205syl3anc 1276 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u m  .x.  X )  =  ( ( invg `  W ) `
 ( m  .x.  X ) ) )
207204, 206eqtrd 2496 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  =  ( ( invg `  W ) `
 ( m  .x.  X ) ) )
208207ad2antrr 737 . . . . . . . 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 2468 . . . . . . 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 4448 . . . . . 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 6348 . . . . . . . 8  |-  ( (
-u ( m  + 
1 )  +  1 )  .x.  X )  e.  _V
212211a1i 11 . . . . . . 7  |-  ( ph  ->  ( ( -u (
m  +  1 )  +  1 )  .x.  X )  e.  _V )
21334, 17pltle 16262 . . . . . . 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 1276 . . . . . 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 6327 . . . . . . . 8  |-  ( n  =  -u ( m  + 
1 )  ->  (
n  .x.  X )  =  ( -u (
m  +  1 ) 
.x.  X ) )
217216breq1d 4428 . . . . . . 7  |-  ( n  =  -u ( m  + 
1 )  ->  (
( n  .x.  X
)  .<  Y  <->  ( -u (
m  +  1 ) 
.x.  X )  .<  Y ) )
218 oveq1 6327 . . . . . . . . 9  |-  ( n  =  -u ( m  + 
1 )  ->  (
n  +  1 )  =  ( -u (
m  +  1 )  +  1 ) )
219218oveq1d 6335 . . . . . . . 8  |-  ( n  =  -u ( m  + 
1 )  ->  (
( n  +  1 )  .x.  X )  =  ( ( -u ( m  +  1
)  +  1 ) 
.x.  X ) )
220219breq2d 4430 . . . . . . 7  |-  ( n  =  -u ( m  + 
1 )  ->  ( Y  .<_  ( ( n  +  1 )  .x.  X )  <->  Y  .<_  ( ( -u ( m  +  1 )  +  1 )  .x.  X
) ) )
221217, 220anbi12d 722 . . . . . 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 3162 . . . . 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 1274 . . . 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 28477 . . . . . 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 1276 . . . . 5  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y )  \/  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) ) )
226225adantr 471 . . . 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 800 . . 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 471 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  W  e. oGrp )
229 archirng.2 . . . . 5  |-  ( ph  ->  W  e. Archi )
230229adantr 471 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  W  e. Archi )
2316adantr 471 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  X  e.  B )
232122adantr 471 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  ( ( invg `  W ) `
 Y )  e.  B )
23316adantr 471 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  .0.  .<  X )
234133breq1d 4428 . . . . . 6  |-  ( ph  ->  ( ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  <->  Y  .<  .0.  )
)
235234biimpar 492 . . . . 5  |-  ( (
ph  /\  Y  .<  .0.  )  ->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  )
2367, 17, 9, 18ogrpinv0lt 28537 . . . . . . 7  |-  ( ( W  e. oGrp  /\  (
( invg `  W ) `  Y
)  e.  B )  ->  (  .0.  .<  ( ( invg `  W ) `  Y
)  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  ) )
2372, 122, 236syl2anc 671 . . . . . 6  |-  ( ph  ->  (  .0.  .<  (
( invg `  W ) `  Y
)  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  ) )
238237biimpar 492 . . . . 5  |-  ( (
ph  /\  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  )  ->  .0.  .< 
( ( invg `  W ) `  Y
) )
239235, 238syldan 477 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  .0.  .<  (
( invg `  W ) `  Y
) )
2407, 18, 17, 34, 8, 228, 230, 231, 232, 233, 239archirng 28556 . . 3  |-  ( (
ph  /\  Y  .<  .0.  )  ->  E. m  e.  NN0  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )
241227, 240r19.29a 2944 . 2  |-  ( (
ph  /\  Y  .<  .0.  )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) )
242 nn0ssz 10992 . . 3  |-  NN0  C_  ZZ
2432adantr 471 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  W  e. oGrp )
244229adantr 471 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  W  e. Archi )
2456adantr 471 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  X  e.  B
)
246120adantr 471 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  Y  e.  B
)
24716adantr 471 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  .0.  .<  X )
248 simpr 467 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  .0.  .<  Y )
2497, 18, 17, 34, 8, 243, 244, 245, 246, 247, 248archirng 28556 . . 3  |-  ( (
ph  /\  .0.  .<  Y )  ->  E. n  e.  NN0  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
250 ssrexv 3506 . . 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 28478 . . 3  |-  ( ( W  e. Toset  /\  Y  e.  B  /\  .0.  e.  B )  ->  ( Y  =  .0.  \/  Y  .<  .0.  \/  .0.  .<  Y ) )
25329, 120, 33, 252syl3anc 1276 . 2  |-  ( ph  ->  ( Y  =  .0. 
\/  Y  .<  .0.  \/  .0.  .<  Y ) )
25458, 241, 251, 253mpjao3dan 1344 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 189    \/ wo 374    /\ wa 375    \/ w3o 990    /\ w3a 991    = wceq 1455    e. wcel 1898   E.wrex 2750   _Vcvv 3057    C_ wss 3416   class class class wbr 4418   ` cfv 5605  (class class class)co 6320   CCcc 9568   0cc0 9570   1c1 9571    + caddc 9573    - cmin 9891   -ucneg 9892   2c2 10692   NN0cn0 10903   ZZcz 10971   Basecbs 15176   +g cplusg 15245   lecple 15252   0gc0g 15393   Posetcpo 16240   ltcplt 16241  Tosetctos 16334   Grpcgrp 16724   invgcminusg 16725  .gcmg 16727  oppgcoppg 17051  oMndcomnd 28511  oGrpcogrp 28512  Archicarchi 28545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-tpos 7004  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-7 10706  df-8 10707  df-9 10708  df-10 10709  df-n0 10904  df-z 10972  df-uz 11194  df-fz 11820  df-seq 12252  df-ndx 15179  df-slot 15180  df-base 15181  df-sets 15182  df-plusg 15258  df-ple 15265  df-0g 15395  df-preset 16228  df-poset 16246  df-plt 16259  df-toset 16335  df-mgm 16543  df-sgrp 16582  df-mnd 16592  df-grp 16728  df-minusg 16729  df-mulg 16731  df-oppg 17052  df-omnd 28513  df-ogrp 28514  df-inftm 28546  df-archi 28547
This theorem is referenced by:  archiabllem2c  28563
  Copyright terms: Public domain W3C validator