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 
|- ( 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 ) )