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 11820

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 11809	. . . . 5 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1071	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3		xrlttr 11805	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
4	3	expcomd 452	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 < 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
5		breq2 4578	. . . . . . 7 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 ↔ 𝐴 < 𝐶))
6	5	biimpd 217	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))
7	6	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
8	4, 7	jaod 393	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
9	2, 8	sylbid 228	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 ≤ 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
10	9	com23 83	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐴 < 𝐵 → (𝐵 ≤ 𝐶 → 𝐴 < 𝐶)))
11	10	impd 445	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 194 ∨ wo 381 ∧ wa 382 ∧ w3a 1030 = wceq 1474 ∈ wcel 1976 class class class wbr 4574 ℝ^*cxr 9926 < clt 9927 ≤ cle 9928

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1712 ax-4 1727 ax-5 1826 ax-6 1874 ax-7 1921 ax-8 1978 ax-9 1985 ax-10 2005 ax-11 2020 ax-12 2032 ax-13 2229 ax-ext 2586 ax-sep 4700 ax-nul 4709 ax-pow 4761 ax-pr 4825 ax-un 6821 ax-cnex 9845 ax-resscn 9846 ax-pre-lttri 9863 ax-pre-lttrn 9864

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-ex 1695 df-nf 1700 df-sb 1867 df-eu 2458 df-mo 2459 df-clab 2593 df-cleq 2599 df-clel 2602 df-nfc 2736 df-ne 2778 df-nel 2779 df-ral 2897 df-rex 2898 df-rab 2901 df-v 3171 df-sbc 3399 df-csb 3496 df-dif 3539 df-un 3541 df-in 3543 df-ss 3550 df-nul 3871 df-if 4033 df-pw 4106 df-sn 4122 df-pr 4124 df-op 4128 df-uni 4364 df-br 4575 df-opab 4635 df-mpt 4636 df-id 4940 df-po 4946 df-so 4947 df-xp 5031 df-rel 5032 df-cnv 5033 df-co 5034 df-dm 5035 df-rn 5036 df-res 5037 df-ima 5038 df-iota 5751 df-fun 5789 df-fn 5790 df-f 5791 df-f1 5792 df-fo 5793 df-f1o 5794 df-fv 5795 df-er 7603 df-en 7816 df-dom 7817 df-sdom 7818 df-pnf 9929 df-mnf 9930 df-xr 9931 df-ltxr 9932 df-le 9933

This theorem is referenced by: xrltletrd 11824 xrre2 11831 xrre3 11832 ge0gtmnf 11833 xrltmin 11843 supxrunb1 11974 iooss2 12035 ioc0 12046 iccssioo 12066 icossico 12067 icossioo 12088 ioossioo 12089 icoun 12120 ioojoin 12127 lecldbas 20772 mnfnei 20774 icopnfcld 22310 ovolicopnf 23013 voliunlem3 23041 volsup 23045 ioombl 23054 volivth 23095 itg2seq 23229 itg2monolem2 23238 dvfsumrlimge0 23511 dvfsumrlim2 23513 itgsubst 23530 abelth 23913 tanord1 24001 rlimcnp 24406 rlimcnp2 24407 dchrisum0lem2a 24920 pnt 25017 joiniooico 28729 esumfsup 29262 relowlssretop 32187 heicant 32414 itg2gt0cn 32435 asindmre 32465 ioounsn 36614 snunioo2 38379 nltle2tri 39744 frgrwopreglem2 41481