![]() |
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 11297 | . . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) | |
2 | 1 | 3adant1 1131 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
3 | 2 | adantr 482 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
4 | lelttr 11301 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
5 | ltle 11299 | . . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) | |
6 | 5 | 3adant2 1132 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) |
7 | 4, 6 | syld 47 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) |
8 | 7 | expdimp 454 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶)) |
9 | breq2 5152 | . . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶)) | |
10 | 9 | biimpcd 248 | . . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶)) |
11 | 10 | adantl 483 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶)) |
12 | 8, 11 | jaod 858 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶)) |
13 | 3, 12 | sylbid 239 | . 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶)) |
14 | 13 | expimpd 455 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 class class class wbr 5148 ℝcr 11106 < clt 11245 ≤ cle 11246 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-resscn 11164 ax-pre-lttri 11181 ax-pre-lttrn 11182 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-er 8700 df-en 8937 df-dom 8938 df-sdom 8939 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 |
This theorem is referenced by: letri 11340 letrd 11368 le2add 11693 le2sub 11710 p1le 12056 lemul12b 12068 lemul12a 12069 zletr 12603 peano2uz2 12647 ledivge1le 13042 lemaxle 13171 elfz1b 13567 elfz0fzfz0 13603 fz0fzelfz0 13604 fz0fzdiffz0 13607 elfzmlbp 13609 difelfznle 13612 elincfzoext 13687 ssfzoulel 13723 ssfzo12bi 13724 flge 13767 flflp1 13769 fldiv4p1lem1div2 13797 fldiv4lem1div2uz2 13798 monoord 13995 le2sq2 14097 leexp2r 14136 expubnd 14139 facwordi 14246 faclbnd3 14249 facavg 14258 fi1uzind 14455 swrdswrdlem 14651 swrdccat 14682 01sqrexlem1 15186 01sqrexlem6 15191 01sqrexlem7 15192 leabs 15243 limsupbnd2 15424 rlim3 15439 lo1bdd2 15465 lo1bddrp 15466 o1lo1 15478 lo1mul 15569 lo1le 15595 isercolllem2 15609 iseraltlem2 15626 fsumabs 15744 cvgrat 15826 ruclem9 16178 algcvga 16513 prmdvdsfz 16639 prmfac1 16655 eulerthlem2 16712 modprm0 16735 prmreclem1 16846 prmreclem4 16849 4sqlem11 16885 vdwnnlem3 16927 zntoslem 21104 gsumbagdiaglemOLD 21483 gsumbagdiaglem 21486 cnllycmp 24464 evth 24467 ovoliunlem2 25012 ovolicc2lem3 25028 itg2monolem1 25260 bddiblnc 25351 coeaddlem 25755 coemullem 25756 aalioulem5 25841 aalioulem6 25842 sincosq1lem 25999 emcllem6 26495 ftalem3 26569 fsumvma2 26707 chpchtsum 26712 bcmono 26770 bposlem5 26781 gausslemma2dlem1a 26858 lgsquadlem1 26873 dchrisum0lem1 27009 pntrsumbnd2 27060 pntleml 27104 brbtwn2 28153 axlowdimlem17 28206 axlowdim 28209 crctcshwlkn0lem3 29056 crctcshwlkn0lem5 29058 wwlksubclwwlk 29301 eupth2lems 29481 nmoub3i 30014 ubthlem1 30111 ubthlem2 30112 nmopub2tALT 31150 nmfnleub2 31167 lnconi 31274 leoptr 31378 pjnmopi 31389 cdj3lem2b 31678 eulerpartlemb 33356 isbasisrelowllem1 36225 isbasisrelowllem2 36226 ltflcei 36465 itg2addnclem2 36529 itg2addnclem3 36530 itg2addnc 36531 dvasin 36561 incsequz 36605 mettrifi 36614 equivbnd 36647 bfplem1 36679 jm2.17b 41686 fmul01lt1lem2 44288 eluzge0nn0 46007 elfz2z 46010 iccpartiltu 46077 iccpartgt 46082 lighneallem2 46261 |
Copyright terms: Public domain | W3C validator |