Proof of Theorem sinhalfpilem
| Step | Hyp | Ref
| Expression |
| 1 | | 0lt1 11785 |
. . . . . 6
⊢ 0 <
1 |
| 2 | | 0re 11263 |
. . . . . . 7
⊢ 0 ∈
ℝ |
| 3 | | 1re 11261 |
. . . . . . 7
⊢ 1 ∈
ℝ |
| 4 | 2, 3 | ltnsymi 11380 |
. . . . . 6
⊢ (0 < 1
→ ¬ 1 < 0) |
| 5 | 1, 4 | ax-mp 5 |
. . . . 5
⊢ ¬ 1
< 0 |
| 6 | | lt0neg1 11769 |
. . . . . 6
⊢ (1 ∈
ℝ → (1 < 0 ↔ 0 < -1)) |
| 7 | 3, 6 | ax-mp 5 |
. . . . 5
⊢ (1 < 0
↔ 0 < -1) |
| 8 | 5, 7 | mtbi 322 |
. . . 4
⊢ ¬ 0
< -1 |
| 9 | | pire 26500 |
. . . . . . . 8
⊢ π
∈ ℝ |
| 10 | 9 | rehalfcli 12515 |
. . . . . . 7
⊢ (π /
2) ∈ ℝ |
| 11 | | 2re 12340 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
| 12 | | pipos 26502 |
. . . . . . . 8
⊢ 0 <
π |
| 13 | | 2pos 12369 |
. . . . . . . 8
⊢ 0 <
2 |
| 14 | 9, 11, 12, 13 | divgt0ii 12185 |
. . . . . . 7
⊢ 0 <
(π / 2) |
| 15 | | 4re 12350 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
| 16 | | pigt2lt4 26498 |
. . . . . . . . . 10
⊢ (2 <
π ∧ π < 4) |
| 17 | 16 | simpri 485 |
. . . . . . . . 9
⊢ π <
4 |
| 18 | 9, 15, 17 | ltleii 11384 |
. . . . . . . 8
⊢ π ≤
4 |
| 19 | 11, 13 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 20 | | ledivmul 12144 |
. . . . . . . . . 10
⊢ ((π
∈ ℝ ∧ 2 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2))
→ ((π / 2) ≤ 2 ↔ π ≤ (2 · 2))) |
| 21 | 9, 11, 19, 20 | mp3an 1463 |
. . . . . . . . 9
⊢ ((π /
2) ≤ 2 ↔ π ≤ (2 · 2)) |
| 22 | | 2t2e4 12430 |
. . . . . . . . . 10
⊢ (2
· 2) = 4 |
| 23 | 22 | breq2i 5151 |
. . . . . . . . 9
⊢ (π
≤ (2 · 2) ↔ π ≤ 4) |
| 24 | 21, 23 | bitr2i 276 |
. . . . . . . 8
⊢ (π
≤ 4 ↔ (π / 2) ≤ 2) |
| 25 | 18, 24 | mpbi 230 |
. . . . . . 7
⊢ (π /
2) ≤ 2 |
| 26 | | 0xr 11308 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 27 | | elioc2 13450 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 2 ∈ ℝ) → ((π / 2) ∈
(0(,]2) ↔ ((π / 2) ∈ ℝ ∧ 0 < (π / 2) ∧ (π /
2) ≤ 2))) |
| 28 | 26, 11, 27 | mp2an 692 |
. . . . . . 7
⊢ ((π /
2) ∈ (0(,]2) ↔ ((π / 2) ∈ ℝ ∧ 0 < (π / 2)
∧ (π / 2) ≤ 2)) |
| 29 | 10, 14, 25, 28 | mpbir3an 1342 |
. . . . . 6
⊢ (π /
2) ∈ (0(,]2) |
| 30 | | sin02gt0 16228 |
. . . . . 6
⊢ ((π /
2) ∈ (0(,]2) → 0 < (sin‘(π / 2))) |
| 31 | 29, 30 | ax-mp 5 |
. . . . 5
⊢ 0 <
(sin‘(π / 2)) |
| 32 | | breq2 5147 |
. . . . 5
⊢
((sin‘(π / 2)) = -1 → (0 < (sin‘(π / 2))
↔ 0 < -1)) |
| 33 | 31, 32 | mpbii 233 |
. . . 4
⊢
((sin‘(π / 2)) = -1 → 0 < -1) |
| 34 | 8, 33 | mto 197 |
. . 3
⊢ ¬
(sin‘(π / 2)) = -1 |
| 35 | | sq1 14234 |
. . . . . 6
⊢
(1↑2) = 1 |
| 36 | | resincl 16176 |
. . . . . . . . . . . . . 14
⊢ ((π /
2) ∈ ℝ → (sin‘(π / 2)) ∈
ℝ) |
| 37 | 10, 36 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(sin‘(π / 2)) ∈ ℝ |
| 38 | 37, 31 | gt0ne0ii 11799 |
. . . . . . . . . . . 12
⊢
(sin‘(π / 2)) ≠ 0 |
| 39 | 38 | neii 2942 |
. . . . . . . . . . 11
⊢ ¬
(sin‘(π / 2)) = 0 |
| 40 | | 2ne0 12370 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
| 41 | 40 | neii 2942 |
. . . . . . . . . . . . 13
⊢ ¬ 2
= 0 |
| 42 | 9 | recni 11275 |
. . . . . . . . . . . . . . . . . 18
⊢ π
∈ ℂ |
| 43 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℂ |
| 44 | 42, 43, 40 | divcan2i 12010 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· (π / 2)) = π |
| 45 | 44 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢
(sin‘(2 · (π / 2))) = (sin‘π) |
| 46 | 10 | recni 11275 |
. . . . . . . . . . . . . . . . 17
⊢ (π /
2) ∈ ℂ |
| 47 | | sin2t 16213 |
. . . . . . . . . . . . . . . . 17
⊢ ((π /
2) ∈ ℂ → (sin‘(2 · (π / 2))) = (2 ·
((sin‘(π / 2)) · (cos‘(π / 2))))) |
| 48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(sin‘(2 · (π / 2))) = (2 · ((sin‘(π /
2)) · (cos‘(π / 2)))) |
| 49 | 45, 48 | eqtr3i 2767 |
. . . . . . . . . . . . . . 15
⊢
(sin‘π) = (2 · ((sin‘(π / 2)) ·
(cos‘(π / 2)))) |
| 50 | | sinpi 26499 |
. . . . . . . . . . . . . . 15
⊢
(sin‘π) = 0 |
| 51 | 49, 50 | eqtr3i 2767 |
. . . . . . . . . . . . . 14
⊢ (2
· ((sin‘(π / 2)) · (cos‘(π / 2)))) =
0 |
| 52 | | sincl 16162 |
. . . . . . . . . . . . . . . . 17
⊢ ((π /
2) ∈ ℂ → (sin‘(π / 2)) ∈
ℂ) |
| 53 | 46, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(sin‘(π / 2)) ∈ ℂ |
| 54 | | coscl 16163 |
. . . . . . . . . . . . . . . . 17
⊢ ((π /
2) ∈ ℂ → (cos‘(π / 2)) ∈
ℂ) |
| 55 | 46, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(cos‘(π / 2)) ∈ ℂ |
| 56 | 53, 55 | mulcli 11268 |
. . . . . . . . . . . . . . 15
⊢
((sin‘(π / 2)) · (cos‘(π / 2))) ∈
ℂ |
| 57 | 43, 56 | mul0ori 11911 |
. . . . . . . . . . . . . 14
⊢ ((2
· ((sin‘(π / 2)) · (cos‘(π / 2)))) = 0 ↔
(2 = 0 ∨ ((sin‘(π / 2)) · (cos‘(π / 2))) =
0)) |
| 58 | 51, 57 | mpbi 230 |
. . . . . . . . . . . . 13
⊢ (2 = 0
∨ ((sin‘(π / 2)) · (cos‘(π / 2))) =
0) |
| 59 | 41, 58 | mtpor 1770 |
. . . . . . . . . . . 12
⊢
((sin‘(π / 2)) · (cos‘(π / 2))) =
0 |
| 60 | 53, 55 | mul0ori 11911 |
. . . . . . . . . . . 12
⊢
(((sin‘(π / 2)) · (cos‘(π / 2))) = 0 ↔
((sin‘(π / 2)) = 0 ∨ (cos‘(π / 2)) = 0)) |
| 61 | 59, 60 | mpbi 230 |
. . . . . . . . . . 11
⊢
((sin‘(π / 2)) = 0 ∨ (cos‘(π / 2)) =
0) |
| 62 | 39, 61 | mtpor 1770 |
. . . . . . . . . 10
⊢
(cos‘(π / 2)) = 0 |
| 63 | 62 | oveq1i 7441 |
. . . . . . . . 9
⊢
((cos‘(π / 2))↑2) = (0↑2) |
| 64 | | sq0 14231 |
. . . . . . . . 9
⊢
(0↑2) = 0 |
| 65 | 63, 64 | eqtri 2765 |
. . . . . . . 8
⊢
((cos‘(π / 2))↑2) = 0 |
| 66 | 65 | oveq2i 7442 |
. . . . . . 7
⊢
(((sin‘(π / 2))↑2) + ((cos‘(π / 2))↑2)) =
(((sin‘(π / 2))↑2) + 0) |
| 67 | | sincossq 16212 |
. . . . . . . 8
⊢ ((π /
2) ∈ ℂ → (((sin‘(π / 2))↑2) + ((cos‘(π /
2))↑2)) = 1) |
| 68 | 46, 67 | ax-mp 5 |
. . . . . . 7
⊢
(((sin‘(π / 2))↑2) + ((cos‘(π / 2))↑2)) =
1 |
| 69 | 66, 68 | eqtr3i 2767 |
. . . . . 6
⊢
(((sin‘(π / 2))↑2) + 0) = 1 |
| 70 | 53 | sqcli 14220 |
. . . . . . 7
⊢
((sin‘(π / 2))↑2) ∈ ℂ |
| 71 | 70 | addridi 11448 |
. . . . . 6
⊢
(((sin‘(π / 2))↑2) + 0) = ((sin‘(π /
2))↑2) |
| 72 | 35, 69, 71 | 3eqtr2ri 2772 |
. . . . 5
⊢
((sin‘(π / 2))↑2) = (1↑2) |
| 73 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 74 | 53, 73 | sqeqori 14253 |
. . . . 5
⊢
(((sin‘(π / 2))↑2) = (1↑2) ↔ ((sin‘(π /
2)) = 1 ∨ (sin‘(π / 2)) = -1)) |
| 75 | 72, 74 | mpbi 230 |
. . . 4
⊢
((sin‘(π / 2)) = 1 ∨ (sin‘(π / 2)) =
-1) |
| 76 | 75 | ori 862 |
. . 3
⊢ (¬
(sin‘(π / 2)) = 1 → (sin‘(π / 2)) = -1) |
| 77 | 34, 76 | mt3 201 |
. 2
⊢
(sin‘(π / 2)) = 1 |
| 78 | 77, 62 | pm3.2i 470 |
1
⊢
((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) =
0) |