cosne0

Description: The cosine function has no zeroes within the vertical strip of the complex plane between real part -upi / 2 and pi / 2 . (Contributed by Mario Carneiro, 2-Apr-2015)

		Ref	Expression
	Assertion	cosne0	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos A \neq 0$

Proof

Step	Hyp	Ref	Expression
1		halfpire	$⊢ \frac{π}{2} \in ℝ$
2	1	recni	$⊢ \frac{π}{2} \in ℂ$
3		simpl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to A \in ℂ$
4		nncan	$⊢ (\frac{π}{2} \in ℂ \land A \in ℂ) \to (\frac{π}{2}) - ((\frac{π}{2}) - A) = A$
5	2 3 4	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{π}{2}) - ((\frac{π}{2}) - A) = A$
6	5	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos ((\frac{π}{2}) - ((\frac{π}{2}) - A)) = \cos A$
7		subcl	$⊢ (\frac{π}{2} \in ℂ \land A \in ℂ) \to (\frac{π}{2}) - A \in ℂ$
8	2 3 7	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{π}{2}) - A \in ℂ$
9		coshalfpim	$⊢ (\frac{π}{2}) - A \in ℂ \to \cos ((\frac{π}{2}) - ((\frac{π}{2}) - A)) = \sin ((\frac{π}{2}) - A)$
10	8 9	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos ((\frac{π}{2}) - ((\frac{π}{2}) - A)) = \sin ((\frac{π}{2}) - A)$
11	6 10	eqtr3d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos A = \sin ((\frac{π}{2}) - A)$
12	5	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to (\frac{π}{2}) - ((\frac{π}{2}) - A) = A$
13		picn	$⊢ π \in ℂ$
14	13	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to π \in ℂ$
15		pire	$⊢ π \in ℝ$
16		pipos	$⊢ 0 < π$
17	15 16	gt0ne0ii	$⊢ π \neq 0$
18	17	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to π \neq 0$
19	8 14 18	divcan1d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{(\frac{π}{2}) - A}{π}) π = (\frac{π}{2}) - A$
20	19	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to (\frac{(\frac{π}{2}) - A}{π}) π = (\frac{π}{2}) - A$
21		zre	$⊢ \frac{(\frac{π}{2}) - A}{π} \in ℤ \to \frac{(\frac{π}{2}) - A}{π} \in ℝ$
22	21	adantl	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to \frac{(\frac{π}{2}) - A}{π} \in ℝ$
23		remulcl	$⊢ (\frac{(\frac{π}{2}) - A}{π} \in ℝ \land π \in ℝ) \to (\frac{(\frac{π}{2}) - A}{π}) π \in ℝ$
24	22 15 23	sylancl	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to (\frac{(\frac{π}{2}) - A}{π}) π \in ℝ$
25	20 24	eqeltrrd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to (\frac{π}{2}) - A \in ℝ$
26		resubcl	$⊢ (\frac{π}{2} \in ℝ \land (\frac{π}{2}) - A \in ℝ) \to (\frac{π}{2}) - ((\frac{π}{2}) - A) \in ℝ$
27	1 25 26	sylancr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to (\frac{π}{2}) - ((\frac{π}{2}) - A) \in ℝ$
28	12 27	eqeltrrd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to A \in ℝ$
29	28	rered	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to ℜ (A) = A$
30		simplr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})$
31	29 30	eqeltrrd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to A \in (- \frac{π}{2}, \frac{π}{2})$
32		0zd	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to 0 \in ℤ$
33		elioore	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to A \in ℝ$
34		resubcl	$⊢ (\frac{π}{2} \in ℝ \land A \in ℝ) \to (\frac{π}{2}) - A \in ℝ$
35	1 33 34	sylancr	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (\frac{π}{2}) - A \in ℝ$
36	15	a1i	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to π \in ℝ$
37		eliooord	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (- \frac{π}{2} < A \land A < \frac{π}{2})$
38	37	simprd	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to A < \frac{π}{2}$
39		posdif	$⊢ (A \in ℝ \land \frac{π}{2} \in ℝ) \to (A < \frac{π}{2} \leftrightarrow 0 < (\frac{π}{2}) - A)$
40	33 1 39	sylancl	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (A < \frac{π}{2} \leftrightarrow 0 < (\frac{π}{2}) - A)$
41	38 40	mpbid	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to 0 < (\frac{π}{2}) - A$
42	16	a1i	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to 0 < π$
43	35 36 41 42	divgt0d	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to 0 < \frac{(\frac{π}{2}) - A}{π}$
44	1	a1i	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to \frac{π}{2} \in ℝ$
45	2	negcli	$⊢ - \frac{π}{2} \in ℂ$
46	13 2	negsubi	$⊢ π + (- \frac{π}{2}) = π - (\frac{π}{2})$
47		pidiv2halves	$⊢ (\frac{π}{2}) + (\frac{π}{2}) = π$
48	13 2 2 47	subaddrii	$⊢ π - (\frac{π}{2}) = \frac{π}{2}$
49	46 48	eqtri	$⊢ π + (- \frac{π}{2}) = \frac{π}{2}$
50	2 13 45 49	subaddrii	$⊢ (\frac{π}{2}) - π = - \frac{π}{2}$
51	37	simpld	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to - \frac{π}{2} < A$
52	50 51	eqbrtrid	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (\frac{π}{2}) - π < A$
53	44 36 33 52	ltsub23d	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (\frac{π}{2}) - A < π$
54	13	mulid1i	$⊢ π \cdot 1 = π$
55	53 54	breqtrrdi	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (\frac{π}{2}) - A < π \cdot 1$
56		1red	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to 1 \in ℝ$
57		ltdivmul	$⊢ ((\frac{π}{2}) - A \in ℝ \land 1 \in ℝ \land (π \in ℝ \land 0 < π)) \to (\frac{(\frac{π}{2}) - A}{π} < 1 \leftrightarrow (\frac{π}{2}) - A < π \cdot 1)$
58	35 56 36 42 57	syl112anc	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to (\frac{(\frac{π}{2}) - A}{π} < 1 \leftrightarrow (\frac{π}{2}) - A < π \cdot 1)$
59	55 58	mpbird	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to \frac{(\frac{π}{2}) - A}{π} < 1$
60		1e0p1	$⊢ 1 = 0 + 1$
61	59 60	breqtrdi	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to \frac{(\frac{π}{2}) - A}{π} < 0 + 1$
62		btwnnz	$⊢ (0 \in ℤ \land 0 < \frac{(\frac{π}{2}) - A}{π} \land \frac{(\frac{π}{2}) - A}{π} < 0 + 1) \to \neg \frac{(\frac{π}{2}) - A}{π} \in ℤ$
63	32 43 61 62	syl3anc	$⊢ A \in (- \frac{π}{2}, \frac{π}{2}) \to \neg \frac{(\frac{π}{2}) - A}{π} \in ℤ$
64	31 63	syl	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land \frac{(\frac{π}{2}) - A}{π} \in ℤ) \to \neg \frac{(\frac{π}{2}) - A}{π} \in ℤ$
65	64	pm2.01da	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \neg \frac{(\frac{π}{2}) - A}{π} \in ℤ$
66		sineq0	$⊢ (\frac{π}{2}) - A \in ℂ \to (\sin ((\frac{π}{2}) - A) = 0 \leftrightarrow \frac{(\frac{π}{2}) - A}{π} \in ℤ)$
67	8 66	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\sin ((\frac{π}{2}) - A) = 0 \leftrightarrow \frac{(\frac{π}{2}) - A}{π} \in ℤ)$
68	67	necon3abid	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\sin ((\frac{π}{2}) - A) \neq 0 \leftrightarrow \neg \frac{(\frac{π}{2}) - A}{π} \in ℤ)$
69	65 68	mpbird	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \sin ((\frac{π}{2}) - A) \neq 0$
70	11 69	eqnetrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos A \neq 0$

Metamath Proof Explorer

Theorem cosne0

Proof