Proof of Theorem oexpreposd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oexpreposd.n | . . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 2 | 1 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑁) → 𝑁 ∈ ℝ) | 
| 3 |  | oexpreposd.m | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 4 | 3 | nnzd 12642 | . . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 5 | 4 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑁) → 𝑀 ∈ ℤ) | 
| 6 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 0 < 𝑁) → 0 < 𝑁) | 
| 7 |  | expgt0 14137 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 0 <
𝑁) → 0 < (𝑁↑𝑀)) | 
| 8 | 2, 5, 6, 7 | syl3anc 1372 | . . 3
⊢ ((𝜑 ∧ 0 < 𝑁) → 0 < (𝑁↑𝑀)) | 
| 9 | 8 | ex 412 | . 2
⊢ (𝜑 → (0 < 𝑁 → 0 < (𝑁↑𝑀))) | 
| 10 |  | 0red 11265 | . . . . 5
⊢ (𝜑 → 0 ∈
ℝ) | 
| 11 | 10, 1 | lttrid 11400 | . . . 4
⊢ (𝜑 → (0 < 𝑁 ↔ ¬ (0 = 𝑁 ∨ 𝑁 < 0))) | 
| 12 | 11 | notbid 318 | . . 3
⊢ (𝜑 → (¬ 0 < 𝑁 ↔ ¬ ¬ (0 = 𝑁 ∨ 𝑁 < 0))) | 
| 13 |  | notnotr 130 | . . . 4
⊢ (¬
¬ (0 = 𝑁 ∨ 𝑁 < 0) → (0 = 𝑁 ∨ 𝑁 < 0)) | 
| 14 |  | 0re 11264 | . . . . . . . . . 10
⊢ 0 ∈
ℝ | 
| 15 | 14 | ltnri 11371 | . . . . . . . . 9
⊢  ¬ 0
< 0 | 
| 16 | 3 | 0expd 14180 | . . . . . . . . . 10
⊢ (𝜑 → (0↑𝑀) = 0) | 
| 17 | 16 | breq2d 5154 | . . . . . . . . 9
⊢ (𝜑 → (0 < (0↑𝑀) ↔ 0 <
0)) | 
| 18 | 15, 17 | mtbiri 327 | . . . . . . . 8
⊢ (𝜑 → ¬ 0 < (0↑𝑀)) | 
| 19 | 18 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 0 = 𝑁) → ¬ 0 < (0↑𝑀)) | 
| 20 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 0 = 𝑁) → 0 = 𝑁) | 
| 21 | 20 | eqcomd 2742 | . . . . . . . . 9
⊢ ((𝜑 ∧ 0 = 𝑁) → 𝑁 = 0) | 
| 22 | 21 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ 0 = 𝑁) → (𝑁↑𝑀) = (0↑𝑀)) | 
| 23 | 22 | breq2d 5154 | . . . . . . 7
⊢ ((𝜑 ∧ 0 = 𝑁) → (0 < (𝑁↑𝑀) ↔ 0 < (0↑𝑀))) | 
| 24 | 19, 23 | mtbird 325 | . . . . . 6
⊢ ((𝜑 ∧ 0 = 𝑁) → ¬ 0 < (𝑁↑𝑀)) | 
| 25 | 24 | ex 412 | . . . . 5
⊢ (𝜑 → (0 = 𝑁 → ¬ 0 < (𝑁↑𝑀))) | 
| 26 | 1 | renegcld 11691 | . . . . . . . . . 10
⊢ (𝜑 → -𝑁 ∈ ℝ) | 
| 27 | 26 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 0 < -𝑁) → -𝑁 ∈ ℝ) | 
| 28 | 4 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 0 < -𝑁) → 𝑀 ∈ ℤ) | 
| 29 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 0 < -𝑁) → 0 < -𝑁) | 
| 30 |  | expgt0 14137 | . . . . . . . . 9
⊢ ((-𝑁 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 0 <
-𝑁) → 0 < (-𝑁↑𝑀)) | 
| 31 | 27, 28, 29, 30 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 0 < -𝑁) → 0 < (-𝑁↑𝑀)) | 
| 32 | 31 | ex 412 | . . . . . . 7
⊢ (𝜑 → (0 < -𝑁 → 0 < (-𝑁↑𝑀))) | 
| 33 | 1 | recnd 11290 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 34 |  | oexpreposd.1 | . . . . . . . . . . . 12
⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ) | 
| 35 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) → (𝑀 / 2) ∈
ℤ) | 
| 36 |  | zq 12997 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 / 2) ∈ ℤ →
(𝑀 / 2) ∈
ℚ) | 
| 37 | 36 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) → (𝑀 / 2) ∈
ℚ) | 
| 38 |  | qden1elz 16795 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 / 2) ∈ ℚ →
((denom‘(𝑀 / 2)) = 1
↔ (𝑀 / 2) ∈
ℤ)) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) →
((denom‘(𝑀 / 2)) = 1
↔ (𝑀 / 2) ∈
ℤ)) | 
| 40 | 35, 39 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) →
(denom‘(𝑀 / 2)) =
1) | 
| 41 | 40 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) → ((𝑀 / 2) ·
(denom‘(𝑀 / 2))) =
((𝑀 / 2) ·
1)) | 
| 42 |  | qmuldeneqnum 16785 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 / 2) ∈ ℚ →
((𝑀 / 2) ·
(denom‘(𝑀 / 2))) =
(numer‘(𝑀 /
2))) | 
| 43 | 37, 42 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) → ((𝑀 / 2) ·
(denom‘(𝑀 / 2))) =
(numer‘(𝑀 /
2))) | 
| 44 | 35 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) → (𝑀 / 2) ∈
ℂ) | 
| 45 | 44 | mulridd 11279 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) → ((𝑀 / 2) · 1) = (𝑀 / 2)) | 
| 46 | 41, 43, 45 | 3eqtr3rd 2785 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) → (𝑀 / 2) = (numer‘(𝑀 / 2))) | 
| 47 | 3 | nnred 12282 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 48 |  | 2re 12341 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ | 
| 49 | 48 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℝ) | 
| 50 | 3 | nngt0d 12316 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 𝑀) | 
| 51 |  | 2pos 12370 | . . . . . . . . . . . . . . . 16
⊢ 0 <
2 | 
| 52 | 51 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 2) | 
| 53 | 47, 49, 50, 52 | divgt0d 12204 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < (𝑀 / 2)) | 
| 54 |  | qgt0numnn 16789 | . . . . . . . . . . . . . 14
⊢ (((𝑀 / 2) ∈ ℚ ∧ 0
< (𝑀 / 2)) →
(numer‘(𝑀 / 2))
∈ ℕ) | 
| 55 | 36, 53, 54 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) →
(numer‘(𝑀 / 2))
∈ ℕ) | 
| 56 | 46, 55 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑀 / 2) ∈ ℤ) → (𝑀 / 2) ∈
ℕ) | 
| 57 | 34, 56 | mtand 815 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℤ) | 
| 58 |  | evend2 16395 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (2
∥ 𝑀 ↔ (𝑀 / 2) ∈
ℤ)) | 
| 59 | 4, 58 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (2 ∥ 𝑀 ↔ (𝑀 / 2) ∈ ℤ)) | 
| 60 | 57, 59 | mtbird 325 | . . . . . . . . . 10
⊢ (𝜑 → ¬ 2 ∥ 𝑀) | 
| 61 |  | oexpneg 16383 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℕ ∧ ¬ 2
∥ 𝑀) → (-𝑁↑𝑀) = -(𝑁↑𝑀)) | 
| 62 | 33, 3, 60, 61 | syl3anc 1372 | . . . . . . . . 9
⊢ (𝜑 → (-𝑁↑𝑀) = -(𝑁↑𝑀)) | 
| 63 | 62 | breq2d 5154 | . . . . . . . 8
⊢ (𝜑 → (0 < (-𝑁↑𝑀) ↔ 0 < -(𝑁↑𝑀))) | 
| 64 | 63 | biimpd 229 | . . . . . . 7
⊢ (𝜑 → (0 < (-𝑁↑𝑀) → 0 < -(𝑁↑𝑀))) | 
| 65 | 3 | nnnn0d 12589 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 66 | 1, 65 | reexpcld 14204 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁↑𝑀) ∈ ℝ) | 
| 67 | 66 | renegcld 11691 | . . . . . . . . 9
⊢ (𝜑 → -(𝑁↑𝑀) ∈ ℝ) | 
| 68 | 10, 67 | lttrid 11400 | . . . . . . . 8
⊢ (𝜑 → (0 < -(𝑁↑𝑀) ↔ ¬ (0 = -(𝑁↑𝑀) ∨ -(𝑁↑𝑀) < 0))) | 
| 69 |  | pm2.46 882 | . . . . . . . 8
⊢ (¬ (0
= -(𝑁↑𝑀) ∨ -(𝑁↑𝑀) < 0) → ¬ -(𝑁↑𝑀) < 0) | 
| 70 | 68, 69 | biimtrdi 253 | . . . . . . 7
⊢ (𝜑 → (0 < -(𝑁↑𝑀) → ¬ -(𝑁↑𝑀) < 0)) | 
| 71 | 32, 64, 70 | 3syld 60 | . . . . . 6
⊢ (𝜑 → (0 < -𝑁 → ¬ -(𝑁↑𝑀) < 0)) | 
| 72 | 1 | lt0neg1d 11833 | . . . . . 6
⊢ (𝜑 → (𝑁 < 0 ↔ 0 < -𝑁)) | 
| 73 | 66 | lt0neg2d 11834 | . . . . . . 7
⊢ (𝜑 → (0 < (𝑁↑𝑀) ↔ -(𝑁↑𝑀) < 0)) | 
| 74 | 73 | notbid 318 | . . . . . 6
⊢ (𝜑 → (¬ 0 < (𝑁↑𝑀) ↔ ¬ -(𝑁↑𝑀) < 0)) | 
| 75 | 71, 72, 74 | 3imtr4d 294 | . . . . 5
⊢ (𝜑 → (𝑁 < 0 → ¬ 0 < (𝑁↑𝑀))) | 
| 76 | 25, 75 | jaod 859 | . . . 4
⊢ (𝜑 → ((0 = 𝑁 ∨ 𝑁 < 0) → ¬ 0 < (𝑁↑𝑀))) | 
| 77 | 13, 76 | syl5 34 | . . 3
⊢ (𝜑 → (¬ ¬ (0 = 𝑁 ∨ 𝑁 < 0) → ¬ 0 < (𝑁↑𝑀))) | 
| 78 | 12, 77 | sylbid 240 | . 2
⊢ (𝜑 → (¬ 0 < 𝑁 → ¬ 0 < (𝑁↑𝑀))) | 
| 79 | 9, 78 | impcon4bid 227 | 1
⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀))) |