Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 1exp | Structured version Visualization version GIF version |
Description: Value of one raised to a nonnegative integer power. (Contributed by NM, 15-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.) |
Ref | Expression |
---|---|
1exp | ⊢ (𝑁 ∈ ℤ → (1↑𝑁) = 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1ex 10826 | . . . 4 ⊢ 1 ∈ V | |
2 | 1 | snid 4574 | . . 3 ⊢ 1 ∈ {1} |
3 | ax-1ne0 10795 | . . 3 ⊢ 1 ≠ 0 | |
4 | ax-1cn 10784 | . . . . 5 ⊢ 1 ∈ ℂ | |
5 | snssi 4718 | . . . . 5 ⊢ (1 ∈ ℂ → {1} ⊆ ℂ) | |
6 | 4, 5 | ax-mp 5 | . . . 4 ⊢ {1} ⊆ ℂ |
7 | elsni 4555 | . . . . . 6 ⊢ (𝑥 ∈ {1} → 𝑥 = 1) | |
8 | elsni 4555 | . . . . . 6 ⊢ (𝑦 ∈ {1} → 𝑦 = 1) | |
9 | oveq12 7219 | . . . . . . 7 ⊢ ((𝑥 = 1 ∧ 𝑦 = 1) → (𝑥 · 𝑦) = (1 · 1)) | |
10 | 1t1e1 11989 | . . . . . . 7 ⊢ (1 · 1) = 1 | |
11 | 9, 10 | eqtrdi 2794 | . . . . . 6 ⊢ ((𝑥 = 1 ∧ 𝑦 = 1) → (𝑥 · 𝑦) = 1) |
12 | 7, 8, 11 | syl2an 599 | . . . . 5 ⊢ ((𝑥 ∈ {1} ∧ 𝑦 ∈ {1}) → (𝑥 · 𝑦) = 1) |
13 | ovex 7243 | . . . . . 6 ⊢ (𝑥 · 𝑦) ∈ V | |
14 | 13 | elsn 4553 | . . . . 5 ⊢ ((𝑥 · 𝑦) ∈ {1} ↔ (𝑥 · 𝑦) = 1) |
15 | 12, 14 | sylibr 237 | . . . 4 ⊢ ((𝑥 ∈ {1} ∧ 𝑦 ∈ {1}) → (𝑥 · 𝑦) ∈ {1}) |
16 | 7 | oveq2d 7226 | . . . . . . 7 ⊢ (𝑥 ∈ {1} → (1 / 𝑥) = (1 / 1)) |
17 | 1div1e1 11519 | . . . . . . 7 ⊢ (1 / 1) = 1 | |
18 | 16, 17 | eqtrdi 2794 | . . . . . 6 ⊢ (𝑥 ∈ {1} → (1 / 𝑥) = 1) |
19 | ovex 7243 | . . . . . . 7 ⊢ (1 / 𝑥) ∈ V | |
20 | 19 | elsn 4553 | . . . . . 6 ⊢ ((1 / 𝑥) ∈ {1} ↔ (1 / 𝑥) = 1) |
21 | 18, 20 | sylibr 237 | . . . . 5 ⊢ (𝑥 ∈ {1} → (1 / 𝑥) ∈ {1}) |
22 | 21 | adantr 484 | . . . 4 ⊢ ((𝑥 ∈ {1} ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ {1}) |
23 | 6, 15, 2, 22 | expcl2lem 13644 | . . 3 ⊢ ((1 ∈ {1} ∧ 1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (1↑𝑁) ∈ {1}) |
24 | 2, 3, 23 | mp3an12 1453 | . 2 ⊢ (𝑁 ∈ ℤ → (1↑𝑁) ∈ {1}) |
25 | elsni 4555 | . 2 ⊢ ((1↑𝑁) ∈ {1} → (1↑𝑁) = 1) | |
26 | 24, 25 | syl 17 | 1 ⊢ (𝑁 ∈ ℤ → (1↑𝑁) = 1) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ≠ wne 2939 ⊆ wss 3863 {csn 4538 (class class class)co 7210 ℂcc 10724 0cc0 10726 1c1 10727 · cmul 10731 / cdiv 11486 ℤcz 12173 ↑cexp 13632 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pow 5255 ax-pr 5319 ax-un 7520 ax-cnex 10782 ax-resscn 10783 ax-1cn 10784 ax-icn 10785 ax-addcl 10786 ax-addrcl 10787 ax-mulcl 10788 ax-mulrcl 10789 ax-mulcom 10790 ax-addass 10791 ax-mulass 10792 ax-distr 10793 ax-i2m1 10794 ax-1ne0 10795 ax-1rid 10796 ax-rnegex 10797 ax-rrecex 10798 ax-cnre 10799 ax-pre-lttri 10800 ax-pre-lttrn 10801 ax-pre-ltadd 10802 ax-pre-mulgt0 10803 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2940 df-nel 3044 df-ral 3063 df-rex 3064 df-reu 3065 df-rmo 3066 df-rab 3067 df-v 3407 df-sbc 3692 df-csb 3809 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-pss 3882 df-nul 4235 df-if 4437 df-pw 4512 df-sn 4539 df-pr 4541 df-tp 4543 df-op 4545 df-uni 4817 df-iun 4903 df-br 5051 df-opab 5113 df-mpt 5133 df-tr 5159 df-id 5452 df-eprel 5457 df-po 5465 df-so 5466 df-fr 5506 df-we 5508 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6157 df-ord 6213 df-on 6214 df-lim 6215 df-suc 6216 df-iota 6335 df-fun 6379 df-fn 6380 df-f 6381 df-f1 6382 df-fo 6383 df-f1o 6384 df-fv 6385 df-riota 7167 df-ov 7213 df-oprab 7214 df-mpo 7215 df-om 7642 df-2nd 7759 df-wrecs 8044 df-recs 8105 df-rdg 8143 df-er 8388 df-en 8624 df-dom 8625 df-sdom 8626 df-pnf 10866 df-mnf 10867 df-xr 10868 df-ltxr 10869 df-le 10870 df-sub 11061 df-neg 11062 df-div 11487 df-nn 11828 df-n0 12088 df-z 12174 df-uz 12436 df-seq 13572 df-exp 13633 |
This theorem is referenced by: exprec 13673 sq1 13761 iexpcyc 13772 faclbnd4lem1 13856 iseraltlem2 15243 iseraltlem3 15244 binom1p 15392 binom11 15393 pwm1geoser 15430 esum 15639 ege2le3 15648 eirrlem 15762 odzdvds 16345 efmnd1hash 18316 iblabsr 24724 iblmulc2 24725 abelthlem1 25320 abelthlem3 25322 abelthlem8 25328 abelthlem9 25329 ef2kpi 25365 root1cj 25639 cxpeq 25640 quart 25741 leibpi 25822 log2cnv 25824 mule1 26027 lgseisenlem1 26253 lgseisenlem4 26256 lgseisen 26257 lgsquadlem1 26258 lgsquad2lem1 26262 m1lgs 26266 dchrisum0flblem1 26386 subfaclim 32860 iblmulc2nc 35577 lcmineqlem1 39769 lcmineqlem3 39771 lcmineqlem12 39780 aks4d1p1p2 39809 nn0rppwr 40039 numdenexp 40043 zrtelqelz 40051 expdioph 40546 lhe4.4ex1a 41618 fprodexp 42808 stoweidlem7 43221 stirlinglem5 43292 stirlinglem7 43294 stirlinglem10 43297 2pwp1prm 44712 m1expevenALTV 44770 4fppr1 44858 altgsumbc 45359 |
Copyright terms: Public domain | W3C validator |