Proof of Theorem sin01gt0
Step | Hyp | Ref
| Expression |
1 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
2 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
3 | | elioc2 12107 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
4 | 1, 2, 3 | mp2an 704 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
5 | 4 | simp1bi 1069 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
6 | | 3nn0 11187 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
7 | | reexpcl 12739 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℝ) |
8 | 5, 6, 7 | sylancl 693 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℝ) |
9 | | 3re 10971 |
. . . . . 6
⊢ 3 ∈
ℝ |
10 | | 3ne0 10992 |
. . . . . 6
⊢ 3 ≠
0 |
11 | | redivcl 10623 |
. . . . . 6
⊢ (((𝐴↑3) ∈ ℝ ∧ 3
∈ ℝ ∧ 3 ≠ 0) → ((𝐴↑3) / 3) ∈
ℝ) |
12 | 9, 10, 11 | mp3an23 1408 |
. . . . 5
⊢ ((𝐴↑3) ∈ ℝ →
((𝐴↑3) / 3) ∈
ℝ) |
13 | 8, 12 | syl 17 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℝ) |
14 | | 3z 11287 |
. . . . . . . . 9
⊢ 3 ∈
ℤ |
15 | | expgt0 12755 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℤ ∧ 0 < 𝐴)
→ 0 < (𝐴↑3)) |
16 | 14, 15 | mp3an2 1404 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (𝐴↑3)) |
17 | 16 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1) → 0 < (𝐴↑3)) |
18 | 4, 17 | sylbi 206 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 0 <
(𝐴↑3)) |
19 | | 0lt1 10429 |
. . . . . . . . 9
⊢ 0 <
1 |
20 | 2, 19 | pm3.2i 470 |
. . . . . . . 8
⊢ (1 ∈
ℝ ∧ 0 < 1) |
21 | | 3pos 10991 |
. . . . . . . . 9
⊢ 0 <
3 |
22 | 9, 21 | pm3.2i 470 |
. . . . . . . 8
⊢ (3 ∈
ℝ ∧ 0 < 3) |
23 | | 1lt3 11073 |
. . . . . . . . 9
⊢ 1 <
3 |
24 | | ltdiv2 10788 |
. . . . . . . . 9
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (3 ∈ ℝ ∧ 0 < 3) ∧
((𝐴↑3) ∈ ℝ
∧ 0 < (𝐴↑3)))
→ (1 < 3 ↔ ((𝐴↑3) / 3) < ((𝐴↑3) / 1))) |
25 | 23, 24 | mpbii 222 |
. . . . . . . 8
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (3 ∈ ℝ ∧ 0 < 3) ∧
((𝐴↑3) ∈ ℝ
∧ 0 < (𝐴↑3)))
→ ((𝐴↑3) / 3)
< ((𝐴↑3) /
1)) |
26 | 20, 22, 25 | mp3an12 1406 |
. . . . . . 7
⊢ (((𝐴↑3) ∈ ℝ ∧ 0
< (𝐴↑3)) →
((𝐴↑3) / 3) <
((𝐴↑3) /
1)) |
27 | 26 | ex 449 |
. . . . . 6
⊢ ((𝐴↑3) ∈ ℝ →
(0 < (𝐴↑3) →
((𝐴↑3) / 3) <
((𝐴↑3) /
1))) |
28 | 8, 18, 27 | sylc 63 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) < ((𝐴↑3) / 1)) |
29 | 8 | recnd 9947 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℂ) |
30 | 29 | div1d 10672 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 1) = (𝐴↑3)) |
31 | 28, 30 | breqtrd 4609 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) < (𝐴↑3)) |
32 | | 1nn0 11185 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 1 ∈
ℕ0) |
34 | | 1le3 11121 |
. . . . . . . 8
⊢ 1 ≤
3 |
35 | | 1z 11284 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
36 | 35 | eluz1i 11571 |
. . . . . . . 8
⊢ (3 ∈
(ℤ≥‘1) ↔ (3 ∈ ℤ ∧ 1 ≤
3)) |
37 | 14, 34, 36 | mpbir2an 957 |
. . . . . . 7
⊢ 3 ∈
(ℤ≥‘1) |
38 | 37 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 3 ∈
(ℤ≥‘1)) |
39 | 4 | simp2bi 1070 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
40 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
41 | | ltle 10005 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
42 | 40, 5, 41 | sylancr 694 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) |
43 | 39, 42 | mpd 15 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) |
44 | 4 | simp3bi 1071 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
45 | 5, 33, 38, 43, 44 | leexp2rd 12904 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ≤ (𝐴↑1)) |
46 | 5 | recnd 9947 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
47 | 46 | exp1d 12865 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑1) = 𝐴) |
48 | 45, 47 | breqtrd 4609 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ≤ 𝐴) |
49 | 13, 8, 5, 31, 48 | ltletrd 10076 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) < 𝐴) |
50 | 13, 5 | posdifd 10493 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 3) < 𝐴 ↔ 0 < (𝐴 − ((𝐴↑3) / 3)))) |
51 | 49, 50 | mpbid 221 |
. 2
⊢ (𝐴 ∈ (0(,]1) → 0 <
(𝐴 − ((𝐴↑3) / 3))) |
52 | | sin01bnd 14754 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) |
53 | 52 | simpld 474 |
. 2
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴)) |
54 | 5, 13 | resubcld 10337 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 3)) ∈
ℝ) |
55 | 5 | resincld 14712 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℝ) |
56 | | lttr 9993 |
. . . 4
⊢ ((0
∈ ℝ ∧ (𝐴
− ((𝐴↑3) / 3))
∈ ℝ ∧ (sin‘𝐴) ∈ ℝ) → ((0 < (𝐴 − ((𝐴↑3) / 3)) ∧ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴)) → 0 <
(sin‘𝐴))) |
57 | 40, 56 | mp3an1 1403 |
. . 3
⊢ (((𝐴 − ((𝐴↑3) / 3)) ∈ ℝ ∧
(sin‘𝐴) ∈
ℝ) → ((0 < (𝐴
− ((𝐴↑3) / 3))
∧ (𝐴 − ((𝐴↑3) / 3)) <
(sin‘𝐴)) → 0
< (sin‘𝐴))) |
58 | 54, 55, 57 | syl2anc 691 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((0 <
(𝐴 − ((𝐴↑3) / 3)) ∧ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴)) → 0 <
(sin‘𝐴))) |
59 | 51, 53, 58 | mp2and 711 |
1
⊢ (𝐴 ∈ (0(,]1) → 0 <
(sin‘𝐴)) |