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	|- ( ph -> A e. NN )
	fltltc.b	|- ( ph -> B e. NN )
	fltltc.c	|- ( ph -> C e. NN )
	fltltc.n	|- ( ph -> N e. ( ZZ>= ` 3 ) )
	fltltc.1	|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
Assertion	fltltc	|- ( ph -> B < C )

Proof

Step	Hyp	Ref	Expression
1		fltltc.a	|- ( ph -> A e. NN )
2		fltltc.b	|- ( ph -> B e. NN )
3		fltltc.c	|- ( ph -> C e. NN )
4		fltltc.n	|- ( ph -> N e. ( ZZ>= ` 3 ) )
5		fltltc.1	|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
6	1	nncnd	|- ( ph -> A e. CC )
7		eluzge3nn	|- ( N e. ( ZZ>= ` 3 ) -> N e. NN )
8	4 7	syl	|- ( ph -> N e. NN )
9	8	nnnn0d	|- ( ph -> N e. NN0 )
10	6 9	expcld	|- ( ph -> ( A ^ N ) e. CC )
11	2	nncnd	|- ( ph -> B e. CC )
12	11 9	expcld	|- ( ph -> ( B ^ N ) e. CC )
13	10 12 5	mvlladdd	|- ( ph -> ( B ^ N ) = ( ( C ^ N ) - ( A ^ N ) ) )
14	3	nnred	|- ( ph -> C e. RR )
15	14 9	reexpcld	|- ( ph -> ( C ^ N ) e. RR )
16	1	nnrpd	|- ( ph -> A e. RR+ )
17	8	nnzd	|- ( ph -> N e. ZZ )
18	16 17	rpexpcld	|- ( ph -> ( A ^ N ) e. RR+ )
19	15 18	ltsubrpd	|- ( ph -> ( ( C ^ N ) - ( A ^ N ) ) < ( C ^ N ) )
20	13 19	eqbrtrd	|- ( ph -> ( B ^ N ) < ( C ^ N ) )
21	2	nnrpd	|- ( ph -> B e. RR+ )
22	3	nnrpd	|- ( ph -> C e. RR+ )
23	21 22 8	ltexp1d	|- ( ph -> ( B < C <-> ( B ^ N ) < ( C ^ N ) ) )
24	20 23	mpbird	|- ( ph -> B < C )