![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1div1e1 | Structured version Visualization version Unicode version |
Description: 1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.) |
Ref | Expression |
---|---|
1div1e1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 9583 |
. 2
![]() ![]() ![]() ![]() | |
2 | div1 10287 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1672 ax-4 1685 ax-5 1761 ax-6 1808 ax-7 1854 ax-8 1892 ax-9 1899 ax-10 1918 ax-11 1923 ax-12 1936 ax-13 2091 ax-ext 2431 ax-sep 4496 ax-nul 4505 ax-pow 4553 ax-pr 4611 ax-un 6570 ax-resscn 9582 ax-1cn 9583 ax-icn 9584 ax-addcl 9585 ax-addrcl 9586 ax-mulcl 9587 ax-mulrcl 9588 ax-mulcom 9589 ax-addass 9590 ax-mulass 9591 ax-distr 9592 ax-i2m1 9593 ax-1ne0 9594 ax-1rid 9595 ax-rnegex 9596 ax-rrecex 9597 ax-cnre 9598 ax-pre-lttri 9599 ax-pre-lttrn 9600 ax-pre-ltadd 9601 ax-pre-mulgt0 9602 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 987 df-3an 988 df-tru 1450 df-ex 1667 df-nf 1671 df-sb 1801 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3014 df-sbc 3235 df-csb 3331 df-dif 3374 df-un 3376 df-in 3378 df-ss 3385 df-nul 3699 df-if 3849 df-pw 3920 df-sn 3936 df-pr 3938 df-op 3942 df-uni 4168 df-br 4374 df-opab 4433 df-mpt 4434 df-id 4726 df-po 4732 df-so 4733 df-xp 4817 df-rel 4818 df-cnv 4819 df-co 4820 df-dm 4821 df-rn 4822 df-res 4823 df-ima 4824 df-iota 5524 df-fun 5562 df-fn 5563 df-f 5564 df-f1 5565 df-fo 5566 df-f1o 5567 df-fv 5568 df-riota 6237 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-er 7349 df-en 7556 df-dom 7557 df-sdom 7558 df-pnf 9663 df-mnf 9664 df-xr 9665 df-ltxr 9666 df-le 9667 df-sub 9848 df-neg 9849 df-div 10258 |
This theorem is referenced by: recdiv 10301 reclt1 10489 recgt1 10490 halflt1 10820 expneg 12273 m1expcl2 12287 1exp 12294 resqrex 13324 trireciplem 13930 fproddiv 14025 ef0lem 14143 eft0val 14176 m1expaddsub 17149 gzrngunit 19043 cnmsgnsubg 19155 psgninv 19160 vitali 22582 advlogexp 23611 logtayllem 23615 efrlim 23906 emcllem2 23933 emcllem7 23938 logexprlim 24164 dchrinvcl 24192 bclbnd 24219 lgseisenlem1 24288 lgseisenlem2 24289 lgsquadlem1 24293 dchrmusum2 24343 dchrvmasum2lem 24345 mulogsum 24381 pntrsumo1 24414 pnt2 24462 pnt 24463 qqh1 28795 faclimlem1 30384 faclim 30387 pellexlem2 35675 elpell1qr2 35719 bccn0 36692 binomcxplemradcnv 36701 mccl 37719 dvnprodlem3 37864 stoweidlem13 37929 stoweidlem42 37959 fourierdlem62 38088 sec0 40804 |
Copyright terms: Public domain | W3C validator |