This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem archirngz

Description: Property of Archimedean left and right ordered groups. (Contributed by Thierry Arnoux, 6-May-2018)

Ref Expression
Hypotheses 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 archirngz 
|- ( ph -> E. n e. ZZ ( ( n .x. X ) .< Y /\ Y .<_ ( ( n + 1 ) .x. X ) ) )

Proof

Step Hyp Ref Expression
1 archirng.b 
 |-  B = ( Base ` W )
2 archirng.0 
 |-  .0. = ( 0g ` W )
3 archirng.i 
 |-  .< = ( lt ` W )
4 archirng.l 
 |-  .<_ = ( le ` W )
5 archirng.x 
 |-  .x. = ( .g ` W )
6 archirng.1 
 |-  ( ph -> W e. oGrp )
7 archirng.2 
 |-  ( ph -> W e. Archi )
8 archirng.3 
 |-  ( ph -> X e. B )
9 archirng.4 
 |-  ( ph -> Y e. B )
10 archirng.5 
 |-  ( ph -> .0. .< X )
11 archirngz.1 
 |-  ( ph -> ( oppG ` W ) e. oGrp )
12 neg1z 
 |-  -u 1 e. ZZ
13 ogrpgrp 
 |-  ( W e. oGrp -> W e. Grp )
14 6 13 syl 
 |-  ( ph -> W e. Grp )
15 1zzd 
 |-  ( ph -> 1 e. ZZ )
16 eqid 
 |-  ( invg ` W ) = ( invg ` W )
17 1 5 16 mulgneg 
 |-  ( ( W e. Grp /\ 1 e. ZZ /\ X e. B ) -> ( -u 1 .x. X ) = ( ( invg ` W ) ` ( 1 .x. X ) ) )
18 14 15 8 17 syl3anc 
 |-  ( ph -> ( -u 1 .x. X ) = ( ( invg ` W ) ` ( 1 .x. X ) ) )
19 1 5 mulg1 
 |-  ( X e. B -> ( 1 .x. X ) = X )
20 8 19 syl 
 |-  ( ph -> ( 1 .x. X ) = X )
21 20 fveq2d 
 |-  ( ph -> ( ( invg ` W ) ` ( 1 .x. X ) ) = ( ( invg ` W ) ` X ) )
22 18 21 eqtrd 
 |-  ( ph -> ( -u 1 .x. X ) = ( ( invg ` W ) ` X ) )
23 1 3 16 2 ogrpinv0lt 
 |-  ( ( W e. oGrp /\ X e. B ) -> ( .0. .< X <-> ( ( invg ` W ) ` X ) .< .0. ) )
24 23 biimpa 
 |-  ( ( ( W e. oGrp /\ X e. B ) /\ .0. .< X ) -> ( ( invg ` W ) ` X ) .< .0. )
25 6 8 10 24 syl21anc 
 |-  ( ph -> ( ( invg ` W ) ` X ) .< .0. )
26 22 25 eqbrtrd 
 |-  ( ph -> ( -u 1 .x. X ) .< .0. )
27 26 adantr 
 |-  ( ( ph /\ Y = .0. ) -> ( -u 1 .x. X ) .< .0. )
28 simpr 
 |-  ( ( ph /\ Y = .0. ) -> Y = .0. )
29 27 28 breqtrrd 
 |-  ( ( ph /\ Y = .0. ) -> ( -u 1 .x. X ) .< Y )
30 isogrp 
 |-  ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) )
31 30 simprbi 
 |-  ( W e. oGrp -> W e. oMnd )
32 omndtos 
 |-  ( W e. oMnd -> W e. Toset )
33 6 31 32 3syl 
 |-  ( ph -> W e. Toset )
34 tospos 
 |-  ( W e. Toset -> W e. Poset )
35 33 34 syl 
 |-  ( ph -> W e. Poset )
36 1 2 grpidcl 
 |-  ( W e. Grp -> .0. e. B )
37 6 13 36 3syl 
 |-  ( ph -> .0. e. B )
38 1 4 posref 
 |-  ( ( W e. Poset /\ .0. e. B ) -> .0. .<_ .0. )
39 35 37 38 syl2anc 
 |-  ( ph -> .0. .<_ .0. )
40 39 adantr 
 |-  ( ( ph /\ Y = .0. ) -> .0. .<_ .0. )
41 1m1e0 
 |-  ( 1 - 1 ) = 0
42 41 negeqi 
 |-  -u ( 1 - 1 ) = -u 0
43 ax-1cn 
 |-  1 e. CC
44 43 43 negsubdii 
 |-  -u ( 1 - 1 ) = ( -u 1 + 1 )
45 neg0 
 |-  -u 0 = 0
46 42 44 45 3eqtr3i 
 |-  ( -u 1 + 1 ) = 0
47 46 oveq1i 
 |-  ( ( -u 1 + 1 ) .x. X ) = ( 0 .x. X )
48 1 2 5 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = .0. )
49 8 48 syl 
 |-  ( ph -> ( 0 .x. X ) = .0. )
50 47 49 eqtrid 
 |-  ( ph -> ( ( -u 1 + 1 ) .x. X ) = .0. )
51 50 adantr 
 |-  ( ( ph /\ Y = .0. ) -> ( ( -u 1 + 1 ) .x. X ) = .0. )
52 40 28 51 3brtr4d 
 |-  ( ( ph /\ Y = .0. ) -> Y .<_ ( ( -u 1 + 1 ) .x. X ) )
53 29 52 jca 
 |-  ( ( ph /\ Y = .0. ) -> ( ( -u 1 .x. X ) .< Y /\ Y .<_ ( ( -u 1 + 1 ) .x. X ) ) )
54 oveq1 
 |-  ( n = -u 1 -> ( n .x. X ) = ( -u 1 .x. X ) )
55 54 breq1d 
 |-  ( n = -u 1 -> ( ( n .x. X ) .< Y <-> ( -u 1 .x. X ) .< Y ) )
56 oveq1 
 |-  ( n = -u 1 -> ( n + 1 ) = ( -u 1 + 1 ) )
57 56 oveq1d 
 |-  ( n = -u 1 -> ( ( n + 1 ) .x. X ) = ( ( -u 1 + 1 ) .x. X ) )
58 57 breq2d 
 |-  ( n = -u 1 -> ( Y .<_ ( ( n + 1 ) .x. X ) <-> Y .<_ ( ( -u 1 + 1 ) .x. X ) ) )
59 55 58 anbi12d 
 |-  ( n = -u 1 -> ( ( ( n .x. X ) .< Y /\ Y .<_ ( ( n + 1 ) .x. X ) ) <-> ( ( -u 1 .x. X ) .< Y /\ Y .<_ ( ( -u 1 + 1 ) .x. X ) ) ) )
60 59 rspcev 
 |-  ( ( -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 ) ) )
61 12 53 60 sylancr 
 |-  ( ( ph /\ Y = .0. ) -> E. n e. ZZ ( ( n .x. X ) .< Y /\ Y .<_ ( ( n + 1 ) .x. X ) ) )
62 simpr 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> m e. NN0 )
63 62 nn0zd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> m e. ZZ )
64 63 ad2antrr 
 |-  ( ( ( ( ( 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 )
65 64 znegcld 
 |-  ( ( ( ( ( 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 )
66 2z 
 |-  2 e. ZZ
67 66 a1i 
 |-  ( ( ( ( ( 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 )
68 65 67 zsubcld 
 |-  ( ( ( ( ( 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 )
69 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
70 69 adantl 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> m e. CC )
71 2cnd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> 2 e. CC )
72 70 71 negdi2d 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> -u ( m + 2 ) = ( -u m - 2 ) )
73 72 oveq1d 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( -u ( m + 2 ) .x. X ) = ( ( -u m - 2 ) .x. X ) )
74 6 ad2antrr 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> W e. oGrp )
75 11 ad2antrr 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( oppG ` W ) e. oGrp )
76 74 75 jca 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( W e. oGrp /\ ( oppG ` W ) e. oGrp ) )
77 14 ad2antrr 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> W e. Grp )
78 63 peano2zd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( m + 1 ) e. ZZ )
79 8 ad2antrr 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> X e. B )
80 1 5 mulgcl 
 |-  ( ( W e. Grp /\ ( m + 1 ) e. ZZ /\ X e. B ) -> ( ( m + 1 ) .x. X ) e. B )
81 77 78 79 80 syl3anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( m + 1 ) .x. X ) e. B )
82 66 a1i 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> 2 e. ZZ )
83 63 82 zaddcld 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( m + 2 ) e. ZZ )
84 1 5 mulgcl 
 |-  ( ( W e. Grp /\ ( m + 2 ) e. ZZ /\ X e. B ) -> ( ( m + 2 ) .x. X ) e. B )
85 77 83 79 84 syl3anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( m + 2 ) .x. X ) e. B )
86 77 36 syl 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> .0. e. B )
87 10 ad2antrr 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> .0. .< X )
88 eqid 
 |-  ( +g ` W ) = ( +g ` W )
89 1 3 88 ogrpaddlt 
 |-  ( ( 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 ) ) )
90 74 86 79 81 87 89 syl131anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( .0. ( +g ` W ) ( ( m + 1 ) .x. X ) ) .< ( X ( +g ` W ) ( ( m + 1 ) .x. X ) ) )
91 1 88 2 grplid 
 |-  ( ( W e. Grp /\ ( ( m + 1 ) .x. X ) e. B ) -> ( .0. ( +g ` W ) ( ( m + 1 ) .x. X ) ) = ( ( m + 1 ) .x. X ) )
92 77 81 91 syl2anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( .0. ( +g ` W ) ( ( m + 1 ) .x. X ) ) = ( ( m + 1 ) .x. X ) )
93 1cnd 
 |-  ( m e. NN0 -> 1 e. CC )
94 69 93 93 addassd 
 |-  ( m e. NN0 -> ( ( m + 1 ) + 1 ) = ( m + ( 1 + 1 ) ) )
95 1p1e2 
 |-  ( 1 + 1 ) = 2
96 95 oveq2i 
 |-  ( m + ( 1 + 1 ) ) = ( m + 2 )
97 94 96 eqtrdi 
 |-  ( m e. NN0 -> ( ( m + 1 ) + 1 ) = ( m + 2 ) )
98 69 93 addcld 
 |-  ( m e. NN0 -> ( m + 1 ) e. CC )
99 98 93 addcomd 
 |-  ( m e. NN0 -> ( ( m + 1 ) + 1 ) = ( 1 + ( m + 1 ) ) )
100 97 99 eqtr3d 
 |-  ( m e. NN0 -> ( m + 2 ) = ( 1 + ( m + 1 ) ) )
101 100 oveq1d 
 |-  ( m e. NN0 -> ( ( m + 2 ) .x. X ) = ( ( 1 + ( m + 1 ) ) .x. X ) )
102 101 adantl 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( m + 2 ) .x. X ) = ( ( 1 + ( m + 1 ) ) .x. X ) )
103 1zzd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> 1 e. ZZ )
104 1 5 88 mulgdir 
 |-  ( ( 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 ) ) )
105 77 103 78 79 104 syl13anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( 1 + ( m + 1 ) ) .x. X ) = ( ( 1 .x. X ) ( +g ` W ) ( ( m + 1 ) .x. X ) ) )
106 79 19 syl 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( 1 .x. X ) = X )
107 106 oveq1d 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( 1 .x. X ) ( +g ` W ) ( ( m + 1 ) .x. X ) ) = ( X ( +g ` W ) ( ( m + 1 ) .x. X ) ) )
108 102 105 107 3eqtrrd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( X ( +g ` W ) ( ( m + 1 ) .x. X ) ) = ( ( m + 2 ) .x. X ) )
109 90 92 108 3brtr3d 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( m + 1 ) .x. X ) .< ( ( m + 2 ) .x. X ) )
110 1 3 16 ogrpinvlt 
 |-  ( ( ( 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 ) ) ) )
111 110 biimpa 
 |-  ( ( ( ( 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 ) ) )
112 76 81 85 109 111 syl31anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( invg ` W ) ` ( ( m + 2 ) .x. X ) ) .< ( ( invg ` W ) ` ( ( m + 1 ) .x. X ) ) )
113 1 5 16 mulgneg 
 |-  ( ( W e. Grp /\ ( m + 2 ) e. ZZ /\ X e. B ) -> ( -u ( m + 2 ) .x. X ) = ( ( invg ` W ) ` ( ( m + 2 ) .x. X ) ) )
114 77 83 79 113 syl3anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( -u ( m + 2 ) .x. X ) = ( ( invg ` W ) ` ( ( m + 2 ) .x. X ) ) )
115 1 5 16 mulgneg 
 |-  ( ( W e. Grp /\ ( m + 1 ) e. ZZ /\ X e. B ) -> ( -u ( m + 1 ) .x. X ) = ( ( invg ` W ) ` ( ( m + 1 ) .x. X ) ) )
116 77 78 79 115 syl3anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( -u ( m + 1 ) .x. X ) = ( ( invg ` W ) ` ( ( m + 1 ) .x. X ) ) )
117 112 114 116 3brtr4d 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( -u ( m + 2 ) .x. X ) .< ( -u ( m + 1 ) .x. X ) )
118 73 117 eqbrtrrd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( -u m - 2 ) .x. X ) .< ( -u ( m + 1 ) .x. X ) )
119 118 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
120 116 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) )
121 35 ad4antr 
 |-  ( ( ( ( ( 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 )
122 1 16 grpinvcl 
 |-  ( ( W e. Grp /\ Y e. B ) -> ( ( invg ` W ) ` Y ) e. B )
123 14 9 122 syl2anc 
 |-  ( ph -> ( ( invg ` W ) ` Y ) e. B )
124 123 ad2antrr 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( invg ` W ) ` Y ) e. B )
125 124 ad2antrr 
 |-  ( ( ( ( ( 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 )
126 81 ad2antrr 
 |-  ( ( ( ( ( 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 )
127 simplrr 
 |-  ( ( ( ( ( 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 ) )
128 simpr 
 |-  ( ( ( ( ( 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 ) )
129 1 4 posasymb 
 |-  ( ( 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 ) ) )
130 129 biimpa 
 |-  ( ( ( 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 ) )
131 121 125 126 127 128 130 syl32anc 
 |-  ( ( ( ( ( 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 ) )
132 131 fveq2d 
 |-  ( ( ( ( ( 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 ) ) )
133 1 16 grpinvinv 
 |-  ( ( W e. Grp /\ Y e. B ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Y ) ) = Y )
134 14 9 133 syl2anc 
 |-  ( ph -> ( ( invg ` W ) ` ( ( invg ` W ) ` Y ) ) = Y )
135 134 ad4antr 
 |-  ( ( ( ( ( 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 )
136 120 132 135 3eqtr2rd 
 |-  ( ( ( ( ( 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 ) )
137 119 136 breqtrrd 
 |-  ( ( ( ( ( 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 )
138 1cnd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> 1 e. CC )
139 70 71 138 addsubassd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( m + 2 ) - 1 ) = ( m + ( 2 - 1 ) ) )
140 2m1e1 
 |-  ( 2 - 1 ) = 1
141 140 oveq2i 
 |-  ( m + ( 2 - 1 ) ) = ( m + 1 )
142 139 141 eqtr2di 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( m + 1 ) = ( ( m + 2 ) - 1 ) )
143 142 negeqd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> -u ( m + 1 ) = -u ( ( m + 2 ) - 1 ) )
144 70 71 addcld 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( m + 2 ) e. CC )
145 144 138 negsubdid 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> -u ( ( m + 2 ) - 1 ) = ( -u ( m + 2 ) + 1 ) )
146 72 oveq1d 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( -u ( m + 2 ) + 1 ) = ( ( -u m - 2 ) + 1 ) )
147 143 145 146 3eqtrrd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( -u m - 2 ) + 1 ) = -u ( m + 1 ) )
148 147 oveq1d 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( ( -u m - 2 ) + 1 ) .x. X ) = ( -u ( m + 1 ) .x. X ) )
149 33 ad2antrr 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> W e. Toset )
150 149 34 syl 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> W e. Poset )
151 63 znegcld 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> -u m e. ZZ )
152 151 82 zsubcld 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( -u m - 2 ) e. ZZ )
153 152 peano2zd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( -u m - 2 ) + 1 ) e. ZZ )
154 1 5 mulgcl 
 |-  ( ( W e. Grp /\ ( ( -u m - 2 ) + 1 ) e. ZZ /\ X e. B ) -> ( ( ( -u m - 2 ) + 1 ) .x. X ) e. B )
155 77 153 79 154 syl3anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( ( -u m - 2 ) + 1 ) .x. X ) e. B )
156 1 4 posref 
 |-  ( ( W e. Poset /\ ( ( ( -u m - 2 ) + 1 ) .x. X ) e. B ) -> ( ( ( -u m - 2 ) + 1 ) .x. X ) .<_ ( ( ( -u m - 2 ) + 1 ) .x. X ) )
157 150 155 156 syl2anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( ( -u m - 2 ) + 1 ) .x. X ) .<_ ( ( ( -u m - 2 ) + 1 ) .x. X ) )
158 148 157 eqbrtrrd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( -u ( m + 1 ) .x. X ) .<_ ( ( ( -u m - 2 ) + 1 ) .x. X ) )
159 158 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
160 136 159 eqbrtrd 
 |-  ( ( ( ( ( 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 ) )
161 oveq1 
 |-  ( n = ( -u m - 2 ) -> ( n .x. X ) = ( ( -u m - 2 ) .x. X ) )
162 161 breq1d 
 |-  ( n = ( -u m - 2 ) -> ( ( n .x. X ) .< Y <-> ( ( -u m - 2 ) .x. X ) .< Y ) )
163 oveq1 
 |-  ( n = ( -u m - 2 ) -> ( n + 1 ) = ( ( -u m - 2 ) + 1 ) )
164 163 oveq1d 
 |-  ( n = ( -u m - 2 ) -> ( ( n + 1 ) .x. X ) = ( ( ( -u m - 2 ) + 1 ) .x. X ) )
165 164 breq2d 
 |-  ( n = ( -u m - 2 ) -> ( Y .<_ ( ( n + 1 ) .x. X ) <-> Y .<_ ( ( ( -u m - 2 ) + 1 ) .x. X ) ) )
166 162 165 anbi12d 
 |-  ( 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 ) ) ) )
167 166 rspcev 
 |-  ( ( ( -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 ) ) )
168 68 137 160 167 syl12anc 
 |-  ( ( ( ( ( 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 ) ) )
169 78 ad2antrr 
 |-  ( ( ( ( ( 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 )
170 169 znegcld 
 |-  ( ( ( ( ( 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 )
171 6 ad2antrr 
 |-  ( ( ( 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 )
172 11 ad2antrr 
 |-  ( ( ( 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 )
173 171 172 jca 
 |-  ( ( ( 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 ) )
174 173 3anassrs 
 |-  ( ( ( ( ( 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 ) )
175 124 ad2antrr 
 |-  ( ( ( ( ( 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 )
176 81 ad2antrr 
 |-  ( ( ( ( ( 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 )
177 simpr 
 |-  ( ( ( ( ( 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 ) )
178 1 3 16 ogrpinvlt 
 |-  ( ( ( 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 ) ) ) )
179 178 biimpa 
 |-  ( ( ( ( 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 ) ) )
180 174 175 176 177 179 syl31anc 
 |-  ( ( ( ( ( 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 ) ) )
181 116 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) )
182 181 eqcomd 
 |-  ( ( ( ( ( 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 ) )
183 134 ad4antr 
 |-  ( ( ( ( ( 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 )
184 180 182 183 3brtr3d 
 |-  ( ( ( ( ( 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 )
185 simp-4l 
 |-  ( ( ( ( ( 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 )
186 1 5 mulgcl 
 |-  ( ( W e. Grp /\ m e. ZZ /\ X e. B ) -> ( m .x. X ) e. B )
187 77 63 79 186 syl3anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( m .x. X ) e. B )
188 1 3 16 ogrpinvlt 
 |-  ( ( ( 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 ) ) ) )
189 76 187 124 188 syl3anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( m .x. X ) .< ( ( invg ` W ) ` Y ) <-> ( ( invg ` W ) ` ( ( invg ` W ) ` Y ) ) .< ( ( invg ` W ) ` ( m .x. X ) ) ) )
190 189 biimpa 
 |-  ( ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) /\ ( m .x. X ) .< ( ( invg ` W ) ` Y ) ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Y ) ) .< ( ( invg ` W ) ` ( m .x. X ) ) )
191 190 adantrr 
 |-  ( ( ( ( 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 ) ) )
192 191 adantr 
 |-  ( ( ( ( ( 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 ) ) )
193 negdi 
 |-  ( ( m e. CC /\ 1 e. CC ) -> -u ( m + 1 ) = ( -u m + -u 1 ) )
194 69 43 193 sylancl 
 |-  ( m e. NN0 -> -u ( m + 1 ) = ( -u m + -u 1 ) )
195 194 oveq1d 
 |-  ( m e. NN0 -> ( -u ( m + 1 ) + 1 ) = ( ( -u m + -u 1 ) + 1 ) )
196 69 negcld 
 |-  ( m e. NN0 -> -u m e. CC )
197 93 negcld 
 |-  ( m e. NN0 -> -u 1 e. CC )
198 196 197 93 addassd 
 |-  ( m e. NN0 -> ( ( -u m + -u 1 ) + 1 ) = ( -u m + ( -u 1 + 1 ) ) )
199 46 oveq2i 
 |-  ( -u m + ( -u 1 + 1 ) ) = ( -u m + 0 )
200 199 a1i 
 |-  ( m e. NN0 -> ( -u m + ( -u 1 + 1 ) ) = ( -u m + 0 ) )
201 196 addridd 
 |-  ( m e. NN0 -> ( -u m + 0 ) = -u m )
202 198 200 201 3eqtrd 
 |-  ( m e. NN0 -> ( ( -u m + -u 1 ) + 1 ) = -u m )
203 195 202 eqtrd 
 |-  ( m e. NN0 -> ( -u ( m + 1 ) + 1 ) = -u m )
204 203 oveq1d 
 |-  ( m e. NN0 -> ( ( -u ( m + 1 ) + 1 ) .x. X ) = ( -u m .x. X ) )
205 204 adantl 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( -u ( m + 1 ) + 1 ) .x. X ) = ( -u m .x. X ) )
206 1 5 16 mulgneg 
 |-  ( ( W e. Grp /\ m e. ZZ /\ X e. B ) -> ( -u m .x. X ) = ( ( invg ` W ) ` ( m .x. X ) ) )
207 77 63 79 206 syl3anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( -u m .x. X ) = ( ( invg ` W ) ` ( m .x. X ) ) )
208 205 207 eqtrd 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( -u ( m + 1 ) + 1 ) .x. X ) = ( ( invg ` W ) ` ( m .x. X ) ) )
209 208 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) )
210 209 eqcomd 
 |-  ( ( ( ( ( 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 ) )
211 192 183 210 3brtr3d 
 |-  ( ( ( ( ( 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 ) )
212 ovexd 
 |-  ( ph -> ( ( -u ( m + 1 ) + 1 ) .x. X ) e. _V )
213 4 3 pltle 
 |-  ( ( 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 ) ) )
214 6 9 212 213 syl3anc 
 |-  ( ph -> ( Y .< ( ( -u ( m + 1 ) + 1 ) .x. X ) -> Y .<_ ( ( -u ( m + 1 ) + 1 ) .x. X ) ) )
215 185 211 214 sylc 
 |-  ( ( ( ( ( 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 
 |-  ( n = -u ( m + 1 ) -> ( n .x. X ) = ( -u ( m + 1 ) .x. X ) )
217 216 breq1d 
 |-  ( n = -u ( m + 1 ) -> ( ( n .x. X ) .< Y <-> ( -u ( m + 1 ) .x. X ) .< Y ) )
218 oveq1 
 |-  ( n = -u ( m + 1 ) -> ( n + 1 ) = ( -u ( m + 1 ) + 1 ) )
219 218 oveq1d 
 |-  ( n = -u ( m + 1 ) -> ( ( n + 1 ) .x. X ) = ( ( -u ( m + 1 ) + 1 ) .x. X ) )
220 219 breq2d 
 |-  ( n = -u ( m + 1 ) -> ( Y .<_ ( ( n + 1 ) .x. X ) <-> Y .<_ ( ( -u ( m + 1 ) + 1 ) .x. X ) ) )
221 217 220 anbi12d 
 |-  ( 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 ) ) ) )
222 221 rspcev 
 |-  ( ( -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 ) ) )
223 170 184 215 222 syl12anc 
 |-  ( ( ( ( ( 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 ) ) )
224 1 4 3 tlt2 
 |-  ( ( 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 ) ) )
225 149 81 124 224 syl3anc 
 |-  ( ( ( ph /\ Y .< .0. ) /\ m e. NN0 ) -> ( ( ( m + 1 ) .x. X ) .<_ ( ( invg ` W ) ` Y ) \/ ( ( invg ` W ) ` Y ) .< ( ( m + 1 ) .x. X ) ) )
226 225 adantr 
 |-  ( ( ( ( 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 ) ) )
227 168 223 226 mpjaodan 
 |-  ( ( ( ( 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 ) ) )
228 6 adantr 
 |-  ( ( ph /\ Y .< .0. ) -> W e. oGrp )
229 7 adantr 
 |-  ( ( ph /\ Y .< .0. ) -> W e. Archi )
230 8 adantr 
 |-  ( ( ph /\ Y .< .0. ) -> X e. B )
231 123 adantr 
 |-  ( ( ph /\ Y .< .0. ) -> ( ( invg ` W ) ` Y ) e. B )
232 10 adantr 
 |-  ( ( ph /\ Y .< .0. ) -> .0. .< X )
233 134 breq1d 
 |-  ( ph -> ( ( ( invg ` W ) ` ( ( invg ` W ) ` Y ) ) .< .0. <-> Y .< .0. ) )
234 233 biimpar 
 |-  ( ( ph /\ Y .< .0. ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` Y ) ) .< .0. )
235 1 3 16 2 ogrpinv0lt 
 |-  ( ( W e. oGrp /\ ( ( invg ` W ) ` Y ) e. B ) -> ( .0. .< ( ( invg ` W ) ` Y ) <-> ( ( invg ` W ) ` ( ( invg ` W ) ` Y ) ) .< .0. ) )
236 6 123 235 syl2anc 
 |-  ( ph -> ( .0. .< ( ( invg ` W ) ` Y ) <-> ( ( invg ` W ) ` ( ( invg ` W ) ` Y ) ) .< .0. ) )
237 236 biimpar 
 |-  ( ( ph /\ ( ( invg ` W ) ` ( ( invg ` W ) ` Y ) ) .< .0. ) -> .0. .< ( ( invg ` W ) ` Y ) )
238 234 237 syldan 
 |-  ( ( ph /\ Y .< .0. ) -> .0. .< ( ( invg ` W ) ` Y ) )
239 1 2 3 4 5 228 229 230 231 232 238 archirng 
 |-  ( ( ph /\ Y .< .0. ) -> E. m e. NN0 ( ( m .x. X ) .< ( ( invg ` W ) ` Y ) /\ ( ( invg ` W ) ` Y ) .<_ ( ( m + 1 ) .x. X ) ) )
240 227 239 r19.29a 
 |-  ( ( ph /\ Y .< .0. ) -> E. n e. ZZ ( ( n .x. X ) .< Y /\ Y .<_ ( ( n + 1 ) .x. X ) ) )
241 nn0ssz 
 |-  NN0 C_ ZZ
242 6 adantr 
 |-  ( ( ph /\ .0. .< Y ) -> W e. oGrp )
243 7 adantr 
 |-  ( ( ph /\ .0. .< Y ) -> W e. Archi )
244 8 adantr 
 |-  ( ( ph /\ .0. .< Y ) -> X e. B )
245 9 adantr 
 |-  ( ( ph /\ .0. .< Y ) -> Y e. B )
246 10 adantr 
 |-  ( ( ph /\ .0. .< Y ) -> .0. .< X )
247 simpr 
 |-  ( ( ph /\ .0. .< Y ) -> .0. .< Y )
248 1 2 3 4 5 242 243 244 245 246 247 archirng 
 |-  ( ( ph /\ .0. .< Y ) -> E. n e. NN0 ( ( n .x. X ) .< Y /\ Y .<_ ( ( n + 1 ) .x. X ) ) )
249 ssrexv 
 |-  ( 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 ) ) ) )
250 241 248 249 mpsyl 
 |-  ( ( ph /\ .0. .< Y ) -> E. n e. ZZ ( ( n .x. X ) .< Y /\ Y .<_ ( ( n + 1 ) .x. X ) ) )
251 1 3 tlt3 
 |-  ( ( W e. Toset /\ Y e. B /\ .0. e. B ) -> ( Y = .0. \/ Y .< .0. \/ .0. .< Y ) )
252 33 9 37 251 syl3anc 
 |-  ( ph -> ( Y = .0. \/ Y .< .0. \/ .0. .< Y ) )
253 61 240 250 252 mpjao3dan 
 |-  ( ph -> E. n e. ZZ ( ( n .x. X ) .< Y /\ Y .<_ ( ( n + 1 ) .x. X ) ) )