This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem expevenpos

Description: Even powers are positive. (Contributed by Thierry Arnoux, 9-Nov-2025)

Ref Expression
Hypotheses expevenpos.mmp.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
expevenpos.mmp.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
expevenpos.mmp.3 ⊢ ( 𝜑 → 2 ∥ 𝑁 )
Assertion expevenpos ( 𝜑 → 0 ≤ ( 𝐴 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 expevenpos.mmp.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 expevenpos.mmp.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 expevenpos.mmp.3 ⊢ ( 𝜑 → 2 ∥ 𝑁 )
4 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → 𝐴 ∈ ℝ )
5 4 resqcld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
6 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → 𝑝 ∈ ℕ0 )
7 4 sqge0d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → 0 ≤ ( 𝐴 ↑ 2 ) )
8 5 6 7 expge0d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → 0 ≤ ( ( 𝐴 ↑ 2 ) ↑ 𝑝 ) )
9 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → ( 2 · 𝑝 ) = 𝑁 )
10 9 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → ( 𝐴 ↑ ( 2 · 𝑝 ) ) = ( 𝐴 ↑ 𝑁 ) )
11 4 recnd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → 𝐴 ∈ ℂ )
12 2nn0 ⊢ 2 ∈ ℕ0
13 12 a1i ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → 2 ∈ ℕ0 )
14 11 6 13 expmuld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → ( 𝐴 ↑ ( 2 · 𝑝 ) ) = ( ( 𝐴 ↑ 2 ) ↑ 𝑝 ) )
15 10 14 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → ( 𝐴 ↑ 𝑁 ) = ( ( 𝐴 ↑ 2 ) ↑ 𝑝 ) )
16 8 15 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℕ0 ) ∧ ( 2 · 𝑝 ) = 𝑁 ) → 0 ≤ ( 𝐴 ↑ 𝑁 ) )
17 evennn02n ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ∥ 𝑁 ↔ ∃ 𝑝 ∈ ℕ0 ( 2 · 𝑝 ) = 𝑁 ) )
18 17 biimpa ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ∥ 𝑁 ) → ∃ 𝑝 ∈ ℕ0 ( 2 · 𝑝 ) = 𝑁 )
19 2 3 18 syl2anc ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℕ0 ( 2 · 𝑝 ) = 𝑁 )
20 16 19 r19.29a ⊢ ( 𝜑 → 0 ≤ ( 𝐴 ↑ 𝑁 ) )