Metamath Proof Explorer

Theorem oexpled

Description: Odd power monomials are monotonic. (Contributed by Thierry Arnoux, 9-Nov-2025)

Ref Expression
Hypotheses oexpled.1 
|- ( ph -> A e. RR )
oexpled.2 
|- ( ph -> B e. RR )
oexpled.3 
|- ( ph -> N e. NN )
oexpled.4 
|- ( ph -> -. 2 || N )
oexpled.5 
|- ( ph -> A <_ B )
Assertion oexpled 
|- ( ph -> ( A ^ N ) <_ ( B ^ N ) )

Proof

Step Hyp Ref Expression
1 oexpled.1 
 |-  ( ph -> A e. RR )
2 oexpled.2 
 |-  ( ph -> B e. RR )
3 oexpled.3 
 |-  ( ph -> N e. NN )
4 oexpled.4 
 |-  ( ph -> -. 2 || N )
5 oexpled.5 
 |-  ( ph -> A <_ B )
6 0red 
 |-  ( ph -> 0 e. RR )
7 0red 
 |-  ( ( ph /\ 0 <_ B ) -> 0 e. RR )
8 1 adantr 
 |-  ( ( ph /\ 0 <_ B ) -> A e. RR )
9 1 adantr 
 |-  ( ( ph /\ 0 <_ A ) -> A e. RR )
10 2 adantr 
 |-  ( ( ph /\ 0 <_ A ) -> B e. RR )
11 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
12 11 adantr 
 |-  ( ( ph /\ 0 <_ A ) -> N e. NN0 )
13 simpr 
 |-  ( ( ph /\ 0 <_ A ) -> 0 <_ A )
14 5 adantr 
 |-  ( ( ph /\ 0 <_ A ) -> A <_ B )
15 9 10 12 13 14 leexp1ad 
 |-  ( ( ph /\ 0 <_ A ) -> ( A ^ N ) <_ ( B ^ N ) )
16 15 adantlr 
 |-  ( ( ( ph /\ 0 <_ B ) /\ 0 <_ A ) -> ( A ^ N ) <_ ( B ^ N ) )
17 1 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> A e. RR )
18 11 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> N e. NN0 )
19 17 18 reexpcld 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( A ^ N ) e. RR )
20 0red 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> 0 e. RR )
21 2 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> B e. RR )
22 21 18 reexpcld 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( B ^ N ) e. RR )
23 3 nncnd 
 |-  ( ph -> N e. CC )
24 1cnd 
 |-  ( ph -> 1 e. CC )
25 23 24 npcand 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
26 25 oveq2d 
 |-  ( ph -> ( A ^ ( ( N - 1 ) + 1 ) ) = ( A ^ N ) )
27 1 recnd 
 |-  ( ph -> A e. CC )
28 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
29 3 28 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
30 27 29 expp1d 
 |-  ( ph -> ( A ^ ( ( N - 1 ) + 1 ) ) = ( ( A ^ ( N - 1 ) ) x. A ) )
31 26 30 eqtr3d 
 |-  ( ph -> ( A ^ N ) = ( ( A ^ ( N - 1 ) ) x. A ) )
32 31 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( A ^ N ) = ( ( A ^ ( N - 1 ) ) x. A ) )
33 1 29 reexpcld 
 |-  ( ph -> ( A ^ ( N - 1 ) ) e. RR )
34 33 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( A ^ ( N - 1 ) ) e. RR )
35 3 nnzd 
 |-  ( ph -> N e. ZZ )
36 oddm1even 
 |-  ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )
37 36 biimpa 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> 2 || ( N - 1 ) )
38 35 4 37 syl2anc 
 |-  ( ph -> 2 || ( N - 1 ) )
39 1 29 38 expevenpos 
 |-  ( ph -> 0 <_ ( A ^ ( N - 1 ) ) )
40 39 ad2antrr 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> 0 <_ ( A ^ ( N - 1 ) ) )
41 simpr 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> A <_ 0 )
42 17 20 34 40 41 lemul2ad 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( ( A ^ ( N - 1 ) ) x. A ) <_ ( ( A ^ ( N - 1 ) ) x. 0 ) )
43 34 recnd 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( A ^ ( N - 1 ) ) e. CC )
44 43 mul01d 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( ( A ^ ( N - 1 ) ) x. 0 ) = 0 )
45 42 44 breqtrd 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( ( A ^ ( N - 1 ) ) x. A ) <_ 0 )
46 32 45 eqbrtrd 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( A ^ N ) <_ 0 )
47 simplr 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> 0 <_ B )
48 21 18 47 expge0d 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> 0 <_ ( B ^ N ) )
49 19 20 22 46 48 letrd 
 |-  ( ( ( ph /\ 0 <_ B ) /\ A <_ 0 ) -> ( A ^ N ) <_ ( B ^ N ) )
50 7 8 16 49 lecasei 
 |-  ( ( ph /\ 0 <_ B ) -> ( A ^ N ) <_ ( B ^ N ) )
51 1 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> A e. RR )
52 11 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> N e. NN0 )
53 51 52 reexpcld 
 |-  ( ( ph /\ B <_ 0 ) -> ( A ^ N ) e. RR )
54 2 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> B e. RR )
55 54 52 reexpcld 
 |-  ( ( ph /\ B <_ 0 ) -> ( B ^ N ) e. RR )
56 2 renegcld 
 |-  ( ph -> -u B e. RR )
57 56 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> -u B e. RR )
58 1 renegcld 
 |-  ( ph -> -u A e. RR )
59 58 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> -u A e. RR )
60 2 le0neg1d 
 |-  ( ph -> ( B <_ 0 <-> 0 <_ -u B ) )
61 60 biimpa 
 |-  ( ( ph /\ B <_ 0 ) -> 0 <_ -u B )
62 5 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> A <_ B )
63 leneg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -u B <_ -u A ) )
64 63 biimpa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> -u B <_ -u A )
65 51 54 62 64 syl21anc 
 |-  ( ( ph /\ B <_ 0 ) -> -u B <_ -u A )
66 57 59 52 61 65 leexp1ad 
 |-  ( ( ph /\ B <_ 0 ) -> ( -u B ^ N ) <_ ( -u A ^ N ) )
67 2 recnd 
 |-  ( ph -> B e. CC )
68 oexpneg 
 |-  ( ( B e. CC /\ N e. NN /\ -. 2 || N ) -> ( -u B ^ N ) = -u ( B ^ N ) )
69 67 3 4 68 syl3anc 
 |-  ( ph -> ( -u B ^ N ) = -u ( B ^ N ) )
70 69 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> ( -u B ^ N ) = -u ( B ^ N ) )
71 oexpneg 
 |-  ( ( A e. CC /\ N e. NN /\ -. 2 || N ) -> ( -u A ^ N ) = -u ( A ^ N ) )
72 27 3 4 71 syl3anc 
 |-  ( ph -> ( -u A ^ N ) = -u ( A ^ N ) )
73 72 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> ( -u A ^ N ) = -u ( A ^ N ) )
74 66 70 73 3brtr3d 
 |-  ( ( ph /\ B <_ 0 ) -> -u ( B ^ N ) <_ -u ( A ^ N ) )
75 leneg 
 |-  ( ( ( A ^ N ) e. RR /\ ( B ^ N ) e. RR ) -> ( ( A ^ N ) <_ ( B ^ N ) <-> -u ( B ^ N ) <_ -u ( A ^ N ) ) )
76 75 biimpar 
 |-  ( ( ( ( A ^ N ) e. RR /\ ( B ^ N ) e. RR ) /\ -u ( B ^ N ) <_ -u ( A ^ N ) ) -> ( A ^ N ) <_ ( B ^ N ) )
77 53 55 74 76 syl21anc 
 |-  ( ( ph /\ B <_ 0 ) -> ( A ^ N ) <_ ( B ^ N ) )
78 6 2 50 77 lecasei 
 |-  ( ph -> ( A ^ N ) <_ ( B ^ N ) )