This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fltltc

Description: ( C ^ N ) is the largest term and therefore B < C . (Contributed by Steven Nguyen, 22-Aug-2023)

Ref Expression
Hypotheses fltltc.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
fltltc.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
fltltc.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
fltltc.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
fltltc.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
Assertion fltltc ( 𝜑 → 𝐵 < 𝐶 )

Proof

Step Hyp Ref Expression
1 fltltc.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 fltltc.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 fltltc.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 fltltc.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
5 fltltc.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
6 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 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 ⊢ ( 𝜑 → 𝐵 < 𝐶 )