Proof of Theorem cosne0
Step | Hyp | Ref
| Expression |
1 | | halfpire 25621 |
. . . . . 6
⊢ (π /
2) ∈ ℝ |
2 | 1 | recni 10989 |
. . . . 5
⊢ (π /
2) ∈ ℂ |
3 | | simpl 483 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ) |
4 | | nncan 11250 |
. . . . 5
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ) → ((π / 2) − ((π / 2) − 𝐴)) = 𝐴) |
5 | 2, 3, 4 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((π / 2) − ((π / 2) −
𝐴)) = 𝐴) |
6 | 5 | fveq2d 6778 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘((π / 2) − ((π / 2)
− 𝐴))) =
(cos‘𝐴)) |
7 | | subcl 11220 |
. . . . 5
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ) → ((π / 2) − 𝐴) ∈ ℂ) |
8 | 2, 3, 7 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((π / 2) − 𝐴) ∈ ℂ) |
9 | | coshalfpim 25652 |
. . . 4
⊢ (((π /
2) − 𝐴) ∈
ℂ → (cos‘((π / 2) − ((π / 2) − 𝐴))) = (sin‘((π / 2)
− 𝐴))) |
10 | 8, 9 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘((π / 2) − ((π / 2)
− 𝐴))) =
(sin‘((π / 2) − 𝐴))) |
11 | 6, 10 | eqtr3d 2780 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) = (sin‘((π / 2) − 𝐴))) |
12 | 5 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) → ((π / 2)
− ((π / 2) − 𝐴)) = 𝐴) |
13 | | picn 25616 |
. . . . . . . . . . . . 13
⊢ π
∈ ℂ |
14 | 13 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → π ∈ ℂ) |
15 | | pire 25615 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℝ |
16 | | pipos 25617 |
. . . . . . . . . . . . . 14
⊢ 0 <
π |
17 | 15, 16 | gt0ne0ii 11511 |
. . . . . . . . . . . . 13
⊢ π ≠
0 |
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → π ≠ 0) |
19 | 8, 14, 18 | divcan1d 11752 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((((π / 2) − 𝐴) / π) · π) = ((π / 2)
− 𝐴)) |
20 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) → ((((π /
2) − 𝐴) / π)
· π) = ((π / 2) − 𝐴)) |
21 | | zre 12323 |
. . . . . . . . . . . 12
⊢ ((((π
/ 2) − 𝐴) / π)
∈ ℤ → (((π / 2) − 𝐴) / π) ∈ ℝ) |
22 | 21 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) → (((π /
2) − 𝐴) / π)
∈ ℝ) |
23 | | remulcl 10956 |
. . . . . . . . . . 11
⊢ (((((π
/ 2) − 𝐴) / π)
∈ ℝ ∧ π ∈ ℝ) → ((((π / 2) − 𝐴) / π) · π) ∈
ℝ) |
24 | 22, 15, 23 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) → ((((π /
2) − 𝐴) / π)
· π) ∈ ℝ) |
25 | 20, 24 | eqeltrrd 2840 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) → ((π / 2)
− 𝐴) ∈
ℝ) |
26 | | resubcl 11285 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℝ ∧ ((π / 2) − 𝐴) ∈ ℝ) → ((π / 2) −
((π / 2) − 𝐴))
∈ ℝ) |
27 | 1, 25, 26 | sylancr 587 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) → ((π / 2)
− ((π / 2) − 𝐴)) ∈ ℝ) |
28 | 12, 27 | eqeltrrd 2840 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) → 𝐴 ∈
ℝ) |
29 | 28 | rered 14935 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) →
(ℜ‘𝐴) = 𝐴) |
30 | | simplr 766 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) →
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) |
31 | 29, 30 | eqeltrrd 2840 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) → 𝐴 ∈ (-(π / 2)(,)(π /
2))) |
32 | | 0zd 12331 |
. . . . . 6
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → 0 ∈ ℤ) |
33 | | elioore 13109 |
. . . . . . . 8
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → 𝐴 ∈
ℝ) |
34 | | resubcl 11285 |
. . . . . . . 8
⊢ (((π /
2) ∈ ℝ ∧ 𝐴
∈ ℝ) → ((π / 2) − 𝐴) ∈ ℝ) |
35 | 1, 33, 34 | sylancr 587 |
. . . . . . 7
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → ((π / 2) − 𝐴) ∈ ℝ) |
36 | 15 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → π ∈ ℝ) |
37 | | eliooord 13138 |
. . . . . . . . 9
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → (-(π / 2) < 𝐴 ∧ 𝐴 < (π / 2))) |
38 | 37 | simprd 496 |
. . . . . . . 8
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → 𝐴 < (π /
2)) |
39 | | posdif 11468 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ) → (𝐴
< (π / 2) ↔ 0 < ((π / 2) − 𝐴))) |
40 | 33, 1, 39 | sylancl 586 |
. . . . . . . 8
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → (𝐴 < (π /
2) ↔ 0 < ((π / 2) − 𝐴))) |
41 | 38, 40 | mpbid 231 |
. . . . . . 7
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → 0 < ((π / 2) − 𝐴)) |
42 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → 0 < π) |
43 | 35, 36, 41, 42 | divgt0d 11910 |
. . . . . 6
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → 0 < (((π / 2) − 𝐴) / π)) |
44 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → (π / 2) ∈ ℝ) |
45 | 2 | negcli 11289 |
. . . . . . . . . . . 12
⊢ -(π /
2) ∈ ℂ |
46 | 13, 2 | negsubi 11299 |
. . . . . . . . . . . . 13
⊢ (π +
-(π / 2)) = (π − (π / 2)) |
47 | | pidiv2halves 25624 |
. . . . . . . . . . . . . 14
⊢ ((π /
2) + (π / 2)) = π |
48 | 13, 2, 2, 47 | subaddrii 11310 |
. . . . . . . . . . . . 13
⊢ (π
− (π / 2)) = (π / 2) |
49 | 46, 48 | eqtri 2766 |
. . . . . . . . . . . 12
⊢ (π +
-(π / 2)) = (π / 2) |
50 | 2, 13, 45, 49 | subaddrii 11310 |
. . . . . . . . . . 11
⊢ ((π /
2) − π) = -(π / 2) |
51 | 37 | simpld 495 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → -(π / 2) < 𝐴) |
52 | 50, 51 | eqbrtrid 5109 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → ((π / 2) − π) < 𝐴) |
53 | 44, 36, 33, 52 | ltsub23d 11580 |
. . . . . . . . 9
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → ((π / 2) − 𝐴) < π) |
54 | 13 | mulid1i 10979 |
. . . . . . . . 9
⊢ (π
· 1) = π |
55 | 53, 54 | breqtrrdi 5116 |
. . . . . . . 8
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → ((π / 2) − 𝐴) < (π · 1)) |
56 | | 1red 10976 |
. . . . . . . . 9
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → 1 ∈ ℝ) |
57 | | ltdivmul 11850 |
. . . . . . . . 9
⊢ ((((π
/ 2) − 𝐴) ∈
ℝ ∧ 1 ∈ ℝ ∧ (π ∈ ℝ ∧ 0 < π))
→ ((((π / 2) − 𝐴) / π) < 1 ↔ ((π / 2) −
𝐴) < (π ·
1))) |
58 | 35, 56, 36, 42, 57 | syl112anc 1373 |
. . . . . . . 8
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → ((((π / 2) − 𝐴) / π) < 1 ↔ ((π / 2) −
𝐴) < (π ·
1))) |
59 | 55, 58 | mpbird 256 |
. . . . . . 7
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → (((π / 2) − 𝐴) / π) < 1) |
60 | | 1e0p1 12479 |
. . . . . . 7
⊢ 1 = (0 +
1) |
61 | 59, 60 | breqtrdi 5115 |
. . . . . 6
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → (((π / 2) − 𝐴) / π) < (0 + 1)) |
62 | | btwnnz 12396 |
. . . . . 6
⊢ ((0
∈ ℤ ∧ 0 < (((π / 2) − 𝐴) / π) ∧ (((π / 2) − 𝐴) / π) < (0 + 1)) →
¬ (((π / 2) − 𝐴) / π) ∈ ℤ) |
63 | 32, 43, 61, 62 | syl3anc 1370 |
. . . . 5
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → ¬ (((π / 2) − 𝐴) / π) ∈ ℤ) |
64 | 31, 63 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (((π / 2) − 𝐴) / π) ∈ ℤ) → ¬
(((π / 2) − 𝐴) /
π) ∈ ℤ) |
65 | 64 | pm2.01da 796 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ¬ (((π / 2) − 𝐴) / π) ∈ ℤ) |
66 | | sineq0 25680 |
. . . . 5
⊢ (((π /
2) − 𝐴) ∈
ℂ → ((sin‘((π / 2) − 𝐴)) = 0 ↔ (((π / 2) − 𝐴) / π) ∈
ℤ)) |
67 | 8, 66 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((sin‘((π / 2) − 𝐴)) = 0 ↔ (((π / 2)
− 𝐴) / π) ∈
ℤ)) |
68 | 67 | necon3abid 2980 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((sin‘((π / 2) − 𝐴)) ≠ 0 ↔ ¬ (((π /
2) − 𝐴) / π)
∈ ℤ)) |
69 | 65, 68 | mpbird 256 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘((π / 2) − 𝐴)) ≠ 0) |
70 | 11, 69 | eqnetrd 3011 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) ≠ 0) |