fltltc

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

Step	Hyp	Ref	Expression
1		fltltc.a	$⊢ φ \to A \in ℕ$
2		fltltc.b	$⊢ φ \to B \in ℕ$
3		fltltc.c	$⊢ φ \to C \in ℕ$
4		fltltc.n	$⊢ φ \to N \in ℤ_{\geq 3}$
5		fltltc.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
6	1	nncnd	$⊢ φ \to A \in ℂ$
7		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
8	4 7	syl	$⊢ φ \to N \in ℕ$
9	8	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
10	6 9	expcld	$⊢ φ \to A^{N} \in ℂ$
11	2	nncnd	$⊢ φ \to B \in ℂ$
12	11 9	expcld	$⊢ φ \to B^{N} \in ℂ$
13	10 12 5	mvlladdd	$⊢ φ \to B^{N} = C^{N} - A^{N}$
14	3	nnred	$⊢ φ \to C \in ℝ$
15	14 9	reexpcld	$⊢ φ \to C^{N} \in ℝ$
16	1	nnrpd	$⊢ φ \to A \in ℝ^{+}$
17	8	nnzd	$⊢ φ \to N \in ℤ$
18	16 17	rpexpcld	$⊢ φ \to A^{N} \in ℝ^{+}$
19	15 18	ltsubrpd	$⊢ φ \to C^{N} - A^{N} < C^{N}$
20	13 19	eqbrtrd	$⊢ φ \to B^{N} < C^{N}$
21	2	nnrpd	$⊢ φ \to B \in ℝ^{+}$
22	3	nnrpd	$⊢ φ \to C \in ℝ^{+}$
23	21 22 8	ltexp1d	$⊢ φ \to (B < C \leftrightarrow B^{N} < C^{N})$
24	20 23	mpbird	$⊢ φ \to B < C$

Metamath Proof Explorer