Proof of Theorem sin01gt0
Step | Hyp | Ref
| Expression |
1 | | 0xr 10880 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
2 | | 1re 10833 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
3 | | elioc2 12998 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))) |
4 | 1, 2, 3 | mp2an 692 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1)) |
5 | 4 | simp1bi 1147 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℝ) |
6 | | 3nn0 12108 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
7 | | reexpcl 13652 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝐴↑3) ∈ ℝ) |
8 | 5, 6, 7 | sylancl 589 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℝ) |
9 | | 3re 11910 |
. . . . . 6
⊢ 3 ∈
ℝ |
10 | | 3ne0 11936 |
. . . . . 6
⊢ 3 ≠
0 |
11 | | redivcl 11551 |
. . . . . 6
⊢ (((𝐴↑3) ∈ ℝ ∧ 3
∈ ℝ ∧ 3 ≠ 0) → ((𝐴↑3) / 3) ∈
ℝ) |
12 | 9, 10, 11 | mp3an23 1455 |
. . . . 5
⊢ ((𝐴↑3) ∈ ℝ →
((𝐴↑3) / 3) ∈
ℝ) |
13 | 8, 12 | syl 17 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) ∈
ℝ) |
14 | | 3z 12210 |
. . . . . . . . 9
⊢ 3 ∈
ℤ |
15 | | expgt0 13668 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 3 ∈
ℤ ∧ 0 < 𝐴)
→ 0 < (𝐴↑3)) |
16 | 14, 15 | mp3an2 1451 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (𝐴↑3)) |
17 | 16 | 3adant3 1134 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 1) → 0 < (𝐴↑3)) |
18 | 4, 17 | sylbi 220 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 0 <
(𝐴↑3)) |
19 | | 0lt1 11354 |
. . . . . . . 8
⊢ 0 <
1 |
20 | 2, 19 | pm3.2i 474 |
. . . . . . 7
⊢ (1 ∈
ℝ ∧ 0 < 1) |
21 | | 3pos 11935 |
. . . . . . . 8
⊢ 0 <
3 |
22 | 9, 21 | pm3.2i 474 |
. . . . . . 7
⊢ (3 ∈
ℝ ∧ 0 < 3) |
23 | | 1lt3 12003 |
. . . . . . . 8
⊢ 1 <
3 |
24 | | ltdiv2 11718 |
. . . . . . . 8
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (3 ∈ ℝ ∧ 0 < 3) ∧
((𝐴↑3) ∈ ℝ
∧ 0 < (𝐴↑3)))
→ (1 < 3 ↔ ((𝐴↑3) / 3) < ((𝐴↑3) / 1))) |
25 | 23, 24 | mpbii 236 |
. . . . . . 7
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (3 ∈ ℝ ∧ 0 < 3) ∧
((𝐴↑3) ∈ ℝ
∧ 0 < (𝐴↑3)))
→ ((𝐴↑3) / 3)
< ((𝐴↑3) /
1)) |
26 | 20, 22, 25 | mp3an12 1453 |
. . . . . 6
⊢ (((𝐴↑3) ∈ ℝ ∧ 0
< (𝐴↑3)) →
((𝐴↑3) / 3) <
((𝐴↑3) /
1)) |
27 | 8, 18, 26 | syl2anc 587 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) < ((𝐴↑3) / 1)) |
28 | 8 | recnd 10861 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ∈
ℂ) |
29 | 28 | div1d 11600 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 1) = (𝐴↑3)) |
30 | 27, 29 | breqtrd 5079 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) < (𝐴↑3)) |
31 | | 1nn0 12106 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
32 | 31 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 1 ∈
ℕ0) |
33 | | 1le3 12042 |
. . . . . . . 8
⊢ 1 ≤
3 |
34 | | 1z 12207 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
35 | 34 | eluz1i 12446 |
. . . . . . . 8
⊢ (3 ∈
(ℤ≥‘1) ↔ (3 ∈ ℤ ∧ 1 ≤
3)) |
36 | 14, 33, 35 | mpbir2an 711 |
. . . . . . 7
⊢ 3 ∈
(ℤ≥‘1) |
37 | 36 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 3 ∈
(ℤ≥‘1)) |
38 | 4 | simp2bi 1148 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → 0 <
𝐴) |
39 | | 0re 10835 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
40 | | ltle 10921 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
41 | 39, 5, 40 | sylancr 590 |
. . . . . . 7
⊢ (𝐴 ∈ (0(,]1) → (0 <
𝐴 → 0 ≤ 𝐴)) |
42 | 38, 41 | mpd 15 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 0 ≤
𝐴) |
43 | 4 | simp3bi 1149 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ≤ 1) |
44 | 5, 32, 37, 42, 43 | leexp2rd 13824 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ≤ (𝐴↑1)) |
45 | 5 | recnd 10861 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈
ℂ) |
46 | 45 | exp1d 13711 |
. . . . 5
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑1) = 𝐴) |
47 | 44, 46 | breqtrd 5079 |
. . . 4
⊢ (𝐴 ∈ (0(,]1) → (𝐴↑3) ≤ 𝐴) |
48 | 13, 8, 5, 30, 47 | ltletrd 10992 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑3) / 3) < 𝐴) |
49 | 13, 5 | posdifd 11419 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → (((𝐴↑3) / 3) < 𝐴 ↔ 0 < (𝐴 − ((𝐴↑3) / 3)))) |
50 | 48, 49 | mpbid 235 |
. 2
⊢ (𝐴 ∈ (0(,]1) → 0 <
(𝐴 − ((𝐴↑3) / 3))) |
51 | | sin01bnd 15746 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) |
52 | 51 | simpld 498 |
. 2
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴)) |
53 | 5, 13 | resubcld 11260 |
. . 3
⊢ (𝐴 ∈ (0(,]1) → (𝐴 − ((𝐴↑3) / 3)) ∈
ℝ) |
54 | 5 | resincld 15704 |
. . 3
⊢ (𝐴 ∈ (0(,]1) →
(sin‘𝐴) ∈
ℝ) |
55 | | lttr 10909 |
. . 3
⊢ ((0
∈ ℝ ∧ (𝐴
− ((𝐴↑3) / 3))
∈ ℝ ∧ (sin‘𝐴) ∈ ℝ) → ((0 < (𝐴 − ((𝐴↑3) / 3)) ∧ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴)) → 0 <
(sin‘𝐴))) |
56 | 39, 53, 54, 55 | mp3an2i 1468 |
. 2
⊢ (𝐴 ∈ (0(,]1) → ((0 <
(𝐴 − ((𝐴↑3) / 3)) ∧ (𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴)) → 0 <
(sin‘𝐴))) |
57 | 50, 52, 56 | mp2and 699 |
1
⊢ (𝐴 ∈ (0(,]1) → 0 <
(sin‘𝐴)) |