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 ≤ ( 𝐴 ↑ 𝑁 ) )