xrltletr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xrltletr		Structured version Visualization version GIF version

Theorem xrltletr 13077

Description: Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)

**Assertion**
Ref	Expression
xrltletr	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))

**Proof of Theorem xrltletr**
Step	Hyp	Ref	Expression
1		xrleloe 13064	. . . 4 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1130	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3		xrlttr 13060	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
4	3	expcomd 416	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 < 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
5		breq2 5099	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 ↔ 𝐴 < 𝐶))
6	5	biimpd 229	. . . . 5 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))
7	6	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
8	4, 7	jaod 859	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
9	2, 8	sylbid 240	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 ≤ 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
10	9	impcomd 411	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 class class class wbr 5095 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-pre-lttri 11102 ax-pre-lttrn 11103

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-po 5531 df-so 5532 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174

This theorem is referenced by: xrltletrd 13081 xrre2 13090 xrre3 13091 ge0gtmnf 13092 xrltmin 13102 supxrunb1 13239 iooss2 13302 ioc0 13313 iccssioo 13336 icossico 13337 icossioo 13361 ioossioo 13362 icoun 13396 ioounsn 13398 ioojoin 13404 lecldbas 23122 mnfnei 23124 icopnfcld 24671 ovolicopnf 25441 voliunlem3 25469 volsup 25473 ioombl 25482 volivth 25524 itg2seq 25659 itg2monolem2 25668 dvfsumrlimge0 25953 dvfsumrlim2 25955 itgsubst 25972 abelth 26367 tanord1 26462 rlimcnp 26891 rlimcnp2 26892 dchrisum0lem2a 27444 pnt 27541 joiniooico 32730 esumfsup 34036 lfuhgr2 35091 relowlssretop 37336 heicant 37634 itg2gt0cn 37654 asindmre 37682 nltle2tri 47298 i0oii 48905

W3C validator