Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > lenltd | GIF version |
Description: 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
Ref | Expression |
---|---|
lenltd | ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | ltd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
3 | lenlt 7995 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
4 | 1, 2, 3 | syl2anc 409 | 1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 104 ∈ wcel 2141 class class class wbr 3989 ℝcr 7773 < clt 7954 ≤ cle 7955 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-14 2144 ax-ext 2152 ax-sep 4107 ax-pow 4160 ax-pr 4194 |
This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-v 2732 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-br 3990 df-opab 4051 df-xp 4617 df-cnv 4619 df-xr 7958 df-le 7960 |
This theorem is referenced by: ltnsymd 8039 nltled 8040 lensymd 8041 leadd1 8349 lemul1 8512 leltap 8544 ap0gt0 8559 prodgt0 8768 prodge0 8770 lediv1 8785 lemuldiv 8797 lerec 8800 lt2msq 8802 le2msq 8817 squeeze0 8820 suprleubex 8870 0mnnnnn0 9167 elnn0z 9225 uzm1 9517 infregelbex 9557 fztri3or 9995 fzdisj 10008 uzdisj 10049 nn0disj 10094 fzouzdisj 10136 elfzonelfzo 10186 flqeqceilz 10274 modifeq2int 10342 modsumfzodifsn 10352 nn0leexp2 10645 expcanlem 10649 fimaxq 10762 resqrexlemoverl 10985 leabs 11038 absle 11053 maxleast 11177 minmax 11193 climge0 11288 pcfac 12302 cxple 13631 |
Copyright terms: Public domain | W3C validator |