Theorem expevenpos

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

	Ref	Expression
Hypotheses	expevenpos.mmp.1	$$⊢\phi \to A\in ℝ$$
	expevenpos.mmp.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	expevenpos.mmp.3	$$⊢\phi \to 2\parallel N$$
Assertion	expevenpos	$$⊢\phi \to 0\le A^N$$

Proof

Step	Hyp	Ref	Expression
1		expevenpos.mmp.1	$$⊢\phi \to A\in ℝ$$
2		expevenpos.mmp.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3		expevenpos.mmp.3	$$⊢\phi \to 2\parallel N$$
4	1	ad2antrr	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to A\in ℝ$$
5	4	resqcld	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to A^2\in ℝ$$
6		simplr	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to p\in {\mathbb{N}}_0$$
7	4	sqge0d	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to 0\le A^2$$
8	5 6 7	expge0d	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to 0\le {\left(A^2\right)}^p$$
9		simpr	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to 2p=N$$
10	9	oveq2d	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to A^{2p}=A^N$$
11	4	recnd	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to A\in ℂ$$
12		2nn0	$$⊢2\in {\mathbb{N}}_0$$
13	12	a1i	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to 2\in {\mathbb{N}}_0$$
14	11 6 13	expmuld	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to A^{2p}={\left(A^2\right)}^p$$
15	10 14	eqtr3d	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to A^N={\left(A^2\right)}^p$$
16	8 15	breqtrrd	$$⊢\left(\left(\phi \wedge p\in {\mathbb{N}}_0\right)\wedge 2p=N\right)\to 0\le A^N$$
17		evennn02n	$$⊢N\in {\mathbb{N}}_0\to \left(2\parallel N\leftrightarrow \exists p\in {\mathbb{N}}_{0}2p=N\right)$$
18	17	biimpa	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2\parallel N\right)\to \exists p\in {\mathbb{N}}_{0}2p=N$$
19	2 3 18	syl2anc	$$⊢\phi \to \exists p\in {\mathbb{N}}_{0}2p=N$$
20	16 19	r19.29a	$$⊢\phi \to 0\le A^N$$