![]() |
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 11246 | . . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) | |
2 | 1 | 3adant1 1131 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
3 | 2 | adantr 482 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
4 | lelttr 11250 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
5 | ltle 11248 | . . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) | |
6 | 5 | 3adant2 1132 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) |
7 | 4, 6 | syld 47 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) |
8 | 7 | expdimp 454 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶)) |
9 | breq2 5110 | . . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶)) | |
10 | 9 | biimpcd 249 | . . . . 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 5106 ℝcr 11055 < clt 11194 ≤ cle 11195 |
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 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 ax-resscn 11113 ax-pre-lttri 11130 ax-pre-lttrn 11131 |
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 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 df-er 8651 df-en 8887 df-dom 8888 df-sdom 8889 df-pnf 11196 df-mnf 11197 df-xr 11198 df-ltxr 11199 df-le 11200 |
This theorem is referenced by: letri 11289 letrd 11317 le2add 11642 le2sub 11659 p1le 12005 lemul12b 12017 lemul12a 12018 zletr 12552 peano2uz2 12596 ledivge1le 12991 lemaxle 13120 elfz1b 13516 elfz0fzfz0 13552 fz0fzelfz0 13553 fz0fzdiffz0 13556 elfzmlbp 13558 difelfznle 13561 elincfzoext 13636 ssfzoulel 13672 ssfzo12bi 13673 flge 13716 flflp1 13718 fldiv4p1lem1div2 13746 fldiv4lem1div2uz2 13747 monoord 13944 le2sq2 14046 leexp2r 14085 expubnd 14088 facwordi 14195 faclbnd3 14198 facavg 14207 fi1uzind 14402 swrdswrdlem 14598 swrdccat 14629 01sqrexlem1 15133 01sqrexlem6 15138 01sqrexlem7 15139 leabs 15190 limsupbnd2 15371 rlim3 15386 lo1bdd2 15412 lo1bddrp 15413 o1lo1 15425 lo1mul 15516 lo1le 15542 isercolllem2 15556 iseraltlem2 15573 fsumabs 15691 cvgrat 15773 ruclem9 16125 algcvga 16460 prmdvdsfz 16586 prmfac1 16602 eulerthlem2 16659 modprm0 16682 prmreclem1 16793 prmreclem4 16796 4sqlem11 16832 vdwnnlem3 16874 zntoslem 20979 gsumbagdiaglemOLD 21356 gsumbagdiaglem 21359 cnllycmp 24335 evth 24338 ovoliunlem2 24883 ovolicc2lem3 24899 itg2monolem1 25131 bddiblnc 25222 coeaddlem 25626 coemullem 25627 aalioulem5 25712 aalioulem6 25713 sincosq1lem 25870 emcllem6 26366 ftalem3 26440 fsumvma2 26578 chpchtsum 26583 bcmono 26641 bposlem5 26652 gausslemma2dlem1a 26729 lgsquadlem1 26744 dchrisum0lem1 26880 pntrsumbnd2 26931 pntleml 26975 brbtwn2 27896 axlowdimlem17 27949 axlowdim 27952 crctcshwlkn0lem3 28799 crctcshwlkn0lem5 28801 wwlksubclwwlk 29044 eupth2lems 29224 nmoub3i 29757 ubthlem1 29854 ubthlem2 29855 nmopub2tALT 30893 nmfnleub2 30910 lnconi 31017 leoptr 31121 pjnmopi 31132 cdj3lem2b 31421 eulerpartlemb 33025 isbasisrelowllem1 35872 isbasisrelowllem2 35873 ltflcei 36112 itg2addnclem2 36176 itg2addnclem3 36177 itg2addnc 36178 dvasin 36208 incsequz 36253 mettrifi 36262 equivbnd 36295 bfplem1 36327 jm2.17b 41328 fmul01lt1lem2 43912 eluzge0nn0 45630 elfz2z 45633 iccpartiltu 45700 iccpartgt 45705 lighneallem2 45884 |
Copyright terms: Public domain | W3C validator |