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	$$⊢\phi \to A\in \mathbb{N}$$
	fltltc.b	$$⊢\phi \to B\in \mathbb{N}$$
	fltltc.c	$$⊢\phi \to C\in \mathbb{N}$$
	fltltc.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	fltltc.1	$$⊢\phi \to A^N+B^N=C^N$$
Assertion	fltltc	$$⊢\phi \to B<C$$

Proof

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