![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > letri3 | Structured version Visualization version GIF version |
Description: Trichotomy law. (Contributed by NM, 14-May-1999.) |
Ref | Expression |
---|---|
letri3 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lttri3 11341 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) | |
2 | 1 | biancomd 463 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐵 < 𝐴 ∧ ¬ 𝐴 < 𝐵))) |
3 | lenlt 11336 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
4 | lenlt 11336 | . . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) | |
5 | 4 | ancoms 458 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
6 | 3, 5 | anbi12d 632 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴) ↔ (¬ 𝐵 < 𝐴 ∧ ¬ 𝐴 < 𝐵))) |
7 | 2, 6 | bitr4d 282 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1536 ∈ wcel 2105 class class class wbr 5147 ℝcr 11151 < clt 11292 ≤ cle 11293 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-resscn 11209 ax-pre-lttri 11226 ax-pre-lttrn 11227 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-po 5596 df-so 5597 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-er 8743 df-en 8984 df-dom 8985 df-sdom 8986 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 |
This theorem is referenced by: eqlelt 11345 eqlei 11368 eqlei2 11369 letri3i 11374 letri3d 11400 lesub0 11777 eqord1 11788 lbreu 12215 nnle1eq1 12293 nn0le0eq0 12551 zextle 12688 uz11 12900 uzin 12915 uzwo 12950 qsqueeze 13239 elfz1eq 13571 faclbnd4lem4 14331 swrdccat3blem 14773 repswswrd 14818 sqeqd 15201 max0add 15345 fsum00 15830 reef11 16151 dvdsabseq 16346 nn0seqcvgd 16603 infpnlem1 16943 gzrngunit 21468 psrbaglesupp 21959 nmoeq0 24772 oprpiece1res2 24996 pcoval2 25062 minveclem7 25482 pjthlem1 25484 iblposlem 25841 dvferm 26040 dveq0 26053 dv11cn 26054 fta1blem 26224 dgrco 26329 aalioulem3 26390 logf1o2 26706 cxpsqrtlem 26758 ang180lem3 26868 chpeq0 27266 chteq0 27267 lgsdir 27390 lgsabs1 27394 minvecolem7 30911 pjhthlem1 31419 pjnormssi 32196 hstles 32259 stge1i 32266 stle0i 32267 stlesi 32269 cdj3lem1 32462 derangen 35156 bfplem2 37809 bfp 37810 acongeq 42971 jm2.26lem3 42989 dvconstbi 44329 zgeltp1eq 47258 zgtp1leeq 48366 |
Copyright terms: Public domain | W3C validator |