Step |
Hyp |
Ref |
Expression |
1 |
|
fltltc.a |
⊢ ( 𝜑 → 𝐴 ∈ ℕ ) |
2 |
|
fltltc.b |
⊢ ( 𝜑 → 𝐵 ∈ ℕ ) |
3 |
|
fltltc.c |
⊢ ( 𝜑 → 𝐶 ∈ ℕ ) |
4 |
|
fltltc.n |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) |
5 |
|
fltltc.1 |
⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) ) |
6 |
|
fltnlta.1 |
⊢ ( 𝜑 → 𝐴 < 𝐵 ) |
7 |
|
eluzge3nn |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ ) |
8 |
4 7
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
9 |
8
|
nnred |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
10 |
3
|
nnred |
⊢ ( 𝜑 → 𝐶 ∈ ℝ ) |
11 |
2
|
nnred |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
12 |
10 11
|
resubcld |
⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℝ ) |
13 |
|
uzuzle23 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) |
14 |
|
uz2m1nn |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ ) |
15 |
4 13 14
|
3syl |
⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ ) |
16 |
15
|
nnnn0d |
⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 ) |
17 |
10 16
|
reexpcld |
⊢ ( 𝜑 → ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℝ ) |
18 |
15
|
nnred |
⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ ) |
19 |
11 16
|
reexpcld |
⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 − 1 ) ) ∈ ℝ ) |
20 |
18 19
|
remulcld |
⊢ ( 𝜑 → ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ ) |
21 |
17 20
|
readdcld |
⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℝ ) |
22 |
12 21
|
remulcld |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) ∈ ℝ ) |
23 |
1
|
nnrpd |
⊢ ( 𝜑 → 𝐴 ∈ ℝ+ ) |
24 |
15
|
nnzd |
⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ ) |
25 |
23 24
|
rpexpcld |
⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ∈ ℝ+ ) |
26 |
22 25
|
rerpdivcld |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ ) |
27 |
1
|
nnred |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
28 |
19 20
|
readdcld |
⊢ ( 𝜑 → ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℝ ) |
29 |
12 28
|
remulcld |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) ∈ ℝ ) |
30 |
29 25
|
rerpdivcld |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ ) |
31 |
12 9
|
remulcld |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · 𝑁 ) ∈ ℝ ) |
32 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
33 |
15
|
nncnd |
⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℂ ) |
34 |
19
|
recnd |
⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 − 1 ) ) ∈ ℂ ) |
35 |
32 33 34
|
adddird |
⊢ ( 𝜑 → ( ( 1 + ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( ( 1 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) |
36 |
8
|
nncnd |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
37 |
32 36
|
pncan3d |
⊢ ( 𝜑 → ( 1 + ( 𝑁 − 1 ) ) = 𝑁 ) |
38 |
37
|
oveq1d |
⊢ ( 𝜑 → ( ( 1 + ( 𝑁 − 1 ) ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) |
39 |
34
|
mulid2d |
⊢ ( 𝜑 → ( 1 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) = ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) |
40 |
39
|
oveq1d |
⊢ ( 𝜑 → ( ( 1 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) = ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) |
41 |
35 38 40
|
3eqtr3rd |
⊢ ( 𝜑 → ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) = ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) |
42 |
41
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) = ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) |
43 |
42
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
44 |
43 30
|
eqeltrrd |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ ) |
45 |
8
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
46 |
45
|
nn0ge0d |
⊢ ( 𝜑 → 0 ≤ 𝑁 ) |
47 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
48 |
1 2 3 4 5
|
fltltc |
⊢ ( 𝜑 → 𝐵 < 𝐶 ) |
49 |
|
nnltp1le |
⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 < 𝐶 ↔ ( 𝐵 + 1 ) ≤ 𝐶 ) ) |
50 |
2 3 49
|
syl2anc |
⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐵 + 1 ) ≤ 𝐶 ) ) |
51 |
48 50
|
mpbid |
⊢ ( 𝜑 → ( 𝐵 + 1 ) ≤ 𝐶 ) |
52 |
11
|
leidd |
⊢ ( 𝜑 → 𝐵 ≤ 𝐵 ) |
53 |
10 11 47 11 51 52
|
lesub3d |
⊢ ( 𝜑 → 1 ≤ ( 𝐶 − 𝐵 ) ) |
54 |
9 12 46 53
|
lemulge12d |
⊢ ( 𝜑 → 𝑁 ≤ ( ( 𝐶 − 𝐵 ) · 𝑁 ) ) |
55 |
12
|
recnd |
⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ ) |
56 |
25
|
rpred |
⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ∈ ℝ ) |
57 |
56
|
recnd |
⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ∈ ℂ ) |
58 |
55 36 57
|
mulassd |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · 𝑁 ) · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) ) |
59 |
58
|
oveq1d |
⊢ ( 𝜑 → ( ( ( ( 𝐶 − 𝐵 ) · 𝑁 ) · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
60 |
55 36
|
mulcld |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · 𝑁 ) ∈ ℂ ) |
61 |
1
|
nncnd |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
62 |
1
|
nnne0d |
⊢ ( 𝜑 → 𝐴 ≠ 0 ) |
63 |
61 62 24
|
expne0d |
⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) ≠ 0 ) |
64 |
60 57 63
|
divcan4d |
⊢ ( 𝜑 → ( ( ( ( 𝐶 − 𝐵 ) · 𝑁 ) · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( 𝐶 − 𝐵 ) · 𝑁 ) ) |
65 |
59 64
|
eqtr3d |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = ( ( 𝐶 − 𝐵 ) · 𝑁 ) ) |
66 |
9 56
|
remulcld |
⊢ ( 𝜑 → ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ ) |
67 |
12 66
|
remulcld |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℝ ) |
68 |
42 29
|
eqeltrrd |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ∈ ℝ ) |
69 |
41 28
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ ) |
70 |
|
difrp |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 ↔ ( 𝐶 − 𝐵 ) ∈ ℝ+ ) ) |
71 |
11 10 70
|
syl2anc |
⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐶 − 𝐵 ) ∈ ℝ+ ) ) |
72 |
48 71
|
mpbid |
⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℝ+ ) |
73 |
8
|
nnrpd |
⊢ ( 𝜑 → 𝑁 ∈ ℝ+ ) |
74 |
2
|
nnrpd |
⊢ ( 𝜑 → 𝐵 ∈ ℝ+ ) |
75 |
23 74 15 6
|
ltexp1dd |
⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − 1 ) ) < ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) |
76 |
56 19 73 75
|
ltmul2dd |
⊢ ( 𝜑 → ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) |
77 |
66 69 72 76
|
ltmul2dd |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) < ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) |
78 |
67 68 25 77
|
ltdiv1dd |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
79 |
65 78
|
eqbrtrrd |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · 𝑁 ) < ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
80 |
9 31 44 54 79
|
lelttrd |
⊢ ( 𝜑 → 𝑁 < ( ( ( 𝐶 − 𝐵 ) · ( 𝑁 · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
81 |
80 43
|
breqtrrd |
⊢ ( 𝜑 → 𝑁 < ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
82 |
3
|
nnrpd |
⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) |
83 |
74 82 15 48
|
ltexp1dd |
⊢ ( 𝜑 → ( 𝐵 ↑ ( 𝑁 − 1 ) ) < ( 𝐶 ↑ ( 𝑁 − 1 ) ) ) |
84 |
19 17 20 83
|
ltadd1dd |
⊢ ( 𝜑 → ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) < ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) |
85 |
28 21 72 84
|
ltmul2dd |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) < ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) ) |
86 |
29 22 25 85
|
ltdiv1dd |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐵 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
87 |
9 30 26 81 86
|
lttrd |
⊢ ( 𝜑 → 𝑁 < ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
88 |
27 45
|
reexpcld |
⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℝ ) |
89 |
1 2 3 4 5
|
fltnltalem |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) < ( 𝐴 ↑ 𝑁 ) ) |
90 |
22 88 25 89
|
ltdiv1dd |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
91 |
36 32
|
nncand |
⊢ ( 𝜑 → ( 𝑁 − ( 𝑁 − 1 ) ) = 1 ) |
92 |
91
|
oveq2d |
⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − ( 𝑁 − 1 ) ) ) = ( 𝐴 ↑ 1 ) ) |
93 |
8
|
nnzd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
94 |
61 62 24 93
|
expsubd |
⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 − ( 𝑁 − 1 ) ) ) = ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) ) |
95 |
61
|
exp1d |
⊢ ( 𝜑 → ( 𝐴 ↑ 1 ) = 𝐴 ) |
96 |
92 94 95
|
3eqtr3d |
⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) = 𝐴 ) |
97 |
90 96
|
breqtrd |
⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) · ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) + ( ( 𝑁 − 1 ) · ( 𝐵 ↑ ( 𝑁 − 1 ) ) ) ) ) / ( 𝐴 ↑ ( 𝑁 − 1 ) ) ) < 𝐴 ) |
98 |
9 26 27 87 97
|
lttrd |
⊢ ( 𝜑 → 𝑁 < 𝐴 ) |