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 ( 𝜑𝐴 ∈ ℕ )
fltltc.b ( 𝜑𝐵 ∈ ℕ )
fltltc.c ( 𝜑𝐶 ∈ ℕ )
fltltc.n ( 𝜑𝑁 ∈ ( ℤ ‘ 3 ) )
fltltc.1 ( 𝜑 → ( ( 𝐴𝑁 ) + ( 𝐵𝑁 ) ) = ( 𝐶𝑁 ) )
Assertion fltltc ( 𝜑𝐵 < 𝐶 )

Proof

Step Hyp Ref Expression
1 fltltc.a ( 𝜑𝐴 ∈ ℕ )
2 fltltc.b ( 𝜑𝐵 ∈ ℕ )
3 fltltc.c ( 𝜑𝐶 ∈ ℕ )
4 fltltc.n ( 𝜑𝑁 ∈ ( ℤ ‘ 3 ) )
5 fltltc.1 ( 𝜑 → ( ( 𝐴𝑁 ) + ( 𝐵𝑁 ) ) = ( 𝐶𝑁 ) )
6 1 nncnd ( 𝜑𝐴 ∈ ℂ )
7 eluzge3nn ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ℕ )
8 4 7 syl ( 𝜑𝑁 ∈ ℕ )
9 8 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
10 6 9 expcld ( 𝜑 → ( 𝐴𝑁 ) ∈ ℂ )
11 2 nncnd ( 𝜑𝐵 ∈ ℂ )
12 11 9 expcld ( 𝜑 → ( 𝐵𝑁 ) ∈ ℂ )
13 10 12 5 mvlladdd ( 𝜑 → ( 𝐵𝑁 ) = ( ( 𝐶𝑁 ) − ( 𝐴𝑁 ) ) )
14 3 nnred ( 𝜑𝐶 ∈ ℝ )
15 14 9 reexpcld ( 𝜑 → ( 𝐶𝑁 ) ∈ ℝ )
16 1 nnrpd ( 𝜑𝐴 ∈ ℝ+ )
17 8 nnzd ( 𝜑𝑁 ∈ ℤ )
18 16 17 rpexpcld ( 𝜑 → ( 𝐴𝑁 ) ∈ ℝ+ )
19 15 18 ltsubrpd ( 𝜑 → ( ( 𝐶𝑁 ) − ( 𝐴𝑁 ) ) < ( 𝐶𝑁 ) )
20 13 19 eqbrtrd ( 𝜑 → ( 𝐵𝑁 ) < ( 𝐶𝑁 ) )
21 2 nnrpd ( 𝜑𝐵 ∈ ℝ+ )
22 3 nnrpd ( 𝜑𝐶 ∈ ℝ+ )
23 21 22 8 ltexp1d ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐵𝑁 ) < ( 𝐶𝑁 ) ) )
24 20 23 mpbird ( 𝜑𝐵 < 𝐶 )