Proof of Theorem expnngt1
| Step | Hyp | Ref
| Expression |
| 1 | | elznn 12629 |
. . 3
⊢ (𝐵 ∈ ℤ ↔ (𝐵 ∈ ℝ ∧ (𝐵 ∈ ℕ ∨ -𝐵 ∈
ℕ0))) |
| 2 | | 2a1 28 |
. . . . . 6
⊢ (𝐵 ∈ ℕ → (𝐴 ∈ ℕ → (1 <
(𝐴↑𝐵) → 𝐵 ∈ ℕ))) |
| 3 | 2 | a1d 25 |
. . . . 5
⊢ (𝐵 ∈ ℕ → (𝐵 ∈ ℝ → (𝐴 ∈ ℕ → (1 <
(𝐴↑𝐵) → 𝐵 ∈ ℕ)))) |
| 4 | | nncn 12274 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
| 5 | 4 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ 𝐴 ∈
ℂ) |
| 6 | | recn 11245 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
| 7 | 6 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ 𝐵 ∈
ℂ) |
| 8 | | simp1 1137 |
. . . . . . . . 9
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ -𝐵 ∈
ℕ0) |
| 9 | | expneg2 14111 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ -𝐵 ∈ ℕ0)
→ (𝐴↑𝐵) = (1 / (𝐴↑-𝐵))) |
| 10 | 5, 7, 8, 9 | syl3anc 1373 |
. . . . . . . 8
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ (𝐴↑𝐵) = (1 / (𝐴↑-𝐵))) |
| 11 | 10 | breq2d 5155 |
. . . . . . 7
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ (1 < (𝐴↑𝐵) ↔ 1 < (1 / (𝐴↑-𝐵)))) |
| 12 | | nnre 12273 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
| 13 | | reexpcl 14119 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℕ0)
→ (𝐴↑-𝐵) ∈
ℝ) |
| 14 | 12, 13 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ -𝐵 ∈ ℕ0)
→ (𝐴↑-𝐵) ∈
ℝ) |
| 15 | 14 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐴 ∈ ℕ)
→ (𝐴↑-𝐵) ∈
ℝ) |
| 16 | 12 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐴 ∈ ℕ)
→ 𝐴 ∈
ℝ) |
| 17 | | nn0z 12638 |
. . . . . . . . . . . . 13
⊢ (-𝐵 ∈ ℕ0
→ -𝐵 ∈
ℤ) |
| 18 | 17 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐴 ∈ ℕ)
→ -𝐵 ∈
ℤ) |
| 19 | | nngt0 12297 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 0 <
𝐴) |
| 20 | 19 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐴 ∈ ℕ)
→ 0 < 𝐴) |
| 21 | | expgt0 14136 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℤ ∧ 0 <
𝐴) → 0 < (𝐴↑-𝐵)) |
| 22 | 16, 18, 20, 21 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐴 ∈ ℕ)
→ 0 < (𝐴↑-𝐵)) |
| 23 | 15, 22 | jca 511 |
. . . . . . . . . 10
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐴 ∈ ℕ)
→ ((𝐴↑-𝐵) ∈ ℝ ∧ 0 <
(𝐴↑-𝐵))) |
| 24 | 23 | 3adant2 1132 |
. . . . . . . . 9
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ ((𝐴↑-𝐵) ∈ ℝ ∧ 0 <
(𝐴↑-𝐵))) |
| 25 | | reclt1 12163 |
. . . . . . . . 9
⊢ (((𝐴↑-𝐵) ∈ ℝ ∧ 0 < (𝐴↑-𝐵)) → ((𝐴↑-𝐵) < 1 ↔ 1 < (1 / (𝐴↑-𝐵)))) |
| 26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ ((𝐴↑-𝐵) < 1 ↔ 1 < (1 /
(𝐴↑-𝐵)))) |
| 27 | 12 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ 𝐴 ∈
ℝ) |
| 28 | | nnge1 12294 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → 1 ≤
𝐴) |
| 29 | 28 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ 1 ≤ 𝐴) |
| 30 | 27, 8, 29 | expge1d 14205 |
. . . . . . . . 9
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ 1 ≤ (𝐴↑-𝐵)) |
| 31 | | 1red 11262 |
. . . . . . . . . . 11
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ 1 ∈ ℝ) |
| 32 | 15 | 3adant2 1132 |
. . . . . . . . . . 11
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ (𝐴↑-𝐵) ∈
ℝ) |
| 33 | 31, 32 | lenltd 11407 |
. . . . . . . . . 10
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ (1 ≤ (𝐴↑-𝐵) ↔ ¬ (𝐴↑-𝐵) < 1)) |
| 34 | | pm2.21 123 |
. . . . . . . . . 10
⊢ (¬
(𝐴↑-𝐵) < 1 → ((𝐴↑-𝐵) < 1 → 𝐵 ∈ ℕ)) |
| 35 | 33, 34 | biimtrdi 253 |
. . . . . . . . 9
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ (1 ≤ (𝐴↑-𝐵) → ((𝐴↑-𝐵) < 1 → 𝐵 ∈ ℕ))) |
| 36 | 30, 35 | mpd 15 |
. . . . . . . 8
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ ((𝐴↑-𝐵) < 1 → 𝐵 ∈
ℕ)) |
| 37 | 26, 36 | sylbird 260 |
. . . . . . 7
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ (1 < (1 / (𝐴↑-𝐵)) → 𝐵 ∈ ℕ)) |
| 38 | 11, 37 | sylbid 240 |
. . . . . 6
⊢ ((-𝐵 ∈ ℕ0
∧ 𝐵 ∈ ℝ
∧ 𝐴 ∈ ℕ)
→ (1 < (𝐴↑𝐵) → 𝐵 ∈ ℕ)) |
| 39 | 38 | 3exp 1120 |
. . . . 5
⊢ (-𝐵 ∈ ℕ0
→ (𝐵 ∈ ℝ
→ (𝐴 ∈ ℕ
→ (1 < (𝐴↑𝐵) → 𝐵 ∈ ℕ)))) |
| 40 | 3, 39 | jaoi 858 |
. . . 4
⊢ ((𝐵 ∈ ℕ ∨ -𝐵 ∈ ℕ0)
→ (𝐵 ∈ ℝ
→ (𝐴 ∈ ℕ
→ (1 < (𝐴↑𝐵) → 𝐵 ∈ ℕ)))) |
| 41 | 40 | impcom 407 |
. . 3
⊢ ((𝐵 ∈ ℝ ∧ (𝐵 ∈ ℕ ∨ -𝐵 ∈ ℕ0))
→ (𝐴 ∈ ℕ
→ (1 < (𝐴↑𝐵) → 𝐵 ∈ ℕ))) |
| 42 | 1, 41 | sylbi 217 |
. 2
⊢ (𝐵 ∈ ℤ → (𝐴 ∈ ℕ → (1 <
(𝐴↑𝐵) → 𝐵 ∈ ℕ))) |
| 43 | 42 | 3imp21 1114 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 1 <
(𝐴↑𝐵)) → 𝐵 ∈ ℕ) |