![]() |
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 11376 | . . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) | |
2 | 1 | 3adant1 1130 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
3 | 2 | adantr 480 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
4 | lelttr 11380 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
5 | ltle 11378 | . . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) | |
6 | 5 | 3adant2 1131 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) |
7 | 4, 6 | syld 47 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) |
8 | 7 | expdimp 452 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶)) |
9 | breq2 5170 | . . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶)) | |
10 | 9 | biimpcd 249 | . . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶)) |
11 | 10 | adantl 481 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶)) |
12 | 8, 11 | jaod 858 | . . 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 846 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 class class class wbr 5166 ℝcr 11183 < clt 11324 ≤ cle 11325 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-resscn 11241 ax-pre-lttri 11258 ax-pre-lttrn 11259 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 |
This theorem is referenced by: letri 11419 letrd 11447 le2add 11772 le2sub 11789 p1le 12139 lemul12b 12151 lemul12a 12152 zletr 12687 peano2uz2 12731 ledivge1le 13128 lemaxle 13257 elfz1b 13653 elfz0fzfz0 13690 fz0fzelfz0 13691 fz0fzdiffz0 13694 elfzmlbp 13696 difelfznle 13699 elincfzoext 13774 ssfzoulel 13810 ssfzo12bi 13811 flge 13856 flflp1 13858 fldiv4p1lem1div2 13886 fldiv4lem1div2uz2 13887 monoord 14083 le2sq2 14185 leexp2r 14224 expubnd 14227 facwordi 14338 faclbnd3 14341 facavg 14350 fi1uzind 14556 swrdswrdlem 14752 swrdccat 14783 01sqrexlem1 15291 01sqrexlem6 15296 01sqrexlem7 15297 leabs 15348 limsupbnd2 15529 rlim3 15544 lo1bdd2 15570 lo1bddrp 15571 o1lo1 15583 lo1mul 15674 lo1le 15700 isercolllem2 15714 iseraltlem2 15731 fsumabs 15849 cvgrat 15931 ruclem9 16286 algcvga 16626 prmdvdsfz 16752 prmfac1 16767 eulerthlem2 16829 modprm0 16852 prmreclem1 16963 prmreclem4 16966 4sqlem11 17002 vdwnnlem3 17044 zntoslem 21598 gsumbagdiaglem 21973 psdmul 22193 cnllycmp 25007 evth 25010 ovoliunlem2 25557 ovolicc2lem3 25573 itg2monolem1 25805 bddiblnc 25897 coeaddlem 26308 coemullem 26309 aalioulem5 26396 aalioulem6 26397 sincosq1lem 26557 emcllem6 27062 ftalem3 27136 fsumvma2 27276 chpchtsum 27281 bcmono 27339 bposlem5 27350 gausslemma2dlem1a 27427 lgsquadlem1 27442 dchrisum0lem1 27578 pntrsumbnd2 27629 pntleml 27673 brbtwn2 28938 axlowdimlem17 28991 axlowdim 28994 crctcshwlkn0lem3 29845 crctcshwlkn0lem5 29847 wwlksubclwwlk 30090 eupth2lems 30270 nmoub3i 30805 ubthlem1 30902 ubthlem2 30903 nmopub2tALT 31941 nmfnleub2 31958 lnconi 32065 leoptr 32169 pjnmopi 32180 cdj3lem2b 32469 eulerpartlemb 34333 isbasisrelowllem1 37321 isbasisrelowllem2 37322 ltflcei 37568 itg2addnclem2 37632 itg2addnclem3 37633 itg2addnc 37634 dvasin 37664 incsequz 37708 mettrifi 37717 equivbnd 37750 bfplem1 37782 jm2.17b 42918 fmul01lt1lem2 45506 eluzge0nn0 47227 elfz2z 47230 iccpartiltu 47296 iccpartgt 47301 lighneallem2 47480 |
Copyright terms: Public domain | W3C validator |