Theorem xrlttri 13127

Description: Ordering on the extended reals satisfies strict trichotomy. New proofs should generally use this instead of ax-pre-lttri 11133 or axlttri 11240. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
xrlttri	⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))

Proof of Theorem xrlttri

Step	Hyp	Ref	Expression
1		xrltnr 13107	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴)
2	1	adantr 483	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 = 𝐵) → ¬ 𝐴 < 𝐴)
3		breq2 5094	. . . . . . . 8 ⊢ (𝐴 = 𝐵 → (𝐴 < 𝐴 ↔ 𝐴 < 𝐵))
4	3	adantl 484	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 = 𝐵) → (𝐴 < 𝐴 ↔ 𝐴 < 𝐵))
5	2, 4	mtbid 326	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 = 𝐵) → ¬ 𝐴 < 𝐵)
6	5	ex 415	. . . . 5 ⊢ (𝐴 ∈ ℝ* → (𝐴 = 𝐵 → ¬ 𝐴 < 𝐵))
7	6	adantr 483	. . . 4 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 → ¬ 𝐴 < 𝐵))
8		xrltnsym 13125	. . . . 5 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐵 < 𝐴 → ¬ 𝐴 < 𝐵))
9	8	ancoms 461	. . . 4 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐵 < 𝐴 → ¬ 𝐴 < 𝐵))
10	7, 9	jaod 868	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴 = 𝐵 ∨ 𝐵 < 𝐴) → ¬ 𝐴 < 𝐵))
11		elxr 13104	. . . 4 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
12		elxr 13104	. . . 4 ⊢ (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
13		axlttri 11240	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
14	13	biimprd 250	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴) → 𝐴 < 𝐵))
15	14	con1d 145	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
16		ltpnf 13108	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
17	16	adantr 483	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < +∞)
18		breq2 5094	. . . . . . . . 9 ⊢ (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 𝐴 < +∞))
19	18	adantl 484	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 𝐴 < +∞))
20	17, 19	mpbird 259	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
21	20	pm2.24d 151	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
22		mnflt 13111	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
23	22	adantr 483	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → -∞ < 𝐴)
24		breq1 5093	. . . . . . . . . 10 ⊢ (𝐵 = -∞ → (𝐵 < 𝐴 ↔ -∞ < 𝐴))
25	24	adantl 484	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 < 𝐴 ↔ -∞ < 𝐴))
26	23, 25	mpbird 259	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐵 < 𝐴)
27	26	olcd 883	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
28	27	a1d 25	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
29	15, 21, 28	3jaodan 1442	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
30		ltpnf 13108	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
31	30	adantl 484	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐵 < +∞)
32		breq2 5094	. . . . . . . . . 10 ⊢ (𝐴 = +∞ → (𝐵 < 𝐴 ↔ 𝐵 < +∞))
33	32	adantr 483	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 < 𝐴 ↔ 𝐵 < +∞))
34	31, 33	mpbird 259	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐵 < 𝐴)
35	34	olcd 883	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
36	35	a1d 25	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
37		eqtr3 2774	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → 𝐴 = 𝐵)
38	37	orcd 882	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
39	38	a1d 25	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
40		mnfltpnf 13114	. . . . . . . . . 10 ⊢ -∞ < +∞
41		breq12 5095	. . . . . . . . . 10 ⊢ ((𝐵 = -∞ ∧ 𝐴 = +∞) → (𝐵 < 𝐴 ↔ -∞ < +∞))
42	40, 41	mpbiri 260	. . . . . . . . 9 ⊢ ((𝐵 = -∞ ∧ 𝐴 = +∞) → 𝐵 < 𝐴)
43	42	ancoms 461	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 < 𝐴)
44	43	olcd 883	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
45	44	a1d 25	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
46	36, 39, 45	3jaodan 1442	. . . . 5 ⊢ ((𝐴 = +∞ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
47		mnflt 13111	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ → -∞ < 𝐵)
48	47	adantl 484	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → -∞ < 𝐵)
49		breq1 5093	. . . . . . . . 9 ⊢ (𝐴 = -∞ → (𝐴 < 𝐵 ↔ -∞ < 𝐵))
50	49	adantr 483	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ -∞ < 𝐵))
51	48, 50	mpbird 259	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 < 𝐵)
52	51	pm2.24d 151	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
53		breq12 5095	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ -∞ < +∞))
54	40, 53	mpbiri 260	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
55	54	pm2.24d 151	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
56		eqtr3 2774	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → 𝐴 = 𝐵)
57	56	orcd 882	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))
58	57	a1d 25	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
59	52, 55, 58	3jaodan 1442	. . . . 5 ⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
60	29, 46, 59	3jaoian 1441	. . . 4 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
61	11, 12, 60	syl2anb 606	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (¬ 𝐴 < 𝐵 → (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
62	10, 61	impbid 214	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴 = 𝐵 ∨ 𝐵 < 𝐴) ↔ ¬ 𝐴 < 𝐵))
63	62	con2bid 356	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 856   ∨ w3o 1094   = wceq 1550   ∈ wcel 2132   class class class wbr 5090  ℝcr 11058  +∞cpnf 11199  -∞cmnf 11200  ℝ^*cxr 11201   < clt 11202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-cnex 11115  ax-resscn 11116  ax-pre-lttri 11133  ax-pre-lttrn 11134

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-xr 11206  df-ltxr 11207

This theorem is referenced by:  xrltso  13129  xrleloe  13132  xrltlen  13134