Proof of Theorem tanhlt1
| Step | Hyp | Ref
| Expression |
| 1 | | ax-icn 11214 |
. . . . . . 7
⊢ i ∈
ℂ |
| 2 | | recn 11245 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 3 | | mulcl 11239 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (i
· 𝐴) ∈
ℂ) |
| 5 | | rpcoshcl 16193 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(cos‘(i · 𝐴))
∈ ℝ+) |
| 6 | 5 | rpne0d 13082 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(cos‘(i · 𝐴))
≠ 0) |
| 7 | | tanval 16164 |
. . . . . 6
⊢ (((i
· 𝐴) ∈ ℂ
∧ (cos‘(i · 𝐴)) ≠ 0) → (tan‘(i ·
𝐴)) = ((sin‘(i
· 𝐴)) /
(cos‘(i · 𝐴)))) |
| 8 | 4, 6, 7 | syl2anc 584 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(tan‘(i · 𝐴))
= ((sin‘(i · 𝐴)) / (cos‘(i · 𝐴)))) |
| 9 | 8 | oveq1d 7446 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((tan‘(i · 𝐴))
/ i) = (((sin‘(i · 𝐴)) / (cos‘(i · 𝐴))) / i)) |
| 10 | 4 | sincld 16166 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(sin‘(i · 𝐴))
∈ ℂ) |
| 11 | | recoshcl 16194 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(cos‘(i · 𝐴))
∈ ℝ) |
| 12 | 11 | recnd 11289 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(cos‘(i · 𝐴))
∈ ℂ) |
| 13 | 1 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℝ → i ∈
ℂ) |
| 14 | | ine0 11698 |
. . . . . 6
⊢ i ≠
0 |
| 15 | 14 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℝ → i ≠
0) |
| 16 | 10, 12, 13, 6, 15 | divdiv32d 12068 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(((sin‘(i · 𝐴)) / (cos‘(i · 𝐴))) / i) = (((sin‘(i
· 𝐴)) / i) /
(cos‘(i · 𝐴)))) |
| 17 | | sinhval 16190 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((sin‘(i · 𝐴))
/ i) = (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) |
| 18 | 2, 17 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((sin‘(i · 𝐴))
/ i) = (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) |
| 19 | | coshval 16191 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(cos‘(i · 𝐴))
= (((exp‘𝐴) +
(exp‘-𝐴)) /
2)) |
| 20 | 2, 19 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(cos‘(i · 𝐴))
= (((exp‘𝐴) +
(exp‘-𝐴)) /
2)) |
| 21 | 18, 20 | oveq12d 7449 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(((sin‘(i · 𝐴)) / i) / (cos‘(i · 𝐴))) = ((((exp‘𝐴) − (exp‘-𝐴)) / 2) / (((exp‘𝐴) + (exp‘-𝐴)) / 2))) |
| 22 | 9, 16, 21 | 3eqtrd 2781 |
. . 3
⊢ (𝐴 ∈ ℝ →
((tan‘(i · 𝐴))
/ i) = ((((exp‘𝐴)
− (exp‘-𝐴)) /
2) / (((exp‘𝐴) +
(exp‘-𝐴)) /
2))) |
| 23 | | reefcl 16123 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(exp‘𝐴) ∈
ℝ) |
| 24 | | renegcl 11572 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) |
| 25 | 24 | reefcld 16124 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(exp‘-𝐴) ∈
ℝ) |
| 26 | 23, 25 | resubcld 11691 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((exp‘𝐴) −
(exp‘-𝐴)) ∈
ℝ) |
| 27 | 26 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((exp‘𝐴) −
(exp‘-𝐴)) ∈
ℂ) |
| 28 | 23, 25 | readdcld 11290 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((exp‘𝐴) +
(exp‘-𝐴)) ∈
ℝ) |
| 29 | 28 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((exp‘𝐴) +
(exp‘-𝐴)) ∈
ℂ) |
| 30 | | 2cnd 12344 |
. . . 4
⊢ (𝐴 ∈ ℝ → 2 ∈
ℂ) |
| 31 | 20, 6 | eqnetrrd 3009 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(((exp‘𝐴) +
(exp‘-𝐴)) / 2) ≠
0) |
| 32 | | 2ne0 12370 |
. . . . . . 7
⊢ 2 ≠
0 |
| 33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 2 ≠
0) |
| 34 | 29, 30, 33 | divne0bd 12055 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(((exp‘𝐴) +
(exp‘-𝐴)) ≠ 0
↔ (((exp‘𝐴) +
(exp‘-𝐴)) / 2) ≠
0)) |
| 35 | 31, 34 | mpbird 257 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((exp‘𝐴) +
(exp‘-𝐴)) ≠
0) |
| 36 | 27, 29, 30, 35, 33 | divcan7d 12071 |
. . 3
⊢ (𝐴 ∈ ℝ →
((((exp‘𝐴) −
(exp‘-𝐴)) / 2) /
(((exp‘𝐴) +
(exp‘-𝐴)) / 2)) =
(((exp‘𝐴) −
(exp‘-𝐴)) /
((exp‘𝐴) +
(exp‘-𝐴)))) |
| 37 | 22, 36 | eqtrd 2777 |
. 2
⊢ (𝐴 ∈ ℝ →
((tan‘(i · 𝐴))
/ i) = (((exp‘𝐴)
− (exp‘-𝐴)) /
((exp‘𝐴) +
(exp‘-𝐴)))) |
| 38 | 24 | rpefcld 16141 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(exp‘-𝐴) ∈
ℝ+) |
| 39 | 23, 38 | ltsubrpd 13109 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((exp‘𝐴) −
(exp‘-𝐴)) <
(exp‘𝐴)) |
| 40 | 23, 38 | ltaddrpd 13110 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(exp‘𝐴) <
((exp‘𝐴) +
(exp‘-𝐴))) |
| 41 | 26, 23, 28, 39, 40 | lttrd 11422 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((exp‘𝐴) −
(exp‘-𝐴)) <
((exp‘𝐴) +
(exp‘-𝐴))) |
| 42 | 29 | mulridd 11278 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(((exp‘𝐴) +
(exp‘-𝐴)) · 1)
= ((exp‘𝐴) +
(exp‘-𝐴))) |
| 43 | 41, 42 | breqtrrd 5171 |
. . 3
⊢ (𝐴 ∈ ℝ →
((exp‘𝐴) −
(exp‘-𝐴)) <
(((exp‘𝐴) +
(exp‘-𝐴)) ·
1)) |
| 44 | | 1red 11262 |
. . . 4
⊢ (𝐴 ∈ ℝ → 1 ∈
ℝ) |
| 45 | | efgt0 16139 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 0 <
(exp‘𝐴)) |
| 46 | | efgt0 16139 |
. . . . . 6
⊢ (-𝐴 ∈ ℝ → 0 <
(exp‘-𝐴)) |
| 47 | 24, 46 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 0 <
(exp‘-𝐴)) |
| 48 | 23, 25, 45, 47 | addgt0d 11838 |
. . . 4
⊢ (𝐴 ∈ ℝ → 0 <
((exp‘𝐴) +
(exp‘-𝐴))) |
| 49 | | ltdivmul 12143 |
. . . 4
⊢
((((exp‘𝐴)
− (exp‘-𝐴))
∈ ℝ ∧ 1 ∈ ℝ ∧ (((exp‘𝐴) + (exp‘-𝐴)) ∈ ℝ ∧ 0 <
((exp‘𝐴) +
(exp‘-𝐴)))) →
((((exp‘𝐴) −
(exp‘-𝐴)) /
((exp‘𝐴) +
(exp‘-𝐴))) < 1
↔ ((exp‘𝐴)
− (exp‘-𝐴))
< (((exp‘𝐴) +
(exp‘-𝐴)) ·
1))) |
| 50 | 26, 44, 28, 48, 49 | syl112anc 1376 |
. . 3
⊢ (𝐴 ∈ ℝ →
((((exp‘𝐴) −
(exp‘-𝐴)) /
((exp‘𝐴) +
(exp‘-𝐴))) < 1
↔ ((exp‘𝐴)
− (exp‘-𝐴))
< (((exp‘𝐴) +
(exp‘-𝐴)) ·
1))) |
| 51 | 43, 50 | mpbird 257 |
. 2
⊢ (𝐴 ∈ ℝ →
(((exp‘𝐴) −
(exp‘-𝐴)) /
((exp‘𝐴) +
(exp‘-𝐴))) <
1) |
| 52 | 37, 51 | eqbrtrd 5165 |
1
⊢ (𝐴 ∈ ℝ →
((tan‘(i · 𝐴))
/ i) < 1) |