Theorem xrlttrt 5553

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 5504	. . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
2	1	3expa 833	. . . . . . . . . . 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 5499	. . . . . . . . . . . . . . . 16 |- (C e. RR -> C e. RR*)
5		pnfnltt 5546	. . . . . . . . . . . . . . . 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 2622	. . . . . . . . . . . . . . 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 715	. . . . . . . . . . . . 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 5499	. . . . . . . . . . . . . . . 16 |- (A e. RR -> A e. RR*)
15		nltmnft 5547	. . . . . . . . . . . . . . . 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 2623	. . . . . . . . . . . . . . 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 715	. . . . . . . . . . . . 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 890	. . . . . . . . 9 |- (((A e. RR /\ C e. RR) /\ (B e. RR \/ B = +oo \/ B = -oo)) -> ((A < B /\ B < C) -> A < C))
25		elxr 5535	. . . . . . . . 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 5542	. . . . . . . . . . 11 |- (A e. RR -> A < +oo)
29	28	adantr 389	. . . . . . . . . 10 |- ((A e. RR /\ C = +oo) -> A < +oo)
30		breq2 2623	. . . . . . . . . . 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 5547	. . . . . . . . . . . 12 |- (B e. RR* -> -. B < -oo)
36	35	adantr 389	. . . . . . . . . . 11 |- ((B e. RR* /\ C = -oo) -> -. B < -oo)
37		breq2 2623	. . . . . . . . . . . 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 715	. . . . . . . . . 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 890	. . . . . 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 5546	. . . . . . . . . 10 |- (B e. RR* -> -. +oo < B)
46	45	adantl 388	. . . . . . . . 9 |- ((A = +oo /\ B e. RR*) -> -. +oo < B)
47		breq1 2622	. . . . . . . . . 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 715	. . . . . . . 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 5543	. . . . . . . . . . 11 |- (C e. RR -> -oo < C)
54	53	adantl 388	. . . . . . . . . 10 |- ((A = -oo /\ C e. RR) -> -oo < C)
55		breq1 2622	. . . . . . . . . . 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 5544	. . . . . . . . . 10 |- -oo < +oo
61		breq12 2624	. . . . . . . . . 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 890	. . . . . 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 889	. . . 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 829	. . 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 5535	. . 3 |- (C e. RR* <-> (C e. RR \/ C = +oo \/ C = -oo))
71	69, 70	syl3an3b 864	. 2 |- (((A e. RR \/ A = +oo \/ A = -oo) /\ B e. RR* /\ C e. RR*) -> ((A < B /\ B < C) -> A < C))
72		elxr 5535	. 2 |- (A e. RR* <-> (A e. RR \/ A = +oo \/ A = -oo))
73	71, 72	syl3an1b 862	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 774   /\ w3a 775   = wceq 956   e. wcel 958   class class class wbr 2619  RRcr 5233   +oocpnf 5483   -oocmnf 5484  RR*cxr 5485   < clt 5486

This theorem is referenced by:  xrltso 5554  xrlelttrt 5562  xrltletrt 5563  xrub 6080  qbtwnxr 6279  ioo0t 6368  elioc2t 6390  elico2t 6391  elioo1t3 10496  truni1 10499

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779  ax-un 2866  ax-inf2 4625

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-nel 1588