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 φ A
fltltc.b φ B
fltltc.c φ C
fltltc.n φ N 3
fltltc.1 φ A N + B N = C N
Assertion fltltc φ B < C

Proof

Step Hyp Ref Expression
1 fltltc.a φ A
2 fltltc.b φ B
3 fltltc.c φ C
4 fltltc.n φ N 3
5 fltltc.1 φ A N + B N = C N
6 1 nncnd φ A
7 eluzge3nn N 3 N
8 4 7 syl φ N
9 8 nnnn0d φ N 0
10 6 9 expcld φ A N
11 2 nncnd φ B
12 11 9 expcld φ B N
13 10 12 5 mvlladdd φ B N = C N A N
14 3 nnred φ C
15 14 9 reexpcld φ C N
16 1 nnrpd φ A +
17 8 nnzd φ N
18 16 17 rpexpcld φ A N +
19 15 18 ltsubrpd φ C N A N < C N
20 13 19 eqbrtrd φ B N < C N
21 2 nnrpd φ B +
22 3 nnrpd φ C +
23 21 22 8 ltexp1d φ B < C B N < C N
24 20 23 mpbird φ B < C