Proof of Theorem sin01gt0
Step | Hyp | Ref
| Expression |
1 | | 0xr 7937 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
2 | | 1re 7890 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
3 | | elioc2 9864 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
4 | 1, 2, 3 | mp2an 423 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
5 | 4 | simp1bi 1001 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
6 | | 3nn0 9124 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
7 | | reexpcl 10463 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℝ) |
8 | 5, 6, 7 | sylancl 410 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℝ) |
9 | | 3re 8923 |
. . . . . 6
⊢ 3 ∈
ℝ |
10 | | 3ap0 8945 |
. . . . . 6
⊢ 3 #
0 |
11 | | redivclap 8619 |
. . . . . 6
⊢ (((𝐴↑3) ∈ ℝ ∧ 3
∈ ℝ ∧ 3 # 0) → ((𝐴↑3) / 3) ∈
ℝ) |
12 | 9, 10, 11 | mp3an23 1318 |
. . . . 5
⊢ ((𝐴↑3) ∈ ℝ →
((𝐴↑3) / 3) ∈
ℝ) |
13 | 8, 12 | syl 14 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℝ) |
14 | | 3z 9212 |
. . . . . . . . 9
⊢ 3 ∈
ℤ |
15 | | expgt0 10479 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℤ ∧ 0 < 𝐴)
→ 0 < (𝐴↑3)) |
16 | 14, 15 | mp3an2 1314 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (𝐴↑3)) |
17 | 16 | 3adant3 1006 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1) → 0 < (𝐴↑3)) |
18 | 4, 17 | sylbi 120 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 0 <
(𝐴↑3)) |
19 | | 0lt1 8017 |
. . . . . . . 8
⊢ 0 <
1 |
20 | 2, 19 | pm3.2i 270 |
. . . . . . 7
⊢ (1 ∈
ℝ ∧ 0 < 1) |
21 | | 3pos 8943 |
. . . . . . . 8
⊢ 0 <
3 |
22 | 9, 21 | pm3.2i 270 |
. . . . . . 7
⊢ (3 ∈
ℝ ∧ 0 < 3) |
23 | | 1lt3 9020 |
. . . . . . . 8
⊢ 1 <
3 |
24 | | ltdiv2 8774 |
. . . . . . . 8
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (3 ∈ ℝ ∧ 0 < 3) ∧
((𝐴↑3) ∈ ℝ
∧ 0 < (𝐴↑3)))
→ (1 < 3 ↔ ((𝐴↑3) / 3) < ((𝐴↑3) / 1))) |
25 | 23, 24 | mpbii 147 |
. . . . . . 7
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (3 ∈ ℝ ∧ 0 < 3) ∧
((𝐴↑3) ∈ ℝ
∧ 0 < (𝐴↑3)))
→ ((𝐴↑3) / 3)
< ((𝐴↑3) /
1)) |
26 | 20, 22, 25 | mp3an12 1316 |
. . . . . 6
⊢ (((𝐴↑3) ∈ ℝ ∧ 0
< (𝐴↑3)) →
((𝐴↑3) / 3) <
((𝐴↑3) /
1)) |
27 | 8, 18, 26 | syl2anc 409 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) < ((𝐴↑3) / 1)) |
28 | 8 | recnd 7919 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℂ) |
29 | 28 | div1d 8668 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 1) = (𝐴↑3)) |
30 | 27, 29 | breqtrd 4003 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) < (𝐴↑3)) |
31 | | 1nn0 9122 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
32 | 31 | a1i 9 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 1 ∈
ℕ0) |
33 | | 1le3 9060 |
. . . . . . . 8
⊢ 1 ≤
3 |
34 | | 1z 9209 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
35 | 34 | eluz1i 9465 |
. . . . . . . 8
⊢ (3 ∈
(ℤ≥‘1) ↔ (3 ∈ ℤ ∧ 1 ≤
3)) |
36 | 14, 33, 35 | mpbir2an 931 |
. . . . . . 7
⊢ 3 ∈
(ℤ≥‘1) |
37 | 36 | a1i 9 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 3 ∈
(ℤ≥‘1)) |
38 | 4 | simp2bi 1002 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
39 | | 0re 7891 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
40 | | ltle 7978 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
41 | 39, 5, 40 | sylancr 411 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) |
42 | 38, 41 | mpd 13 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) |
43 | 4 | simp3bi 1003 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
44 | 5, 32, 37, 42, 43 | leexp2rd 10608 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ≤ (𝐴↑1)) |
45 | 5 | recnd 7919 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
46 | 45 | exp1d 10573 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑1) = 𝐴) |
47 | 44, 46 | breqtrd 4003 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ≤ 𝐴) |
48 | 13, 8, 5, 30, 47 | ltletrd 8313 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) < 𝐴) |
49 | 13, 5 | posdifd 8422 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 3) < 𝐴 ↔ 0 < (𝐴 − ((𝐴↑3) / 3)))) |
50 | 48, 49 | mpbid 146 |
. 2
⊢ (𝐴 ∈ (0(,]1) → 0 <
(𝐴 − ((𝐴↑3) / 3))) |
51 | | sin01bnd 11688 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) |
52 | 51 | simpld 111 |
. 2
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴)) |
53 | 5, 13 | resubcld 8271 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 3)) ∈
ℝ) |
54 | 5 | resincld 11654 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℝ) |
55 | | lttr 7964 |
. . 3
⊢ ((0
∈ ℝ ∧ (𝐴
− ((𝐴↑3) / 3))
∈ ℝ ∧ (sin‘𝐴) ∈ ℝ) → ((0 < (𝐴 − ((𝐴↑3) / 3)) ∧ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴)) → 0 <
(sin‘𝐴))) |
56 | 39, 53, 54, 55 | mp3an2i 1331 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((0 <
(𝐴 − ((𝐴↑3) / 3)) ∧ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴)) → 0 <
(sin‘𝐴))) |
57 | 50, 52, 56 | mp2and 430 |
1
⊢ (𝐴 ∈ (0(,]1) → 0 <
(sin‘𝐴)) |