iccpartlt

Description: If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 in GS's mathbox. (Contributed by AV, 12-Jul-2020)

	Ref	Expression
Hypotheses	iccpartgtprec.m	$⊢ φ \to M \in ℕ$
	iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
Assertion	iccpartlt	$⊢ φ \to P (0) < P (M)$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3		lbfzo0	$⊢ 0 \in (0 ..^M) \leftrightarrow M \in ℕ$
4	1 3	sylibr	$⊢ φ \to 0 \in (0 ..^M)$
5		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))$
6	1 2 4 5	syl3anc	$⊢ φ \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (0) < P (0 + 1))$
7	6	simprd	$⊢ φ \to P (0) < P (0 + 1)$
8	7	adantl	$⊢ (M = 1 \land φ) \to P (0) < P (0 + 1)$
9		fveq2	$⊢ M = 1 \to P (M) = P (1)$
10		1e0p1	$⊢ 1 = 0 + 1$
11	10	fveq2i	$⊢ P (1) = P (0 + 1)$
12	9 11	eqtrdi	$⊢ M = 1 \to P (M) = P (0 + 1)$
13	12	adantr	$⊢ (M = 1 \land φ) \to P (M) = P (0 + 1)$
14	8 13	breqtrrd	$⊢ (M = 1 \land φ) \to P (0) < P (M)$
15	14	ex	$⊢ M = 1 \to (φ \to P (0) < P (M))$
16	1 2	iccpartiltu	$⊢ φ \to \forall i \in (1 ..^M) P (i) < P (M)$
17	1 2	iccpartigtl	$⊢ φ \to \forall i \in (1 ..^M) P (0) < P (i)$
18		1nn	$⊢ 1 \in ℕ$
19	18	a1i	$⊢ (φ \land \neg M = 1) \to 1 \in ℕ$
20	1	adantr	$⊢ (φ \land \neg M = 1) \to M \in ℕ$
21		df-ne	$⊢ M \neq 1 \leftrightarrow \neg M = 1$
22	1	nnge1d	$⊢ φ \to 1 \leq M$
23		1red	$⊢ φ \to 1 \in ℝ$
24	1	nnred	$⊢ φ \to M \in ℝ$
25	23 24	ltlend	$⊢ φ \to (1 < M \leftrightarrow (1 \leq M \land M \neq 1))$
26	25	biimprd	$⊢ φ \to ((1 \leq M \land M \neq 1) \to 1 < M)$
27	22 26	mpand	$⊢ φ \to (M \neq 1 \to 1 < M)$
28	21 27	biimtrrid	$⊢ φ \to (\neg M = 1 \to 1 < M)$
29	28	imp	$⊢ (φ \land \neg M = 1) \to 1 < M$
30		elfzo1	$⊢ 1 \in (1 ..^M) \leftrightarrow (1 \in ℕ \land M \in ℕ \land 1 < M)$
31	19 20 29 30	syl3anbrc	$⊢ (φ \land \neg M = 1) \to 1 \in (1 ..^M)$
32		fveq2	$⊢ i = 1 \to P (i) = P (1)$
33	32	breq2d	$⊢ i = 1 \to (P (0) < P (i) \leftrightarrow P (0) < P (1))$
34	33	rspcv	$⊢ 1 \in (1 ..^M) \to (\forall i \in (1 ..^M) P (0) < P (i) \to P (0) < P (1))$
35	31 34	syl	$⊢ (φ \land \neg M = 1) \to (\forall i \in (1 ..^M) P (0) < P (i) \to P (0) < P (1))$
36	32	breq1d	$⊢ i = 1 \to (P (i) < P (M) \leftrightarrow P (1) < P (M))$
37	36	rspcv	$⊢ 1 \in (1 ..^M) \to (\forall i \in (1 ..^M) P (i) < P (M) \to P (1) < P (M))$
38	31 37	syl	$⊢ (φ \land \neg M = 1) \to (\forall i \in (1 ..^M) P (i) < P (M) \to P (1) < P (M))$
39		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
40		0elfz	$⊢ M \in ℕ_{0} \to 0 \in (0 \dots M)$
41	1 39 40	3syl	$⊢ φ \to 0 \in (0 \dots M)$
42	1 2 41	iccpartxr	$⊢ φ \to P (0) \in ℝ^{*}$
43	42	adantr	$⊢ (φ \land \neg M = 1) \to P (0) \in ℝ^{*}$
44	2	adantr	$⊢ (φ \land \neg M = 1) \to P \in RePart (M)$
45		1nn0	$⊢ 1 \in ℕ_{0}$
46	45	a1i	$⊢ (φ \land \neg M = 1) \to 1 \in ℕ_{0}$
47	1 39	syl	$⊢ φ \to M \in ℕ_{0}$
48	47	adantr	$⊢ (φ \land \neg M = 1) \to M \in ℕ_{0}$
49	22	adantr	$⊢ (φ \land \neg M = 1) \to 1 \leq M$
50		elfz2nn0	$⊢ 1 \in (0 \dots M) \leftrightarrow (1 \in ℕ_{0} \land M \in ℕ_{0} \land 1 \leq M)$
51	46 48 49 50	syl3anbrc	$⊢ (φ \land \neg M = 1) \to 1 \in (0 \dots M)$
52	20 44 51	iccpartxr	$⊢ (φ \land \neg M = 1) \to P (1) \in ℝ^{*}$
53		nn0fz0	$⊢ M \in ℕ_{0} \leftrightarrow M \in (0 \dots M)$
54	39 53	sylib	$⊢ M \in ℕ \to M \in (0 \dots M)$
55	1 54	syl	$⊢ φ \to M \in (0 \dots M)$
56	1 2 55	iccpartxr	$⊢ φ \to P (M) \in ℝ^{*}$
57	56	adantr	$⊢ (φ \land \neg M = 1) \to P (M) \in ℝ^{*}$
58		xrlttr	$⊢ (P (0) \in ℝ^{} \land P (1) \in ℝ^{} \land P (M) \in ℝ^{*}) \to ((P (0) < P (1) \land P (1) < P (M)) \to P (0) < P (M))$
59	43 52 57 58	syl3anc	$⊢ (φ \land \neg M = 1) \to ((P (0) < P (1) \land P (1) < P (M)) \to P (0) < P (M))$
60	59	expcomd	$⊢ (φ \land \neg M = 1) \to (P (1) < P (M) \to (P (0) < P (1) \to P (0) < P (M)))$
61	38 60	syld	$⊢ (φ \land \neg M = 1) \to (\forall i \in (1 ..^M) P (i) < P (M) \to (P (0) < P (1) \to P (0) < P (M)))$
62	61	com23	$⊢ (φ \land \neg M = 1) \to (P (0) < P (1) \to (\forall i \in (1 ..^M) P (i) < P (M) \to P (0) < P (M)))$
63	35 62	syld	$⊢ (φ \land \neg M = 1) \to (\forall i \in (1 ..^M) P (0) < P (i) \to (\forall i \in (1 ..^M) P (i) < P (M) \to P (0) < P (M)))$
64	63	ex	$⊢ φ \to (\neg M = 1 \to (\forall i \in (1 ..^M) P (0) < P (i) \to (\forall i \in (1 ..^M) P (i) < P (M) \to P (0) < P (M))))$
65	64	com24	$⊢ φ \to (\forall i \in (1 ..^M) P (i) < P (M) \to (\forall i \in (1 ..^M) P (0) < P (i) \to (\neg M = 1 \to P (0) < P (M))))$
66	16 17 65	mp2d	$⊢ φ \to (\neg M = 1 \to P (0) < P (M))$
67	66	com12	$⊢ \neg M = 1 \to (φ \to P (0) < P (M))$
68	15 67	pm2.61i	$⊢ φ \to P (0) < P (M)$

Metamath Proof Explorer

Theorem iccpartlt

Proof