Theorem xrlttr

Description: Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005)

	Ref	Expression
Assertion	xrlttr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elxr	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2		elxr	⊢ ( 𝐶 ∈ ℝ* ↔ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) )
3		elxr	⊢ ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
4		lttr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
5	4	3expa	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
6	5	an32s	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
7		rexr	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* )
8		pnfnlt	⊢ ( 𝐶 ∈ ℝ* → ¬ +∞ < 𝐶 )
9	7 8	syl	⊢ ( 𝐶 ∈ ℝ → ¬ +∞ < 𝐶 )
10	9	adantr	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 = +∞ ) → ¬ +∞ < 𝐶 )
11		breq1	⊢ ( 𝐵 = +∞ → ( 𝐵 < 𝐶 ↔ +∞ < 𝐶 ) )
12	11	adantl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐵 < 𝐶 ↔ +∞ < 𝐶 ) )
13	10 12	mtbird	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 = +∞ ) → ¬ 𝐵 < 𝐶 )
14	13	pm2.21d	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐵 < 𝐶 → 𝐴 < 𝐶 ) )
15	14	adantll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 = +∞ ) → ( 𝐵 < 𝐶 → 𝐴 < 𝐶 ) )
16	15	adantld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 = +∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
17		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
18		nltmnf	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < -∞ )
19	17 18	syl	⊢ ( 𝐴 ∈ ℝ → ¬ 𝐴 < -∞ )
20	19	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ¬ 𝐴 < -∞ )
21		breq2	⊢ ( 𝐵 = -∞ → ( 𝐴 < 𝐵 ↔ 𝐴 < -∞ ) )
22	21	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 ↔ 𝐴 < -∞ ) )
23	20 22	mtbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ¬ 𝐴 < 𝐵 )
24	23	pm2.21d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 → 𝐴 < 𝐶 ) )
25	24	adantlr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 → 𝐴 < 𝐶 ) )
26	25	adantrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 = -∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
27	6 16 26	3jaodan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
28	3 27	sylan2b	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
29	28	an32s	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
30		ltpnf	⊢ ( 𝐴 ∈ ℝ → 𝐴 < +∞ )
31	30	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 = +∞ ) → 𝐴 < +∞ )
32		breq2	⊢ ( 𝐶 = +∞ → ( 𝐴 < 𝐶 ↔ 𝐴 < +∞ ) )
33	32	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 = +∞ ) → ( 𝐴 < 𝐶 ↔ 𝐴 < +∞ ) )
34	31 33	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 = +∞ ) → 𝐴 < 𝐶 )
35	34	adantlr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = +∞ ) → 𝐴 < 𝐶 )
36	35	a1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = +∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
37		nltmnf	⊢ ( 𝐵 ∈ ℝ* → ¬ 𝐵 < -∞ )
38	37	adantr	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ¬ 𝐵 < -∞ )
39		breq2	⊢ ( 𝐶 = -∞ → ( 𝐵 < 𝐶 ↔ 𝐵 < -∞ ) )
40	39	adantl	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ( 𝐵 < 𝐶 ↔ 𝐵 < -∞ ) )
41	38 40	mtbird	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ¬ 𝐵 < 𝐶 )
42	41	pm2.21d	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ( 𝐵 < 𝐶 → 𝐴 < 𝐶 ) )
43	42	adantld	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 = -∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
44	43	adantll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
45	29 36 44	3jaodan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
46	45	anasss	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
47		pnfnlt	⊢ ( 𝐵 ∈ ℝ* → ¬ +∞ < 𝐵 )
48	47	adantl	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ¬ +∞ < 𝐵 )
49		breq1	⊢ ( 𝐴 = +∞ → ( 𝐴 < 𝐵 ↔ +∞ < 𝐵 ) )
50	49	adantr	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ +∞ < 𝐵 ) )
51	48 50	mtbird	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ¬ 𝐴 < 𝐵 )
52	51	pm2.21d	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → 𝐴 < 𝐶 ) )
53	52	adantrd	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
54	53	adantrr	⊢ ( ( 𝐴 = +∞ ∧ ( 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
55		mnflt	⊢ ( 𝐶 ∈ ℝ → -∞ < 𝐶 )
56	55	adantl	⊢ ( ( 𝐴 = -∞ ∧ 𝐶 ∈ ℝ ) → -∞ < 𝐶 )
57		breq1	⊢ ( 𝐴 = -∞ → ( 𝐴 < 𝐶 ↔ -∞ < 𝐶 ) )
58	57	adantr	⊢ ( ( 𝐴 = -∞ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐶 ↔ -∞ < 𝐶 ) )
59	56 58	mpbird	⊢ ( ( 𝐴 = -∞ ∧ 𝐶 ∈ ℝ ) → 𝐴 < 𝐶 )
60	59	a1d	⊢ ( ( 𝐴 = -∞ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
61	60	adantlr	⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
62		mnfltpnf	⊢ -∞ < +∞
63		breq12	⊢ ( ( 𝐴 = -∞ ∧ 𝐶 = +∞ ) → ( 𝐴 < 𝐶 ↔ -∞ < +∞ ) )
64	62 63	mpbiri	⊢ ( ( 𝐴 = -∞ ∧ 𝐶 = +∞ ) → 𝐴 < 𝐶 )
65	64	a1d	⊢ ( ( 𝐴 = -∞ ∧ 𝐶 = +∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
66	65	adantlr	⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = +∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
67	43	adantll	⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 = -∞ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
68	61 66 67	3jaodan	⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
69	68	anasss	⊢ ( ( 𝐴 = -∞ ∧ ( 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
70	46 54 69	3jaoian	⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
71	70	3impb	⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ∧ 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞ ) ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
72	2 71	syl3an3b	⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )
73	1 72	syl3an1b	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝐶 ) )