Metamath Proof Explorer

Theorem oexpled

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

Ref Expression
Hypotheses oexpled.1 ⊢ φ → A ∈ ℝ
oexpled.2 ⊢ φ → B ∈ ℝ
oexpled.3 ⊢ φ → N ∈ ℕ
oexpled.4 ⊢ φ → ¬ 2 ∥ N
oexpled.5 ⊢ φ → A ≤ B
Assertion oexpled ⊢ φ → A N ≤ B N

Proof

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