Step |
Hyp |
Ref |
Expression |
1 |
|
fltltc.a |
⊢ ( 𝜑 → 𝐴 ∈ ℕ ) |
2 |
|
fltltc.b |
⊢ ( 𝜑 → 𝐵 ∈ ℕ ) |
3 |
|
fltltc.c |
⊢ ( 𝜑 → 𝐶 ∈ ℕ ) |
4 |
|
fltltc.n |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) |
5 |
|
fltltc.1 |
⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) ) |
6 |
1
|
nncnd |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
7 |
|
eluzge3nn |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ ) |
8 |
4 7
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
9 |
8
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
10 |
6 9
|
expcld |
⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ ) |
11 |
2
|
nncnd |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
12 |
11 9
|
expcld |
⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) ∈ ℂ ) |
13 |
10 12 5
|
mvlladdd |
⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) = ( ( 𝐶 ↑ 𝑁 ) − ( 𝐴 ↑ 𝑁 ) ) ) |
14 |
3
|
nnred |
⊢ ( 𝜑 → 𝐶 ∈ ℝ ) |
15 |
14 9
|
reexpcld |
⊢ ( 𝜑 → ( 𝐶 ↑ 𝑁 ) ∈ ℝ ) |
16 |
1
|
nnrpd |
⊢ ( 𝜑 → 𝐴 ∈ ℝ+ ) |
17 |
8
|
nnzd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
18 |
16 17
|
rpexpcld |
⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ ) |
19 |
15 18
|
ltsubrpd |
⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝑁 ) − ( 𝐴 ↑ 𝑁 ) ) < ( 𝐶 ↑ 𝑁 ) ) |
20 |
13 19
|
eqbrtrd |
⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) < ( 𝐶 ↑ 𝑁 ) ) |
21 |
2
|
nnrpd |
⊢ ( 𝜑 → 𝐵 ∈ ℝ+ ) |
22 |
3
|
nnrpd |
⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) |
23 |
21 22 8
|
ltexp1d |
⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐵 ↑ 𝑁 ) < ( 𝐶 ↑ 𝑁 ) ) ) |
24 |
20 23
|
mpbird |
⊢ ( 𝜑 → 𝐵 < 𝐶 ) |