fourierdlem24

Description: A sufficient condition for module being nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	fourierdlem24	$⊢ A \in ([- π, π] ∖ \{0\}) \to A \mod 2 π \neq 0$

Proof

Step	Hyp	Ref	Expression
1		0zd	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to 0 \in ℤ$
2		pire	$⊢ π \in ℝ$
3	2	renegcli	$⊢ - π \in ℝ$
4		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
5	3 2 4	mp2an	$⊢ [- π, π] \subseteq ℝ$
6		eldifi	$⊢ A \in ([- π, π] ∖ \{0\}) \to A \in [- π, π]$
7	5 6	sselid	$⊢ A \in ([- π, π] ∖ \{0\}) \to A \in ℝ$
8	7	adantr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to A \in ℝ$
9		2re	$⊢ 2 \in ℝ$
10	9 2	remulcli	$⊢ 2 π \in ℝ$
11	10	a1i	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to 2 π \in ℝ$
12		simpr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to 0 < A$
13		2pos	$⊢ 0 < 2$
14		pipos	$⊢ 0 < π$
15	9 2 13 14	mulgt0ii	$⊢ 0 < 2 π$
16	15	a1i	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to 0 < 2 π$
17	8 11 12 16	divgt0d	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to 0 < \frac{A}{2 π}$
18	11 16	elrpd	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to 2 π \in ℝ^{+}$
19	2	a1i	$⊢ A \in ([- π, π] ∖ \{0\}) \to π \in ℝ$
20	10	a1i	$⊢ A \in ([- π, π] ∖ \{0\}) \to 2 π \in ℝ$
21	3	rexri	$⊢ - π \in ℝ^{*}$
22	21	a1i	$⊢ A \in ([- π, π] ∖ \{0\}) \to - π \in ℝ^{*}$
23	19	rexrd	$⊢ A \in ([- π, π] ∖ \{0\}) \to π \in ℝ^{*}$
24		iccleub	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land A \in [- π, π]) \to A \leq π$
25	22 23 6 24	syl3anc	$⊢ A \in ([- π, π] ∖ \{0\}) \to A \leq π$
26		pirp	$⊢ π \in ℝ^{+}$
27		2timesgt	$⊢ π \in ℝ^{+} \to π < 2 π$
28	26 27	mp1i	$⊢ A \in ([- π, π] ∖ \{0\}) \to π < 2 π$
29	7 19 20 25 28	lelttrd	$⊢ A \in ([- π, π] ∖ \{0\}) \to A < 2 π$
30	29	adantr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to A < 2 π$
31	8 11 18 30	ltdiv1dd	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to \frac{A}{2 π} < \frac{2 π}{2 π}$
32	10	recni	$⊢ 2 π \in ℂ$
33	10 15	gt0ne0ii	$⊢ 2 π \neq 0$
34	32 33	dividi	$⊢ \frac{2 π}{2 π} = 1$
35	31 34	breqtrdi	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to \frac{A}{2 π} < 1$
36		0p1e1	$⊢ 0 + 1 = 1$
37	35 36	breqtrrdi	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to \frac{A}{2 π} < 0 + 1$
38		btwnnz	$⊢ (0 \in ℤ \land 0 < \frac{A}{2 π} \land \frac{A}{2 π} < 0 + 1) \to \neg \frac{A}{2 π} \in ℤ$
39	1 17 37 38	syl3anc	$⊢ (A \in ([- π, π] ∖ \{0\}) \land 0 < A) \to \neg \frac{A}{2 π} \in ℤ$
40		simpl	$⊢ (A \in ([- π, π] ∖ \{0\}) \land \neg 0 < A) \to A \in ([- π, π] ∖ \{0\})$
41	7	adantr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land \neg 0 < A) \to A \in ℝ$
42		0red	$⊢ (A \in ([- π, π] ∖ \{0\}) \land \neg 0 < A) \to 0 \in ℝ$
43		simpr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land \neg 0 < A) \to \neg 0 < A$
44	41 42 43	nltled	$⊢ (A \in ([- π, π] ∖ \{0\}) \land \neg 0 < A) \to A \leq 0$
45		eldifsni	$⊢ A \in ([- π, π] ∖ \{0\}) \to A \neq 0$
46	45	necomd	$⊢ A \in ([- π, π] ∖ \{0\}) \to 0 \neq A$
47	46	adantr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land \neg 0 < A) \to 0 \neq A$
48	41 42 44 47	leneltd	$⊢ (A \in ([- π, π] ∖ \{0\}) \land \neg 0 < A) \to A < 0$
49		neg1z	$⊢ - 1 \in ℤ$
50	49	a1i	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to - 1 \in ℤ$
51	33	a1i	$⊢ A \in ([- π, π] ∖ \{0\}) \to 2 π \neq 0$
52	7 20 51	redivcld	$⊢ A \in ([- π, π] ∖ \{0\}) \to \frac{A}{2 π} \in ℝ$
53	52	adantr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to \frac{A}{2 π} \in ℝ$
54		1red	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to 1 \in ℝ$
55	7	recnd	$⊢ A \in ([- π, π] ∖ \{0\}) \to A \in ℂ$
56	55	adantr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to A \in ℂ$
57	32	a1i	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to 2 π \in ℂ$
58	33	a1i	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to 2 π \neq 0$
59	56 57 58	divnegd	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to - \frac{A}{2 π} = \frac{- A}{2 π}$
60	7	renegcld	$⊢ A \in ([- π, π] ∖ \{0\}) \to - A \in ℝ$
61	60	adantr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to - A \in ℝ$
62	10	a1i	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to 2 π \in ℝ$
63		2rp	$⊢ 2 \in ℝ^{+}$
64		rpmulcl	$⊢ (2 \in ℝ^{+} \land π \in ℝ^{+}) \to 2 π \in ℝ^{+}$
65	63 26 64	mp2an	$⊢ 2 π \in ℝ^{+}$
66	65	a1i	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to 2 π \in ℝ^{+}$
67		iccgelb	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land A \in [- π, π]) \to - π \leq A$
68	22 23 6 67	syl3anc	$⊢ A \in ([- π, π] ∖ \{0\}) \to - π \leq A$
69	19 7 68	lenegcon1d	$⊢ A \in ([- π, π] ∖ \{0\}) \to - A \leq π$
70	60 19 20 69 28	lelttrd	$⊢ A \in ([- π, π] ∖ \{0\}) \to - A < 2 π$
71	70	adantr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to - A < 2 π$
72	61 62 66 71	ltdiv1dd	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to \frac{- A}{2 π} < \frac{2 π}{2 π}$
73	72 34	breqtrdi	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to \frac{- A}{2 π} < 1$
74	59 73	eqbrtrd	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to - \frac{A}{2 π} < 1$
75	53 54 74	ltnegcon1d	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to - 1 < \frac{A}{2 π}$
76	7	adantr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to A \in ℝ$
77		simpr	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to A < 0$
78	76 66 77	divlt0gt0d	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to \frac{A}{2 π} < 0$
79		neg1cn	$⊢ - 1 \in ℂ$
80		ax-1cn	$⊢ 1 \in ℂ$
81	79 80	addcomi	$⊢ - 1 + 1 = 1 + -1$
82		1pneg1e0	$⊢ 1 + -1 = 0$
83	81 82	eqtr2i	$⊢ 0 = - 1 + 1$
84	78 83	breqtrdi	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to \frac{A}{2 π} < - 1 + 1$
85		btwnnz	$⊢ (- 1 \in ℤ \land - 1 < \frac{A}{2 π} \land \frac{A}{2 π} < - 1 + 1) \to \neg \frac{A}{2 π} \in ℤ$
86	50 75 84 85	syl3anc	$⊢ (A \in ([- π, π] ∖ \{0\}) \land A < 0) \to \neg \frac{A}{2 π} \in ℤ$
87	40 48 86	syl2anc	$⊢ (A \in ([- π, π] ∖ \{0\}) \land \neg 0 < A) \to \neg \frac{A}{2 π} \in ℤ$
88	39 87	pm2.61dan	$⊢ A \in ([- π, π] ∖ \{0\}) \to \neg \frac{A}{2 π} \in ℤ$
89	65	a1i	$⊢ A \in ([- π, π] ∖ \{0\}) \to 2 π \in ℝ^{+}$
90		mod0	$⊢ (A \in ℝ \land 2 π \in ℝ^{+}) \to (A \mod 2 π = 0 \leftrightarrow \frac{A}{2 π} \in ℤ)$
91	7 89 90	syl2anc	$⊢ A \in ([- π, π] ∖ \{0\}) \to (A \mod 2 π = 0 \leftrightarrow \frac{A}{2 π} \in ℤ)$
92	88 91	mtbird	$⊢ A \in ([- π, π] ∖ \{0\}) \to \neg A \mod 2 π = 0$
93	92	neqned	$⊢ A \in ([- π, π] ∖ \{0\}) \to A \mod 2 π \neq 0$

Metamath Proof Explorer

Theorem fourierdlem24

Proof