Metamath Proof Explorer

Theorem archiabllem2c

Description: Lemma for archiabl . (Contributed by Thierry Arnoux, 1-May-2018)

Ref Expression
Hypotheses archiabllem.b 
|- B = ( Base ` W )
archiabllem.0 
|- .0. = ( 0g ` W )
archiabllem.e 
|- .<_ = ( le ` W )
archiabllem.t 
|- .< = ( lt ` W )
archiabllem.m 
|- .x. = ( .g ` W )
archiabllem.g 
|- ( ph -> W e. oGrp )
archiabllem.a 
|- ( ph -> W e. Archi )
archiabllem2.1 
|- .+ = ( +g ` W )
archiabllem2.2 
|- ( ph -> ( oppG ` W ) e. oGrp )
archiabllem2.3 
|- ( ( ph /\ a e. B /\ .0. .< a ) -> E. b e. B ( .0. .< b /\ b .< a ) )
archiabllem2b.4 
|- ( ph -> X e. B )
archiabllem2b.5 
|- ( ph -> Y e. B )
Assertion archiabllem2c 
|- ( ph -> -. ( X .+ Y ) .< ( Y .+ X ) )

Proof

Step Hyp Ref Expression
1 archiabllem.b 
 |-  B = ( Base ` W )
2 archiabllem.0 
 |-  .0. = ( 0g ` W )
3 archiabllem.e 
 |-  .<_ = ( le ` W )
4 archiabllem.t 
 |-  .< = ( lt ` W )
5 archiabllem.m 
 |-  .x. = ( .g ` W )
6 archiabllem.g 
 |-  ( ph -> W e. oGrp )
7 archiabllem.a 
 |-  ( ph -> W e. Archi )
8 archiabllem2.1 
 |-  .+ = ( +g ` W )
9 archiabllem2.2 
 |-  ( ph -> ( oppG ` W ) e. oGrp )
10 archiabllem2.3 
 |-  ( ( ph /\ a e. B /\ .0. .< a ) -> E. b e. B ( .0. .< b /\ b .< a ) )
11 archiabllem2b.4 
 |-  ( ph -> X e. B )
12 archiabllem2b.5 
 |-  ( ph -> Y e. B )
13 simprr 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B ) /\ ( .0. .< t /\ ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) ) ) -> ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
14 simpl1l 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ph )
15 14 6 syl 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> W e. oGrp )
16 simpl1r 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( X .+ Y ) .< ( Y .+ X ) )
17 6 adantr 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> W e. oGrp )
18 ogrpgrp 
 |-  ( W e. oGrp -> W e. Grp )
19 17 18 syl 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> W e. Grp )
20 12 adantr 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> Y e. B )
21 11 adantr 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> X e. B )
22 1 8 grpcl 
 |-  ( ( W e. Grp /\ Y e. B /\ X e. B ) -> ( Y .+ X ) e. B )
23 19 20 21 22 syl3anc 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( Y .+ X ) e. B )
24 14 16 23 syl2anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( Y .+ X ) e. B )
25 14 6 18 3syl 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> W e. Grp )
26 simpr2 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> m e. ZZ )
27 26 peano2zd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( m + 1 ) e. ZZ )
28 simp2 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> t e. B )
29 28 adantr 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> t e. B )
30 1 5 mulgcl 
 |-  ( ( W e. Grp /\ ( m + 1 ) e. ZZ /\ t e. B ) -> ( ( m + 1 ) .x. t ) e. B )
31 25 27 29 30 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( m + 1 ) .x. t ) e. B )
32 simpr1 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> n e. ZZ )
33 32 peano2zd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( n + 1 ) e. ZZ )
34 1 5 mulgcl 
 |-  ( ( W e. Grp /\ ( n + 1 ) e. ZZ /\ t e. B ) -> ( ( n + 1 ) .x. t ) e. B )
35 25 33 29 34 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( n + 1 ) .x. t ) e. B )
36 1 8 grpcl 
 |-  ( ( W e. Grp /\ ( ( m + 1 ) .x. t ) e. B /\ ( ( n + 1 ) .x. t ) e. B ) -> ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) e. B )
37 25 31 35 36 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) e. B )
38 21 3ad2ant1 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> X e. B )
39 38 adantr 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> X e. B )
40 20 3ad2ant1 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> Y e. B )
41 40 adantr 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> Y e. B )
42 1 8 grpcl 
 |-  ( ( W e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
43 25 39 41 42 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( X .+ Y ) e. B )
44 isogrp 
 |-  ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) )
45 44 simprbi 
 |-  ( W e. oGrp -> W e. oMnd )
46 14 6 45 3syl 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> W e. oMnd )
47 simpr3 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) )
48 47 simprd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) )
49 48 simprd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> Y .<_ ( ( m + 1 ) .x. t ) )
50 47 simpld 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) )
51 50 simprd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> X .<_ ( ( n + 1 ) .x. t ) )
52 isogrp 
 |-  ( ( oppG ` W ) e. oGrp <-> ( ( oppG ` W ) e. Grp /\ ( oppG ` W ) e. oMnd ) )
53 52 simprbi 
 |-  ( ( oppG ` W ) e. oGrp -> ( oppG ` W ) e. oMnd )
54 14 9 53 3syl 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( oppG ` W ) e. oMnd )
55 1 3 8 46 35 41 39 31 49 51 54 omndadd2rd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( Y .+ X ) .<_ ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) )
56 eqid 
 |-  ( -g ` W ) = ( -g ` W )
57 1 3 56 ogrpsub 
 |-  ( ( W e. oGrp /\ ( ( Y .+ X ) e. B /\ ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) e. B /\ ( X .+ Y ) e. B ) /\ ( Y .+ X ) .<_ ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .<_ ( ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) ( -g ` W ) ( X .+ Y ) ) )
58 15 24 37 43 55 57 syl131anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .<_ ( ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) ( -g ` W ) ( X .+ Y ) ) )
59 26 zcnd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> m e. CC )
60 32 zcnd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> n e. CC )
61 1cnd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> 1 e. CC )
62 59 60 61 61 add4d 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( m + n ) + ( 1 + 1 ) ) = ( ( m + 1 ) + ( n + 1 ) ) )
63 1p1e2 
 |-  ( 1 + 1 ) = 2
64 63 oveq2i 
 |-  ( ( m + n ) + ( 1 + 1 ) ) = ( ( m + n ) + 2 )
65 addcom 
 |-  ( ( m e. CC /\ n e. CC ) -> ( m + n ) = ( n + m ) )
66 65 oveq1d 
 |-  ( ( m e. CC /\ n e. CC ) -> ( ( m + n ) + 2 ) = ( ( n + m ) + 2 ) )
67 64 66 eqtrid 
 |-  ( ( m e. CC /\ n e. CC ) -> ( ( m + n ) + ( 1 + 1 ) ) = ( ( n + m ) + 2 ) )
68 2cnd 
 |-  ( ( m e. CC /\ n e. CC ) -> 2 e. CC )
69 simpr 
 |-  ( ( m e. CC /\ n e. CC ) -> n e. CC )
70 simpl 
 |-  ( ( m e. CC /\ n e. CC ) -> m e. CC )
71 69 70 addcld 
 |-  ( ( m e. CC /\ n e. CC ) -> ( n + m ) e. CC )
72 68 71 addcomd 
 |-  ( ( m e. CC /\ n e. CC ) -> ( 2 + ( n + m ) ) = ( ( n + m ) + 2 ) )
73 67 72 eqtr4d 
 |-  ( ( m e. CC /\ n e. CC ) -> ( ( m + n ) + ( 1 + 1 ) ) = ( 2 + ( n + m ) ) )
74 59 60 73 syl2anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( m + n ) + ( 1 + 1 ) ) = ( 2 + ( n + m ) ) )
75 62 74 eqtr3d 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( m + 1 ) + ( n + 1 ) ) = ( 2 + ( n + m ) ) )
76 75 oveq1d 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( m + 1 ) + ( n + 1 ) ) .x. t ) = ( ( 2 + ( n + m ) ) .x. t ) )
77 2z 
 |-  2 e. ZZ
78 77 a1i 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> 2 e. ZZ )
79 32 26 zaddcld 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( n + m ) e. ZZ )
80 1 5 8 mulgdir 
 |-  ( ( W e. Grp /\ ( 2 e. ZZ /\ ( n + m ) e. ZZ /\ t e. B ) ) -> ( ( 2 + ( n + m ) ) .x. t ) = ( ( 2 .x. t ) .+ ( ( n + m ) .x. t ) ) )
81 25 78 79 29 80 syl13anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( 2 + ( n + m ) ) .x. t ) = ( ( 2 .x. t ) .+ ( ( n + m ) .x. t ) ) )
82 76 81 eqtrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( m + 1 ) + ( n + 1 ) ) .x. t ) = ( ( 2 .x. t ) .+ ( ( n + m ) .x. t ) ) )
83 1 5 8 mulgdir 
 |-  ( ( W e. Grp /\ ( ( m + 1 ) e. ZZ /\ ( n + 1 ) e. ZZ /\ t e. B ) ) -> ( ( ( m + 1 ) + ( n + 1 ) ) .x. t ) = ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) )
84 25 27 33 29 83 syl13anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( m + 1 ) + ( n + 1 ) ) .x. t ) = ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) )
85 1 5 8 mulg2 
 |-  ( t e. B -> ( 2 .x. t ) = ( t .+ t ) )
86 29 85 syl 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( 2 .x. t ) = ( t .+ t ) )
87 86 oveq1d 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( 2 .x. t ) .+ ( ( n + m ) .x. t ) ) = ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) )
88 82 84 87 3eqtr3d 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) = ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) )
89 88 oveq1d 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( ( m + 1 ) .x. t ) .+ ( ( n + 1 ) .x. t ) ) ( -g ` W ) ( X .+ Y ) ) = ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) ( -g ` W ) ( X .+ Y ) ) )
90 58 89 breqtrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .<_ ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) ( -g ` W ) ( X .+ Y ) ) )
91 88 37 eqeltrrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) e. B )
92 eqid 
 |-  ( invg ` W ) = ( invg ` W )
93 1 8 92 56 grpsubval 
 |-  ( ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) e. B /\ ( X .+ Y ) e. B ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) ( -g ` W ) ( X .+ Y ) ) = ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) )
94 91 43 93 syl2anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) ( -g ` W ) ( X .+ Y ) ) = ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) )
95 90 94 breqtrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .<_ ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) )
96 14 9 syl 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( oppG ` W ) e. oGrp )
97 1 92 grpinvcl 
 |-  ( ( W e. Grp /\ ( X .+ Y ) e. B ) -> ( ( invg ` W ) ` ( X .+ Y ) ) e. B )
98 25 43 97 syl2anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( invg ` W ) ` ( X .+ Y ) ) e. B )
99 79 znegcld 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> -u ( n + m ) e. ZZ )
100 1 5 mulgcl 
 |-  ( ( W e. Grp /\ -u ( n + m ) e. ZZ /\ t e. B ) -> ( -u ( n + m ) .x. t ) e. B )
101 25 99 29 100 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( -u ( n + m ) .x. t ) e. B )
102 1 5 8 mulgdir 
 |-  ( ( W e. Grp /\ ( n e. ZZ /\ m e. ZZ /\ t e. B ) ) -> ( ( n + m ) .x. t ) = ( ( n .x. t ) .+ ( m .x. t ) ) )
103 25 32 26 29 102 syl13anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( n + m ) .x. t ) = ( ( n .x. t ) .+ ( m .x. t ) ) )
104 1 5 mulgcl 
 |-  ( ( W e. Grp /\ n e. ZZ /\ t e. B ) -> ( n .x. t ) e. B )
105 25 32 29 104 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( n .x. t ) e. B )
106 1 5 mulgcl 
 |-  ( ( W e. Grp /\ m e. ZZ /\ t e. B ) -> ( m .x. t ) e. B )
107 25 26 29 106 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( m .x. t ) e. B )
108 50 simpld 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( n .x. t ) .< X )
109 1 4 8 ogrpaddlt 
 |-  ( ( W e. oGrp /\ ( ( n .x. t ) e. B /\ X e. B /\ ( m .x. t ) e. B ) /\ ( n .x. t ) .< X ) -> ( ( n .x. t ) .+ ( m .x. t ) ) .< ( X .+ ( m .x. t ) ) )
110 15 105 39 107 108 109 syl131anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( n .x. t ) .+ ( m .x. t ) ) .< ( X .+ ( m .x. t ) ) )
111 48 simpld 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( m .x. t ) .< Y )
112 1 4 8 15 96 107 41 39 111 ogrpaddltrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( X .+ ( m .x. t ) ) .< ( X .+ Y ) )
113 omndtos 
 |-  ( W e. oMnd -> W e. Toset )
114 tospos 
 |-  ( W e. Toset -> W e. Poset )
115 46 113 114 3syl 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> W e. Poset )
116 1 8 grpcl 
 |-  ( ( W e. Grp /\ ( n .x. t ) e. B /\ ( m .x. t ) e. B ) -> ( ( n .x. t ) .+ ( m .x. t ) ) e. B )
117 25 105 107 116 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( n .x. t ) .+ ( m .x. t ) ) e. B )
118 1 8 grpcl 
 |-  ( ( W e. Grp /\ X e. B /\ ( m .x. t ) e. B ) -> ( X .+ ( m .x. t ) ) e. B )
119 25 39 107 118 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( X .+ ( m .x. t ) ) e. B )
120 1 4 plttr 
 |-  ( ( W e. Poset /\ ( ( ( n .x. t ) .+ ( m .x. t ) ) e. B /\ ( X .+ ( m .x. t ) ) e. B /\ ( X .+ Y ) e. B ) ) -> ( ( ( ( n .x. t ) .+ ( m .x. t ) ) .< ( X .+ ( m .x. t ) ) /\ ( X .+ ( m .x. t ) ) .< ( X .+ Y ) ) -> ( ( n .x. t ) .+ ( m .x. t ) ) .< ( X .+ Y ) ) )
121 115 117 119 43 120 syl13anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( ( n .x. t ) .+ ( m .x. t ) ) .< ( X .+ ( m .x. t ) ) /\ ( X .+ ( m .x. t ) ) .< ( X .+ Y ) ) -> ( ( n .x. t ) .+ ( m .x. t ) ) .< ( X .+ Y ) ) )
122 110 112 121 mp2and 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( n .x. t ) .+ ( m .x. t ) ) .< ( X .+ Y ) )
123 103 122 eqbrtrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( n + m ) .x. t ) .< ( X .+ Y ) )
124 103 117 eqeltrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( n + m ) .x. t ) e. B )
125 1 4 92 ogrpinvlt 
 |-  ( ( ( W e. oGrp /\ ( oppG ` W ) e. oGrp ) /\ ( ( n + m ) .x. t ) e. B /\ ( X .+ Y ) e. B ) -> ( ( ( n + m ) .x. t ) .< ( X .+ Y ) <-> ( ( invg ` W ) ` ( X .+ Y ) ) .< ( ( invg ` W ) ` ( ( n + m ) .x. t ) ) ) )
126 15 96 124 43 125 syl211anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( n + m ) .x. t ) .< ( X .+ Y ) <-> ( ( invg ` W ) ` ( X .+ Y ) ) .< ( ( invg ` W ) ` ( ( n + m ) .x. t ) ) ) )
127 123 126 mpbid 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( invg ` W ) ` ( X .+ Y ) ) .< ( ( invg ` W ) ` ( ( n + m ) .x. t ) ) )
128 1 5 92 mulgneg 
 |-  ( ( W e. Grp /\ ( n + m ) e. ZZ /\ t e. B ) -> ( -u ( n + m ) .x. t ) = ( ( invg ` W ) ` ( ( n + m ) .x. t ) ) )
129 25 79 29 128 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( -u ( n + m ) .x. t ) = ( ( invg ` W ) ` ( ( n + m ) .x. t ) ) )
130 127 129 breqtrrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( invg ` W ) ` ( X .+ Y ) ) .< ( -u ( n + m ) .x. t ) )
131 1 4 8 15 96 98 101 91 130 ogrpaddltrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) .< ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) )
132 1 56 grpsubcl 
 |-  ( ( W e. Grp /\ ( Y .+ X ) e. B /\ ( X .+ Y ) e. B ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) e. B )
133 25 24 43 132 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) e. B )
134 1 8 grpcl 
 |-  ( ( W e. Grp /\ ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) e. B /\ ( ( invg ` W ) ` ( X .+ Y ) ) e. B ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) e. B )
135 25 91 98 134 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) e. B )
136 1 8 grpcl 
 |-  ( ( W e. Grp /\ ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) e. B /\ ( -u ( n + m ) .x. t ) e. B ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) e. B )
137 25 91 101 136 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) e. B )
138 1 3 4 plelttr 
 |-  ( ( W e. Poset /\ ( ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) e. B /\ ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) e. B /\ ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) e. B ) ) -> ( ( ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .<_ ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) /\ ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) .< ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .< ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) ) )
139 115 133 135 137 138 syl13anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .<_ ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) /\ ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( ( invg ` W ) ` ( X .+ Y ) ) ) .< ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .< ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) ) )
140 95 131 139 mp2and 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .< ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) )
141 1 8 grpcl 
 |-  ( ( W e. Grp /\ t e. B /\ t e. B ) -> ( t .+ t ) e. B )
142 25 29 29 141 syl3anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( t .+ t ) e. B )
143 1 8 grpass 
 |-  ( ( W e. Grp /\ ( ( t .+ t ) e. B /\ ( ( n + m ) .x. t ) e. B /\ ( -u ( n + m ) .x. t ) e. B ) ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) = ( ( t .+ t ) .+ ( ( ( n + m ) .x. t ) .+ ( -u ( n + m ) .x. t ) ) ) )
144 25 142 124 101 143 syl13anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) = ( ( t .+ t ) .+ ( ( ( n + m ) .x. t ) .+ ( -u ( n + m ) .x. t ) ) ) )
145 60 59 addcld 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( n + m ) e. CC )
146 145 negidd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( n + m ) + -u ( n + m ) ) = 0 )
147 146 oveq1d 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( n + m ) + -u ( n + m ) ) .x. t ) = ( 0 .x. t ) )
148 1 5 8 mulgdir 
 |-  ( ( W e. Grp /\ ( ( n + m ) e. ZZ /\ -u ( n + m ) e. ZZ /\ t e. B ) ) -> ( ( ( n + m ) + -u ( n + m ) ) .x. t ) = ( ( ( n + m ) .x. t ) .+ ( -u ( n + m ) .x. t ) ) )
149 25 79 99 29 148 syl13anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( n + m ) + -u ( n + m ) ) .x. t ) = ( ( ( n + m ) .x. t ) .+ ( -u ( n + m ) .x. t ) ) )
150 1 2 5 mulg0 
 |-  ( t e. B -> ( 0 .x. t ) = .0. )
151 29 150 syl 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( 0 .x. t ) = .0. )
152 147 149 151 3eqtr3d 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( n + m ) .x. t ) .+ ( -u ( n + m ) .x. t ) ) = .0. )
153 152 oveq2d 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( t .+ t ) .+ ( ( ( n + m ) .x. t ) .+ ( -u ( n + m ) .x. t ) ) ) = ( ( t .+ t ) .+ .0. ) )
154 1 8 2 grprid 
 |-  ( ( W e. Grp /\ ( t .+ t ) e. B ) -> ( ( t .+ t ) .+ .0. ) = ( t .+ t ) )
155 25 142 154 syl2anc 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( t .+ t ) .+ .0. ) = ( t .+ t ) )
156 144 153 155 3eqtrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( ( t .+ t ) .+ ( ( n + m ) .x. t ) ) .+ ( -u ( n + m ) .x. t ) ) = ( t .+ t ) )
157 140 156 breqtrd 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ ( n e. ZZ /\ m e. ZZ /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .< ( t .+ t ) )
158 157 3anassrs 
 |-  ( ( ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) /\ n e. ZZ ) /\ m e. ZZ ) /\ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .< ( t .+ t ) )
159 17 3ad2ant1 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> W e. oGrp )
160 7 adantr 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> W e. Archi )
161 160 3ad2ant1 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> W e. Archi )
162 simp3 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> .0. .< t )
163 9 adantr 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( oppG ` W ) e. oGrp )
164 163 3ad2ant1 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> ( oppG ` W ) e. oGrp )
165 1 2 4 3 5 159 161 28 38 162 164 archirngz 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> E. n e. ZZ ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) )
166 1 2 4 3 5 159 161 28 40 162 164 archirngz 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> E. m e. ZZ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) )
167 reeanv 
 |-  ( E. n e. ZZ E. m e. ZZ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) <-> ( E. n e. ZZ ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ E. m e. ZZ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) )
168 165 166 167 sylanbrc 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> E. n e. ZZ E. m e. ZZ ( ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) /\ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) ) )
169 158 168 r19.29vva 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .< ( t .+ t ) )
170 159 45 113 3syl 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> W e. Toset )
171 19 21 20 42 syl3anc 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( X .+ Y ) e. B )
172 19 23 171 132 syl3anc 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) e. B )
173 172 3ad2ant1 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) e. B )
174 159 18 syl 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> W e. Grp )
175 174 28 28 141 syl3anc 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> ( t .+ t ) e. B )
176 1 3 4 tltnle 
 |-  ( ( W e. Toset /\ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) e. B /\ ( t .+ t ) e. B ) -> ( ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .< ( t .+ t ) <-> -. ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) ) )
177 170 173 175 176 syl3anc 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> ( ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .< ( t .+ t ) <-> -. ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) ) )
178 169 177 mpbid 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> -. ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
179 178 3expa 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B ) /\ .0. .< t ) -> -. ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
180 179 adantrr 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B ) /\ ( .0. .< t /\ ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) ) ) -> -. ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
181 13 180 pm2.21fal 
 |-  ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B ) /\ ( .0. .< t /\ ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) ) ) -> F. )
182 10 3adant1r 
 |-  ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ a e. B /\ .0. .< a ) -> E. b e. B ( .0. .< b /\ b .< a ) )
183 1 2 56 grpsubid 
 |-  ( ( W e. Grp /\ ( X .+ Y ) e. B ) -> ( ( X .+ Y ) ( -g ` W ) ( X .+ Y ) ) = .0. )
184 19 171 183 syl2anc 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( ( X .+ Y ) ( -g ` W ) ( X .+ Y ) ) = .0. )
185 simpr 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( X .+ Y ) .< ( Y .+ X ) )
186 1 4 56 ogrpsublt 
 |-  ( ( W e. oGrp /\ ( ( X .+ Y ) e. B /\ ( Y .+ X ) e. B /\ ( X .+ Y ) e. B ) /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( ( X .+ Y ) ( -g ` W ) ( X .+ Y ) ) .< ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
187 17 171 23 171 185 186 syl131anc 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( ( X .+ Y ) ( -g ` W ) ( X .+ Y ) ) .< ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
188 184 187 eqbrtrrd 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> .0. .< ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
189 1 2 3 4 5 17 160 8 163 182 172 188 archiabllem2a 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> E. t e. B ( .0. .< t /\ ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) ) )
190 181 189 r19.29a 
 |-  ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> F. )
191 190 inegd 
 |-  ( ph -> -. ( X .+ Y ) .< ( Y .+ X ) )