iccpartigtl

Description: If there is a partition, then all intermediate points are strictly greater than the lower bound. (Contributed by AV, 12-Jul-2020)

	Ref	Expression
Hypotheses	iccpartgtprec.m	$⊢ φ \to M \in ℕ$
	iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
Assertion	iccpartigtl	$⊢ φ \to \forall i \in (1 ..^M) P (0) < P (i)$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3		ral0	$⊢ \forall i \in \emptyset P (0) < P (i)$
4		oveq2	$⊢ M = 1 \to (1 ..^M) = (1 ..^1)$
5		fzo0	$⊢ (1 ..^1) = \emptyset$
6	4 5	eqtrdi	$⊢ M = 1 \to (1 ..^M) = \emptyset$
7	6	raleqdv	$⊢ M = 1 \to (\forall i \in (1 ..^M) P (0) < P (i) \leftrightarrow \forall i \in \emptyset P (0) < P (i))$
8	3 7	mpbiri	$⊢ M = 1 \to \forall i \in (1 ..^M) P (0) < P (i)$
9	8	a1d	$⊢ M = 1 \to (φ \to \forall i \in (1 ..^M) P (0) < P (i))$
10	1	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
11		0elfz	$⊢ M \in ℕ_{0} \to 0 \in (0 \dots M)$
12	10 11	syl	$⊢ φ \to 0 \in (0 \dots M)$
13	1 2 12	iccpartxr	$⊢ φ \to P (0) \in ℝ^{*}$
14	13	adantr	$⊢ (φ \land \neg M = 1) \to P (0) \in ℝ^{*}$
15		elxr	$⊢ P (0) \in ℝ^{*} \leftrightarrow (P (0) \in ℝ \lor P (0) = +∞ \lor P (0) = −∞)$
16		0zd	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to 0 \in ℤ$
17		elfzouz	$⊢ i \in (1 ..^M) \to i \in ℤ_{\geq 1}$
18		0p1e1	$⊢ 0 + 1 = 1$
19	18	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
20	17 19	eleqtrrdi	$⊢ i \in (1 ..^M) \to i \in ℤ_{\geq (0 + 1)}$
21	20	adantl	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to i \in ℤ_{\geq (0 + 1)}$
22		fveq2	$⊢ k = 0 \to P (k) = P (0)$
23	22	eqcomd	$⊢ k = 0 \to P (0) = P (k)$
24	23	eleq1d	$⊢ k = 0 \to (P (0) \in ℝ \leftrightarrow P (k) \in ℝ)$
25	24	biimpcd	$⊢ P (0) \in ℝ \to (k = 0 \to P (k) \in ℝ)$
26	25	ad3antrrr	$⊢ (((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \land k \in (0 \dots i)) \to (k = 0 \to P (k) \in ℝ)$
27	1	adantr	$⊢ (φ \land (i \in (1 ..^M) \land (k \in (0 \dots i) \land k \neq 0))) \to M \in ℕ$
28	2	adantr	$⊢ (φ \land (i \in (1 ..^M) \land (k \in (0 \dots i) \land k \neq 0))) \to P \in RePart (M)$
29		elfz2nn0	$⊢ k \in (0 \dots i) \leftrightarrow (k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i)$
30		elfzo2	$⊢ i \in (1 ..^M) \leftrightarrow (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M)$
31		simpl1	$⊢ ((k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i) \land (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M)) \to k \in ℕ_{0}$
32		simpr2	$⊢ ((k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i) \land (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M)) \to M \in ℤ$
33		nn0ge0	$⊢ i \in ℕ_{0} \to 0 \leq i$
34		0red	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ) \to 0 \in ℝ$
35		eluzelre	$⊢ i \in ℤ_{\geq 1} \to i \in ℝ$
36	35	adantr	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ) \to i \in ℝ$
37		zre	$⊢ M \in ℤ \to M \in ℝ$
38	37	adantl	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ) \to M \in ℝ$
39		lelttr	$⊢ (0 \in ℝ \land i \in ℝ \land M \in ℝ) \to ((0 \leq i \land i < M) \to 0 < M)$
40	34 36 38 39	syl3anc	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ) \to ((0 \leq i \land i < M) \to 0 < M)$
41	40	expcomd	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ) \to (i < M \to (0 \leq i \to 0 < M))$
42	41	3impia	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to (0 \leq i \to 0 < M)$
43	33 42	syl5com	$⊢ i \in ℕ_{0} \to ((i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to 0 < M)$
44	43	3ad2ant2	$⊢ (k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i) \to ((i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to 0 < M)$
45	44	imp	$⊢ ((k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i) \land (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M)) \to 0 < M$
46		elnnz	$⊢ M \in ℕ \leftrightarrow (M \in ℤ \land 0 < M)$
47	32 45 46	sylanbrc	$⊢ ((k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i) \land (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M)) \to M \in ℕ$
48		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
49	48	ad2antrl	$⊢ ((i \in ℤ_{\geq 1} \land M \in ℤ) \land (k \in ℕ_{0} \land i \in ℕ_{0})) \to k \in ℝ$
50		nn0re	$⊢ i \in ℕ_{0} \to i \in ℝ$
51	50	adantl	$⊢ (k \in ℕ_{0} \land i \in ℕ_{0}) \to i \in ℝ$
52	51	adantl	$⊢ ((i \in ℤ_{\geq 1} \land M \in ℤ) \land (k \in ℕ_{0} \land i \in ℕ_{0})) \to i \in ℝ$
53	38	adantr	$⊢ ((i \in ℤ_{\geq 1} \land M \in ℤ) \land (k \in ℕ_{0} \land i \in ℕ_{0})) \to M \in ℝ$
54		lelttr	$⊢ (k \in ℝ \land i \in ℝ \land M \in ℝ) \to ((k \leq i \land i < M) \to k < M)$
55	54	expd	$⊢ (k \in ℝ \land i \in ℝ \land M \in ℝ) \to (k \leq i \to (i < M \to k < M))$
56	49 52 53 55	syl3anc	$⊢ ((i \in ℤ_{\geq 1} \land M \in ℤ) \land (k \in ℕ_{0} \land i \in ℕ_{0})) \to (k \leq i \to (i < M \to k < M))$
57	56	exp31	$⊢ i \in ℤ_{\geq 1} \to (M \in ℤ \to ((k \in ℕ_{0} \land i \in ℕ_{0}) \to (k \leq i \to (i < M \to k < M))))$
58	57	com34	$⊢ i \in ℤ_{\geq 1} \to (M \in ℤ \to (k \leq i \to ((k \in ℕ_{0} \land i \in ℕ_{0}) \to (i < M \to k < M))))$
59	58	com35	$⊢ i \in ℤ_{\geq 1} \to (M \in ℤ \to (i < M \to ((k \in ℕ_{0} \land i \in ℕ_{0}) \to (k \leq i \to k < M))))$
60	59	3imp	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to ((k \in ℕ_{0} \land i \in ℕ_{0}) \to (k \leq i \to k < M))$
61	60	expdcom	$⊢ k \in ℕ_{0} \to (i \in ℕ_{0} \to ((i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to (k \leq i \to k < M)))$
62	61	com34	$⊢ k \in ℕ_{0} \to (i \in ℕ_{0} \to (k \leq i \to ((i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to k < M)))$
63	62	3imp1	$⊢ ((k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i) \land (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M)) \to k < M$
64		elfzo0	$⊢ k \in (0 ..^M) \leftrightarrow (k \in ℕ_{0} \land M \in ℕ \land k < M)$
65	31 47 63 64	syl3anbrc	$⊢ ((k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i) \land (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M)) \to k \in (0 ..^M)$
66	65	ex	$⊢ (k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i) \to ((i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to k \in (0 ..^M))$
67	30 66	biimtrid	$⊢ (k \in ℕ_{0} \land i \in ℕ_{0} \land k \leq i) \to (i \in (1 ..^M) \to k \in (0 ..^M))$
68	29 67	sylbi	$⊢ k \in (0 \dots i) \to (i \in (1 ..^M) \to k \in (0 ..^M))$
69	68	adantr	$⊢ (k \in (0 \dots i) \land k \neq 0) \to (i \in (1 ..^M) \to k \in (0 ..^M))$
70	69	impcom	$⊢ (i \in (1 ..^M) \land (k \in (0 \dots i) \land k \neq 0)) \to k \in (0 ..^M)$
71		simpr	$⊢ (k \in (0 \dots i) \land k \neq 0) \to k \neq 0$
72	71	adantl	$⊢ (i \in (1 ..^M) \land (k \in (0 \dots i) \land k \neq 0)) \to k \neq 0$
73		fzo1fzo0n0	$⊢ k \in (1 ..^M) \leftrightarrow (k \in (0 ..^M) \land k \neq 0)$
74	70 72 73	sylanbrc	$⊢ (i \in (1 ..^M) \land (k \in (0 \dots i) \land k \neq 0)) \to k \in (1 ..^M)$
75	74	adantl	$⊢ (φ \land (i \in (1 ..^M) \land (k \in (0 \dots i) \land k \neq 0))) \to k \in (1 ..^M)$
76	27 28 75	iccpartipre	$⊢ (φ \land (i \in (1 ..^M) \land (k \in (0 \dots i) \land k \neq 0))) \to P (k) \in ℝ$
77	76	exp32	$⊢ φ \to (i \in (1 ..^M) \to ((k \in (0 \dots i) \land k \neq 0) \to P (k) \in ℝ))$
78	77	ad2antrl	$⊢ (P (0) \in ℝ \land (φ \land \neg M = 1)) \to (i \in (1 ..^M) \to ((k \in (0 \dots i) \land k \neq 0) \to P (k) \in ℝ))$
79	78	imp	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to ((k \in (0 \dots i) \land k \neq 0) \to P (k) \in ℝ)$
80	79	expdimp	$⊢ (((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \land k \in (0 \dots i)) \to (k \neq 0 \to P (k) \in ℝ)$
81	26 80	pm2.61dne	$⊢ (((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \land k \in (0 \dots i)) \to P (k) \in ℝ$
82	1	adantr	$⊢ (φ \land \neg M = 1) \to M \in ℕ$
83	82	ad3antlr	$⊢ (((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \land k \in (0 \dots i - 1)) \to M \in ℕ$
84	2	adantr	$⊢ (φ \land \neg M = 1) \to P \in RePart (M)$
85	84	ad3antlr	$⊢ (((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \land k \in (0 \dots i - 1)) \to P \in RePart (M)$
86		elfzoelz	$⊢ i \in (1 ..^M) \to i \in ℤ$
87	86	adantl	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to i \in ℤ$
88		fzoval	$⊢ i \in ℤ \to (0 ..^i) = (0 \dots i - 1)$
89	88	eqcomd	$⊢ i \in ℤ \to (0 \dots i - 1) = (0 ..^i)$
90	87 89	syl	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to (0 \dots i - 1) = (0 ..^i)$
91	90	eleq2d	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to (k \in (0 \dots i - 1) \leftrightarrow k \in (0 ..^i))$
92		elfzouz2	$⊢ i \in (1 ..^M) \to M \in ℤ_{\geq i}$
93	92	adantl	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to M \in ℤ_{\geq i}$
94		fzoss2	$⊢ M \in ℤ_{\geq i} \to (0 ..^i) \subseteq (0 ..^M)$
95	93 94	syl	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to (0 ..^i) \subseteq (0 ..^M)$
96	95	sseld	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to (k \in (0 ..^i) \to k \in (0 ..^M))$
97	91 96	sylbid	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to (k \in (0 \dots i - 1) \to k \in (0 ..^M))$
98	97	imp	$⊢ (((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \land k \in (0 \dots i - 1)) \to k \in (0 ..^M)$
99		iccpartimp	$⊢ (M \in ℕ \land P \in RePart (M) \land k \in (0 ..^M)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (k) < P (k + 1))$
100	83 85 98 99	syl3anc	$⊢ (((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \land k \in (0 \dots i - 1)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (k) < P (k + 1))$
101	100	simprd	$⊢ (((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \land k \in (0 \dots i - 1)) \to P (k) < P (k + 1)$
102	16 21 81 101	smonoord	$⊢ ((P (0) \in ℝ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to P (0) < P (i)$
103	102	ralrimiva	$⊢ (P (0) \in ℝ \land (φ \land \neg M = 1)) \to \forall i \in (1 ..^M) P (0) < P (i)$
104	103	ex	$⊢ P (0) \in ℝ \to ((φ \land \neg M = 1) \to \forall i \in (1 ..^M) P (0) < P (i))$
105		lbfzo0	$⊢ 0 \in (0 ..^M) \leftrightarrow M \in ℕ$
106	1 105	sylibr	$⊢ φ \to 0 \in (0 ..^M)$
107	1 2 106	3jca	$⊢ φ \to (M \in ℕ \land P \in RePart (M) \land 0 \in (0 ..^M))$
108	107	ad2antrl	$⊢ (P (0) = +∞ \land (φ \land \neg M = 1)) \to (M \in ℕ \land P \in RePart (M) \land 0 \in (0 ..^M))$
109	108	adantr	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to (M \in ℕ \land P \in RePart (M) \land 0 \in (0 ..^M))$
110		iccpartimp	$⊢ (M \in ℕ \land P \in RePart (M) \land 0 \in (0 ..^M)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (0) < P (0 + 1))$
111	109 110	syl	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (0) < P (0 + 1))$
112	111	simprd	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to P (0) < P (0 + 1)$
113		breq1	$⊢ P (0) = +∞ \to (P (0) < P (0 + 1) \leftrightarrow +∞ < P (0 + 1))$
114	113	adantr	$⊢ (P (0) = +∞ \land (φ \land \neg M = 1)) \to (P (0) < P (0 + 1) \leftrightarrow +∞ < P (0 + 1))$
115	114	adantr	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to (P (0) < P (0 + 1) \leftrightarrow +∞ < P (0 + 1))$
116	112 115	mpbid	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to +∞ < P (0 + 1)$
117	1	ad2antrl	$⊢ (P (0) = +∞ \land (φ \land \neg M = 1)) \to M \in ℕ$
118	117	adantr	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to M \in ℕ$
119	2	ad2antrl	$⊢ (P (0) = +∞ \land (φ \land \neg M = 1)) \to P \in RePart (M)$
120	119	adantr	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to P \in RePart (M)$
121		1nn0	$⊢ 1 \in ℕ_{0}$
122	121	a1i	$⊢ M \in ℕ \to 1 \in ℕ_{0}$
123		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
124		nnge1	$⊢ M \in ℕ \to 1 \leq M$
125	122 123 124	3jca	$⊢ M \in ℕ \to (1 \in ℕ_{0} \land M \in ℕ_{0} \land 1 \leq M)$
126	1 125	syl	$⊢ φ \to (1 \in ℕ_{0} \land M \in ℕ_{0} \land 1 \leq M)$
127		elfz2nn0	$⊢ 1 \in (0 \dots M) \leftrightarrow (1 \in ℕ_{0} \land M \in ℕ_{0} \land 1 \leq M)$
128	126 127	sylibr	$⊢ φ \to 1 \in (0 \dots M)$
129	18 128	eqeltrid	$⊢ φ \to 0 + 1 \in (0 \dots M)$
130	129	ad2antrl	$⊢ (P (0) = +∞ \land (φ \land \neg M = 1)) \to 0 + 1 \in (0 \dots M)$
131	130	adantr	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to 0 + 1 \in (0 \dots M)$
132	118 120 131	iccpartxr	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to P (0 + 1) \in ℝ^{*}$
133		pnfnlt	$⊢ P (0 + 1) \in ℝ^{*} \to \neg +∞ < P (0 + 1)$
134	132 133	syl	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to \neg +∞ < P (0 + 1)$
135	116 134	pm2.21dd	$⊢ ((P (0) = +∞ \land (φ \land \neg M = 1)) \land i \in (1 ..^M)) \to P (0) < P (i)$
136	135	ralrimiva	$⊢ (P (0) = +∞ \land (φ \land \neg M = 1)) \to \forall i \in (1 ..^M) P (0) < P (i)$
137	136	ex	$⊢ P (0) = +∞ \to ((φ \land \neg M = 1) \to \forall i \in (1 ..^M) P (0) < P (i))$
138	1	adantr	$⊢ (φ \land i \in (1 ..^M)) \to M \in ℕ$
139	2	adantr	$⊢ (φ \land i \in (1 ..^M)) \to P \in RePart (M)$
140		simpr	$⊢ (φ \land i \in (1 ..^M)) \to i \in (1 ..^M)$
141	138 139 140	iccpartipre	$⊢ (φ \land i \in (1 ..^M)) \to P (i) \in ℝ$
142		mnflt	$⊢ P (i) \in ℝ \to −∞ < P (i)$
143	141 142	syl	$⊢ (φ \land i \in (1 ..^M)) \to −∞ < P (i)$
144	143	ralrimiva	$⊢ φ \to \forall i \in (1 ..^M) −∞ < P (i)$
145	144	ad2antrl	$⊢ (P (0) = −∞ \land (φ \land \neg M = 1)) \to \forall i \in (1 ..^M) −∞ < P (i)$
146		breq1	$⊢ P (0) = −∞ \to (P (0) < P (i) \leftrightarrow −∞ < P (i))$
147	146	adantr	$⊢ (P (0) = −∞ \land (φ \land \neg M = 1)) \to (P (0) < P (i) \leftrightarrow −∞ < P (i))$
148	147	ralbidv	$⊢ (P (0) = −∞ \land (φ \land \neg M = 1)) \to (\forall i \in (1 ..^M) P (0) < P (i) \leftrightarrow \forall i \in (1 ..^M) −∞ < P (i))$
149	145 148	mpbird	$⊢ (P (0) = −∞ \land (φ \land \neg M = 1)) \to \forall i \in (1 ..^M) P (0) < P (i)$
150	149	ex	$⊢ P (0) = −∞ \to ((φ \land \neg M = 1) \to \forall i \in (1 ..^M) P (0) < P (i))$
151	104 137 150	3jaoi	$⊢ (P (0) \in ℝ \lor P (0) = +∞ \lor P (0) = −∞) \to ((φ \land \neg M = 1) \to \forall i \in (1 ..^M) P (0) < P (i))$
152	15 151	sylbi	$⊢ P (0) \in ℝ^{*} \to ((φ \land \neg M = 1) \to \forall i \in (1 ..^M) P (0) < P (i))$
153	14 152	mpcom	$⊢ (φ \land \neg M = 1) \to \forall i \in (1 ..^M) P (0) < P (i)$
154	153	expcom	$⊢ \neg M = 1 \to (φ \to \forall i \in (1 ..^M) P (0) < P (i))$
155	9 154	pm2.61i	$⊢ φ \to \forall i \in (1 ..^M) P (0) < P (i)$

Metamath Proof Explorer

Theorem iccpartigtl

Proof