Theorem 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	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) ≠ 0 )

Proof

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