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 
|- ( 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 eluz3nn 
 |-  ( 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 )