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	⊢ ( 𝜑 → 𝐵 < 𝐶 )