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
|
syl5eq |
|- ( 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
|
addid1d |
|- ( 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 ) ) ) |