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

Theorem archirngz 26139
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 10677 . . 3  |-  -u 1  e.  ZZ
2 archirng.1 . . . . . . . . . 10  |-  ( ph  ->  W  e. oGrp )
3 isogrp 26098 . . . . . . . . . . 11  |-  ( W  e. oGrp 
<->  ( W  e.  Grp  /\  W  e. oMnd ) )
43simplbi 457 . . . . . . . . . 10  |-  ( W  e. oGrp  ->  W  e.  Grp )
52, 4syl 16 . . . . . . . . 9  |-  ( ph  ->  W  e.  Grp )
6 1z 10672 . . . . . . . . . 10  |-  1  e.  ZZ
76a1i 11 . . . . . . . . 9  |-  ( ph  ->  1  e.  ZZ )
8 archirng.3 . . . . . . . . 9  |-  ( ph  ->  X  e.  B )
9 archirng.b . . . . . . . . . 10  |-  B  =  ( Base `  W
)
10 archirng.x . . . . . . . . . 10  |-  .x.  =  (.g
`  W )
11 eqid 2441 . . . . . . . . . 10  |-  ( invg `  W )  =  ( invg `  W )
129, 10, 11mulgneg 15638 . . . . . . . . 9  |-  ( ( W  e.  Grp  /\  1  e.  ZZ  /\  X  e.  B )  ->  ( -u 1  .x.  X )  =  ( ( invg `  W ) `
 ( 1  .x. 
X ) ) )
135, 7, 8, 12syl3anc 1213 . . . . . . . 8  |-  ( ph  ->  ( -u 1  .x. 
X )  =  ( ( invg `  W ) `  (
1  .x.  X )
) )
149, 10mulg1 15627 . . . . . . . . . 10  |-  ( X  e.  B  ->  (
1  .x.  X )  =  X )
158, 14syl 16 . . . . . . . . 9  |-  ( ph  ->  ( 1  .x.  X
)  =  X )
1615fveq2d 5692 . . . . . . . 8  |-  ( ph  ->  ( ( invg `  W ) `  (
1  .x.  X )
)  =  ( ( invg `  W
) `  X )
)
1713, 16eqtrd 2473 . . . . . . 7  |-  ( ph  ->  ( -u 1  .x. 
X )  =  ( ( invg `  W ) `  X
) )
18 archirng.5 . . . . . . . 8  |-  ( ph  ->  .0.  .<  X )
19 archirng.i . . . . . . . . . 10  |-  .<  =  ( lt `  W )
20 archirng.0 . . . . . . . . . 10  |-  .0.  =  ( 0g `  W )
219, 19, 11, 20ogrpinv0lt 26119 . . . . . . . . 9  |-  ( ( W  e. oGrp  /\  X  e.  B )  ->  (  .0.  .<  X  <->  ( ( invg `  W ) `
 X )  .<  .0.  ) )
2221biimpa 481 . . . . . . . 8  |-  ( ( ( W  e. oGrp  /\  X  e.  B )  /\  .0.  .<  X )  ->  ( ( invg `  W ) `  X
)  .<  .0.  )
232, 8, 18, 22syl21anc 1212 . . . . . . 7  |-  ( ph  ->  ( ( invg `  W ) `  X
)  .<  .0.  )
2417, 23eqbrtrd 4309 . . . . . 6  |-  ( ph  ->  ( -u 1  .x. 
X )  .<  .0.  )
2524adantr 462 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( -u
1  .x.  X )  .<  .0.  )
26 simpr 458 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  Y  =  .0.  )
2725, 26breqtrrd 4315 . . . 4  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( -u
1  .x.  X )  .<  Y )
283simprbi 461 . . . . . . . . 9  |-  ( W  e. oGrp  ->  W  e. oMnd )
29 omndtos 26101 . . . . . . . . 9  |-  ( W  e. oMnd  ->  W  e. Toset )
302, 28, 293syl 20 . . . . . . . 8  |-  ( ph  ->  W  e. Toset )
31 tospos 26052 . . . . . . . 8  |-  ( W  e. Toset  ->  W  e.  Poset )
3230, 31syl 16 . . . . . . 7  |-  ( ph  ->  W  e.  Poset )
339, 20grpidcl 15559 . . . . . . . 8  |-  ( W  e.  Grp  ->  .0.  e.  B )
342, 4, 333syl 20 . . . . . . 7  |-  ( ph  ->  .0.  e.  B )
35 archirng.l . . . . . . . 8  |-  .<_  =  ( le `  W )
369, 35posref 15117 . . . . . . 7  |-  ( ( W  e.  Poset  /\  .0.  e.  B )  ->  .0.  .<_  .0.  )
3732, 34, 36syl2anc 656 . . . . . 6  |-  ( ph  ->  .0.  .<_  .0.  )
3837adantr 462 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  .0.  .<_  .0.  )
39 1m1e0 10386 . . . . . . . . . 10  |-  ( 1  -  1 )  =  0
4039negeqi 9599 . . . . . . . . 9  |-  -u (
1  -  1 )  =  -u 0
41 ax-1cn 9336 . . . . . . . . . 10  |-  1  e.  CC
4241, 41negsubdii 9689 . . . . . . . . 9  |-  -u (
1  -  1 )  =  ( -u 1  +  1 )
43 neg0 9651 . . . . . . . . 9  |-  -u 0  =  0
4440, 42, 433eqtr3i 2469 . . . . . . . 8  |-  ( -u
1  +  1 )  =  0
4544oveq1i 6100 . . . . . . 7  |-  ( (
-u 1  +  1 )  .x.  X )  =  ( 0  .x. 
X )
469, 20, 10mulg0 15625 . . . . . . . 8  |-  ( X  e.  B  ->  (
0  .x.  X )  =  .0.  )
478, 46syl 16 . . . . . . 7  |-  ( ph  ->  ( 0  .x.  X
)  =  .0.  )
4845, 47syl5eq 2485 . . . . . 6  |-  ( ph  ->  ( ( -u 1  +  1 )  .x.  X )  =  .0.  )
4948adantr 462 . . . . 5  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( (
-u 1  +  1 )  .x.  X )  =  .0.  )
5038, 26, 493brtr4d 4319 . . . 4  |-  ( (
ph  /\  Y  =  .0.  )  ->  Y  .<_  ( ( -u 1  +  1 )  .x.  X
) )
5127, 50jca 529 . . 3  |-  ( (
ph  /\  Y  =  .0.  )  ->  ( (
-u 1  .x.  X
)  .<  Y  /\  Y  .<_  ( ( -u 1  +  1 )  .x.  X ) ) )
52 oveq1 6097 . . . . . 6  |-  ( n  =  -u 1  ->  (
n  .x.  X )  =  ( -u 1  .x.  X ) )
5352breq1d 4299 . . . . 5  |-  ( n  =  -u 1  ->  (
( n  .x.  X
)  .<  Y  <->  ( -u 1  .x.  X )  .<  Y ) )
54 oveq1 6097 . . . . . . 7  |-  ( n  =  -u 1  ->  (
n  +  1 )  =  ( -u 1  +  1 ) )
5554oveq1d 6105 . . . . . 6  |-  ( n  =  -u 1  ->  (
( n  +  1 )  .x.  X )  =  ( ( -u
1  +  1 ) 
.x.  X ) )
5655breq2d 4301 . . . . 5  |-  ( n  =  -u 1  ->  ( Y  .<_  ( ( n  +  1 )  .x.  X )  <->  Y  .<_  ( ( -u 1  +  1 )  .x.  X
) ) )
5753, 56anbi12d 705 . . . 4  |-  ( n  =  -u 1  ->  (
( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) )  <->  ( ( -u 1  .x.  X ) 
.<  Y  /\  Y  .<_  ( ( -u 1  +  1 )  .x.  X
) ) ) )
5857rspcev 3070 . . 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 ) ) )
591, 51, 58sylancr 658 . 2  |-  ( (
ph  /\  Y  =  .0.  )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) )
60 nn0ssz 10663 . . . . . . . . 9  |-  NN0  C_  ZZ
61 simpr 458 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  m  e.  NN0 )
6260, 61sseldi 3351 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  m  e.  ZZ )
6362ad2antrr 720 . . . . . . 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 )
6463znegcld 10745 . . . . . 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 )
65 2z 10674 . . . . . . 7  |-  2  e.  ZZ
6665a1i 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 )
6764, 66zsubcld 10748 . . . . 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 )
68 nn0cn 10585 . . . . . . . . . . 11  |-  ( m  e.  NN0  ->  m  e.  CC )
6961, 68syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  m  e.  CC )
70 2cnd 10390 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  2  e.  CC )
7169, 70negdi2d 9729 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u (
m  +  2 )  =  ( -u m  -  2 ) )
7271oveq1d 6105 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  .x.  X )  =  ( ( -u m  -  2 ) 
.x.  X ) )
732adantr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  .<  .0.  )  ->  W  e. oGrp )
7473adantr 462 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e. oGrp )
75 archirngz.1 . . . . . . . . . . . . 13  |-  ( ph  ->  (oppg
`  W )  e. oGrp
)
7675adantr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  .<  .0.  )  ->  (oppg
`  W )  e. oGrp
)
7776adantr 462 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (oppg `  W
)  e. oGrp )
7874, 77jca 529 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( W  e. oGrp  /\  (oppg `  W
)  e. oGrp ) )
795ad2antrr 720 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e.  Grp )
8062peano2zd 10746 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  1 )  e.  ZZ )
818adantr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  Y  .<  .0.  )  ->  X  e.  B )
8281adantr 462 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  X  e.  B )
839, 10mulgcl 15637 . . . . . . . . . . 11  |-  ( ( W  e.  Grp  /\  ( m  +  1
)  e.  ZZ  /\  X  e.  B )  ->  ( ( m  + 
1 )  .x.  X
)  e.  B )
8479, 80, 82, 83syl3anc 1213 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  1 )  .x.  X )  e.  B )
8565a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  2  e.  ZZ )
8662, 85zaddcld 10747 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  2 )  e.  ZZ )
879, 10mulgcl 15637 . . . . . . . . . . 11  |-  ( ( W  e.  Grp  /\  ( m  +  2
)  e.  ZZ  /\  X  e.  B )  ->  ( ( m  + 
2 )  .x.  X
)  e.  B )
8879, 86, 82, 87syl3anc 1213 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  2 )  .x.  X )  e.  B )
8979, 33syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  .0.  e.  B )
9018adantr 462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  Y  .<  .0.  )  ->  .0.  .<  X )
9190adantr 462 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  .0.  .<  X )
92 eqid 2441 . . . . . . . . . . . . 13  |-  ( +g  `  W )  =  ( +g  `  W )
939, 19, 92ogrpaddlt 26114 . . . . . . . . . . . 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 ) ) )
9474, 89, 82, 84, 91, 93syl131anc 1226 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (  .0.  ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  .< 
( X ( +g  `  W ) ( ( m  +  1 ) 
.x.  X ) ) )
959, 92, 20grplid 15561 . . . . . . . . . . . 12  |-  ( ( W  e.  Grp  /\  ( ( m  + 
1 )  .x.  X
)  e.  B )  ->  (  .0.  ( +g  `  W ) ( ( m  +  1 )  .x.  X ) )  =  ( ( m  +  1 ) 
.x.  X ) )
9679, 84, 95syl2anc 656 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (  .0.  ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  =  ( ( m  + 
1 )  .x.  X
) )
9741a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  NN0  ->  1  e.  CC )
9868, 97, 97addassd 9404 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN0  ->  ( ( m  +  1 )  +  1 )  =  ( m  +  ( 1  +  1 ) ) )
99 1p1e2 10431 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  1 )  =  2
10099oveq2i 6101 . . . . . . . . . . . . . . . 16  |-  ( m  +  ( 1  +  1 ) )  =  ( m  +  2 )
10198, 100syl6eq 2489 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( ( m  +  1 )  +  1 )  =  ( m  +  2 ) )
10268, 97addcld 9401 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN0  ->  ( m  +  1 )  e.  CC )
103102, 97addcomd 9567 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( ( m  +  1 )  +  1 )  =  ( 1  +  ( m  +  1 ) ) )
104101, 103eqtr3d 2475 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( m  +  2 )  =  ( 1  +  ( m  +  1 ) ) )
105104oveq1d 6105 . . . . . . . . . . . . 13  |-  ( m  e.  NN0  ->  ( ( m  +  2 ) 
.x.  X )  =  ( ( 1  +  ( m  +  1 ) )  .x.  X
) )
10661, 105syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  2 )  .x.  X )  =  ( ( 1  +  ( m  + 
1 ) )  .x.  X ) )
1076a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  1  e.  ZZ )
1089, 10, 92mulgdir 15645 . . . . . . . . . . . . 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 ) ) )
10979, 107, 80, 82, 108syl13anc 1215 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( 1  +  ( m  +  1 ) )  .x.  X )  =  ( ( 1 
.x.  X ) ( +g  `  W ) ( ( m  + 
1 )  .x.  X
) ) )
11082, 14syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
1  .x.  X )  =  X )
111110oveq1d 6105 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( 1  .x.  X
) ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  =  ( X ( +g  `  W ) ( ( m  +  1 ) 
.x.  X ) ) )
112106, 109, 1113eqtrrd 2478 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( X ( +g  `  W
) ( ( m  +  1 )  .x.  X ) )  =  ( ( m  + 
2 )  .x.  X
) )
11394, 96, 1123brtr3d 4318 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  1 )  .x.  X ) 
.<  ( ( m  + 
2 )  .x.  X
) )
1149, 19, 11ogrpinvlt 26120 . . . . . . . . . . 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 ) ) ) )
115114biimpa 481 . . . . . . . . . 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 ) ) )
11678, 84, 88, 113, 115syl31anc 1216 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( invg `  W ) `  (
( m  +  2 )  .x.  X ) )  .<  ( ( invg `  W ) `
 ( ( m  +  1 )  .x.  X ) ) )
1179, 10, 11mulgneg 15638 . . . . . . . . . 10  |-  ( ( W  e.  Grp  /\  ( m  +  2
)  e.  ZZ  /\  X  e.  B )  ->  ( -u ( m  +  2 )  .x.  X )  =  ( ( invg `  W ) `  (
( m  +  2 )  .x.  X ) ) )
11879, 86, 82, 117syl3anc 1213 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  .x.  X )  =  ( ( invg `  W ) `
 ( ( m  +  2 )  .x.  X ) ) )
1199, 10, 11mulgneg 15638 . . . . . . . . . 10  |-  ( ( W  e.  Grp  /\  ( m  +  1
)  e.  ZZ  /\  X  e.  B )  ->  ( -u ( m  +  1 )  .x.  X )  =  ( ( invg `  W ) `  (
( m  +  1 )  .x.  X ) ) )
12079, 80, 82, 119syl3anc 1213 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  1 )  .x.  X )  =  ( ( invg `  W ) `
 ( ( m  +  1 )  .x.  X ) ) )
121116, 118, 1203brtr4d 4319 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  .x.  X ) 
.<  ( -u ( m  +  1 )  .x.  X ) )
12272, 121eqbrtrrd 4311 . . . . . . 7  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u m  -  2 )  .x.  X ) 
.<  ( -u ( m  +  1 )  .x.  X ) )
123122ad2antrr 720 . . . . . 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
) )
124120ad2antrr 720 . . . . . . 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 ) ) )
12532ad4antr 726 . . . . . . . . 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 )
126 archirng.4 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  B )
1279, 11grpinvcl 15576 . . . . . . . . . . . . 13  |-  ( ( W  e.  Grp  /\  Y  e.  B )  ->  ( ( invg `  W ) `  Y
)  e.  B )
1285, 126, 127syl2anc 656 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( invg `  W ) `  Y
)  e.  B )
129128adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  Y  .<  .0.  )  ->  ( ( invg `  W ) `
 Y )  e.  B )
130129adantr 462 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( invg `  W ) `  Y
)  e.  B )
131130ad2antrr 720 . . . . . . . . 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 )
13284ad2antrr 720 . . . . . . . . 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
)
133 simplrr 755 . . . . . . . . 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
) )
134 simpr 458 . . . . . . . . 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 )
)
1359, 35posasymb 15118 . . . . . . . . . 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
) ) )
136135biimpa 481 . . . . . . . . 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 ) )
137125, 131, 132, 133, 134, 136syl32anc 1221 . . . . . . . 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
) )
138137fveq2d 5692 . . . . . . 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 ) ) )
1399, 11grpinvinv 15586 . . . . . . . . 9  |-  ( ( W  e.  Grp  /\  Y  e.  B )  ->  ( ( invg `  W ) `  (
( invg `  W ) `  Y
) )  =  Y )
1405, 126, 139syl2anc 656 . . . . . . . 8  |-  ( ph  ->  ( ( invg `  W ) `  (
( invg `  W ) `  Y
) )  =  Y )
141140ad4antr 726 . . . . . . 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 )
142124, 138, 1413eqtr2rd 2480 . . . . . 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
) )
143123, 142breqtrrd 4315 . . . . 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 )
14441a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  1  e.  CC )
14569, 70, 144addsubassd 9735 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  +  2 )  -  1 )  =  ( m  +  ( 2  -  1 ) ) )
146 2m1e1 10432 . . . . . . . . . . . . 13  |-  ( 2  -  1 )  =  1
147146oveq2i 6101 . . . . . . . . . . . 12  |-  ( m  +  ( 2  -  1 ) )  =  ( m  +  1 )
148145, 147syl6req 2490 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  1 )  =  ( ( m  +  2 )  - 
1 ) )
149148negeqd 9600 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u (
m  +  1 )  =  -u ( ( m  +  2 )  - 
1 ) )
15069, 70addcld 9401 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  +  2 )  e.  CC )
151150, 144negsubdid 9730 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u (
( m  +  2 )  -  1 )  =  ( -u (
m  +  2 )  +  1 ) )
15271oveq1d 6105 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  2 )  +  1 )  =  ( ( -u m  -  2 )  +  1 ) )
153149, 151, 1523eqtrrd 2478 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u m  -  2 )  +  1 )  =  -u ( m  + 
1 ) )
154153oveq1d 6105 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  =  ( -u ( m  +  1
)  .x.  X )
)
15530ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e. Toset )
156155, 31syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  W  e.  Poset )
15762znegcld 10745 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  -u m  e.  ZZ )
158157, 85zsubcld 10748 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u m  -  2 )  e.  ZZ )
159158peano2zd 10746 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u m  -  2 )  +  1 )  e.  ZZ )
1609, 10mulgcl 15637 . . . . . . . . . 10  |-  ( ( W  e.  Grp  /\  ( ( -u m  -  2 )  +  1 )  e.  ZZ  /\  X  e.  B )  ->  ( ( (
-u m  -  2 )  +  1 ) 
.x.  X )  e.  B )
16179, 159, 82, 160syl3anc 1213 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  e.  B )
1629, 35posref 15117 . . . . . . . . 9  |-  ( ( W  e.  Poset  /\  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  e.  B )  ->  ( ( (
-u m  -  2 )  +  1 ) 
.x.  X )  .<_  ( ( ( -u m  -  2 )  +  1 )  .x.  X ) )
163156, 161, 162syl2anc 656 . . . . . . . 8  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( -u m  -  2 )  +  1 )  .x.  X
)  .<_  ( ( (
-u m  -  2 )  +  1 ) 
.x.  X ) )
164154, 163eqbrtrrd 4311 . . . . . . 7  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u ( m  +  1 )  .x.  X ) 
.<_  ( ( ( -u m  -  2 )  +  1 )  .x.  X ) )
165164ad2antrr 720 . . . . . 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 ) )
166142, 165eqbrtrd 4309 . . . . 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 ) )
167 oveq1 6097 . . . . . . . 8  |-  ( n  =  ( -u m  -  2 )  -> 
( n  .x.  X
)  =  ( (
-u m  -  2 )  .x.  X ) )
168167breq1d 4299 . . . . . . 7  |-  ( n  =  ( -u m  -  2 )  -> 
( ( n  .x.  X )  .<  Y  <->  ( ( -u m  -  2 ) 
.x.  X )  .<  Y ) )
169 oveq1 6097 . . . . . . . . 9  |-  ( n  =  ( -u m  -  2 )  -> 
( n  +  1 )  =  ( (
-u m  -  2 )  +  1 ) )
170169oveq1d 6105 . . . . . . . 8  |-  ( n  =  ( -u m  -  2 )  -> 
( ( n  + 
1 )  .x.  X
)  =  ( ( ( -u m  - 
2 )  +  1 )  .x.  X ) )
171170breq2d 4301 . . . . . . 7  |-  ( n  =  ( -u m  -  2 )  -> 
( Y  .<_  ( ( n  +  1 ) 
.x.  X )  <->  Y  .<_  ( ( ( -u m  -  2 )  +  1 )  .x.  X
) ) )
172168, 171anbi12d 705 . . . . . 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 ) ) ) )
173172rspcev 3070 . . . . 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 ) ) )
17467, 143, 166, 173syl12anc 1211 . . . 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 ) ) )
17580ad2antrr 720 . . . . . 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 )
176175znegcld 10745 . . . . 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 )
17773adantr 462 . . . . . . . . 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 )
17876adantr 462 . . . . . . . . 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
)
179177, 178jca 529 . . . . . . . 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
) )
1801793anassrs 1204 . . . . . . 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 )
)
181130ad2antrr 720 . . . . . . 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 )
18284ad2antrr 720 . . . . . . 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 )
183 simpr 458 . . . . . . 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 ) )
1849, 19, 11ogrpinvlt 26120 . . . . . . . 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
) ) ) )
185184biimpa 481 . . . . . . 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 ) ) )
186180, 181, 182, 183, 185syl31anc 1216 . . . . . 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 ) ) )
187120ad2antrr 720 . . . . . . 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 ) ) )
188187eqcomd 2446 . . . . . 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 )
)
189140ad4antr 726 . . . . . 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 )
190186, 188, 1893brtr3d 4318 . . . . 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 )
191 simp-4l 760 . . . . . 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 )
1929, 10mulgcl 15637 . . . . . . . . . . . 12  |-  ( ( W  e.  Grp  /\  m  e.  ZZ  /\  X  e.  B )  ->  (
m  .x.  X )  e.  B )
19379, 62, 82, 192syl3anc 1213 . . . . . . . . . . 11  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
m  .x.  X )  e.  B )
1949, 19, 11ogrpinvlt 26120 . . . . . . . . . . 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 )
) ) )
19578, 193, 130, 194syl3anc 1213 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( m  .x.  X
)  .<  ( ( invg `  W ) `
 Y )  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  ( ( invg `  W ) `  (
m  .x.  X )
) ) )
196195biimpa 481 . . . . . . . . 9  |-  ( ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  /\  ( m  .x.  X ) 
.<  ( ( invg `  W ) `  Y
) )  ->  (
( invg `  W ) `  (
( invg `  W ) `  Y
) )  .<  (
( invg `  W ) `  (
m  .x.  X )
) )
197196adantrr 711 . . . . . . . 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 )
) )
198197adantr 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 ) `  (
( invg `  W ) `  Y
) )  .<  (
( invg `  W ) `  (
m  .x.  X )
) )
199 negdi 9662 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  CC  /\  1  e.  CC )  -> 
-u ( m  + 
1 )  =  (
-u m  +  -u
1 ) )
20068, 41, 199sylancl 657 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  -u (
m  +  1 )  =  ( -u m  +  -u 1 ) )
201200oveq1d 6105 . . . . . . . . . . . . 13  |-  ( m  e.  NN0  ->  ( -u ( m  +  1
)  +  1 )  =  ( ( -u m  +  -u 1 )  +  1 ) )
20268negcld 9702 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  -u m  e.  CC )
20397negcld 9702 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  -u 1  e.  CC )
204202, 203, 97addassd 9404 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( (
-u m  +  -u
1 )  +  1 )  =  ( -u m  +  ( -u 1  +  1 ) ) )
20544oveq2i 6101 . . . . . . . . . . . . . . 15  |-  ( -u m  +  ( -u 1  +  1 ) )  =  ( -u m  +  0 )
206205a1i 11 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( -u m  +  ( -u 1  +  1 ) )  =  ( -u m  +  0 ) )
207202addid1d 9565 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( -u m  +  0 )  =  -u m )
208204, 206, 2073eqtrd 2477 . . . . . . . . . . . . 13  |-  ( m  e.  NN0  ->  ( (
-u m  +  -u
1 )  +  1 )  =  -u m
)
209201, 208eqtrd 2473 . . . . . . . . . . . 12  |-  ( m  e.  NN0  ->  ( -u ( m  +  1
)  +  1 )  =  -u m )
210209oveq1d 6105 . . . . . . . . . . 11  |-  ( m  e.  NN0  ->  ( (
-u ( m  + 
1 )  +  1 )  .x.  X )  =  ( -u m  .x.  X ) )
21161, 210syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  =  ( -u m  .x.  X ) )
2129, 10, 11mulgneg 15638 . . . . . . . . . . 11  |-  ( ( W  e.  Grp  /\  m  e.  ZZ  /\  X  e.  B )  ->  ( -u m  .x.  X )  =  ( ( invg `  W ) `
 ( m  .x.  X ) ) )
21379, 62, 82, 212syl3anc 1213 . . . . . . . . . 10  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  ( -u m  .x.  X )  =  ( ( invg `  W ) `
 ( m  .x.  X ) ) )
214211, 213eqtrd 2473 . . . . . . . . 9  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  =  ( ( invg `  W ) `
 ( m  .x.  X ) ) )
215214ad2antrr 720 . . . . . . . 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 )
) )
216215eqcomd 2446 . . . . . . 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 ) )
217198, 189, 2163brtr3d 4318 . . . . . 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 ) )
218 ovex 6115 . . . . . . . . 9  |-  ( (
-u ( m  + 
1 )  +  1 )  .x.  X )  e.  _V
219218a1i 11 . . . . . . . 8  |-  ( ph  ->  ( ( -u (
m  +  1 )  +  1 )  .x.  X )  e.  _V )
22035, 19pltle 15127 . . . . . . . 8  |-  ( ( 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 ) ) )
2212, 126, 219, 220syl3anc 1213 . . . . . . 7  |-  ( ph  ->  ( Y  .<  (
( -u ( m  + 
1 )  +  1 )  .x.  X )  ->  Y  .<_  ( (
-u ( m  + 
1 )  +  1 )  .x.  X ) ) )
222221imp 429 . . . . . 6  |-  ( (
ph  /\  Y  .<  ( ( -u ( m  +  1 )  +  1 )  .x.  X
) )  ->  Y  .<_  ( ( -u (
m  +  1 )  +  1 )  .x.  X ) )
223191, 217, 222syl2anc 656 . . . . 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 ) )
224 oveq1 6097 . . . . . . . 8  |-  ( n  =  -u ( m  + 
1 )  ->  (
n  .x.  X )  =  ( -u (
m  +  1 ) 
.x.  X ) )
225224breq1d 4299 . . . . . . 7  |-  ( n  =  -u ( m  + 
1 )  ->  (
( n  .x.  X
)  .<  Y  <->  ( -u (
m  +  1 ) 
.x.  X )  .<  Y ) )
226 oveq1 6097 . . . . . . . . 9  |-  ( n  =  -u ( m  + 
1 )  ->  (
n  +  1 )  =  ( -u (
m  +  1 )  +  1 ) )
227226oveq1d 6105 . . . . . . . 8  |-  ( n  =  -u ( m  + 
1 )  ->  (
( n  +  1 )  .x.  X )  =  ( ( -u ( m  +  1
)  +  1 ) 
.x.  X ) )
228227breq2d 4301 . . . . . . 7  |-  ( n  =  -u ( m  + 
1 )  ->  ( Y  .<_  ( ( n  +  1 )  .x.  X )  <->  Y  .<_  ( ( -u ( m  +  1 )  +  1 )  .x.  X
) ) )
229225, 228anbi12d 705 . . . . . 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
) ) ) )
230229rspcev 3070 . . . . 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 ) ) )
231176, 190, 223, 230syl12anc 1211 . . . 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 ) ) )
2329, 35, 19tlt2 26058 . . . . . 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
) ) )
233155, 84, 130, 232syl3anc 1213 . . . . 5  |-  ( ( ( ph  /\  Y  .<  .0.  )  /\  m  e.  NN0 )  ->  (
( ( m  + 
1 )  .x.  X
)  .<_  ( ( invg `  W ) `
 Y )  \/  ( ( invg `  W ) `  Y
)  .<  ( ( m  +  1 )  .x.  X ) ) )
234233adantr 462 . . . 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 ) ) )
235174, 231, 234mpjaodan 779 . . 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 ) ) )
236 archirng.2 . . . . 5  |-  ( ph  ->  W  e. Archi )
237236adantr 462 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  W  e. Archi )
238140breq1d 4299 . . . . . 6  |-  ( ph  ->  ( ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  <->  Y  .<  .0.  )
)
239238biimpar 482 . . . . 5  |-  ( (
ph  /\  Y  .<  .0.  )  ->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  )
2409, 19, 11, 20ogrpinv0lt 26119 . . . . . . 7  |-  ( ( W  e. oGrp  /\  (
( invg `  W ) `  Y
)  e.  B )  ->  (  .0.  .<  ( ( invg `  W ) `  Y
)  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  ) )
2412, 128, 240syl2anc 656 . . . . . 6  |-  ( ph  ->  (  .0.  .<  (
( invg `  W ) `  Y
)  <->  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  ) )
242241biimpar 482 . . . . 5  |-  ( (
ph  /\  ( ( invg `  W ) `
 ( ( invg `  W ) `
 Y ) ) 
.<  .0.  )  ->  .0.  .< 
( ( invg `  W ) `  Y
) )
243239, 242syldan 467 . . . 4  |-  ( (
ph  /\  Y  .<  .0.  )  ->  .0.  .<  (
( invg `  W ) `  Y
) )
2449, 20, 19, 35, 10, 73, 237, 81, 129, 90, 243archirng 26138 . . 3  |-  ( (
ph  /\  Y  .<  .0.  )  ->  E. m  e.  NN0  ( ( m 
.x.  X )  .< 
( ( invg `  W ) `  Y
)  /\  ( ( invg `  W ) `
 Y )  .<_  ( ( m  + 
1 )  .x.  X
) ) )
245235, 244r19.29a 2860 . 2  |-  ( (
ph  /\  Y  .<  .0.  )  ->  E. n  e.  ZZ  ( ( n 
.x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 ) 
.x.  X ) ) )
2462adantr 462 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  W  e. oGrp )
247236adantr 462 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  W  e. Archi )
2488adantr 462 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  X  e.  B
)
249126adantr 462 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  Y  e.  B
)
25018adantr 462 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  .0.  .<  X )
251 simpr 458 . . . 4  |-  ( (
ph  /\  .0.  .<  Y )  ->  .0.  .<  Y )
2529, 20, 19, 35, 10, 246, 247, 248, 249, 250, 251archirng 26138 . . 3  |-  ( (
ph  /\  .0.  .<  Y )  ->  E. n  e.  NN0  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
253 ssrexv 3414 . . 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 ) ) ) )
25460, 252, 253mpsyl 63 . 2  |-  ( (
ph  /\  .0.  .<  Y )  ->  E. n  e.  ZZ  ( ( n  .x.  X )  .<  Y  /\  Y  .<_  ( ( n  +  1 )  .x.  X ) ) )
2559, 19tlt3 26059 . . 3  |-  ( ( W  e. Toset  /\  Y  e.  B  /\  .0.  e.  B )  ->  ( Y  =  .0.  \/  Y  .<  .0.  \/  .0.  .<  Y ) )
25630, 126, 34, 255syl3anc 1213 . 2  |-  ( ph  ->  ( Y  =  .0. 
\/  Y  .<  .0.  \/  .0.  .<  Y ) )
25759, 245, 254, 256mpjao3dan 1280 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 184    \/ wo 368    /\ wa 369    \/ w3o 959    /\ w3a 960    = wceq 1364    e. wcel 1761   E.wrex 2714   _Vcvv 2970    C_ wss 3325   class class class wbr 4289   ` cfv 5415  (class class class)co 6090   CCcc 9276   0cc0 9278   1c1 9279    + caddc 9281    - cmin 9591   -ucneg 9592   2c2 10367   NN0cn0 10575   ZZcz 10642   Basecbs 14170   +g cplusg 14234   lecple 14241   0gc0g 14374   Posetcpo 15106   ltcplt 15107  Tosetctos 15199   Grpcgrp 15406   invgcminusg 15407  .gcmg 15410  oppgcoppg 15853  oMndcomnd 26093  oGrpcogrp 26094  Archicarchi 26127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-tpos 6744  df-recs 6828  df-rdg 6862  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-nn 10319  df-2 10376  df-3 10377  df-4 10378  df-5 10379  df-6 10380  df-7 10381  df-8 10382  df-9 10383  df-10 10384  df-n0 10576  df-z 10643  df-uz 10858  df-fz 11434  df-seq 11803  df-ndx 14173  df-slot 14174  df-base 14175  df-sets 14176  df-plusg 14247  df-ple 14254  df-0g 14376  df-poset 15112  df-plt 15124  df-toset 15200  df-mnd 15411  df-grp 15538  df-minusg 15539  df-mulg 15541  df-oppg 15854  df-omnd 26095  df-ogrp 26096  df-inftm 26128  df-archi 26129
This theorem is referenced by:  archiabllem2c  26145
  Copyright terms: Public domain W3C validator