Step |
Hyp |
Ref |
Expression |
1 |
|
peano2rem |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℝ ) |
2 |
1
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( 𝐴 − 1 ) ∈ ℝ ) |
3 |
|
simp2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → 𝑁 ∈ ℕ0 ) |
4 |
|
df-neg |
⊢ - 1 = ( 0 − 1 ) |
5 |
|
0re |
⊢ 0 ∈ ℝ |
6 |
|
1re |
⊢ 1 ∈ ℝ |
7 |
|
lesub1 |
⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 − 1 ) ≤ ( 𝐴 − 1 ) ) ) |
8 |
5 6 7
|
mp3an13 |
⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ( 0 − 1 ) ≤ ( 𝐴 − 1 ) ) ) |
9 |
8
|
biimpa |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 − 1 ) ≤ ( 𝐴 − 1 ) ) |
10 |
4 9
|
eqbrtrid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → - 1 ≤ ( 𝐴 − 1 ) ) |
11 |
10
|
3adant2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → - 1 ≤ ( 𝐴 − 1 ) ) |
12 |
|
bernneq |
⊢ ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ - 1 ≤ ( 𝐴 − 1 ) ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) ≤ ( ( 1 + ( 𝐴 − 1 ) ) ↑ 𝑁 ) ) |
13 |
2 3 11 12
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) ≤ ( ( 1 + ( 𝐴 − 1 ) ) ↑ 𝑁 ) ) |
14 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
15 |
1
|
recnd |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℂ ) |
16 |
|
nn0cn |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ ) |
17 |
|
mulcl |
⊢ ( ( ( 𝐴 − 1 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐴 − 1 ) · 𝑁 ) ∈ ℂ ) |
18 |
15 16 17
|
syl2an |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 − 1 ) · 𝑁 ) ∈ ℂ ) |
19 |
|
addcom |
⊢ ( ( 1 ∈ ℂ ∧ ( ( 𝐴 − 1 ) · 𝑁 ) ∈ ℂ ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) = ( ( ( 𝐴 − 1 ) · 𝑁 ) + 1 ) ) |
20 |
14 18 19
|
sylancr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) = ( ( ( 𝐴 − 1 ) · 𝑁 ) + 1 ) ) |
21 |
20
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( 1 + ( ( 𝐴 − 1 ) · 𝑁 ) ) = ( ( ( 𝐴 − 1 ) · 𝑁 ) + 1 ) ) |
22 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
23 |
|
pncan3 |
⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 + ( 𝐴 − 1 ) ) = 𝐴 ) |
24 |
14 22 23
|
sylancr |
⊢ ( 𝐴 ∈ ℝ → ( 1 + ( 𝐴 − 1 ) ) = 𝐴 ) |
25 |
24
|
oveq1d |
⊢ ( 𝐴 ∈ ℝ → ( ( 1 + ( 𝐴 − 1 ) ) ↑ 𝑁 ) = ( 𝐴 ↑ 𝑁 ) ) |
26 |
25
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( ( 1 + ( 𝐴 − 1 ) ) ↑ 𝑁 ) = ( 𝐴 ↑ 𝑁 ) ) |
27 |
13 21 26
|
3brtr3d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( ( ( 𝐴 − 1 ) · 𝑁 ) + 1 ) ≤ ( 𝐴 ↑ 𝑁 ) ) |