Proof of Theorem sin02gt0
| Step | Hyp | Ref
| Expression |
| 1 | | 0xr 11308 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
| 2 | | 2re 12340 |
. . . . . . 7
⊢ 2 ∈
ℝ |
| 3 | | elioc2 13450 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ 2 ∈ ℝ) → (𝐴 ∈ (0(,]2) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 2))) |
| 4 | 1, 2, 3 | mp2an 692 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]2) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 2)) |
| 5 | | rehalfcl 12492 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ) |
| 6 | 5 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 2) → (𝐴 / 2) ∈ ℝ) |
| 7 | 4, 6 | sylbi 217 |
. . . . 5
⊢ (𝐴 ∈ (0(,]2) → (𝐴 / 2) ∈
ℝ) |
| 8 | | resincl 16176 |
. . . . . 6
⊢ ((𝐴 / 2) ∈ ℝ →
(sin‘(𝐴 / 2)) ∈
ℝ) |
| 9 | | recoscl 16177 |
. . . . . 6
⊢ ((𝐴 / 2) ∈ ℝ →
(cos‘(𝐴 / 2)) ∈
ℝ) |
| 10 | 8, 9 | remulcld 11291 |
. . . . 5
⊢ ((𝐴 / 2) ∈ ℝ →
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))) ∈ ℝ) |
| 11 | 7, 10 | syl 17 |
. . . 4
⊢ (𝐴 ∈ (0(,]2) →
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))) ∈ ℝ) |
| 12 | | 2pos 12369 |
. . . . . . . . . 10
⊢ 0 <
2 |
| 13 | | divgt0 12136 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (2 ∈ ℝ
∧ 0 < 2)) → 0 < (𝐴 / 2)) |
| 14 | 2, 12, 13 | mpanr12 705 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (𝐴 / 2)) |
| 15 | 14 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 2) → 0 < (𝐴 / 2)) |
| 16 | 2, 12 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 17 | | lediv1 12133 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 2 ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐴 ≤ 2 ↔ (𝐴 / 2) ≤ (2 / 2))) |
| 18 | 2, 16, 17 | mp3an23 1455 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 2 ↔ (𝐴 / 2) ≤ (2 /
2))) |
| 19 | 18 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 2) → (𝐴 / 2) ≤ (2 /
2)) |
| 20 | | 2div2e1 12407 |
. . . . . . . . . 10
⊢ (2 / 2) =
1 |
| 21 | 19, 20 | breqtrdi 5184 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 2) → (𝐴 / 2) ≤ 1) |
| 22 | 21 | 3adant2 1132 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 2) → (𝐴 / 2) ≤ 1) |
| 23 | 6, 15, 22 | 3jca 1129 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 ≤ 2) → ((𝐴 / 2) ∈ ℝ ∧ 0 < (𝐴 / 2) ∧ (𝐴 / 2) ≤ 1)) |
| 24 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 25 | | elioc2 13450 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → ((𝐴 / 2) ∈ (0(,]1) ↔ ((𝐴 / 2) ∈ ℝ ∧ 0
< (𝐴 / 2) ∧ (𝐴 / 2) ≤ 1))) |
| 26 | 1, 24, 25 | mp2an 692 |
. . . . . . 7
⊢ ((𝐴 / 2) ∈ (0(,]1) ↔
((𝐴 / 2) ∈ ℝ
∧ 0 < (𝐴 / 2) ∧
(𝐴 / 2) ≤
1)) |
| 27 | 23, 4, 26 | 3imtr4i 292 |
. . . . . 6
⊢ (𝐴 ∈ (0(,]2) → (𝐴 / 2) ∈
(0(,]1)) |
| 28 | | sin01gt0 16226 |
. . . . . 6
⊢ ((𝐴 / 2) ∈ (0(,]1) → 0
< (sin‘(𝐴 /
2))) |
| 29 | 27, 28 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ (0(,]2) → 0 <
(sin‘(𝐴 /
2))) |
| 30 | | cos01gt0 16227 |
. . . . . 6
⊢ ((𝐴 / 2) ∈ (0(,]1) → 0
< (cos‘(𝐴 /
2))) |
| 31 | 27, 30 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ (0(,]2) → 0 <
(cos‘(𝐴 /
2))) |
| 32 | | axmulgt0 11335 |
. . . . . . 7
⊢
(((sin‘(𝐴 /
2)) ∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ) → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
| 33 | 8, 9, 32 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 / 2) ∈ ℝ → ((0
< (sin‘(𝐴 / 2))
∧ 0 < (cos‘(𝐴
/ 2))) → 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
| 34 | 7, 33 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ (0(,]2) → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
| 35 | 29, 31, 34 | mp2and 699 |
. . . 4
⊢ (𝐴 ∈ (0(,]2) → 0 <
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2)))) |
| 36 | | axmulgt0 11335 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) ∈ ℝ) →
((0 < 2 ∧ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) → 0 < (2
· ((sin‘(𝐴 /
2)) · (cos‘(𝐴
/ 2)))))) |
| 37 | 2, 36 | mpan 690 |
. . . . 5
⊢
(((sin‘(𝐴 /
2)) · (cos‘(𝐴
/ 2))) ∈ ℝ → ((0 < 2 ∧ 0 < ((sin‘(𝐴 / 2)) ·
(cos‘(𝐴 / 2))))
→ 0 < (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))) |
| 38 | 12, 37 | mpani 696 |
. . . 4
⊢
(((sin‘(𝐴 /
2)) · (cos‘(𝐴
/ 2))) ∈ ℝ → (0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) → 0 < (2
· ((sin‘(𝐴 /
2)) · (cos‘(𝐴
/ 2)))))) |
| 39 | 11, 35, 38 | sylc 65 |
. . 3
⊢ (𝐴 ∈ (0(,]2) → 0 < (2
· ((sin‘(𝐴 /
2)) · (cos‘(𝐴
/ 2))))) |
| 40 | 7 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ (0(,]2) → (𝐴 / 2) ∈
ℂ) |
| 41 | | sin2t 16213 |
. . . 4
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
| 42 | 40, 41 | syl 17 |
. . 3
⊢ (𝐴 ∈ (0(,]2) →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
| 43 | 39, 42 | breqtrrd 5171 |
. 2
⊢ (𝐴 ∈ (0(,]2) → 0 <
(sin‘(2 · (𝐴 /
2)))) |
| 44 | 4 | simp1bi 1146 |
. . . . 5
⊢ (𝐴 ∈ (0(,]2) → 𝐴 ∈
ℝ) |
| 45 | 44 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ (0(,]2) → 𝐴 ∈
ℂ) |
| 46 | | 2cn 12341 |
. . . . 5
⊢ 2 ∈
ℂ |
| 47 | | 2ne0 12370 |
. . . . 5
⊢ 2 ≠
0 |
| 48 | | divcan2 11930 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝐴 / 2)) = 𝐴) |
| 49 | 46, 47, 48 | mp3an23 1455 |
. . . 4
⊢ (𝐴 ∈ ℂ → (2
· (𝐴 / 2)) = 𝐴) |
| 50 | 45, 49 | syl 17 |
. . 3
⊢ (𝐴 ∈ (0(,]2) → (2
· (𝐴 / 2)) = 𝐴) |
| 51 | 50 | fveq2d 6910 |
. 2
⊢ (𝐴 ∈ (0(,]2) →
(sin‘(2 · (𝐴 /
2))) = (sin‘𝐴)) |
| 52 | 43, 51 | breqtrd 5169 |
1
⊢ (𝐴 ∈ (0(,]2) → 0 <
(sin‘𝐴)) |