| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > letr | Structured version Visualization version GIF version | ||
| Description: Transitive law. (Contributed by NM, 12-Nov-1999.) |
| Ref | Expression |
|---|---|
| letr | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leloe 11199 | . . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) | |
| 2 | 1 | 3adant1 1130 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
| 3 | 2 | adantr 480 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
| 4 | lelttr 11203 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
| 5 | ltle 11201 | . . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) | |
| 6 | 5 | 3adant2 1131 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) |
| 7 | 4, 6 | syld 47 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) |
| 8 | 7 | expdimp 452 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶)) |
| 9 | breq2 5093 | . . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶)) | |
| 10 | 9 | biimpcd 249 | . . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶)) |
| 11 | 10 | adantl 481 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶)) |
| 12 | 8, 11 | jaod 859 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶)) |
| 13 | 3, 12 | sylbid 240 | . 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶)) |
| 14 | 13 | expimpd 453 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 class class class wbr 5089 ℝcr 11005 < clt 11146 ≤ cle 11147 |
| 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 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-resscn 11063 ax-pre-lttri 11080 ax-pre-lttrn 11081 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 |
| This theorem is referenced by: letri 11242 letrd 11270 le2add 11599 le2sub 11616 p1le 11966 lemul12b 11978 lemul12a 11979 zletr 12516 peano2uz2 12561 ledivge1le 12963 lemaxle 13094 elfz1b 13493 elfz0fzfz0 13533 fz0fzelfz0 13534 fz0fzdiffz0 13537 elfzmlbp 13539 difelfznle 13542 elincfzoext 13623 ssfzoulel 13660 ssfzo12bi 13661 flge 13709 flflp1 13711 fldiv4p1lem1div2 13739 fldiv4lem1div2uz2 13740 monoord 13939 le2sq2 14042 leexp2r 14081 expubnd 14085 facwordi 14196 faclbnd3 14199 facavg 14208 fi1uzind 14414 swrdswrdlem 14611 swrdccat 14642 01sqrexlem1 15149 01sqrexlem6 15154 01sqrexlem7 15155 leabs 15206 limsupbnd2 15390 rlim3 15405 lo1bdd2 15431 lo1bddrp 15432 o1lo1 15444 lo1mul 15535 lo1le 15559 isercolllem2 15573 iseraltlem2 15590 fsumabs 15708 cvgrat 15790 ruclem9 16147 algcvga 16490 prmdvdsfz 16616 prmfac1 16631 eulerthlem2 16693 modprm0 16717 prmreclem1 16828 prmreclem4 16831 4sqlem11 16867 vdwnnlem3 16909 zntoslem 21493 gsumbagdiaglem 21867 psdmul 22081 cnllycmp 24882 evth 24885 ovoliunlem2 25431 ovolicc2lem3 25447 itg2monolem1 25678 bddiblnc 25770 coeaddlem 26181 coemullem 26182 aalioulem5 26271 aalioulem6 26272 sincosq1lem 26433 emcllem6 26938 ftalem3 27012 fsumvma2 27152 chpchtsum 27157 bcmono 27215 bposlem5 27226 gausslemma2dlem1a 27303 lgsquadlem1 27318 dchrisum0lem1 27454 pntrsumbnd2 27505 pntleml 27549 brbtwn2 28883 axlowdimlem17 28936 axlowdim 28939 crctcshwlkn0lem3 29790 crctcshwlkn0lem5 29792 wwlksubclwwlk 30038 eupth2lems 30218 nmoub3i 30753 ubthlem1 30850 ubthlem2 30851 nmopub2tALT 31889 nmfnleub2 31906 lnconi 32013 leoptr 32117 pjnmopi 32128 cdj3lem2b 32417 eulerpartlemb 34381 isbasisrelowllem1 37399 isbasisrelowllem2 37400 ltflcei 37647 itg2addnclem2 37711 itg2addnclem3 37712 itg2addnc 37713 dvasin 37743 incsequz 37787 mettrifi 37796 equivbnd 37829 bfplem1 37861 jm2.17b 43053 fmul01lt1lem2 45684 eluzge0nn0 47411 elfz2z 47414 iccpartiltu 47521 iccpartgt 47526 lighneallem2 47705 |
| Copyright terms: Public domain | W3C validator |