pilem3

Description: Lemma for pire , pigt2lt4 and sinpi . Existence part. (Contributed by Paul Chapman, 23-Jan-2008) (Proof shortened by Mario Carneiro, 18-Jun-2014) (Revised by AV, 14-Sep-2020) (Proof shortened by BJ, 30-Jun-2022)

		Ref	Expression
	Assertion	pilem3	$⊢ (π \in (2, 4) \land \sin π = 0)$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2	1	a1i	$⊢ ⊤ \to 2 \in ℝ$
3		4re	$⊢ 4 \in ℝ$
4	3	a1i	$⊢ ⊤ \to 4 \in ℝ$
5		0red	$⊢ ⊤ \to 0 \in ℝ$
6		2lt4	$⊢ 2 < 4$
7	6	a1i	$⊢ ⊤ \to 2 < 4$
8		iccssre	$⊢ (2 \in ℝ \land 4 \in ℝ) \to [2, 4] \subseteq ℝ$
9	1 3 8	mp2an	$⊢ [2, 4] \subseteq ℝ$
10		ax-resscn	$⊢ ℝ \subseteq ℂ$
11	9 10	sstri	$⊢ [2, 4] \subseteq ℂ$
12	11	a1i	$⊢ ⊤ \to [2, 4] \subseteq ℂ$
13		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
14	13	a1i	$⊢ ⊤ \to \sin : ℂ \underset{cn}{⟶} ℂ$
15	9	sseli	$⊢ y \in [2, 4] \to y \in ℝ$
16	15	resincld	$⊢ y \in [2, 4] \to \sin y \in ℝ$
17	16	adantl	$⊢ (⊤ \land y \in [2, 4]) \to \sin y \in ℝ$
18		sin4lt0	$⊢ \sin 4 < 0$
19		sincos2sgn	$⊢ (0 < \sin 2 \land \cos 2 < 0)$
20	19	simpli	$⊢ 0 < \sin 2$
21	18 20	pm3.2i	$⊢ (\sin 4 < 0 \land 0 < \sin 2)$
22	21	a1i	$⊢ ⊤ \to (\sin 4 < 0 \land 0 < \sin 2)$
23	2 4 5 7 12 14 17 22	ivth2	$⊢ ⊤ \to \exists x \in (2, 4) \sin x = 0$
24	23	mptru	$⊢ \exists x \in (2, 4) \sin x = 0$
25		df-pi	$⊢ π = inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <)$
26		inss1	$⊢ ℝ^{+} \cap \sin^{-1} [\{0\}] \subseteq ℝ^{+}$
27		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
28	26 27	sstri	$⊢ ℝ^{+} \cap \sin^{-1} [\{0\}] \subseteq ℝ$
29		0re	$⊢ 0 \in ℝ$
30	26	sseli	$⊢ z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) \to z \in ℝ^{+}$
31	30	rpge0d	$⊢ z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) \to 0 \leq z$
32	31	rgen	$⊢ \forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) 0 \leq z$
33		breq1	$⊢ y = 0 \to (y \leq z \leftrightarrow 0 \leq z)$
34	33	ralbidv	$⊢ y = 0 \to (\forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) y \leq z \leftrightarrow \forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) 0 \leq z)$
35	34	rspcev	$⊢ (0 \in ℝ \land \forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) 0 \leq z) \to \exists y \in ℝ \forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) y \leq z$
36	29 32 35	mp2an	$⊢ \exists y \in ℝ \forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) y \leq z$
37		elioore	$⊢ x \in (2, 4) \to x \in ℝ$
38	37	adantr	$⊢ (x \in (2, 4) \land \sin x = 0) \to x \in ℝ$
39		0red	$⊢ (x \in (2, 4) \land \sin x = 0) \to 0 \in ℝ$
40	1	a1i	$⊢ (x \in (2, 4) \land \sin x = 0) \to 2 \in ℝ$
41		2pos	$⊢ 0 < 2$
42	41	a1i	$⊢ (x \in (2, 4) \land \sin x = 0) \to 0 < 2$
43		eliooord	$⊢ x \in (2, 4) \to (2 < x \land x < 4)$
44	43	simpld	$⊢ x \in (2, 4) \to 2 < x$
45	44	adantr	$⊢ (x \in (2, 4) \land \sin x = 0) \to 2 < x$
46	39 40 38 42 45	lttrd	$⊢ (x \in (2, 4) \land \sin x = 0) \to 0 < x$
47	38 46	elrpd	$⊢ (x \in (2, 4) \land \sin x = 0) \to x \in ℝ^{+}$
48		simpr	$⊢ (x \in (2, 4) \land \sin x = 0) \to \sin x = 0$
49		pilem1	$⊢ x \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) \leftrightarrow (x \in ℝ^{+} \land \sin x = 0)$
50	47 48 49	sylanbrc	$⊢ (x \in (2, 4) \land \sin x = 0) \to x \in (ℝ^{+} \cap \sin^{-1} [\{0\}])$
51		infrelb	$⊢ (ℝ^{+} \cap \sin^{-1} [\{0\}] \subseteq ℝ \land \exists y \in ℝ \forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) y \leq z \land x \in (ℝ^{+} \cap \sin^{-1} [\{0\}])) \to inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <) \leq x$
52	28 36 50 51	mp3an12i	$⊢ (x \in (2, 4) \land \sin x = 0) \to inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <) \leq x$
53	25 52	eqbrtrid	$⊢ (x \in (2, 4) \land \sin x = 0) \to π \leq x$
54		simpll	$⊢ ((x \in (2, 4) \land \sin x = 0) \land y \in (ℝ^{+} \cap \sin^{-1} [\{0\}])) \to x \in (2, 4)$
55		pilem1	$⊢ y \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) \leftrightarrow (y \in ℝ^{+} \land \sin y = 0)$
56	55	bilani	$⊢ ((x \in (2, 4) \land \sin x = 0) \land y \in (ℝ^{+} \cap \sin^{-1} [\{0\}])) \to (y \in ℝ^{+} \land \sin y = 0)$
57	56	simpld	$⊢ ((x \in (2, 4) \land \sin x = 0) \land y \in (ℝ^{+} \cap \sin^{-1} [\{0\}])) \to y \in ℝ^{+}$
58		simplr	$⊢ ((x \in (2, 4) \land \sin x = 0) \land y \in (ℝ^{+} \cap \sin^{-1} [\{0\}])) \to \sin x = 0$
59	56	simprd	$⊢ ((x \in (2, 4) \land \sin x = 0) \land y \in (ℝ^{+} \cap \sin^{-1} [\{0\}])) \to \sin y = 0$
60	54 57 58 59	pilem2	$⊢ ((x \in (2, 4) \land \sin x = 0) \land y \in (ℝ^{+} \cap \sin^{-1} [\{0\}])) \to \frac{π + x}{2} \leq y$
61	60	ralrimiva	$⊢ (x \in (2, 4) \land \sin x = 0) \to \forall y \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) \frac{π + x}{2} \leq y$
62	28	a1i	$⊢ (x \in (2, 4) \land \sin x = 0) \to ℝ^{+} \cap \sin^{-1} [\{0\}] \subseteq ℝ$
63	50	ne0d	$⊢ (x \in (2, 4) \land \sin x = 0) \to ℝ^{+} \cap \sin^{-1} [\{0\}] \neq \emptyset$
64	36	a1i	$⊢ (x \in (2, 4) \land \sin x = 0) \to \exists y \in ℝ \forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) y \leq z$
65		infrecl	$⊢ (ℝ^{+} \cap \sin^{-1} [\{0\}] \subseteq ℝ \land ℝ^{+} \cap \sin^{-1} [\{0\}] \neq \emptyset \land \exists y \in ℝ \forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) y \leq z) \to inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <) \in ℝ$
66	28 36 65	mp3an13	$⊢ ℝ^{+} \cap \sin^{-1} [\{0\}] \neq \emptyset \to inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <) \in ℝ$
67	63 66	syl	$⊢ (x \in (2, 4) \land \sin x = 0) \to inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <) \in ℝ$
68	25 67	eqeltrid	$⊢ (x \in (2, 4) \land \sin x = 0) \to π \in ℝ$
69	68 38	readdcld	$⊢ (x \in (2, 4) \land \sin x = 0) \to π + x \in ℝ$
70	69	rehalfcld	$⊢ (x \in (2, 4) \land \sin x = 0) \to \frac{π + x}{2} \in ℝ$
71		infregelb	$⊢ ((ℝ^{+} \cap \sin^{-1} [\{0\}] \subseteq ℝ \land ℝ^{+} \cap \sin^{-1} [\{0\}] \neq \emptyset \land \exists y \in ℝ \forall z \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) y \leq z) \land \frac{π + x}{2} \in ℝ) \to (\frac{π + x}{2} \leq inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <) \leftrightarrow \forall y \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) \frac{π + x}{2} \leq y)$
72	62 63 64 70 71	syl31anc	$⊢ (x \in (2, 4) \land \sin x = 0) \to (\frac{π + x}{2} \leq inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <) \leftrightarrow \forall y \in (ℝ^{+} \cap \sin^{-1} [\{0\}]) \frac{π + x}{2} \leq y)$
73	61 72	mpbird	$⊢ (x \in (2, 4) \land \sin x = 0) \to \frac{π + x}{2} \leq inf (ℝ^{+} \cap \sin^{-1} [\{0\}] ℝ <)$
74	73 25	breqtrrdi	$⊢ (x \in (2, 4) \land \sin x = 0) \to \frac{π + x}{2} \leq π$
75	68	recnd	$⊢ (x \in (2, 4) \land \sin x = 0) \to π \in ℂ$
76	38	recnd	$⊢ (x \in (2, 4) \land \sin x = 0) \to x \in ℂ$
77	75 76	addcomd	$⊢ (x \in (2, 4) \land \sin x = 0) \to π + x = x + π$
78	77	oveq1d	$⊢ (x \in (2, 4) \land \sin x = 0) \to \frac{π + x}{2} = \frac{x + π}{2}$
79	78	breq1d	$⊢ (x \in (2, 4) \land \sin x = 0) \to (\frac{π + x}{2} \leq π \leftrightarrow \frac{x + π}{2} \leq π)$
80		avgle2	$⊢ (x \in ℝ \land π \in ℝ) \to (x \leq π \leftrightarrow \frac{x + π}{2} \leq π)$
81	38 68 80	syl2anc	$⊢ (x \in (2, 4) \land \sin x = 0) \to (x \leq π \leftrightarrow \frac{x + π}{2} \leq π)$
82	79 81	bitr4d	$⊢ (x \in (2, 4) \land \sin x = 0) \to (\frac{π + x}{2} \leq π \leftrightarrow x \leq π)$
83	74 82	mpbid	$⊢ (x \in (2, 4) \land \sin x = 0) \to x \leq π$
84	68 38	letri3d	$⊢ (x \in (2, 4) \land \sin x = 0) \to (π = x \leftrightarrow (π \leq x \land x \leq π))$
85	53 83 84	mpbir2and	$⊢ (x \in (2, 4) \land \sin x = 0) \to π = x$
86		simpl	$⊢ (x \in (2, 4) \land \sin x = 0) \to x \in (2, 4)$
87	85 86	eqeltrd	$⊢ (x \in (2, 4) \land \sin x = 0) \to π \in (2, 4)$
88	85	fveq2d	$⊢ (x \in (2, 4) \land \sin x = 0) \to \sin π = \sin x$
89	88 48	eqtrd	$⊢ (x \in (2, 4) \land \sin x = 0) \to \sin π = 0$
90	87 89	jca	$⊢ (x \in (2, 4) \land \sin x = 0) \to (π \in (2, 4) \land \sin π = 0)$
91	90	rexlimiva	$⊢ \exists x \in (2, 4) \sin x = 0 \to (π \in (2, 4) \land \sin π = 0)$
92	24 91	ax-mp	$⊢ (π \in (2, 4) \land \sin π = 0)$

Metamath Proof Explorer

Theorem pilem3

Proof