Theorem expevenpos

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

	Ref	Expression
Hypotheses	expevenpos.mmp.1	|- ( ph -> A e. RR )
	expevenpos.mmp.2	|- ( ph -> N e. NN0 )
	expevenpos.mmp.3	|- ( ph -> 2 || N )
Assertion	expevenpos	|- ( ph -> 0 <_ ( A ^ N ) )

Proof

Step	Hyp	Ref	Expression
1		expevenpos.mmp.1	|- ( ph -> A e. RR )
2		expevenpos.mmp.2	|- ( ph -> N e. NN0 )
3		expevenpos.mmp.3	|- ( ph -> 2 || N )
4	1	ad2antrr	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> A e. RR )
5	4	resqcld	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> ( A ^ 2 ) e. RR )
6		simplr	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> p e. NN0 )
7	4	sqge0d	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> 0 <_ ( A ^ 2 ) )
8	5 6 7	expge0d	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> 0 <_ ( ( A ^ 2 ) ^ p ) )
9		simpr	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> ( 2 x. p ) = N )
10	9	oveq2d	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> ( A ^ ( 2 x. p ) ) = ( A ^ N ) )
11	4	recnd	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> A e. CC )
12		2nn0	|- 2 e. NN0
13	12	a1i	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> 2 e. NN0 )
14	11 6 13	expmuld	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> ( A ^ ( 2 x. p ) ) = ( ( A ^ 2 ) ^ p ) )
15	10 14	eqtr3d	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> ( A ^ N ) = ( ( A ^ 2 ) ^ p ) )
16	8 15	breqtrrd	|- ( ( ( ph /\ p e. NN0 ) /\ ( 2 x. p ) = N ) -> 0 <_ ( A ^ N ) )
17		evennn02n	|- ( N e. NN0 -> ( 2 || N <-> E. p e. NN0 ( 2 x. p ) = N ) )
18	17	biimpa	|- ( ( N e. NN0 /\ 2 || N ) -> E. p e. NN0 ( 2 x. p ) = N )
19	2 3 18	syl2anc	|- ( ph -> E. p e. NN0 ( 2 x. p ) = N )
20	16 19	r19.29a	|- ( ph -> 0 <_ ( A ^ N ) )