![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpexpcl | Structured version Visualization version GIF version |
Description: Closure law for exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.) |
Ref | Expression |
---|---|
rpexpcl | ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 483 | . 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℝ+) | |
2 | rpne0 12260 | . . 3 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0) | |
3 | 2 | adantr 481 | . 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → 𝐴 ≠ 0) |
4 | simpr 485 | . 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ) | |
5 | rpssre 12251 | . . . 4 ⊢ ℝ+ ⊆ ℝ | |
6 | ax-resscn 10445 | . . . 4 ⊢ ℝ ⊆ ℂ | |
7 | 5, 6 | sstri 3902 | . . 3 ⊢ ℝ+ ⊆ ℂ |
8 | rpmulcl 12267 | . . 3 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 · 𝑦) ∈ ℝ+) | |
9 | 1rp 12248 | . . 3 ⊢ 1 ∈ ℝ+ | |
10 | rpreccl 12270 | . . . 4 ⊢ (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ+) | |
11 | 10 | adantr 481 | . . 3 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ ℝ+) |
12 | 7, 8, 9, 11 | expcl2lem 13296 | . 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+) |
13 | 1, 3, 4, 12 | syl3anc 1364 | 1 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2081 ≠ wne 2984 (class class class)co 7021 ℂcc 10386 ℝcr 10387 0cc0 10388 1c1 10389 / cdiv 11150 ℤcz 11834 ℝ+crp 12244 ↑cexp 13284 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-cnex 10444 ax-resscn 10445 ax-1cn 10446 ax-icn 10447 ax-addcl 10448 ax-addrcl 10449 ax-mulcl 10450 ax-mulrcl 10451 ax-mulcom 10452 ax-addass 10453 ax-mulass 10454 ax-distr 10455 ax-i2m1 10456 ax-1ne0 10457 ax-1rid 10458 ax-rnegex 10459 ax-rrecex 10460 ax-cnre 10461 ax-pre-lttri 10462 ax-pre-lttrn 10463 ax-pre-ltadd 10464 ax-pre-mulgt0 10465 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-pss 3880 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-tp 4481 df-op 4483 df-uni 4750 df-iun 4831 df-br 4967 df-opab 5029 df-mpt 5046 df-tr 5069 df-id 5353 df-eprel 5358 df-po 5367 df-so 5368 df-fr 5407 df-we 5409 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-pred 6028 df-ord 6074 df-on 6075 df-lim 6076 df-suc 6077 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-riota 6982 df-ov 7024 df-oprab 7025 df-mpo 7026 df-om 7442 df-2nd 7551 df-wrecs 7803 df-recs 7865 df-rdg 7903 df-er 8144 df-en 8363 df-dom 8364 df-sdom 8365 df-pnf 10528 df-mnf 10529 df-xr 10530 df-ltxr 10531 df-le 10532 df-sub 10724 df-neg 10725 df-div 11151 df-nn 11492 df-n0 11751 df-z 11835 df-uz 12099 df-rp 12245 df-seq 13225 df-exp 13285 |
This theorem is referenced by: expgt0 13317 ltexp2a 13385 expcan 13388 ltexp2 13389 leexp2a 13391 ltexp2r 13392 expnlbnd2 13450 rpexpcld 13463 expcnv 15057 effsumlt 15302 ef01bndlem 15375 rpnnen2lem11 15415 iscmet3lem3 23581 iscmet3lem1 23582 iscmet3lem2 23583 iscmet3 23584 minveclem3 23720 pjthlem1 23728 aaliou3lem1 24619 aaliou3lem2 24620 aaliou3lem3 24621 aaliou3lem8 24622 aaliou3lem5 24624 aaliou3lem6 24625 aaliou3lem7 24626 aaliou3lem9 24627 tanregt0 24809 asinlem3 25135 cxp2limlem 25240 ftalem5 25341 basellem3 25347 basellem4 25348 basellem8 25352 chebbnd1lem3 25734 dchrisum0lem1a 25749 dchrisum0lem1b 25778 dchrisum0lem1 25779 dchrisum0lem2a 25780 dchrisum0lem2 25781 dchrisum0lem3 25782 pntlemd 25857 pntlema 25859 pntlemb 25860 pntlemh 25862 pntlemr 25865 pntlemi 25867 pntlemf 25868 pntlemo 25870 pntlem3 25872 pntleml 25874 ostth2lem1 25881 ostth3 25901 minvecolem3 28349 pjhthlem1 28864 dpexpp1 30273 dya2icoseg 31157 faclimlem3 32591 geomcau 34591 dignnld 44170 |
Copyright terms: Public domain | W3C validator |