pmltpc

Description: Any function on the reals is either increasing, decreasing, or has a triple of points in a vee formation. (This theorem was created on demand by Mario Carneiro for the 6PCM conference in Bialystok, 1-Jul-2014.) (Contributed by Mario Carneiro, 1-Jul-2014)

		Ref	Expression
	Assertion	pmltpc	$⊢ (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \to (\forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \lor \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x)) \lor \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c)))))$

Proof

Step	Hyp	Ref	Expression
1		rexanali	$⊢ \exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \leftrightarrow \neg \forall y \in A (x \leq y \to F (x) \leq F (y))$
2	1	rexbii	$⊢ \exists x \in A \exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \leftrightarrow \exists x \in A \neg \forall y \in A (x \leq y \to F (x) \leq F (y))$
3		rexnal	$⊢ \exists x \in A \neg \forall y \in A (x \leq y \to F (x) \leq F (y)) \leftrightarrow \neg \forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y))$
4	2 3	bitri	$⊢ \exists x \in A \exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \leftrightarrow \neg \forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y))$
5		rexanali	$⊢ \exists w \in A (z \leq w \land \neg F (w) \leq F (z)) \leftrightarrow \neg \forall w \in A (z \leq w \to F (w) \leq F (z))$
6	5	rexbii	$⊢ \exists z \in A \exists w \in A (z \leq w \land \neg F (w) \leq F (z)) \leftrightarrow \exists z \in A \neg \forall w \in A (z \leq w \to F (w) \leq F (z))$
7		rexnal	$⊢ \exists z \in A \neg \forall w \in A (z \leq w \to F (w) \leq F (z)) \leftrightarrow \neg \forall z \in A \forall w \in A (z \leq w \to F (w) \leq F (z))$
8		breq1	$⊢ z = x \to (z \leq w \leftrightarrow x \leq w)$
9		fveq2	$⊢ z = x \to F (z) = F (x)$
10	9	breq2d	$⊢ z = x \to (F (w) \leq F (z) \leftrightarrow F (w) \leq F (x))$
11	8 10	imbi12d	$⊢ z = x \to ((z \leq w \to F (w) \leq F (z)) \leftrightarrow (x \leq w \to F (w) \leq F (x)))$
12		breq2	$⊢ w = y \to (x \leq w \leftrightarrow x \leq y)$
13		fveq2	$⊢ w = y \to F (w) = F (y)$
14	13	breq1d	$⊢ w = y \to (F (w) \leq F (x) \leftrightarrow F (y) \leq F (x))$
15	12 14	imbi12d	$⊢ w = y \to ((x \leq w \to F (w) \leq F (x)) \leftrightarrow (x \leq y \to F (y) \leq F (x)))$
16	11 15	cbvral2vw	$⊢ \forall z \in A \forall w \in A (z \leq w \to F (w) \leq F (z)) \leftrightarrow \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x))$
17	7 16	xchbinx	$⊢ \exists z \in A \neg \forall w \in A (z \leq w \to F (w) \leq F (z)) \leftrightarrow \neg \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x))$
18	6 17	bitri	$⊢ \exists z \in A \exists w \in A (z \leq w \land \neg F (w) \leq F (z)) \leftrightarrow \neg \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x))$
19	4 18	anbi12i	$⊢ (\exists x \in A \exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \land \exists z \in A \exists w \in A (z \leq w \land \neg F (w) \leq F (z))) \leftrightarrow (\neg \forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \land \neg \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x)))$
20		reeanv	$⊢ \exists x \in A \exists z \in A (\exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \land \exists w \in A (z \leq w \land \neg F (w) \leq F (z))) \leftrightarrow (\exists x \in A \exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \land \exists z \in A \exists w \in A (z \leq w \land \neg F (w) \leq F (z)))$
21		ioran	$⊢ \neg (\forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \lor \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x))) \leftrightarrow (\neg \forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \land \neg \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x)))$
22	19 20 21	3bitr4i	$⊢ \exists x \in A \exists z \in A (\exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \land \exists w \in A (z \leq w \land \neg F (w) \leq F (z))) \leftrightarrow \neg (\forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \lor \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x)))$
23		reeanv	$⊢ \exists y \in A \exists w \in A ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z))) \leftrightarrow (\exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \land \exists w \in A (z \leq w \land \neg F (w) \leq F (z)))$
24		simplll	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F)$
25	24	simpld	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to F \in (ℝ ↑_{𝑝𝑚} ℝ)$
26	24	simprd	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to A \subseteq dom F$
27		simpllr	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to (x \in A \land z \in A)$
28	27	simpld	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to x \in A$
29		simplrl	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to y \in A$
30	27	simprd	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to z \in A$
31		simplrr	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to w \in A$
32		simprll	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to x \leq y$
33		simprrl	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to z \leq w$
34		simprlr	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to \neg F (x) \leq F (y)$
35		simprrr	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to \neg F (w) \leq F (z)$
36	25 26 28 29 30 31 32 33 34 35	pmltpclem2	$⊢ ((((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \land ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z)))) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))$
37	36	ex	$⊢ (((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \land (y \in A \land w \in A)) \to (((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z))) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c)))))$
38	37	rexlimdvva	$⊢ ((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \to (\exists y \in A \exists w \in A ((x \leq y \land \neg F (x) \leq F (y)) \land (z \leq w \land \neg F (w) \leq F (z))) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c)))))$
39	23 38	syl5bir	$⊢ ((F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \land (x \in A \land z \in A)) \to ((\exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \land \exists w \in A (z \leq w \land \neg F (w) \leq F (z))) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c)))))$
40	39	rexlimdvva	$⊢ (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \to (\exists x \in A \exists z \in A (\exists y \in A (x \leq y \land \neg F (x) \leq F (y)) \land \exists w \in A (z \leq w \land \neg F (w) \leq F (z))) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c)))))$
41	22 40	syl5bir	$⊢ (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \to (\neg (\forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \lor \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x))) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c)))))$
42	41	orrd	$⊢ (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \to ((\forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \lor \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x))) \lor \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c)))))$
43		df-3or	$⊢ (\forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \lor \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x)) \lor \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))) \leftrightarrow ((\forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \lor \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x))) \lor \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c)))))$
44	42 43	sylibr	$⊢ (F \in (ℝ ↑_{𝑝𝑚} ℝ) \land A \subseteq dom F) \to (\forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y)) \lor \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x)) \lor \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c)))))$

Metamath Proof Explorer

Theorem pmltpc

Proof