![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > gt0ne0d | GIF version |
Description: Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
gt0ne0d.1 | ⊢ (𝜑 → 0 < 𝐴) |
Ref | Expression |
---|---|
gt0ne0d | ⊢ (𝜑 → 𝐴 ≠ 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 7409 | . 2 ⊢ 0 ∈ ℝ | |
2 | gt0ne0d.1 | . 2 ⊢ (𝜑 → 0 < 𝐴) | |
3 | ltne 7491 | . 2 ⊢ ((0 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0) | |
4 | 1, 2, 3 | sylancr 405 | 1 ⊢ (𝜑 → 𝐴 ≠ 0) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1436 ≠ wne 2251 class class class wbr 3814 ℝcr 7270 0cc0 7271 < clt 7443 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-10 1439 ax-11 1440 ax-i12 1441 ax-bndl 1442 ax-4 1443 ax-13 1447 ax-14 1448 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 ax-sep 3925 ax-pow 3977 ax-pr 4003 ax-un 4227 ax-setind 4319 ax-cnex 7357 ax-resscn 7358 ax-1re 7360 ax-addrcl 7363 ax-rnegex 7375 ax-pre-ltirr 7378 |
This theorem depends on definitions: df-bi 115 df-3an 924 df-tru 1290 df-fal 1293 df-nf 1393 df-sb 1690 df-eu 1948 df-mo 1949 df-clab 2072 df-cleq 2078 df-clel 2081 df-nfc 2214 df-ne 2252 df-nel 2347 df-ral 2360 df-rex 2361 df-rab 2364 df-v 2616 df-dif 2988 df-un 2990 df-in 2992 df-ss 2999 df-pw 3411 df-sn 3431 df-pr 3432 df-op 3434 df-uni 3631 df-br 3815 df-opab 3869 df-xp 4410 df-pnf 7445 df-mnf 7446 df-ltxr 7448 |
This theorem is referenced by: modqval 9634 modqvalr 9635 modqcl 9636 flqpmodeq 9637 modq0 9639 modqge0 9642 modqlt 9643 modqdiffl 9645 modqdifz 9646 modqvalp1 9653 modqid 9659 modqcyc 9669 modqadd1 9671 modqmuladd 9676 modqmuladdnn0 9678 modqmul1 9687 modqdi 9702 modqsubdir 9703 |
Copyright terms: Public domain | W3C validator |