Metamath Proof Explorer

Theorem oexpreposd

Description: Lemma for dffltz . TODO-SN?: This can be used to show exp11d holds for all integers when the exponent is odd. The more standard -. 2 || M should be used. (Contributed by SN, 4-Mar-2023)

Ref Expression
Hypotheses oexpreposd.n ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
oexpreposd.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
oexpreposd.1 ⊢ ( 𝜑 → ¬ ( 𝑀 / 2 ) ∈ ℕ )
Assertion oexpreposd ( 𝜑 → ( 0 < 𝑁 ↔ 0 < ( 𝑁 ↑ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 oexpreposd.n ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
2 oexpreposd.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 oexpreposd.1 ⊢ ( 𝜑 → ¬ ( 𝑀 / 2 ) ∈ ℕ )
4 1 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑁 ∈ ℝ )
5 2 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6 5 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑀 ∈ ℤ )
7 simpr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 0 < 𝑁 )
8 expgt0 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑁 ) → 0 < ( 𝑁 ↑ 𝑀 ) )
9 4 6 7 8 syl3anc ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 0 < ( 𝑁 ↑ 𝑀 ) )
10 9 ex ⊢ ( 𝜑 → ( 0 < 𝑁 → 0 < ( 𝑁 ↑ 𝑀 ) ) )
11 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
12 11 1 lttrid ⊢ ( 𝜑 → ( 0 < 𝑁 ↔ ¬ ( 0 = 𝑁 ∨ 𝑁 < 0 ) ) )
13 12 notbid ⊢ ( 𝜑 → ( ¬ 0 < 𝑁 ↔ ¬ ¬ ( 0 = 𝑁 ∨ 𝑁 < 0 ) ) )
14 notnotr ⊢ ( ¬ ¬ ( 0 = 𝑁 ∨ 𝑁 < 0 ) → ( 0 = 𝑁 ∨ 𝑁 < 0 ) )
15 0re ⊢ 0 ∈ ℝ
16 15 ltnri ⊢ ¬ 0 < 0
17 2 0expd ⊢ ( 𝜑 → ( 0 ↑ 𝑀 ) = 0 )
18 17 breq2d ⊢ ( 𝜑 → ( 0 < ( 0 ↑ 𝑀 ) ↔ 0 < 0 ) )
19 16 18 mtbiri ⊢ ( 𝜑 → ¬ 0 < ( 0 ↑ 𝑀 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → ¬ 0 < ( 0 ↑ 𝑀 ) )
21 simpr ⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → 0 = 𝑁 )
22 21 eqcomd ⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → 𝑁 = 0 )
23 22 oveq1d ⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → ( 𝑁 ↑ 𝑀 ) = ( 0 ↑ 𝑀 ) )
24 23 breq2d ⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → ( 0 < ( 𝑁 ↑ 𝑀 ) ↔ 0 < ( 0 ↑ 𝑀 ) ) )
25 20 24 mtbird ⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → ¬ 0 < ( 𝑁 ↑ 𝑀 ) )
26 25 ex ⊢ ( 𝜑 → ( 0 = 𝑁 → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
27 1 renegcld ⊢ ( 𝜑 → - 𝑁 ∈ ℝ )
28 27 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝑁 ) → - 𝑁 ∈ ℝ )
29 5 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝑁 ) → 𝑀 ∈ ℤ )
30 simpr ⊢ ( ( 𝜑 ∧ 0 < - 𝑁 ) → 0 < - 𝑁 )
31 expgt0 ⊢ ( ( - 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 0 < - 𝑁 ) → 0 < ( - 𝑁 ↑ 𝑀 ) )
32 28 29 30 31 syl3anc ⊢ ( ( 𝜑 ∧ 0 < - 𝑁 ) → 0 < ( - 𝑁 ↑ 𝑀 ) )
33 32 ex ⊢ ( 𝜑 → ( 0 < - 𝑁 → 0 < ( - 𝑁 ↑ 𝑀 ) ) )
34 1 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
35 simpr ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) ∈ ℤ )
36 zq ⊢ ( ( 𝑀 / 2 ) ∈ ℤ → ( 𝑀 / 2 ) ∈ ℚ )
37 36 adantl ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) ∈ ℚ )
38 qden1elz ⊢ ( ( 𝑀 / 2 ) ∈ ℚ → ( ( denom ‘ ( 𝑀 / 2 ) ) = 1 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
39 37 38 syl ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( ( denom ‘ ( 𝑀 / 2 ) ) = 1 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
40 35 39 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( denom ‘ ( 𝑀 / 2 ) ) = 1 )
41 40 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( ( 𝑀 / 2 ) · ( denom ‘ ( 𝑀 / 2 ) ) ) = ( ( 𝑀 / 2 ) · 1 ) )
42 qmuldeneqnum ⊢ ( ( 𝑀 / 2 ) ∈ ℚ → ( ( 𝑀 / 2 ) · ( denom ‘ ( 𝑀 / 2 ) ) ) = ( numer ‘ ( 𝑀 / 2 ) ) )
43 37 42 syl ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( ( 𝑀 / 2 ) · ( denom ‘ ( 𝑀 / 2 ) ) ) = ( numer ‘ ( 𝑀 / 2 ) ) )
44 35 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) ∈ ℂ )
45 44 mulid1d ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( ( 𝑀 / 2 ) · 1 ) = ( 𝑀 / 2 ) )
46 41 43 45 3eqtr3rd ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) = ( numer ‘ ( 𝑀 / 2 ) ) )
47 2 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
48 2re ⊢ 2 ∈ ℝ
49 48 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
50 2 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
51 2pos ⊢ 0 < 2
52 51 a1i ⊢ ( 𝜑 → 0 < 2 )
53 47 49 50 52 divgt0d ⊢ ( 𝜑 → 0 < ( 𝑀 / 2 ) )
54 qgt0numnn ⊢ ( ( ( 𝑀 / 2 ) ∈ ℚ ∧ 0 < ( 𝑀 / 2 ) ) → ( numer ‘ ( 𝑀 / 2 ) ) ∈ ℕ )
55 36 53 54 syl2anr ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( numer ‘ ( 𝑀 / 2 ) ) ∈ ℕ )
56 46 55 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) ∈ ℕ )
57 3 56 mtand ⊢ ( 𝜑 → ¬ ( 𝑀 / 2 ) ∈ ℤ )
58 evend2 ⊢ ( 𝑀 ∈ ℤ → ( 2 ∥ 𝑀 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
59 5 58 syl ⊢ ( 𝜑 → ( 2 ∥ 𝑀 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
60 57 59 mtbird ⊢ ( 𝜑 → ¬ 2 ∥ 𝑀 )
61 oexpneg ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) → ( - 𝑁 ↑ 𝑀 ) = - ( 𝑁 ↑ 𝑀 ) )
62 34 2 60 61 syl3anc ⊢ ( 𝜑 → ( - 𝑁 ↑ 𝑀 ) = - ( 𝑁 ↑ 𝑀 ) )
63 62 breq2d ⊢ ( 𝜑 → ( 0 < ( - 𝑁 ↑ 𝑀 ) ↔ 0 < - ( 𝑁 ↑ 𝑀 ) ) )
64 63 biimpd ⊢ ( 𝜑 → ( 0 < ( - 𝑁 ↑ 𝑀 ) → 0 < - ( 𝑁 ↑ 𝑀 ) ) )
65 2 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
66 1 65 reexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ 𝑀 ) ∈ ℝ )
67 66 renegcld ⊢ ( 𝜑 → - ( 𝑁 ↑ 𝑀 ) ∈ ℝ )
68 11 67 lttrid ⊢ ( 𝜑 → ( 0 < - ( 𝑁 ↑ 𝑀 ) ↔ ¬ ( 0 = - ( 𝑁 ↑ 𝑀 ) ∨ - ( 𝑁 ↑ 𝑀 ) < 0 ) ) )
69 pm2.46 ⊢ ( ¬ ( 0 = - ( 𝑁 ↑ 𝑀 ) ∨ - ( 𝑁 ↑ 𝑀 ) < 0 ) → ¬ - ( 𝑁 ↑ 𝑀 ) < 0 )
70 68 69 syl6bi ⊢ ( 𝜑 → ( 0 < - ( 𝑁 ↑ 𝑀 ) → ¬ - ( 𝑁 ↑ 𝑀 ) < 0 ) )
71 33 64 70 3syld ⊢ ( 𝜑 → ( 0 < - 𝑁 → ¬ - ( 𝑁 ↑ 𝑀 ) < 0 ) )
72 1 lt0neg1d ⊢ ( 𝜑 → ( 𝑁 < 0 ↔ 0 < - 𝑁 ) )
73 66 lt0neg2d ⊢ ( 𝜑 → ( 0 < ( 𝑁 ↑ 𝑀 ) ↔ - ( 𝑁 ↑ 𝑀 ) < 0 ) )
74 73 notbid ⊢ ( 𝜑 → ( ¬ 0 < ( 𝑁 ↑ 𝑀 ) ↔ ¬ - ( 𝑁 ↑ 𝑀 ) < 0 ) )
75 71 72 74 3imtr4d ⊢ ( 𝜑 → ( 𝑁 < 0 → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
76 26 75 jaod ⊢ ( 𝜑 → ( ( 0 = 𝑁 ∨ 𝑁 < 0 ) → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
77 14 76 syl5 ⊢ ( 𝜑 → ( ¬ ¬ ( 0 = 𝑁 ∨ 𝑁 < 0 ) → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
78 13 77 sylbid ⊢ ( 𝜑 → ( ¬ 0 < 𝑁 → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
79 10 78 impcon4bid ⊢ ( 𝜑 → ( 0 < 𝑁 ↔ 0 < ( 𝑁 ↑ 𝑀 ) ) )