Theorem xrlttrt 5536

Description: Ordering on the extended reals is transitive.

Assertion

Ref	Expression
xrlttrt	|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B < C) -> A < C))

Proof of Theorem xrlttrt

Step	Hyp	Ref	Expression
1		axlttrn 5487	. . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
2	1	3expa 832	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR) /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
3	2	an1rs 489	. . . . . . . . . 10 |- (((A e. RR /\ C e. RR) /\ B e. RR) -> ((A < B /\ B < C) -> A < C))
4		rexrt 5482	. . . . . . . . . . . . . . . 16 |- (C e. RR -> C e. RR*)
5		pnfnltt 5529	. . . . . . . . . . . . . . . 16 |- (C e. RR* -> -. +oo < C)
6	4, 5	syl 10	. . . . . . . . . . . . . . 15 |- (C e. RR -> -. +oo < C)
7	6	adantr 389	. . . . . . . . . . . . . 14 |- ((C e. RR /\ B = +oo) -> -. +oo < C)
8		breq1 2618	. . . . . . . . . . . . . . 15 |- (B = +oo -> (B < C <-> +oo < C))
9	8	adantl 388	. . . . . . . . . . . . . 14 |- ((C e. RR /\ B = +oo) -> (B < C <-> +oo < C))
10	7, 9	mtbird 714	. . . . . . . . . . . . 13 |- ((C e. RR /\ B = +oo) -> -. B < C)
11	10	pm2.21d 78	. . . . . . . . . . . 12 |- ((C e. RR /\ B = +oo) -> (B < C -> A < C))
12	11	adantll 392	. . . . . . . . . . 11 |- (((A e. RR /\ C e. RR) /\ B = +oo) -> (B < C -> A < C))
13	12	adantld 390	. . . . . . . . . 10 |- (((A e. RR /\ C e. RR) /\ B = +oo) -> ((A < B /\ B < C) -> A < C))
14		rexrt 5482	. . . . . . . . . . . . . . . 16 |- (A e. RR -> A e. RR*)
15		nltmnft 5530	. . . . . . . . . . . . . . . 16 |- (A e. RR* -> -. A < -oo)
16	14, 15	syl 10	. . . . . . . . . . . . . . 15 |- (A e. RR -> -. A < -oo)
17	16	adantr 389	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B = -oo) -> -. A < -oo)
18		breq2 2619	. . . . . . . . . . . . . . 15 |- (B = -oo -> (A < B <-> A < -oo))
19	18	adantl 388	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B = -oo) -> (A < B <-> A < -oo))
20	17, 19	mtbird 714	. . . . . . . . . . . . 13 |- ((A e. RR /\ B = -oo) -> -. A < B)
21	20	pm2.21d 78	. . . . . . . . . . . 12 |- ((A e. RR /\ B = -oo) -> (A < B -> A < C))
22	21	adantlr 393	. . . . . . . . . . 11 |- (((A e. RR /\ C e. RR) /\ B = -oo) -> (A < B -> A < C))
23	22	adantrd 391	. . . . . . . . . 10 |- (((A e. RR /\ C e. RR) /\ B = -oo) -> ((A < B /\ B < C) -> A < C))
24	3, 13, 23	3jaodan 889	. . . . . . . . 9 |- (((A e. RR /\ C e. RR) /\ (B e. RR \/ B = +oo \/ B = -oo)) -> ((A < B /\ B < C) -> A < C))
25		elxr 5518	. . . . . . . . 9 |- (B e. RR* <-> (B e. RR \/ B = +oo \/ B = -oo))
26	24, 25	sylan2b 452	. . . . . . . 8 |- (((A e. RR /\ C e. RR) /\ B e. RR*) -> ((A < B /\ B < C) -> A < C))
27	26	an1rs 489	. . . . . . 7 |- (((A e. RR /\ B e. RR*) /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
28		ltpnft 5525	. . . . . . . . . . 11 |- (A e. RR -> A < +oo)
29	28	adantr 389	. . . . . . . . . 10 |- ((A e. RR /\ C = +oo) -> A < +oo)
30		breq2 2619	. . . . . . . . . . 11 |- (C = +oo -> (A < C <-> A < +oo))
31	30	adantl 388	. . . . . . . . . 10 |- ((A e. RR /\ C = +oo) -> (A < C <-> A < +oo))
32	29, 31	mpbird 196	. . . . . . . . 9 |- ((A e. RR /\ C = +oo) -> A < C)
33	32	adantlr 393	. . . . . . . 8 |- (((A e. RR /\ B e. RR*) /\ C = +oo) -> A < C)
34	33	a1d 12	. . . . . . 7 |- (((A e. RR /\ B e. RR*) /\ C = +oo) -> ((A < B /\ B < C) -> A < C))
35		nltmnft 5530	. . . . . . . . . . . 12 |- (B e. RR* -> -. B < -oo)
36	35	adantr 389	. . . . . . . . . . 11 |- ((B e. RR* /\ C = -oo) -> -. B < -oo)
37		breq2 2619	. . . . . . . . . . . 12 |- (C = -oo -> (B < C <-> B < -oo))
38	37	adantl 388	. . . . . . . . . . 11 |- ((B e. RR* /\ C = -oo) -> (B < C <-> B < -oo))
39	36, 38	mtbird 714	. . . . . . . . . 10 |- ((B e. RR* /\ C = -oo) -> -. B < C)
40	39	pm2.21d 78	. . . . . . . . 9 |- ((B e. RR* /\ C = -oo) -> (B < C -> A < C))
41	40	adantld 390	. . . . . . . 8 |- ((B e. RR* /\ C = -oo) -> ((A < B /\ B < C) -> A < C))
42	41	adantll 392	. . . . . . 7 |- (((A e. RR /\ B e. RR*) /\ C = -oo) -> ((A < B /\ B < C) -> A < C))
43	27, 34, 42	3jaodan 889	. . . . . 6 |- (((A e. RR /\ B e. RR*) /\ (C e. RR \/ C = +oo \/ C = -oo)) -> ((A < B /\ B < C) -> A < C))
44	43	anasss 440	. . . . 5 |- ((A e. RR /\ (B e. RR* /\ (C e. RR \/ C = +oo \/ C = -oo))) -> ((A < B /\ B < C) -> A < C))
45		pnfnltt 5529	. . . . . . . . . 10 |- (B e. RR* -> -. +oo < B)
46	45	adantl 388	. . . . . . . . 9 |- ((A = +oo /\ B e. RR*) -> -. +oo < B)
47		breq1 2618	. . . . . . . . . 10 |- (A = +oo -> (A < B <-> +oo < B))
48	47	adantr 389	. . . . . . . . 9 |- ((A = +oo /\ B e. RR*) -> (A < B <-> +oo < B))
49	46, 48	mtbird 714	. . . . . . . 8 |- ((A = +oo /\ B e. RR*) -> -. A < B)
50	49	pm2.21d 78	. . . . . . 7 |- ((A = +oo /\ B e. RR*) -> (A < B -> A < C))
51	50	adantrd 391	. . . . . 6 |- ((A = +oo /\ B e. RR*) -> ((A < B /\ B < C) -> A < C))
52	51	adantrr 395	. . . . 5 |- ((A = +oo /\ (B e. RR* /\ (C e. RR \/ C = +oo \/ C = -oo))) -> ((A < B /\ B < C) -> A < C))
53		mnfltt 5526	. . . . . . . . . . 11 |- (C e. RR -> -oo < C)
54	53	adantl 388	. . . . . . . . . 10 |- ((A = -oo /\ C e. RR) -> -oo < C)
55		breq1 2618	. . . . . . . . . . 11 |- (A = -oo -> (A < C <-> -oo < C))
56	55	adantr 389	. . . . . . . . . 10 |- ((A = -oo /\ C e. RR) -> (A < C <-> -oo < C))
57	54, 56	mpbird 196	. . . . . . . . 9 |- ((A = -oo /\ C e. RR) -> A < C)
58	57	a1d 12	. . . . . . . 8 |- ((A = -oo /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
59	58	adantlr 393	. . . . . . 7 |- (((A = -oo /\ B e. RR*) /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
60		mnfltpnf 5527	. . . . . . . . . 10 |- -oo < +oo
61		breq12 2620	. . . . . . . . . 10 |- ((A = -oo /\ C = +oo) -> (A < C <-> -oo < +oo))
62	60, 61	mpbiri 194	. . . . . . . . 9 |- ((A = -oo /\ C = +oo) -> A < C)
63	62	a1d 12	. . . . . . . 8 |- ((A = -oo /\ C = +oo) -> ((A < B /\ B < C) -> A < C))
64	63	adantlr 393	. . . . . . 7 |- (((A = -oo /\ B e. RR*) /\ C = +oo) -> ((A < B /\ B < C) -> A < C))
65	41	adantll 392	. . . . . . 7 |- (((A = -oo /\ B e. RR*) /\ C = -oo) -> ((A < B /\ B < C) -> A < C))
66	59, 64, 65	3jaodan 889	. . . . . 6 |- (((A = -oo /\ B e. RR*) /\ (C e. RR \/ C = +oo \/ C = -oo)) -> ((A < B /\ B < C) -> A < C))
67	66	anasss 440	. . . . 5 |- ((A = -oo /\ (B e. RR* /\ (C e. RR \/ C = +oo \/ C = -oo))) -> ((A < B /\ B < C) -> A < C))
68	44, 52, 67	3jaoian 888	. . . 4 |- (((A e. RR \/ A = +oo \/ A = -oo) /\ (B e. RR* /\ (C e. RR \/ C = +oo \/ C = -oo))) -> ((A < B /\ B < C) -> A < C))
69	68	3impb 828	. . 3 |- (((A e. RR \/ A = +oo \/ A = -oo) /\ B e. RR* /\ (C e. RR \/ C = +oo \/ C = -oo)) -> ((A < B /\ B < C) -> A < C))
70		elxr 5518	. . 3 |- (C e. RR* <-> (C e. RR \/ C = +oo \/ C = -oo))
71	69, 70	syl3an3b 863	. 2 |- (((A e. RR \/ A = +oo \/ A = -oo) /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B < C) -> A < C))
72		elxr 5518	. 2 |- (A e. RR* <-> (A e. RR \/ A = +oo \/ A = -oo))
73	71, 72	syl3an1b 861	1 |- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B < C) -> A < C))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   \/ w3o 773   /\ w3a 774   = wceq 955   e. wcel 957   class class class wbr 2615  RRcr 5216   +oocpnf 5466   -oocmnf 5467  RR*cxr 5468   < clt 5469

This theorem is referenced by:  xrltso 5537  xrlelttrt 5545  xrltletrt 5546  xrub 6037  qbtwnxr 6229  ioo0t 6318  elioc2t 6335  elico2t 6336  elioo1t3 10442  truni1 10445

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2862  ax-inf2 4608

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-nel 1586  df-ral