xrlelttr - Metamath Proof Explorer

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

Theorem xrlelttr 13070

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

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

**Proof of Theorem xrlelttr**
Step	Hyp	Ref	Expression
1		xrleloe 13058	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
2	1	3adant3 1132	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3		xrlttr 13054	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
4	3	expd 415	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐴 < 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
5		breq1 5101	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
6	5	biimprd 248	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶))
7	6	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
8	4, 7	jaod 859	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵) → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
9	2, 8	sylbid 240	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐴 ≤ 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
10	9	impd 410	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 class class class wbr 5098 ℝ^*cxr 11165 < clt 11166 ≤ cle 11167

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-pre-lttri 11100 ax-pre-lttrn 11101

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-po 5532 df-so 5533 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-er 8635 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172

This theorem is referenced by: xrletr 13072 xrlelttrd 13074 xrre 13084 xrre2 13085 xrmaxlt 13096 supxrun 13231 iooss1 13296 ico0 13307 iccssioo 13331 iccssico 13334 iocssioo 13355 ioossioo 13357 snunioo 13394 leordtval2 23156 lecldbas 23163 pnfnei 23164 bldisj 24342 xbln0 24358 prdsbl 24435 blsscls2 24448 metcnpi3 24490 iocmnfcld 24712 iscau3 25234 ismbf3d 25611 itgsubst 26012 mdegaddle 26035 mdegmullem 26039 ply1divmo 26097 psercnlem2 26390 ftc1anclem6 37895 ftc1anc 37898 asindmre 37900 snunioo1 45754 io1ii 49162

W3C validator