icceuelpartlem

	Ref	Expression
Hypotheses	iccpartiun.m	$⊢ φ \to M \in ℕ$
	iccpartiun.p	$⊢ φ \to P \in RePart (M)$
Assertion	icceuelpartlem	$⊢ φ \to ((I \in (0 ..^M) \land J \in (0 ..^M)) \to (I < J \to P (I + 1) \leq P (J)))$

Proof

Step	Hyp	Ref	Expression
1		iccpartiun.m	$⊢ φ \to M \in ℕ$
2		iccpartiun.p	$⊢ φ \to P \in RePart (M)$
3		fveq2	$⊢ I + 1 = J \to P (I + 1) = P (J)$
4	3	olcd	$⊢ I + 1 = J \to (P (I + 1) < P (J) \lor P (I + 1) = P (J))$
5	4	a1d	$⊢ I + 1 = J \to (((φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \land I < J) \to (P (I + 1) < P (J) \lor P (I + 1) = P (J)))$
6		elfzoelz	$⊢ I \in (0 ..^M) \to I \in ℤ$
7		elfzoelz	$⊢ J \in (0 ..^M) \to J \in ℤ$
8		zltp1le	$⊢ (I \in ℤ \land J \in ℤ) \to (I < J \leftrightarrow I + 1 \leq J)$
9	8	biimpcd	$⊢ I < J \to ((I \in ℤ \land J \in ℤ) \to I + 1 \leq J)$
10	9	adantr	$⊢ (I < J \land \neg I + 1 = J) \to ((I \in ℤ \land J \in ℤ) \to I + 1 \leq J)$
11	10	impcom	$⊢ ((I \in ℤ \land J \in ℤ) \land (I < J \land \neg I + 1 = J)) \to I + 1 \leq J$
12		df-ne	$⊢ I + 1 \neq J \leftrightarrow \neg I + 1 = J$
13		necom	$⊢ I + 1 \neq J \leftrightarrow J \neq I + 1$
14	12 13	sylbb1	$⊢ \neg I + 1 = J \to J \neq I + 1$
15	14	adantl	$⊢ (I < J \land \neg I + 1 = J) \to J \neq I + 1$
16	15	adantl	$⊢ ((I \in ℤ \land J \in ℤ) \land (I < J \land \neg I + 1 = J)) \to J \neq I + 1$
17	11 16	jca	$⊢ ((I \in ℤ \land J \in ℤ) \land (I < J \land \neg I + 1 = J)) \to (I + 1 \leq J \land J \neq I + 1)$
18		peano2z	$⊢ I \in ℤ \to I + 1 \in ℤ$
19	18	zred	$⊢ I \in ℤ \to I + 1 \in ℝ$
20		zre	$⊢ J \in ℤ \to J \in ℝ$
21	19 20	anim12i	$⊢ (I \in ℤ \land J \in ℤ) \to (I + 1 \in ℝ \land J \in ℝ)$
22	21	adantr	$⊢ ((I \in ℤ \land J \in ℤ) \land (I < J \land \neg I + 1 = J)) \to (I + 1 \in ℝ \land J \in ℝ)$
23		ltlen	$⊢ (I + 1 \in ℝ \land J \in ℝ) \to (I + 1 < J \leftrightarrow (I + 1 \leq J \land J \neq I + 1))$
24	22 23	syl	$⊢ ((I \in ℤ \land J \in ℤ) \land (I < J \land \neg I + 1 = J)) \to (I + 1 < J \leftrightarrow (I + 1 \leq J \land J \neq I + 1))$
25	17 24	mpbird	$⊢ ((I \in ℤ \land J \in ℤ) \land (I < J \land \neg I + 1 = J)) \to I + 1 < J$
26	25	ex	$⊢ (I \in ℤ \land J \in ℤ) \to ((I < J \land \neg I + 1 = J) \to I + 1 < J)$
27	6 7 26	syl2an	$⊢ (I \in (0 ..^M) \land J \in (0 ..^M)) \to ((I < J \land \neg I + 1 = J) \to I + 1 < J)$
28	27	adantl	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to ((I < J \land \neg I + 1 = J) \to I + 1 < J)$
29	1 2	iccpartgt	$⊢ φ \to \forall i \in (0 \dots M) \forall j \in (0 \dots M) (i < j \to P (i) < P (j))$
30		fzofzp1	$⊢ I \in (0 ..^M) \to I + 1 \in (0 \dots M)$
31		elfzofz	$⊢ J \in (0 ..^M) \to J \in (0 \dots M)$
32		breq1	$⊢ i = I + 1 \to (i < j \leftrightarrow I + 1 < j)$
33		fveq2	$⊢ i = I + 1 \to P (i) = P (I + 1)$
34	33	breq1d	$⊢ i = I + 1 \to (P (i) < P (j) \leftrightarrow P (I + 1) < P (j))$
35	32 34	imbi12d	$⊢ i = I + 1 \to ((i < j \to P (i) < P (j)) \leftrightarrow (I + 1 < j \to P (I + 1) < P (j)))$
36		breq2	$⊢ j = J \to (I + 1 < j \leftrightarrow I + 1 < J)$
37		fveq2	$⊢ j = J \to P (j) = P (J)$
38	37	breq2d	$⊢ j = J \to (P (I + 1) < P (j) \leftrightarrow P (I + 1) < P (J))$
39	36 38	imbi12d	$⊢ j = J \to ((I + 1 < j \to P (I + 1) < P (j)) \leftrightarrow (I + 1 < J \to P (I + 1) < P (J)))$
40	35 39	rspc2v	$⊢ (I + 1 \in (0 \dots M) \land J \in (0 \dots M)) \to (\forall i \in (0 \dots M) \forall j \in (0 \dots M) (i < j \to P (i) < P (j)) \to (I + 1 < J \to P (I + 1) < P (J)))$
41	30 31 40	syl2an	$⊢ (I \in (0 ..^M) \land J \in (0 ..^M)) \to (\forall i \in (0 \dots M) \forall j \in (0 \dots M) (i < j \to P (i) < P (j)) \to (I + 1 < J \to P (I + 1) < P (J)))$
42	29 41	mpan9	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to (I + 1 < J \to P (I + 1) < P (J))$
43	28 42	syld	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to ((I < J \land \neg I + 1 = J) \to P (I + 1) < P (J))$
44	43	expdimp	$⊢ ((φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \land I < J) \to (\neg I + 1 = J \to P (I + 1) < P (J))$
45	44	impcom	$⊢ (\neg I + 1 = J \land ((φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \land I < J)) \to P (I + 1) < P (J)$
46	45	orcd	$⊢ (\neg I + 1 = J \land ((φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \land I < J)) \to (P (I + 1) < P (J) \lor P (I + 1) = P (J))$
47	46	ex	$⊢ \neg I + 1 = J \to (((φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \land I < J) \to (P (I + 1) < P (J) \lor P (I + 1) = P (J)))$
48	5 47	pm2.61i	$⊢ ((φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \land I < J) \to (P (I + 1) < P (J) \lor P (I + 1) = P (J))$
49	1	adantr	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to M \in ℕ$
50	2	adantr	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to P \in RePart (M)$
51	30	adantr	$⊢ (I \in (0 ..^M) \land J \in (0 ..^M)) \to I + 1 \in (0 \dots M)$
52	51	adantl	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to I + 1 \in (0 \dots M)$
53	49 50 52	iccpartxr	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to P (I + 1) \in ℝ^{*}$
54	31	adantl	$⊢ (I \in (0 ..^M) \land J \in (0 ..^M)) \to J \in (0 \dots M)$
55	54	adantl	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to J \in (0 \dots M)$
56	49 50 55	iccpartxr	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to P (J) \in ℝ^{*}$
57	53 56	jca	$⊢ (φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \to (P (I + 1) \in ℝ^{} \land P (J) \in ℝ^{})$
58	57	adantr	$⊢ ((φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \land I < J) \to (P (I + 1) \in ℝ^{} \land P (J) \in ℝ^{})$
59		xrleloe	$⊢ (P (I + 1) \in ℝ^{} \land P (J) \in ℝ^{}) \to (P (I + 1) \leq P (J) \leftrightarrow (P (I + 1) < P (J) \lor P (I + 1) = P (J)))$
60	58 59	syl	$⊢ ((φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \land I < J) \to (P (I + 1) \leq P (J) \leftrightarrow (P (I + 1) < P (J) \lor P (I + 1) = P (J)))$
61	48 60	mpbird	$⊢ ((φ \land (I \in (0 ..^M) \land J \in (0 ..^M))) \land I < J) \to P (I + 1) \leq P (J)$
62	61	exp31	$⊢ φ \to ((I \in (0 ..^M) \land J \in (0 ..^M)) \to (I < J \to P (I + 1) \leq P (J)))$

Metamath Proof Explorer

Theorem icceuelpartlem

Proof