Metamath Proof Explorer

Theorem 2exp11

Description: Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021)

Ref Expression
Assertion 2exp11 ( 2 ↑ 1 1 ) = 2 0 4 8

Proof

Step Hyp Ref Expression
1 8p3e11 ⊢ ( 8 + 3 ) = 1 1
2 1 eqcomi ⊢ 1 1 = ( 8 + 3 )
3 2 oveq2i ⊢ ( 2 ↑ 1 1 ) = ( 2 ↑ ( 8 + 3 ) )
4 2cn ⊢ 2 ∈ ℂ
5 8nn0 ⊢ 8 ∈ ℕ0
6 3nn0 ⊢ 3 ∈ ℕ0
7 expadd ⊢ ( ( 2 ∈ ℂ ∧ 8 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) → ( 2 ↑ ( 8 + 3 ) ) = ( ( 2 ↑ 8 ) · ( 2 ↑ 3 ) ) )
8 4 5 6 7 mp3an ⊢ ( 2 ↑ ( 8 + 3 ) ) = ( ( 2 ↑ 8 ) · ( 2 ↑ 3 ) )
9 3 8 eqtri ⊢ ( 2 ↑ 1 1 ) = ( ( 2 ↑ 8 ) · ( 2 ↑ 3 ) )
10 2exp8 ⊢ ( 2 ↑ 8 ) = 2 5 6
11 cu2 ⊢ ( 2 ↑ 3 ) = 8
12 10 11 oveq12i ⊢ ( ( 2 ↑ 8 ) · ( 2 ↑ 3 ) ) = ( 2 5 6 · 8 )
13 2nn0 ⊢ 2 ∈ ℕ0
14 5nn0 ⊢ 5 ∈ ℕ0
15 13 14 deccl ⊢ 2 5 ∈ ℕ0
16 6nn0 ⊢ 6 ∈ ℕ0
17 eqid ⊢ 2 5 6 = 2 5 6
18 4nn0 ⊢ 4 ∈ ℕ0
19 0nn0 ⊢ 0 ∈ ℕ0
20 13 19 deccl ⊢ 2 0 ∈ ℕ0
21 eqid ⊢ 2 5 = 2 5
22 1nn0 ⊢ 1 ∈ ℕ0
23 8cn ⊢ 8 ∈ ℂ
24 8t2e16 ⊢ ( 8 · 2 ) = 1 6
25 23 4 24 mulcomli ⊢ ( 2 · 8 ) = 1 6
26 1p1e2 ⊢ ( 1 + 1 ) = 2
27 6p4e10 ⊢ ( 6 + 4 ) = 1 0
28 22 16 18 25 26 19 27 decaddci ⊢ ( ( 2 · 8 ) + 4 ) = 2 0
29 5cn ⊢ 5 ∈ ℂ
30 8t5e40 ⊢ ( 8 · 5 ) = 4 0
31 23 29 30 mulcomli ⊢ ( 5 · 8 ) = 4 0
32 5 13 14 21 19 18 28 31 decmul1c ⊢ ( 2 5 · 8 ) = 2 0 0
33 4cn ⊢ 4 ∈ ℂ
34 33 addlidi ⊢ ( 0 + 4 ) = 4
35 20 19 18 32 34 decaddi ⊢ ( ( 2 5 · 8 ) + 4 ) = 2 0 4
36 6cn ⊢ 6 ∈ ℂ
37 8t6e48 ⊢ ( 8 · 6 ) = 4 8
38 23 36 37 mulcomli ⊢ ( 6 · 8 ) = 4 8
39 5 15 16 17 5 18 35 38 decmul1c ⊢ ( 2 5 6 · 8 ) = 2 0 4 8
40 12 39 eqtri ⊢ ( ( 2 ↑ 8 ) · ( 2 ↑ 3 ) ) = 2 0 4 8
41 9 40 eqtri ⊢ ( 2 ↑ 1 1 ) = 2 0 4 8