iccpartnel

Description: A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 8-Jul-2020)

	Ref	Expression
Hypotheses	iccpartnel.m	$⊢ φ \to M \in ℕ$
	iccpartnel.p	$⊢ φ \to P \in RePart (M)$
	iccpartnel.x	$⊢ φ \to X \in ran P$
Assertion	iccpartnel	$⊢ (φ \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1))$

Proof

Step	Hyp	Ref	Expression
1		iccpartnel.m	$⊢ φ \to M \in ℕ$
2		iccpartnel.p	$⊢ φ \to P \in RePart (M)$
3		iccpartnel.x	$⊢ φ \to X \in ran P$
4		elioo3g	$⊢ X \in (P (I), P (I + 1)) \leftrightarrow ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1)))$
5		iccpart	$⊢ M \in ℕ \to (P \in RePart (M) \leftrightarrow (P \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)))$
6	1 5	syl	$⊢ φ \to (P \in RePart (M) \leftrightarrow (P \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)))$
7		elmapfn	$⊢ P \in ({ℝ^{*}}^{(0 \dots M)}) \to P Fn (0 \dots M)$
8	7	adantr	$⊢ (P \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)) \to P Fn (0 \dots M)$
9	6 8	syl6bi	$⊢ φ \to (P \in RePart (M) \to P Fn (0 \dots M))$
10	2 9	mpd	$⊢ φ \to P Fn (0 \dots M)$
11		fvelrnb	$⊢ P Fn (0 \dots M) \to (X \in ran P \leftrightarrow \exists x \in (0 \dots M) P (x) = X)$
12	10 11	syl	$⊢ φ \to (X \in ran P \leftrightarrow \exists x \in (0 \dots M) P (x) = X)$
13	3 12	mpbid	$⊢ φ \to \exists x \in (0 \dots M) P (x) = X$
14		elfzelz	$⊢ x \in (0 \dots M) \to x \in ℤ$
15	14	zred	$⊢ x \in (0 \dots M) \to x \in ℝ$
16	15	adantl	$⊢ (φ \land x \in (0 \dots M)) \to x \in ℝ$
17		elfzoelz	$⊢ I \in (0 ..^M) \to I \in ℤ$
18	17	zred	$⊢ I \in (0 ..^M) \to I \in ℝ$
19		lelttric	$⊢ (x \in ℝ \land I \in ℝ) \to (x \leq I \lor I < x)$
20	16 18 19	syl2an	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (x \leq I \lor I < x)$
21		breq2	$⊢ P (x) = X \to (P (I) < P (x) \leftrightarrow P (I) < X)$
22		breq1	$⊢ P (x) = X \to (P (x) < P (I + 1) \leftrightarrow X < P (I + 1))$
23	21 22	anbi12d	$⊢ P (x) = X \to ((P (I) < P (x) \land P (x) < P (I + 1)) \leftrightarrow (P (I) < X \land X < P (I + 1)))$
24		leloe	$⊢ (x \in ℝ \land I \in ℝ) \to (x \leq I \leftrightarrow (x < I \lor x = I))$
25	16 18 24	syl2an	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (x \leq I \leftrightarrow (x < I \lor x = I))$
26	1 2	iccpartgt	$⊢ φ \to \forall i \in (0 \dots M) \forall k \in (0 \dots M) (i < k \to P (i) < P (k))$
27	26	adantr	$⊢ (φ \land x \in (0 \dots M)) \to \forall i \in (0 \dots M) \forall k \in (0 \dots M) (i < k \to P (i) < P (k))$
28	27	adantr	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \forall i \in (0 \dots M) \forall k \in (0 \dots M) (i < k \to P (i) < P (k))$
29		simpr	$⊢ (φ \land x \in (0 \dots M)) \to x \in (0 \dots M)$
30		elfzofz	$⊢ I \in (0 ..^M) \to I \in (0 \dots M)$
31		breq1	$⊢ i = x \to (i < k \leftrightarrow x < k)$
32		fveq2	$⊢ i = x \to P (i) = P (x)$
33	32	breq1d	$⊢ i = x \to (P (i) < P (k) \leftrightarrow P (x) < P (k))$
34	31 33	imbi12d	$⊢ i = x \to ((i < k \to P (i) < P (k)) \leftrightarrow (x < k \to P (x) < P (k)))$
35		breq2	$⊢ k = I \to (x < k \leftrightarrow x < I)$
36		fveq2	$⊢ k = I \to P (k) = P (I)$
37	36	breq2d	$⊢ k = I \to (P (x) < P (k) \leftrightarrow P (x) < P (I))$
38	35 37	imbi12d	$⊢ k = I \to ((x < k \to P (x) < P (k)) \leftrightarrow (x < I \to P (x) < P (I)))$
39	34 38	rspc2v	$⊢ (x \in (0 \dots M) \land I \in (0 \dots M)) \to (\forall i \in (0 \dots M) \forall k \in (0 \dots M) (i < k \to P (i) < P (k)) \to (x < I \to P (x) < P (I)))$
40	29 30 39	syl2an	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (\forall i \in (0 \dots M) \forall k \in (0 \dots M) (i < k \to P (i) < P (k)) \to (x < I \to P (x) < P (I)))$
41	28 40	mpd	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (x < I \to P (x) < P (I))$
42		pm3.35	$⊢ (x < I \land (x < I \to P (x) < P (I))) \to P (x) < P (I)$
43	1	adantr	$⊢ (φ \land x \in (0 \dots M)) \to M \in ℕ$
44	2	adantr	$⊢ (φ \land x \in (0 \dots M)) \to P \in RePart (M)$
45	43 44 29	iccpartxr	$⊢ (φ \land x \in (0 \dots M)) \to P (x) \in ℝ^{*}$
46	45	adantr	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to P (x) \in ℝ^{*}$
47		simp1	$⊢ (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{}) \to P (I) \in ℝ^{}$
48		xrltle	$⊢ (P (x) \in ℝ^{} \land P (I) \in ℝ^{}) \to (P (x) < P (I) \to P (x) \leq P (I))$
49	46 47 48	syl2anr	$⊢ ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M))) \to (P (x) < P (I) \to P (x) \leq P (I))$
50		xrlenlt	$⊢ (P (x) \in ℝ^{} \land P (I) \in ℝ^{}) \to (P (x) \leq P (I) \leftrightarrow \neg P (I) < P (x))$
51	46 47 50	syl2anr	$⊢ ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M))) \to (P (x) \leq P (I) \leftrightarrow \neg P (I) < P (x))$
52	49 51	sylibd	$⊢ ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M))) \to (P (x) < P (I) \to \neg P (I) < P (x))$
53	52	ex	$⊢ (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (P (x) < P (I) \to \neg P (I) < P (x)))$
54	53	com13	$⊢ P (x) < P (I) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to \neg P (I) < P (x)))$
55	54	imp	$⊢ (P (x) < P (I) \land ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M))) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to \neg P (I) < P (x))$
56	55	imp	$⊢ ((P (x) < P (I) \land ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M))) \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \to \neg P (I) < P (x)$
57	56	pm2.21d	$⊢ ((P (x) < P (I) \land ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M))) \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))$
58	57	ex	$⊢ (P (x) < P (I) \land ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M))) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1))))$
59	58	ex	$⊢ P (x) < P (I) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
60	42 59	syl	$⊢ (x < I \land (x < I \to P (x) < P (I))) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
61	60	ex	$⊢ x < I \to ((x < I \to P (x) < P (I)) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1))))))$
62	61	com13	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((x < I \to P (x) < P (I)) \to (x < I \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1))))))$
63	41 62	mpd	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (x < I \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
64	63	com12	$⊢ x < I \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
65		fveq2	$⊢ x = I \to P (x) = P (I)$
66	65	breq2d	$⊢ x = I \to (P (I) < P (x) \leftrightarrow P (I) < P (I))$
67	66	adantr	$⊢ (x = I \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \to (P (I) < P (x) \leftrightarrow P (I) < P (I))$
68		xrltnr	$⊢ P (I) \in ℝ^{*} \to \neg P (I) < P (I)$
69	68	3ad2ant1	$⊢ (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to \neg P (I) < P (I)$
70	69	adantl	$⊢ (x = I \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \to \neg P (I) < P (I)$
71	70	pm2.21d	$⊢ (x = I \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \to (P (I) < P (I) \to \neg X \in (P (I), P (I + 1)))$
72	67 71	sylbid	$⊢ (x = I \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))$
73	72	ex	$⊢ x = I \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1))))$
74	73	a1d	$⊢ x = I \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
75	64 74	jaoi	$⊢ (x < I \lor x = I) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
76	75	com12	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((x < I \lor x = I) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
77	25 76	sylbid	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (x \leq I \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
78	77	com23	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (x \leq I \to (P (I) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
79	78	com14	$⊢ P (I) < P (x) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (x \leq I \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1)))))$
80	79	adantr	$⊢ (P (I) < P (x) \land P (x) < P (I + 1)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (x \leq I \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1)))))$
81	23 80	syl6bir	$⊢ P (x) = X \to ((P (I) < X \land X < P (I + 1)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (x \leq I \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1))))))$
82	81	com14	$⊢ x \leq I \to ((P (I) < X \land X < P (I + 1)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (x) = X \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1))))))$
83	82	com23	$⊢ x \leq I \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < X \land X < P (I + 1)) \to (P (x) = X \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1))))))$
84	83	impd	$⊢ x \leq I \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to (P (x) = X \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1)))))$
85	84	com24	$⊢ x \leq I \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (P (x) = X \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1)))))$
86	14	adantl	$⊢ (φ \land x \in (0 \dots M)) \to x \in ℤ$
87		zltp1le	$⊢ (I \in ℤ \land x \in ℤ) \to (I < x \leftrightarrow I + 1 \leq x)$
88	17 86 87	syl2anr	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (I < x \leftrightarrow I + 1 \leq x)$
89	17	peano2zd	$⊢ I \in (0 ..^M) \to I + 1 \in ℤ$
90	89	zred	$⊢ I \in (0 ..^M) \to I + 1 \in ℝ$
91		leloe	$⊢ (I + 1 \in ℝ \land x \in ℝ) \to (I + 1 \leq x \leftrightarrow (I + 1 < x \lor I + 1 = x))$
92	90 16 91	syl2anr	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (I + 1 \leq x \leftrightarrow (I + 1 < x \lor I + 1 = x))$
93	88 92	bitrd	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (I < x \leftrightarrow (I + 1 < x \lor I + 1 = x))$
94		fzofzp1	$⊢ I \in (0 ..^M) \to I + 1 \in (0 \dots M)$
95		breq1	$⊢ i = I + 1 \to (i < k \leftrightarrow I + 1 < k)$
96		fveq2	$⊢ i = I + 1 \to P (i) = P (I + 1)$
97	96	breq1d	$⊢ i = I + 1 \to (P (i) < P (k) \leftrightarrow P (I + 1) < P (k))$
98	95 97	imbi12d	$⊢ i = I + 1 \to ((i < k \to P (i) < P (k)) \leftrightarrow (I + 1 < k \to P (I + 1) < P (k)))$
99		breq2	$⊢ k = x \to (I + 1 < k \leftrightarrow I + 1 < x)$
100		fveq2	$⊢ k = x \to P (k) = P (x)$
101	100	breq2d	$⊢ k = x \to (P (I + 1) < P (k) \leftrightarrow P (I + 1) < P (x))$
102	99 101	imbi12d	$⊢ k = x \to ((I + 1 < k \to P (I + 1) < P (k)) \leftrightarrow (I + 1 < x \to P (I + 1) < P (x)))$
103	98 102	rspc2v	$⊢ (I + 1 \in (0 \dots M) \land x \in (0 \dots M)) \to (\forall i \in (0 \dots M) \forall k \in (0 \dots M) (i < k \to P (i) < P (k)) \to (I + 1 < x \to P (I + 1) < P (x)))$
104	94 29 103	syl2anr	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (\forall i \in (0 \dots M) \forall k \in (0 \dots M) (i < k \to P (i) < P (k)) \to (I + 1 < x \to P (I + 1) < P (x)))$
105	28 104	mpd	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (I + 1 < x \to P (I + 1) < P (x))$
106		pm3.35	$⊢ (I + 1 < x \land (I + 1 < x \to P (I + 1) < P (x))) \to P (I + 1) < P (x)$
107		simp2	$⊢ (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{}) \to P (I + 1) \in ℝ^{}$
108		xrltnsym	$⊢ (P (x) \in ℝ^{} \land P (I + 1) \in ℝ^{}) \to (P (x) < P (I + 1) \to \neg P (I + 1) < P (x))$
109	46 107 108	syl2an	$⊢ (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \to (P (x) < P (I + 1) \to \neg P (I + 1) < P (x))$
110	109	imp	$⊢ ((((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \land P (x) < P (I + 1)) \to \neg P (I + 1) < P (x)$
111	110	pm2.21d	$⊢ ((((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \land P (x) < P (I + 1)) \to (P (I + 1) < P (x) \to \neg X \in (P (I), P (I + 1)))$
112	111	expcom	$⊢ P (x) < P (I + 1) \to ((((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \land (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*})) \to (P (I + 1) < P (x) \to \neg X \in (P (I), P (I + 1))))$
113	112	expd	$⊢ P (x) < P (I + 1) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I + 1) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
114	113	adantl	$⊢ (P (I) < P (x) \land P (x) < P (I + 1)) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I + 1) < P (x) \to \neg X \in (P (I), P (I + 1)))))$
115	114	com14	$⊢ P (I + 1) < P (x) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1)))))$
116	106 115	syl	$⊢ (I + 1 < x \land (I + 1 < x \to P (I + 1) < P (x))) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1)))))$
117	116	ex	$⊢ I + 1 < x \to ((I + 1 < x \to P (I + 1) < P (x)) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1))))))$
118	117	com13	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((I + 1 < x \to P (I + 1) < P (x)) \to (I + 1 < x \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1))))))$
119	105 118	mpd	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (I + 1 < x \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1)))))$
120	119	com12	$⊢ I + 1 < x \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1)))))$
121		fveq2	$⊢ I + 1 = x \to P (I + 1) = P (x)$
122	121	breq2d	$⊢ I + 1 = x \to (P (I) < P (I + 1) \leftrightarrow P (I) < P (x))$
123	121	breq1d	$⊢ I + 1 = x \to (P (I + 1) < P (I + 1) \leftrightarrow P (x) < P (I + 1))$
124	122 123	anbi12d	$⊢ I + 1 = x \to ((P (I) < P (I + 1) \land P (I + 1) < P (I + 1)) \leftrightarrow (P (I) < P (x) \land P (x) < P (I + 1)))$
125		xrltnr	$⊢ P (I + 1) \in ℝ^{*} \to \neg P (I + 1) < P (I + 1)$
126	125	3ad2ant2	$⊢ (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to \neg P (I + 1) < P (I + 1)$
127	126	pm2.21d	$⊢ (P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (I + 1) < P (I + 1) \to \neg X \in (P (I), P (I + 1)))$
128	127	com12	$⊢ P (I + 1) < P (I + 1) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to \neg X \in (P (I), P (I + 1)))$
129	128	adantl	$⊢ (P (I) < P (I + 1) \land P (I + 1) < P (I + 1)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to \neg X \in (P (I), P (I + 1)))$
130	124 129	syl6bir	$⊢ I + 1 = x \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to \neg X \in (P (I), P (I + 1))))$
131	130	com23	$⊢ I + 1 = x \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1))))$
132	131	a1d	$⊢ I + 1 = x \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1)))))$
133	120 132	jaoi	$⊢ (I + 1 < x \lor I + 1 = x) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1)))))$
134	133	com12	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((I + 1 < x \lor I + 1 = x) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1)))))$
135	93 134	sylbid	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (I < x \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1)))))$
136	135	com23	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (I < x \to ((P (I) < P (x) \land P (x) < P (I + 1)) \to \neg X \in (P (I), P (I + 1)))))$
137	136	com14	$⊢ (P (I) < P (x) \land P (x) < P (I + 1)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (I < x \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1)))))$
138	23 137	syl6bir	$⊢ P (x) = X \to ((P (I) < X \land X < P (I + 1)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (I < x \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1))))))$
139	138	com14	$⊢ I < x \to ((P (I) < X \land X < P (I + 1)) \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (P (x) = X \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1))))))$
140	139	com23	$⊢ I < x \to ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to ((P (I) < X \land X < P (I + 1)) \to (P (x) = X \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1))))))$
141	140	impd	$⊢ I < x \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to (P (x) = X \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1)))))$
142	141	com24	$⊢ I < x \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (P (x) = X \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1)))))$
143	85 142	jaoi	$⊢ (x \leq I \lor I < x) \to (((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (P (x) = X \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1)))))$
144	143	com12	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to ((x \leq I \lor I < x) \to (P (x) = X \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1)))))$
145	20 144	mpd	$⊢ ((φ \land x \in (0 \dots M)) \land I \in (0 ..^M)) \to (P (x) = X \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1))))$
146	145	ex	$⊢ (φ \land x \in (0 \dots M)) \to (I \in (0 ..^M) \to (P (x) = X \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1)))))$
147	146	com23	$⊢ (φ \land x \in (0 \dots M)) \to (P (x) = X \to (I \in (0 ..^M) \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1)))))$
148	147	rexlimdva	$⊢ φ \to (\exists x \in (0 \dots M) P (x) = X \to (I \in (0 ..^M) \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1)))))$
149	13 148	mpd	$⊢ φ \to (I \in (0 ..^M) \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1))))$
150	149	imp	$⊢ (φ \land I \in (0 ..^M)) \to (((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to \neg X \in (P (I), P (I + 1)))$
151	150	com12	$⊢ ((P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (P (I) < X \land X < P (I + 1))) \to ((φ \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1)))$
152	4 151	sylbi	$⊢ X \in (P (I), P (I + 1)) \to ((φ \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1)))$
153		ax-1	$⊢ \neg X \in (P (I), P (I + 1)) \to ((φ \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1)))$
154	152 153	pm2.61i	$⊢ (φ \land I \in (0 ..^M)) \to \neg X \in (P (I), P (I + 1))$

Metamath Proof Explorer

Theorem iccpartnel

Proof