Proof of Theorem sincos4thpi
| Step | Hyp | Ref
| Expression |
| 1 | | halfcn 12481 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℂ |
| 2 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 3 | | 2halves 12494 |
. . . . . . . . . . 11
⊢ (1 ∈
ℂ → ((1 / 2) + (1 / 2)) = 1) |
| 4 | 2, 3 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((1 / 2)
+ (1 / 2)) = 1 |
| 5 | | sincosq1eq 26554 |
. . . . . . . . . 10
⊢ (((1 / 2)
∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ ((1 / 2) + (1 / 2)) = 1)
→ (sin‘((1 / 2) · (π / 2))) = (cos‘((1 / 2) ·
(π / 2)))) |
| 6 | 1, 1, 4, 5 | mp3an 1463 |
. . . . . . . . 9
⊢
(sin‘((1 / 2) · (π / 2))) = (cos‘((1 / 2) ·
(π / 2))) |
| 7 | 6 | oveq2i 7442 |
. . . . . . . 8
⊢
((sin‘((1 / 2) · (π / 2))) · (sin‘((1 / 2)
· (π / 2)))) = ((sin‘((1 / 2) · (π / 2))) ·
(cos‘((1 / 2) · (π / 2)))) |
| 8 | 7 | oveq2i 7442 |
. . . . . . 7
⊢ (2
· ((sin‘((1 / 2) · (π / 2))) · (sin‘((1 /
2) · (π / 2))))) = (2 · ((sin‘((1 / 2) · (π /
2))) · (cos‘((1 / 2) · (π / 2))))) |
| 9 | | 2cn 12341 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
| 10 | | pire 26500 |
. . . . . . . . . . . . 13
⊢ π
∈ ℝ |
| 11 | 10 | recni 11275 |
. . . . . . . . . . . 12
⊢ π
∈ ℂ |
| 12 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 13 | 2, 9, 11, 9, 12, 12 | divmuldivi 12027 |
. . . . . . . . . . 11
⊢ ((1 / 2)
· (π / 2)) = ((1 · π) / (2 · 2)) |
| 14 | 11 | mullidi 11266 |
. . . . . . . . . . . 12
⊢ (1
· π) = π |
| 15 | | 2t2e4 12430 |
. . . . . . . . . . . 12
⊢ (2
· 2) = 4 |
| 16 | 14, 15 | oveq12i 7443 |
. . . . . . . . . . 11
⊢ ((1
· π) / (2 · 2)) = (π / 4) |
| 17 | 13, 16 | eqtri 2765 |
. . . . . . . . . 10
⊢ ((1 / 2)
· (π / 2)) = (π / 4) |
| 18 | 17 | fveq2i 6909 |
. . . . . . . . 9
⊢
(sin‘((1 / 2) · (π / 2))) = (sin‘(π /
4)) |
| 19 | 18, 18 | oveq12i 7443 |
. . . . . . . 8
⊢
((sin‘((1 / 2) · (π / 2))) · (sin‘((1 / 2)
· (π / 2)))) = ((sin‘(π / 4)) · (sin‘(π /
4))) |
| 20 | 19 | oveq2i 7442 |
. . . . . . 7
⊢ (2
· ((sin‘((1 / 2) · (π / 2))) · (sin‘((1 /
2) · (π / 2))))) = (2 · ((sin‘(π / 4)) ·
(sin‘(π / 4)))) |
| 21 | 9, 12 | recidi 11998 |
. . . . . . . . . . 11
⊢ (2
· (1 / 2)) = 1 |
| 22 | 21 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((2
· (1 / 2)) · (π / 2)) = (1 · (π /
2)) |
| 23 | | 2re 12340 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
| 24 | 10, 23, 12 | redivcli 12034 |
. . . . . . . . . . . 12
⊢ (π /
2) ∈ ℝ |
| 25 | 24 | recni 11275 |
. . . . . . . . . . 11
⊢ (π /
2) ∈ ℂ |
| 26 | 9, 1, 25 | mulassi 11272 |
. . . . . . . . . 10
⊢ ((2
· (1 / 2)) · (π / 2)) = (2 · ((1 / 2) · (π /
2))) |
| 27 | 25 | mullidi 11266 |
. . . . . . . . . 10
⊢ (1
· (π / 2)) = (π / 2) |
| 28 | 22, 26, 27 | 3eqtr3i 2773 |
. . . . . . . . 9
⊢ (2
· ((1 / 2) · (π / 2))) = (π / 2) |
| 29 | 28 | fveq2i 6909 |
. . . . . . . 8
⊢
(sin‘(2 · ((1 / 2) · (π / 2)))) =
(sin‘(π / 2)) |
| 30 | 1, 25 | mulcli 11268 |
. . . . . . . . 9
⊢ ((1 / 2)
· (π / 2)) ∈ ℂ |
| 31 | | sin2t 16213 |
. . . . . . . . 9
⊢ (((1 / 2)
· (π / 2)) ∈ ℂ → (sin‘(2 · ((1 / 2)
· (π / 2)))) = (2 · ((sin‘((1 / 2) · (π / 2)))
· (cos‘((1 / 2) · (π / 2)))))) |
| 32 | 30, 31 | ax-mp 5 |
. . . . . . . 8
⊢
(sin‘(2 · ((1 / 2) · (π / 2)))) = (2 ·
((sin‘((1 / 2) · (π / 2))) · (cos‘((1 / 2)
· (π / 2))))) |
| 33 | | sinhalfpi 26510 |
. . . . . . . 8
⊢
(sin‘(π / 2)) = 1 |
| 34 | 29, 32, 33 | 3eqtr3i 2773 |
. . . . . . 7
⊢ (2
· ((sin‘((1 / 2) · (π / 2))) · (cos‘((1 /
2) · (π / 2))))) = 1 |
| 35 | 8, 20, 34 | 3eqtr3i 2773 |
. . . . . 6
⊢ (2
· ((sin‘(π / 4)) · (sin‘(π / 4)))) =
1 |
| 36 | 35 | fveq2i 6909 |
. . . . 5
⊢
(√‘(2 · ((sin‘(π / 4)) ·
(sin‘(π / 4))))) = (√‘1) |
| 37 | | 4re 12350 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
| 38 | | 4ne0 12374 |
. . . . . . . . 9
⊢ 4 ≠
0 |
| 39 | 10, 37, 38 | redivcli 12034 |
. . . . . . . 8
⊢ (π /
4) ∈ ℝ |
| 40 | | resincl 16176 |
. . . . . . . 8
⊢ ((π /
4) ∈ ℝ → (sin‘(π / 4)) ∈
ℝ) |
| 41 | 39, 40 | ax-mp 5 |
. . . . . . 7
⊢
(sin‘(π / 4)) ∈ ℝ |
| 42 | 41, 41 | remulcli 11277 |
. . . . . 6
⊢
((sin‘(π / 4)) · (sin‘(π / 4))) ∈
ℝ |
| 43 | | 0le2 12368 |
. . . . . 6
⊢ 0 ≤
2 |
| 44 | 41 | msqge0i 11801 |
. . . . . 6
⊢ 0 ≤
((sin‘(π / 4)) · (sin‘(π / 4))) |
| 45 | 23, 42, 43, 44 | sqrtmulii 15425 |
. . . . 5
⊢
(√‘(2 · ((sin‘(π / 4)) ·
(sin‘(π / 4))))) = ((√‘2) ·
(√‘((sin‘(π / 4)) · (sin‘(π /
4))))) |
| 46 | | sqrt1 15310 |
. . . . 5
⊢
(√‘1) = 1 |
| 47 | 36, 45, 46 | 3eqtr3ri 2774 |
. . . 4
⊢ 1 =
((√‘2) · (√‘((sin‘(π / 4)) ·
(sin‘(π / 4))))) |
| 48 | 42 | sqrtcli 15410 |
. . . . . . 7
⊢ (0 ≤
((sin‘(π / 4)) · (sin‘(π / 4))) →
(√‘((sin‘(π / 4)) · (sin‘(π / 4)))) ∈
ℝ) |
| 49 | 44, 48 | ax-mp 5 |
. . . . . 6
⊢
(√‘((sin‘(π / 4)) · (sin‘(π / 4))))
∈ ℝ |
| 50 | 49 | recni 11275 |
. . . . 5
⊢
(√‘((sin‘(π / 4)) · (sin‘(π / 4))))
∈ ℂ |
| 51 | | sqrt2re 16286 |
. . . . . . 7
⊢
(√‘2) ∈ ℝ |
| 52 | 51 | recni 11275 |
. . . . . 6
⊢
(√‘2) ∈ ℂ |
| 53 | | sqrt00 15302 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → ((√‘2) = 0 ↔ 2 =
0)) |
| 54 | 23, 43, 53 | mp2an 692 |
. . . . . . . 8
⊢
((√‘2) = 0 ↔ 2 = 0) |
| 55 | 54 | necon3bii 2993 |
. . . . . . 7
⊢
((√‘2) ≠ 0 ↔ 2 ≠ 0) |
| 56 | 12, 55 | mpbir 231 |
. . . . . 6
⊢
(√‘2) ≠ 0 |
| 57 | 52, 56 | pm3.2i 470 |
. . . . 5
⊢
((√‘2) ∈ ℂ ∧ (√‘2) ≠
0) |
| 58 | | divmul2 11926 |
. . . . 5
⊢ ((1
∈ ℂ ∧ (√‘((sin‘(π / 4)) ·
(sin‘(π / 4)))) ∈ ℂ ∧ ((√‘2) ∈ ℂ
∧ (√‘2) ≠ 0)) → ((1 / (√‘2)) =
(√‘((sin‘(π / 4)) · (sin‘(π / 4)))) ↔
1 = ((√‘2) · (√‘((sin‘(π / 4)) ·
(sin‘(π / 4))))))) |
| 59 | 2, 50, 57, 58 | mp3an 1463 |
. . . 4
⊢ ((1 /
(√‘2)) = (√‘((sin‘(π / 4)) ·
(sin‘(π / 4)))) ↔ 1 = ((√‘2) ·
(√‘((sin‘(π / 4)) · (sin‘(π /
4)))))) |
| 60 | 47, 59 | mpbir 231 |
. . 3
⊢ (1 /
(√‘2)) = (√‘((sin‘(π / 4)) ·
(sin‘(π / 4)))) |
| 61 | | 0re 11263 |
. . . . 5
⊢ 0 ∈
ℝ |
| 62 | | pipos 26502 |
. . . . . . . 8
⊢ 0 <
π |
| 63 | | 4pos 12373 |
. . . . . . . 8
⊢ 0 <
4 |
| 64 | 10, 37, 62, 63 | divgt0ii 12185 |
. . . . . . 7
⊢ 0 <
(π / 4) |
| 65 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 66 | | pigt2lt4 26498 |
. . . . . . . . . . 11
⊢ (2 <
π ∧ π < 4) |
| 67 | 66 | simpri 485 |
. . . . . . . . . 10
⊢ π <
4 |
| 68 | 10, 37, 37, 63 | ltdiv1ii 12197 |
. . . . . . . . . 10
⊢ (π
< 4 ↔ (π / 4) < (4 / 4)) |
| 69 | 67, 68 | mpbi 230 |
. . . . . . . . 9
⊢ (π /
4) < (4 / 4) |
| 70 | 37 | recni 11275 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
| 71 | 70, 38 | dividi 12000 |
. . . . . . . . 9
⊢ (4 / 4) =
1 |
| 72 | 69, 71 | breqtri 5168 |
. . . . . . . 8
⊢ (π /
4) < 1 |
| 73 | 39, 65, 72 | ltleii 11384 |
. . . . . . 7
⊢ (π /
4) ≤ 1 |
| 74 | | 0xr 11308 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 75 | | elioc2 13450 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → ((π / 4) ∈
(0(,]1) ↔ ((π / 4) ∈ ℝ ∧ 0 < (π / 4) ∧ (π /
4) ≤ 1))) |
| 76 | 74, 65, 75 | mp2an 692 |
. . . . . . 7
⊢ ((π /
4) ∈ (0(,]1) ↔ ((π / 4) ∈ ℝ ∧ 0 < (π / 4)
∧ (π / 4) ≤ 1)) |
| 77 | 39, 64, 73, 76 | mpbir3an 1342 |
. . . . . 6
⊢ (π /
4) ∈ (0(,]1) |
| 78 | | sin01gt0 16226 |
. . . . . 6
⊢ ((π /
4) ∈ (0(,]1) → 0 < (sin‘(π / 4))) |
| 79 | 77, 78 | ax-mp 5 |
. . . . 5
⊢ 0 <
(sin‘(π / 4)) |
| 80 | 61, 41, 79 | ltleii 11384 |
. . . 4
⊢ 0 ≤
(sin‘(π / 4)) |
| 81 | 41 | sqrtmsqi 15412 |
. . . 4
⊢ (0 ≤
(sin‘(π / 4)) → (√‘((sin‘(π / 4)) ·
(sin‘(π / 4)))) = (sin‘(π / 4))) |
| 82 | 80, 81 | ax-mp 5 |
. . 3
⊢
(√‘((sin‘(π / 4)) · (sin‘(π / 4))))
= (sin‘(π / 4)) |
| 83 | 60, 82 | eqtr2i 2766 |
. 2
⊢
(sin‘(π / 4)) = (1 / (√‘2)) |
| 84 | 60, 82 | eqtri 2765 |
. . 3
⊢ (1 /
(√‘2)) = (sin‘(π / 4)) |
| 85 | 17 | fveq2i 6909 |
. . . 4
⊢
(cos‘((1 / 2) · (π / 2))) = (cos‘(π /
4)) |
| 86 | 6, 18, 85 | 3eqtr3i 2773 |
. . 3
⊢
(sin‘(π / 4)) = (cos‘(π / 4)) |
| 87 | 84, 86 | eqtr2i 2766 |
. 2
⊢
(cos‘(π / 4)) = (1 / (√‘2)) |
| 88 | 83, 87 | pm3.2i 470 |
1
⊢
((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π
/ 4)) = (1 / (√‘2))) |