Theorem archiabllem2c 29749

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

Hypotheses

Ref	Expression
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

Ref	Expression
archiabllem2c	|- ( ph -> -. ( X .+ Y ) .< ( Y .+ X ) )

Distinct variable groups:   a, b, B   W, a, b   X, a, b   Y, a, b   ph, a, b   .+ , a, b   .<_ , a, b   .< , a, b   .0. , a, b

Allowed substitution hints:   .x. ( a, b)

Proof of Theorem archiabllem2c

Dummy variables m n t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprr 796	. . . 4 |- ( ( ( ( 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 ) ) )
2		simpl1l 1112	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
3		archiabllem.g	. . . . . . . . . . . . . . 15 |- ( ph -> W e. oGrp )
4	2, 3	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
5		simpl1r 1113	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) )
6	3	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> W e. oGrp )
7		ogrpgrp 29703	. . . . . . . . . . . . . . . . 17 |- ( W e. oGrp -> W e. Grp )
8	6, 7	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> W e. Grp )
9		archiabllem2b.5	. . . . . . . . . . . . . . . . 17 |- ( ph -> Y e. B )
10	9	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> Y e. B )
11		archiabllem2b.4	. . . . . . . . . . . . . . . . 17 |- ( ph -> X e. B )
12	11	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> X e. B )
13		archiabllem.b	. . . . . . . . . . . . . . . . 17 |- B = ( Base ` W )
14		archiabllem2.1	. . . . . . . . . . . . . . . . 17 |- .+ = ( +g ` W )
15	13, 14	grpcl 17430	. . . . . . . . . . . . . . . 16 |- ( ( W e. Grp /\ Y e. B /\ X e. B ) -> ( Y .+ X ) e. B )
16	8, 10, 12, 15	syl3anc 1326	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( Y .+ X ) e. B )
17	2, 5, 16	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
18	2, 3, 7	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
19		simpr2 1068	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
20	19	peano2zd 11485	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
21		simp2 1062	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> t e. B )
22	21	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
23		archiabllem.m	. . . . . . . . . . . . . . . . 17 |- .x. = (.g ` W )
24	13, 23	mulgcl 17559	. . . . . . . . . . . . . . . 16 |- ( ( W e. Grp /\ ( m + 1 ) e. ZZ /\ t e. B ) -> ( ( m + 1 ) .x. t ) e. B )
25	18, 20, 22, 24	syl3anc 1326	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
26		simpr1 1067	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
27	26	peano2zd 11485	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
28	13, 23	mulgcl 17559	. . . . . . . . . . . . . . . 16 |- ( ( W e. Grp /\ ( n + 1 ) e. ZZ /\ t e. B ) -> ( ( n + 1 ) .x. t ) e. B )
29	18, 27, 22, 28	syl3anc 1326	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
30	13, 14	grpcl 17430	. . . . . . . . . . . . . . 15 |- ( ( 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 )
31	18, 25, 29, 30	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
32	12	3ad2ant1 1082	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> X e. B )
33	32	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
34	10	3ad2ant1 1082	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> Y e. B )
35	34	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
36	13, 14	grpcl 17430	. . . . . . . . . . . . . . 15 |- ( ( W e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
37	18, 33, 35, 36	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
38		archiabllem.e	. . . . . . . . . . . . . . 15 |- .<_ = ( le ` W )
39		isogrp 29702	. . . . . . . . . . . . . . . . 17 |- ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) )
40	39	simprbi 480	. . . . . . . . . . . . . . . 16 |- ( W e. oGrp -> W e. oMnd )
41	2, 3, 40	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
42		simpr3 1069	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) ) ) )
43	42	simprd 479	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
44	43	simprd 479	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) )
45	42	simpld 475	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
46	45	simprd 479	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) )
47		archiabllem2.2	. . . . . . . . . . . . . . . 16 |- ( ph -> (oppg ` W ) e. oGrp )
48		isogrp 29702	. . . . . . . . . . . . . . . . 17 |- ( (oppg ` W ) e. oGrp <-> ( (oppg ` W ) e. Grp /\ (oppg ` W ) e. oMnd ) )
49	48	simprbi 480	. . . . . . . . . . . . . . . 16 |- ( (oppg ` W ) e. oGrp -> (oppg ` W ) e. oMnd )
50	2, 47, 49	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
51	13, 38, 14, 41, 29, 35, 33, 25, 44, 46, 50	omndadd2rd 29709	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) )
52		eqid 2622	. . . . . . . . . . . . . . 15 |- ( -g ` W ) = ( -g ` W )
53	13, 38, 52	ogrpsub 29717	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
54	4, 17, 31, 37, 51, 53	syl131anc 1339	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
55	19	zcnd 11483	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 )
56	26	zcnd 11483	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 )
57		1cnd 10056	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 )
58	55, 56, 57, 57	add4d 10264	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 ) ) )
59		1p1e2 11134	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 + 1 ) = 2
60	59	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m + n ) + ( 1 + 1 ) ) = ( ( m + n ) + 2 )
61		addcom 10222	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( m e. CC /\ n e. CC ) -> ( m + n ) = ( n + m ) )
62	61	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. CC /\ n e. CC ) -> ( ( m + n ) + 2 ) = ( ( n + m ) + 2 ) )
63	60, 62	syl5eq 2668	. . . . . . . . . . . . . . . . . . . 20 |- ( ( m e. CC /\ n e. CC ) -> ( ( m + n ) + ( 1 + 1 ) ) = ( ( n + m ) + 2 ) )
64		2cnd 11093	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. CC /\ n e. CC ) -> 2 e. CC )
65		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( m e. CC /\ n e. CC ) -> n e. CC )
66		simpl 473	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( m e. CC /\ n e. CC ) -> m e. CC )
67	65, 66	addcld 10059	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. CC /\ n e. CC ) -> ( n + m ) e. CC )
68	64, 67	addcomd 10238	. . . . . . . . . . . . . . . . . . . 20 |- ( ( m e. CC /\ n e. CC ) -> ( 2 + ( n + m ) ) = ( ( n + m ) + 2 ) )
69	63, 68	eqtr4d 2659	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. CC /\ n e. CC ) -> ( ( m + n ) + ( 1 + 1 ) ) = ( 2 + ( n + m ) ) )
70	55, 56, 69	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 ) ) )
71	58, 70	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) ) )
72	71	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) )
73		2z 11409	. . . . . . . . . . . . . . . . . 18 |- 2 e. ZZ
74	73	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
75	26, 19	zaddcld 11486	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
76	13, 23, 14	mulgdir 17573	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) )
77	18, 74, 75, 22, 76	syl13anc 1328	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
78	72, 77	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
79	13, 23, 14	mulgdir 17573	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
80	18, 20, 27, 22, 79	syl13anc 1328	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
81	13, 23, 14	mulg2 17550	. . . . . . . . . . . . . . . . 17 |- ( t e. B -> ( 2 .x. t ) = ( t .+ t ) )
82	22, 81	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) )
83	82	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
84	78, 80, 83	3eqtr3d 2664	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) )
85	84	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
86	54, 85	breqtrd 4679	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
87	84, 31	eqeltrrd 2702	. . . . . . . . . . . . 13 |- ( ( ( ( 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 )
88		eqid 2622	. . . . . . . . . . . . . 14 |- ( invg ` W ) = ( invg ` W )
89	13, 14, 88, 52	grpsubval 17465	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) )
90	87, 37, 89	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) )
91	86, 90	breqtrd 4679	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) )
92		archiabllem.t	. . . . . . . . . . . 12 |- .< = ( lt ` W )
93	2, 47	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( 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 )
94	13, 88	grpinvcl 17467	. . . . . . . . . . . . 13 |- ( ( W e. Grp /\ ( X .+ Y ) e. B ) -> ( ( invg ` W ) ` ( X .+ Y ) ) e. B )
95	18, 37, 94	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ( 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 )
96	75	znegcld 11484	. . . . . . . . . . . . 13 |- ( ( ( ( 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 )
97	13, 23	mulgcl 17559	. . . . . . . . . . . . 13 |- ( ( W e. Grp /\ -u ( n + m ) e. ZZ /\ t e. B ) -> ( -u ( n + m ) .x. t ) e. B )
98	18, 96, 22, 97	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ( 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 )
99	13, 23, 14	mulgdir 17573	. . . . . . . . . . . . . . . 16 |- ( ( W e. Grp /\ ( n e. ZZ /\ m e. ZZ /\ t e. B ) ) -> ( ( n + m ) .x. t ) = ( ( n .x. t ) .+ ( m .x. t ) ) )
100	18, 26, 19, 22, 99	syl13anc 1328	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
101	13, 23	mulgcl 17559	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. Grp /\ n e. ZZ /\ t e. B ) -> ( n .x. t ) e. B )
102	18, 26, 22, 101	syl3anc 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
103	13, 23	mulgcl 17559	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. Grp /\ m e. ZZ /\ t e. B ) -> ( m .x. t ) e. B )
104	18, 19, 22, 103	syl3anc 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
105	45	simpld 475	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
106	13, 92, 14	ogrpaddlt 29718	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) )
107	4, 102, 33, 104, 105, 106	syl131anc 1339	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
108	43	simpld 475	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
109	13, 92, 14, 4, 93, 104, 35, 33, 108	ogrpaddltrd 29720	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) )
110		omndtos 29705	. . . . . . . . . . . . . . . . . 18 |- ( W e. oMnd -> W e. Toset )
111		tospos 29658	. . . . . . . . . . . . . . . . . 18 |- ( W e. Toset -> W e. Poset )
112	41, 110, 111	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
113	13, 14	grpcl 17430	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. Grp /\ ( n .x. t ) e. B /\ ( m .x. t ) e. B ) -> ( ( n .x. t ) .+ ( m .x. t ) ) e. B )
114	18, 102, 104, 113	syl3anc 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
115	13, 14	grpcl 17430	. . . . . . . . . . . . . . . . . 18 |- ( ( W e. Grp /\ X e. B /\ ( m .x. t ) e. B ) -> ( X .+ ( m .x. t ) ) e. B )
116	18, 33, 104, 115	syl3anc 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
117	13, 92	plttr 16970	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) )
118	112, 114, 116, 37, 117	syl13anc 1328	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
119	107, 109, 118	mp2and 715	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) )
120	100, 119	eqbrtrd 4675	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
121	100, 114	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
122	13, 92, 88	ogrpinvlt 29724	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) )
123	4, 93, 121, 37, 122	syl211anc 1332	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) ) )
124	120, 123	mpbid 222	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
125	13, 23, 88	mulgneg 17560	. . . . . . . . . . . . . 14 |- ( ( W e. Grp /\ ( n + m ) e. ZZ /\ t e. B ) -> ( -u ( n + m ) .x. t ) = ( ( invg ` W ) ` ( ( n + m ) .x. t ) ) )
126	18, 75, 22, 125	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
127	124, 126	breqtrrd 4681	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
128	13, 92, 14, 4, 93, 95, 98, 87, 127	ogrpaddltrd 29720	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
129	13, 52	grpsubcl 17495	. . . . . . . . . . . . 13 |- ( ( W e. Grp /\ ( Y .+ X ) e. B /\ ( X .+ Y ) e. B ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) e. B )
130	18, 17, 37, 129	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ( 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 )
131	13, 14	grpcl 17430	. . . . . . . . . . . . 13 |- ( ( 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 )
132	18, 87, 95, 131	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ( 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 )
133	13, 14	grpcl 17430	. . . . . . . . . . . . 13 |- ( ( 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 )
134	18, 87, 98, 133	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ( 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 )
135	13, 38, 92	plelttr 16972	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
136	112, 130, 132, 134, 135	syl13anc 1328	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) )
137	91, 128, 136	mp2and 715	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
138	13, 14	grpcl 17430	. . . . . . . . . . . . 13 |- ( ( W e. Grp /\ t e. B /\ t e. B ) -> ( t .+ t ) e. B )
139	18, 22, 22, 138	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ( 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 )
140	13, 14	grpass 17431	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
141	18, 139, 121, 98, 140	syl13anc 1328	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) )
142	56, 55	addcld 10059	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
143	142	negidd 10382	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
144	143	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
145	13, 23, 14	mulgdir 17573	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
146	18, 75, 96, 22, 145	syl13anc 1328	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
147		archiabllem.0	. . . . . . . . . . . . . . 15 |- .0. = ( 0g ` W )
148	13, 147, 23	mulg0 17546	. . . . . . . . . . . . . 14 |- ( t e. B -> ( 0 .x. t ) = .0. )
149	22, 148	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( 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. )
150	144, 146, 149	3eqtr3d 2664	. . . . . . . . . . . 12 |- ( ( ( ( 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. )
151	150	oveq2d 6666	. . . . . . . . . . 11 |- ( ( ( ( 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. ) )
152	13, 14, 147	grprid 17453	. . . . . . . . . . . 12 |- ( ( W e. Grp /\ ( t .+ t ) e. B ) -> ( ( t .+ t ) .+ .0. ) = ( t .+ t ) )
153	18, 139, 152	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
154	141, 151, 153	3eqtrd 2660	. . . . . . . . . 10 |- ( ( ( ( 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 ) )
155	137, 154	breqtrd 4679	. . . . . . . . 9 |- ( ( ( ( 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 ) )
156	155	3anassrs 1290	. . . . . . . 8 |- ( ( ( ( ( ( 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 ) )
157	6	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> W e. oGrp )
158		archiabllem.a	. . . . . . . . . . . 12 |- ( ph -> W e. Archi )
159	158	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> W e. Archi )
160	159	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> W e. Archi )
161		simp3 1063	. . . . . . . . . 10 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> .0. .< t )
162	47	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> (oppg ` W ) e. oGrp )
163	162	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> (oppg ` W ) e. oGrp )
164	13, 147, 92, 38, 23, 157, 160, 21, 32, 161, 163	archirngz 29743	. . . . . . . . 9 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> E. n e. ZZ ( ( n .x. t ) .< X /\ X .<_ ( ( n + 1 ) .x. t ) ) )
165	13, 147, 92, 38, 23, 157, 160, 21, 34, 161, 163	archirngz 29743	. . . . . . . . 9 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> E. m e. ZZ ( ( m .x. t ) .< Y /\ Y .<_ ( ( m + 1 ) .x. t ) ) )
166		reeanv 3107	. . . . . . . . 9 |- ( 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 ) ) ) )
167	164, 165, 166	sylanbrc 698	. . . . . . . 8 |- ( ( ( 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 ) ) ) )
168	156, 167	r19.29vva 3081	. . . . . . 7 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) .< ( t .+ t ) )
169	157, 40, 110	3syl 18	. . . . . . . 8 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> W e. Toset )
170	8, 12, 10, 36	syl3anc 1326	. . . . . . . . . 10 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( X .+ Y ) e. B )
171	8, 16, 170, 129	syl3anc 1326	. . . . . . . . 9 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) e. B )
172	171	3ad2ant1 1082	. . . . . . . 8 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) e. B )
173	157, 7	syl 17	. . . . . . . . 9 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> W e. Grp )
174	173, 21, 21, 138	syl3anc 1326	. . . . . . . 8 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> ( t .+ t ) e. B )
175	13, 38, 92	tltnle 29662	. . . . . . . 8 |- ( ( 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 ) ) ) )
176	169, 172, 174, 175	syl3anc 1326	. . . . . . 7 |- ( ( ( 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 ) ) ) )
177	168, 176	mpbid 222	. . . . . 6 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B /\ .0. .< t ) -> -. ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
178	177	3expa 1265	. . . . 5 |- ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B ) /\ .0. .< t ) -> -. ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
179	178	adantrr 753	. . . 4 |- ( ( ( ( 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 ) ) )
180	1, 179	pm2.21fal 1505	. . 3 |- ( ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ t e. B ) /\ ( .0. .< t /\ ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) ) ) -> F. )
181		archiabllem2.3	. . . . 5 |- ( ( ph /\ a e. B /\ .0. .< a ) -> E. b e. B ( .0. .< b /\ b .< a ) )
182	181	3adant1r 1319	. . . 4 |- ( ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) /\ a e. B /\ .0. .< a ) -> E. b e. B ( .0. .< b /\ b .< a ) )
183	13, 147, 52	grpsubid 17499	. . . . . 6 |- ( ( W e. Grp /\ ( X .+ Y ) e. B ) -> ( ( X .+ Y ) ( -g ` W ) ( X .+ Y ) ) = .0. )
184	8, 170, 183	syl2anc 693	. . . . 5 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( ( X .+ Y ) ( -g ` W ) ( X .+ Y ) ) = .0. )
185		simpr 477	. . . . . 6 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( X .+ Y ) .< ( Y .+ X ) )
186	13, 92, 52	ogrpsublt 29722	. . . . . 6 |- ( ( 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	6, 170, 16, 170, 185, 186	syl131anc 1339	. . . . 5 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> ( ( X .+ Y ) ( -g ` W ) ( X .+ Y ) ) .< ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
188	184, 187	eqbrtrrd 4677	. . . 4 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> .0. .< ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) )
189	13, 147, 38, 92, 23, 6, 159, 14, 162, 182, 171, 188	archiabllem2a 29748	. . 3 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> E. t e. B ( .0. .< t /\ ( t .+ t ) .<_ ( ( Y .+ X ) ( -g ` W ) ( X .+ Y ) ) ) )
190	180, 189	r19.29a 3078	. 2 |- ( ( ph /\ ( X .+ Y ) .< ( Y .+ X ) ) -> F. )
191	190	inegd 1503	1 |- ( ph -> -. ( X .+ Y ) .< ( Y .+ X ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   F. wfal 1488   e. wcel 1990   E.wrex 2913   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   CCcc 9934   0cc0 9936   1c1 9937   + caddc 9939   -ucneg 10267   2c2 11070   ZZcz 11377   Basecbs 15857   +g cplusg 15941   lecple 15948   0gc0g 16100   Posetcpo 16940   ltcplt 16941  Tosetctos 17033   Grpcgrp 17422   invgcminusg 17423   -gcsg 17424  ._gcmg 17540  opp_gcoppg 17775  oMndcomnd 29697  oGrpcogrp 29698  Archicarchi 29731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-fz 12327  df-seq 12802  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-plusg 15954  df-ple 15961  df-0g 16102  df-preset 16928  df-poset 16946  df-plt 16958  df-toset 17034  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-oppg 17776  df-omnd 29699  df-ogrp 29700  df-inftm 29732  df-archi 29733

This theorem is referenced by:  archiabllem2b  29750