This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oexpled

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

Ref Expression
Hypotheses oexpled.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
oexpled.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
oexpled.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
oexpled.4 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
oexpled.5 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
Assertion oexpled ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oexpled.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 oexpled.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 oexpled.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 oexpled.4 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
5 oexpled.5 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
6 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
7 0red ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → 0 ∈ ℝ )
8 1 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
9 1 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
10 2 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → 𝐵 ∈ ℝ )
11 3 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12 11 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → 𝑁 ∈ ℕ0 )
13 simpr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → 0 ≤ 𝐴 )
14 5 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → 𝐴 ≤ 𝐵 )
15 9 10 12 13 14 leexp1ad ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐴 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )
16 15 adantlr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 0 ≤ 𝐴 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )
17 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ∈ ℝ )
18 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → 𝑁 ∈ ℕ0 )
19 17 18 reexpcld ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
20 0red ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → 0 ∈ ℝ )
21 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → 𝐵 ∈ ℝ )
22 21 18 reexpcld ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℝ )
23 3 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
24 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
25 23 24 npcand ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
26 25 oveq2d ⊢ ( 𝜑 → ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝐴 ↑ 𝑁 ) )
27 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
28 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
29 3 28 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
30 27 29 expp1d ⊢ ( 𝜑 → ( 𝐴 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 𝐴 ) )
31 26 30 eqtr3d ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) = ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 𝐴 ) )
32 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 ↑ 𝑁 ) = ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 𝐴 ) )
33 1 29 reexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
35 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
36 oddm1even ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) )
37 36 biimpa ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → 2 ∥ ( 𝑁 − 1 ) )
38 35 4 37 syl2anc ⊢ ( 𝜑 → 2 ∥ ( 𝑁 − 1 ) )
39 1 29 38 expevenpos ⊢ ( 𝜑 → 0 ≤ ( 𝐴 ↑ ( 𝑁 − 1 ) ) )
40 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → 0 ≤ ( 𝐴 ↑ ( 𝑁 − 1 ) ) )
41 simpr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ≤ 0 )
42 17 20 34 40 41 lemul2ad ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 𝐴 ) ≤ ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 0 ) )
43 34 recnd ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
44 43 mul01d ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 0 ) = 0 )
45 42 44 breqtrd ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) · 𝐴 ) ≤ 0 )
46 32 45 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 ↑ 𝑁 ) ≤ 0 )
47 simplr ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → 0 ≤ 𝐵 )
48 21 18 47 expge0d ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → 0 ≤ ( 𝐵 ↑ 𝑁 ) )
49 19 20 22 46 48 letrd ⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝐵 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )
50 7 8 16 49 lecasei ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )
51 1 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → 𝐴 ∈ ℝ )
52 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → 𝑁 ∈ ℕ0 )
53 51 52 reexpcld ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
54 2 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → 𝐵 ∈ ℝ )
55 54 52 reexpcld ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℝ )
56 2 renegcld ⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → - 𝐵 ∈ ℝ )
58 1 renegcld ⊢ ( 𝜑 → - 𝐴 ∈ ℝ )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → - 𝐴 ∈ ℝ )
60 2 le0neg1d ⊢ ( 𝜑 → ( 𝐵 ≤ 0 ↔ 0 ≤ - 𝐵 ) )
61 60 biimpa ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → 0 ≤ - 𝐵 )
62 5 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → 𝐴 ≤ 𝐵 )
63 leneg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ - 𝐵 ≤ - 𝐴 ) )
64 63 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → - 𝐵 ≤ - 𝐴 )
65 51 54 62 64 syl21anc ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → - 𝐵 ≤ - 𝐴 )
66 57 59 52 61 65 leexp1ad ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( - 𝐵 ↑ 𝑁 ) ≤ ( - 𝐴 ↑ 𝑁 ) )
67 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
68 oexpneg ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( - 𝐵 ↑ 𝑁 ) = - ( 𝐵 ↑ 𝑁 ) )
69 67 3 4 68 syl3anc ⊢ ( 𝜑 → ( - 𝐵 ↑ 𝑁 ) = - ( 𝐵 ↑ 𝑁 ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( - 𝐵 ↑ 𝑁 ) = - ( 𝐵 ↑ 𝑁 ) )
71 oexpneg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )
72 27 3 4 71 syl3anc ⊢ ( 𝜑 → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )
74 66 70 73 3brtr3d ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → - ( 𝐵 ↑ 𝑁 ) ≤ - ( 𝐴 ↑ 𝑁 ) )
75 leneg ⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℝ ∧ ( 𝐵 ↑ 𝑁 ) ∈ ℝ ) → ( ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) ↔ - ( 𝐵 ↑ 𝑁 ) ≤ - ( 𝐴 ↑ 𝑁 ) ) )
76 75 biimpar ⊢ ( ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℝ ∧ ( 𝐵 ↑ 𝑁 ) ∈ ℝ ) ∧ - ( 𝐵 ↑ 𝑁 ) ≤ - ( 𝐴 ↑ 𝑁 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )
77 53 55 74 76 syl21anc ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )
78 6 2 50 77 lecasei ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )