Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem xrlttrt 5526

Description: Ordering on the extended reals is transitive.

Assertion

Ref	Expression
xrlttrt

---

Proof of Theorem xrlttrt

Step	Hyp	Ref	Expression
1		axlttrn 5476	. . . . . . . . . . . 12
2	1	3expa 831	. . . . . . . . . . 11
3	2	an1rs 488	. . . . . . . . . 10
4		rexrt 5471	. . . . . . . . . . . . . . . 16
5		pnfnltt 5519	. . . . . . . . . . . . . . . 16
6	4, 5	syl 10	. . . . . . . . . . . . . . 15
7	6	adantr 389	. . . . . . . . . . . . . 14
8		breq1 2612	. . . . . . . . . . . . . . 15
9	8	adantl 388	. . . . . . . . . . . . . 14
10	7, 9	mtbird 713	. . . . . . . . . . . . 13
11	10	pm2.21d 78	. . . . . . . . . . . 12
12	11	adantll 392	. . . . . . . . . . 11
13	12	adantld 390	. . . . . . . . . 10
14		rexrt 5471	. . . . . . . . . . . . . . . 16
15		nltmnft 5520	. . . . . . . . . . . . . . . 16
16	14, 15	syl 10	. . . . . . . . . . . . . . 15
17	16	adantr 389	. . . . . . . . . . . . . 14
18		breq2 2613	. . . . . . . . . . . . . . 15
19	18	adantl 388	. . . . . . . . . . . . . 14
20	17, 19	mtbird 713	. . . . . . . . . . . . 13
21	20	pm2.21d 78	. . . . . . . . . . . 12
22	21	adantlr 393	. . . . . . . . . . 11
23	22	adantrd 391	. . . . . . . . . 10
24	3, 13, 23	3jaodan 887	. . . . . . . . 9
25		elxr 5508	. . . . . . . . 9
26	24, 25	sylan2b 452	. . . . . . . 8
27	26	an1rs 488	. . . . . . 7
28		ltpnft 5515	. . . . . . . . . . 11
29	28	adantr 389	. . . . . . . . . 10
30		breq2 2613	. . . . . . . . . . 11
31	30	adantl 388	. . . . . . . . . 10
32	29, 31	mpbird 196	. . . . . . . . 9
33	32	adantlr 393	. . . . . . . 8
34	33	a1d 12	. . . . . . 7
35		nltmnft 5520	. . . . . . . . . . . 12
36	35	adantr 389	. . . . . . . . . . 11
37		breq2 2613	. . . . . . . . . . . 12
38	37	adantl 388	. . . . . . . . . . 11
39	36, 38	mtbird 713	. . . . . . . . . 10
40	39	pm2.21d 78	. . . . . . . . 9
41	40	adantld 390	. . . . . . . 8
42	41	adantll 392	. . . . . . 7
43	27, 34, 42	3jaodan 887	. . . . . 6
44	43	anasss 440	. . . . 5
45		pnfnltt 5519	. . . . . . . . . 10
46	45	adantl 388	. . . . . . . . 9
47		breq1 2612	. . . . . . . . . 10
48	47	adantr 389	. . . . . . . . 9
49	46, 48	mtbird 713	. . . . . . . 8
50	49	pm2.21d 78	. . . . . . 7
51	50	adantrd 391	. . . . . 6
52	51	adantrr 395	. . . . 5
53		mnfltt 5516	. . . . . . . . . . 11
54	53	adantl 388	. . . . . . . . . 10
55		breq1 2612	. . . . . . . . . . 11
56	55	adantr 389	. . . . . . . . . 10
57	54, 56	mpbird 196	. . . . . . . . 9
58	57	a1d 12	. . . . . . . 8
59	58	adantlr 393	. . . . . . 7
60		mnfltpnf 5517	. . . . . . . . . 10
61		breq12 2614	. . . . . . . . . 10
62	60, 61	mpbiri 194	. . . . . . . . 9
63	62	a1d 12	. . . . . . . 8
64	63	adantlr 393	. . . . . . 7
65	41	adantll 392	. . . . . . 7
66	59, 64, 65	3jaodan 887	. . . . . 6
67	66	anasss 440	. . . . 5
68	44, 52, 67	3jaoian 886	. . . 4
69	68	3impb 827	. . 3
70		elxr 5508	. . 3
71	69, 70	syl3an3b 862	. 2
72		elxr 5508	. 2
73	71, 72	syl3an1b 860	1

Colors of variables: wff set class

Syntax hints:   wn 2   wi 3   wb 146   wa 223   w3o 772   w3a 773   wceq 953   wcel 955   class class class wbr 2609  cr 5205   cpnf 5455   cmnf 5456  cxr 5457   clt 5458

This theorem is referenced by:  xrltso 5527  xrlelttrt 5535  xrltletrt 5536  xrub 6027  qbtwnxr 6217  ioo0t 6305  elioc2t 6322  elico2t 6323  elioo1t3 10383  truni1 10386

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580  df-ral