![]() |
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 11300 | . . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) | |
2 | 1 | 3adant1 1131 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
3 | 2 | adantr 482 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
4 | lelttr 11304 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
5 | ltle 11302 | . . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) | |
6 | 5 | 3adant2 1132 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) |
7 | 4, 6 | syld 47 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) |
8 | 7 | expdimp 454 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶)) |
9 | breq2 5153 | . . . . . 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 5149 ℝcr 11109 < clt 11248 ≤ cle 11249 |
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 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-resscn 11167 ax-pre-lttri 11184 ax-pre-lttrn 11185 |
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 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 |
This theorem is referenced by: letri 11343 letrd 11371 le2add 11696 le2sub 11713 p1le 12059 lemul12b 12071 lemul12a 12072 zletr 12606 peano2uz2 12650 ledivge1le 13045 lemaxle 13174 elfz1b 13570 elfz0fzfz0 13606 fz0fzelfz0 13607 fz0fzdiffz0 13610 elfzmlbp 13612 difelfznle 13615 elincfzoext 13690 ssfzoulel 13726 ssfzo12bi 13727 flge 13770 flflp1 13772 fldiv4p1lem1div2 13800 fldiv4lem1div2uz2 13801 monoord 13998 le2sq2 14100 leexp2r 14139 expubnd 14142 facwordi 14249 faclbnd3 14252 facavg 14261 fi1uzind 14458 swrdswrdlem 14654 swrdccat 14685 01sqrexlem1 15189 01sqrexlem6 15194 01sqrexlem7 15195 leabs 15246 limsupbnd2 15427 rlim3 15442 lo1bdd2 15468 lo1bddrp 15469 o1lo1 15481 lo1mul 15572 lo1le 15598 isercolllem2 15612 iseraltlem2 15629 fsumabs 15747 cvgrat 15829 ruclem9 16181 algcvga 16516 prmdvdsfz 16642 prmfac1 16658 eulerthlem2 16715 modprm0 16738 prmreclem1 16849 prmreclem4 16852 4sqlem11 16888 vdwnnlem3 16930 zntoslem 21112 gsumbagdiaglemOLD 21491 gsumbagdiaglem 21494 cnllycmp 24472 evth 24475 ovoliunlem2 25020 ovolicc2lem3 25036 itg2monolem1 25268 bddiblnc 25359 coeaddlem 25763 coemullem 25764 aalioulem5 25849 aalioulem6 25850 sincosq1lem 26007 emcllem6 26505 ftalem3 26579 fsumvma2 26717 chpchtsum 26722 bcmono 26780 bposlem5 26791 gausslemma2dlem1a 26868 lgsquadlem1 26883 dchrisum0lem1 27019 pntrsumbnd2 27070 pntleml 27114 brbtwn2 28163 axlowdimlem17 28216 axlowdim 28219 crctcshwlkn0lem3 29066 crctcshwlkn0lem5 29068 wwlksubclwwlk 29311 eupth2lems 29491 nmoub3i 30026 ubthlem1 30123 ubthlem2 30124 nmopub2tALT 31162 nmfnleub2 31179 lnconi 31286 leoptr 31390 pjnmopi 31401 cdj3lem2b 31690 eulerpartlemb 33367 isbasisrelowllem1 36236 isbasisrelowllem2 36237 ltflcei 36476 itg2addnclem2 36540 itg2addnclem3 36541 itg2addnc 36542 dvasin 36572 incsequz 36616 mettrifi 36625 equivbnd 36658 bfplem1 36690 jm2.17b 41700 fmul01lt1lem2 44301 eluzge0nn0 46020 elfz2z 46023 iccpartiltu 46090 iccpartgt 46095 lighneallem2 46274 |
Copyright terms: Public domain | W3C validator |