iccpartiltu

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

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

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 (i) < P (1)$
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		fveq2	$⊢ M = 1 \to P (M) = P (1)$
8	7	breq2d	$⊢ M = 1 \to (P (i) < P (M) \leftrightarrow P (i) < P (1))$
9	6 8	raleqbidv	$⊢ M = 1 \to (\forall i \in (1 ..^M) P (i) < P (M) \leftrightarrow \forall i \in \emptyset P (i) < P (1))$
10	3 9	mpbiri	$⊢ M = 1 \to \forall i \in (1 ..^M) P (i) < P (M)$
11	10	2a1d	$⊢ M = 1 \to (φ \to (M \in ℕ \to \forall i \in (1 ..^M) P (i) < P (M)))$
12		simpr	$⊢ ((φ \land \neg M = 1) \land M \in ℕ) \to M \in ℕ$
13	2	adantr	$⊢ (φ \land \neg M = 1) \to P \in RePart (M)$
14	13	adantr	$⊢ ((φ \land \neg M = 1) \land M \in ℕ) \to P \in RePart (M)$
15		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
16		nn0fz0	$⊢ M \in ℕ_{0} \leftrightarrow M \in (0 \dots M)$
17	15 16	sylib	$⊢ M \in ℕ \to M \in (0 \dots M)$
18	17	adantl	$⊢ ((φ \land \neg M = 1) \land M \in ℕ) \to M \in (0 \dots M)$
19	12 14 18	iccpartxr	$⊢ ((φ \land \neg M = 1) \land M \in ℕ) \to P (M) \in ℝ^{*}$
20		elxr	$⊢ P (M) \in ℝ^{*} \leftrightarrow (P (M) \in ℝ \lor P (M) = +∞ \lor P (M) = −∞)$
21		elfzoelz	$⊢ i \in (1 ..^M) \to i \in ℤ$
22	21	ad2antll	$⊢ (P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to i \in ℤ$
23		elfzo2	$⊢ i \in (1 ..^M) \leftrightarrow (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M)$
24		eluzelz	$⊢ i \in ℤ_{\geq 1} \to i \in ℤ$
25	24	peano2zd	$⊢ i \in ℤ_{\geq 1} \to i + 1 \in ℤ$
26	25	3ad2ant1	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to i + 1 \in ℤ$
27		simp2	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to M \in ℤ$
28		zltp1le	$⊢ (i \in ℤ \land M \in ℤ) \to (i < M \leftrightarrow i + 1 \leq M)$
29	24 28	sylan	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ) \to (i < M \leftrightarrow i + 1 \leq M)$
30	29	biimp3a	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to i + 1 \leq M$
31		eluz2	$⊢ M \in ℤ_{\geq (i + 1)} \leftrightarrow (i + 1 \in ℤ \land M \in ℤ \land i + 1 \leq M)$
32	26 27 30 31	syl3anbrc	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to M \in ℤ_{\geq (i + 1)}$
33	23 32	sylbi	$⊢ i \in (1 ..^M) \to M \in ℤ_{\geq (i + 1)}$
34	33	ad2antll	$⊢ (P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to M \in ℤ_{\geq (i + 1)}$
35		fveq2	$⊢ k = M \to P (k) = P (M)$
36	35	eqcomd	$⊢ k = M \to P (M) = P (k)$
37	36	eleq1d	$⊢ k = M \to (P (M) \in ℝ \leftrightarrow P (k) \in ℝ)$
38	37	biimpcd	$⊢ P (M) \in ℝ \to (k = M \to P (k) \in ℝ)$
39	38	adantr	$⊢ (P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to (k = M \to P (k) \in ℝ)$
40	39	adantr	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M)) \to (k = M \to P (k) \in ℝ)$
41	40	com12	$⊢ k = M \to (((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M)) \to P (k) \in ℝ)$
42	12	adantr	$⊢ (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to M \in ℕ$
43	42	adantl	$⊢ (P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to M \in ℕ$
44	43	adantr	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M)) \to M \in ℕ$
45	44	adantl	$⊢ (\neg k = M \land ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M))) \to M \in ℕ$
46	14	adantr	$⊢ (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to P \in RePart (M)$
47	46	adantl	$⊢ (P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to P \in RePart (M)$
48	47	adantr	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M)) \to P \in RePart (M)$
49	48	adantl	$⊢ (\neg k = M \land ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M))) \to P \in RePart (M)$
50		elfz2	$⊢ k \in (i \dots M) \leftrightarrow ((i \in ℤ \land M \in ℤ \land k \in ℤ) \land (i \leq k \land k \leq M))$
51		eluz2	$⊢ i \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land i \in ℤ \land 1 \leq i)$
52		1red	$⊢ (i \in ℤ \land k \in ℤ) \to 1 \in ℝ$
53		zre	$⊢ i \in ℤ \to i \in ℝ$
54	53	adantr	$⊢ (i \in ℤ \land k \in ℤ) \to i \in ℝ$
55		zre	$⊢ k \in ℤ \to k \in ℝ$
56	55	adantl	$⊢ (i \in ℤ \land k \in ℤ) \to k \in ℝ$
57		letr	$⊢ (1 \in ℝ \land i \in ℝ \land k \in ℝ) \to ((1 \leq i \land i \leq k) \to 1 \leq k)$
58	52 54 56 57	syl3anc	$⊢ (i \in ℤ \land k \in ℤ) \to ((1 \leq i \land i \leq k) \to 1 \leq k)$
59	58	expcomd	$⊢ (i \in ℤ \land k \in ℤ) \to (i \leq k \to (1 \leq i \to 1 \leq k))$
60	59	adantrd	$⊢ (i \in ℤ \land k \in ℤ) \to ((i \leq k \land k \leq M) \to (1 \leq i \to 1 \leq k))$
61	60	3adant2	$⊢ (i \in ℤ \land M \in ℤ \land k \in ℤ) \to ((i \leq k \land k \leq M) \to (1 \leq i \to 1 \leq k))$
62	61	imp	$⊢ ((i \in ℤ \land M \in ℤ \land k \in ℤ) \land (i \leq k \land k \leq M)) \to (1 \leq i \to 1 \leq k)$
63	62	com12	$⊢ 1 \leq i \to (((i \in ℤ \land M \in ℤ \land k \in ℤ) \land (i \leq k \land k \leq M)) \to 1 \leq k)$
64	63	3ad2ant3	$⊢ (1 \in ℤ \land i \in ℤ \land 1 \leq i) \to (((i \in ℤ \land M \in ℤ \land k \in ℤ) \land (i \leq k \land k \leq M)) \to 1 \leq k)$
65	51 64	sylbi	$⊢ i \in ℤ_{\geq 1} \to (((i \in ℤ \land M \in ℤ \land k \in ℤ) \land (i \leq k \land k \leq M)) \to 1 \leq k)$
66	65	3ad2ant1	$⊢ (i \in ℤ_{\geq 1} \land M \in ℤ \land i < M) \to (((i \in ℤ \land M \in ℤ \land k \in ℤ) \land (i \leq k \land k \leq M)) \to 1 \leq k)$
67	23 66	sylbi	$⊢ i \in (1 ..^M) \to (((i \in ℤ \land M \in ℤ \land k \in ℤ) \land (i \leq k \land k \leq M)) \to 1 \leq k)$
68	50 67	biimtrid	$⊢ i \in (1 ..^M) \to (k \in (i \dots M) \to 1 \leq k)$
69	68	imp	$⊢ (i \in (1 ..^M) \land k \in (i \dots M)) \to 1 \leq k$
70	69	3adant3	$⊢ (i \in (1 ..^M) \land k \in (i \dots M) \land \neg k = M) \to 1 \leq k$
71		zre	$⊢ M \in ℤ \to M \in ℝ$
72	71 55	anim12ci	$⊢ (M \in ℤ \land k \in ℤ) \to (k \in ℝ \land M \in ℝ)$
73	72	3adant1	$⊢ (i \in ℤ \land M \in ℤ \land k \in ℤ) \to (k \in ℝ \land M \in ℝ)$
74		ltlen	$⊢ (k \in ℝ \land M \in ℝ) \to (k < M \leftrightarrow (k \leq M \land M \neq k))$
75	73 74	syl	$⊢ (i \in ℤ \land M \in ℤ \land k \in ℤ) \to (k < M \leftrightarrow (k \leq M \land M \neq k))$
76		nesym	$⊢ M \neq k \leftrightarrow \neg k = M$
77	76	anbi2i	$⊢ (k \leq M \land M \neq k) \leftrightarrow (k \leq M \land \neg k = M)$
78	75 77	bitr2di	$⊢ (i \in ℤ \land M \in ℤ \land k \in ℤ) \to ((k \leq M \land \neg k = M) \leftrightarrow k < M)$
79	78	biimpd	$⊢ (i \in ℤ \land M \in ℤ \land k \in ℤ) \to ((k \leq M \land \neg k = M) \to k < M)$
80	79	expd	$⊢ (i \in ℤ \land M \in ℤ \land k \in ℤ) \to (k \leq M \to (\neg k = M \to k < M))$
81	80	adantld	$⊢ (i \in ℤ \land M \in ℤ \land k \in ℤ) \to ((i \leq k \land k \leq M) \to (\neg k = M \to k < M))$
82	81	imp	$⊢ ((i \in ℤ \land M \in ℤ \land k \in ℤ) \land (i \leq k \land k \leq M)) \to (\neg k = M \to k < M)$
83	50 82	sylbi	$⊢ k \in (i \dots M) \to (\neg k = M \to k < M)$
84	83	imp	$⊢ (k \in (i \dots M) \land \neg k = M) \to k < M$
85	84	3adant1	$⊢ (i \in (1 ..^M) \land k \in (i \dots M) \land \neg k = M) \to k < M$
86	70 85	jca	$⊢ (i \in (1 ..^M) \land k \in (i \dots M) \land \neg k = M) \to (1 \leq k \land k < M)$
87		elfzelz	$⊢ k \in (i \dots M) \to k \in ℤ$
88		1zzd	$⊢ k \in (i \dots M) \to 1 \in ℤ$
89		elfzel2	$⊢ k \in (i \dots M) \to M \in ℤ$
90	87 88 89	3jca	$⊢ k \in (i \dots M) \to (k \in ℤ \land 1 \in ℤ \land M \in ℤ)$
91	90	3ad2ant2	$⊢ (i \in (1 ..^M) \land k \in (i \dots M) \land \neg k = M) \to (k \in ℤ \land 1 \in ℤ \land M \in ℤ)$
92		elfzo	$⊢ (k \in ℤ \land 1 \in ℤ \land M \in ℤ) \to (k \in (1 ..^M) \leftrightarrow (1 \leq k \land k < M))$
93	91 92	syl	$⊢ (i \in (1 ..^M) \land k \in (i \dots M) \land \neg k = M) \to (k \in (1 ..^M) \leftrightarrow (1 \leq k \land k < M))$
94	86 93	mpbird	$⊢ (i \in (1 ..^M) \land k \in (i \dots M) \land \neg k = M) \to k \in (1 ..^M)$
95	94	3exp	$⊢ i \in (1 ..^M) \to (k \in (i \dots M) \to (\neg k = M \to k \in (1 ..^M)))$
96	95	ad2antll	$⊢ (P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to (k \in (i \dots M) \to (\neg k = M \to k \in (1 ..^M)))$
97	96	imp	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M)) \to (\neg k = M \to k \in (1 ..^M))$
98	97	impcom	$⊢ (\neg k = M \land ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M))) \to k \in (1 ..^M)$
99	45 49 98	iccpartipre	$⊢ (\neg k = M \land ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M))) \to P (k) \in ℝ$
100	99	ex	$⊢ \neg k = M \to (((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M)) \to P (k) \in ℝ)$
101	41 100	pm2.61i	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M)) \to P (k) \in ℝ$
102	43	adantr	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M - 1)) \to M \in ℕ$
103	47	adantr	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M - 1)) \to P \in RePart (M)$
104		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
105		fzoss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 ..^M) \subseteq (0 ..^M)$
106	104 105	mp1i	$⊢ (i \in (1 ..^M) \land k \in (i \dots M - 1)) \to (1 ..^M) \subseteq (0 ..^M)$
107		elfzoel2	$⊢ i \in (1 ..^M) \to M \in ℤ$
108		fzoval	$⊢ M \in ℤ \to (i ..^M) = (i \dots M - 1)$
109	107 108	syl	$⊢ i \in (1 ..^M) \to (i ..^M) = (i \dots M - 1)$
110	109	eqcomd	$⊢ i \in (1 ..^M) \to (i \dots M - 1) = (i ..^M)$
111	110	eleq2d	$⊢ i \in (1 ..^M) \to (k \in (i \dots M - 1) \leftrightarrow k \in (i ..^M))$
112		elfzouz	$⊢ i \in (1 ..^M) \to i \in ℤ_{\geq 1}$
113		fzoss1	$⊢ i \in ℤ_{\geq 1} \to (i ..^M) \subseteq (1 ..^M)$
114	112 113	syl	$⊢ i \in (1 ..^M) \to (i ..^M) \subseteq (1 ..^M)$
115	114	sseld	$⊢ i \in (1 ..^M) \to (k \in (i ..^M) \to k \in (1 ..^M))$
116	111 115	sylbid	$⊢ i \in (1 ..^M) \to (k \in (i \dots M - 1) \to k \in (1 ..^M))$
117	116	imp	$⊢ (i \in (1 ..^M) \land k \in (i \dots M - 1)) \to k \in (1 ..^M)$
118	106 117	sseldd	$⊢ (i \in (1 ..^M) \land k \in (i \dots M - 1)) \to k \in (0 ..^M)$
119	118	ex	$⊢ i \in (1 ..^M) \to (k \in (i \dots M - 1) \to k \in (0 ..^M))$
120	119	ad2antll	$⊢ (P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to (k \in (i \dots M - 1) \to k \in (0 ..^M))$
121	120	imp	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M - 1)) \to k \in (0 ..^M)$
122		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))$
123	102 103 121 122	syl3anc	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M - 1)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (k) < P (k + 1))$
124	123	simprd	$⊢ ((P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \land k \in (i \dots M - 1)) \to P (k) < P (k + 1)$
125	22 34 101 124	smonoord	$⊢ (P (M) \in ℝ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to P (i) < P (M)$
126	125	ex	$⊢ P (M) \in ℝ \to ((((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to P (i) < P (M))$
127		simpr	$⊢ (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to i \in (1 ..^M)$
128	42 46 127	iccpartipre	$⊢ (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to P (i) \in ℝ$
129		ltpnf	$⊢ P (i) \in ℝ \to P (i) < +∞$
130	128 129	syl	$⊢ (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to P (i) < +∞$
131		breq2	$⊢ P (M) = +∞ \to (P (i) < P (M) \leftrightarrow P (i) < +∞)$
132	130 131	imbitrrid	$⊢ P (M) = +∞ \to ((((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to P (i) < P (M))$
133	42	adantl	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to M \in ℕ$
134	46	adantl	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to P \in RePart (M)$
135		elfzofz	$⊢ i \in (1 ..^M) \to i \in (1 \dots M)$
136	135	ad2antll	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to i \in (1 \dots M)$
137		elfzubelfz	$⊢ i \in (1 \dots M) \to M \in (1 \dots M)$
138	136 137	syl	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to M \in (1 \dots M)$
139	133 134 138	iccpartgtprec	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to P (M - 1) < P (M)$
140		breq2	$⊢ −∞ = P (M) \to (P (M - 1) < −∞ \leftrightarrow P (M - 1) < P (M))$
141	140	eqcoms	$⊢ P (M) = −∞ \to (P (M - 1) < −∞ \leftrightarrow P (M - 1) < P (M))$
142	141	adantr	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to (P (M - 1) < −∞ \leftrightarrow P (M - 1) < P (M))$
143	139 142	mpbird	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to P (M - 1) < −∞$
144	15	adantl	$⊢ ((φ \land \neg M = 1) \land M \in ℕ) \to M \in ℕ_{0}$
145	144	adantr	$⊢ (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to M \in ℕ_{0}$
146		nnne0	$⊢ M \in ℕ \to M \neq 0$
147	146	adantl	$⊢ ((φ \land \neg M = 1) \land M \in ℕ) \to M \neq 0$
148		df-ne	$⊢ M \neq 1 \leftrightarrow \neg M = 1$
149	148	bilanri	$⊢ (φ \land \neg M = 1) \to M \neq 1$
150	149	adantr	$⊢ ((φ \land \neg M = 1) \land M \in ℕ) \to M \neq 1$
151	144 147 150	3jca	$⊢ ((φ \land \neg M = 1) \land M \in ℕ) \to (M \in ℕ_{0} \land M \neq 0 \land M \neq 1)$
152	151	adantr	$⊢ (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to (M \in ℕ_{0} \land M \neq 0 \land M \neq 1)$
153		nn0n0n1ge2	$⊢ (M \in ℕ_{0} \land M \neq 0 \land M \neq 1) \to 2 \leq M$
154	152 153	syl	$⊢ (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to 2 \leq M$
155	145 154	jca	$⊢ (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to (M \in ℕ_{0} \land 2 \leq M)$
156	155	adantl	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to (M \in ℕ_{0} \land 2 \leq M)$
157		ige2m1fz	$⊢ (M \in ℕ_{0} \land 2 \leq M) \to M - 1 \in (0 \dots M)$
158	156 157	syl	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to M - 1 \in (0 \dots M)$
159	133 134 158	iccpartxr	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to P (M - 1) \in ℝ^{*}$
160		nltmnf	$⊢ P (M - 1) \in ℝ^{*} \to \neg P (M - 1) < −∞$
161	159 160	syl	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to \neg P (M - 1) < −∞$
162	143 161	pm2.21dd	$⊢ (P (M) = −∞ \land (((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M))) \to P (i) < P (M)$
163	162	ex	$⊢ P (M) = −∞ \to ((((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to P (i) < P (M))$
164	126 132 163	3jaoi	$⊢ (P (M) \in ℝ \lor P (M) = +∞ \lor P (M) = −∞) \to ((((φ \land \neg M = 1) \land M \in ℕ) \land i \in (1 ..^M)) \to P (i) < P (M))$
165	164	impl	$⊢ (((P (M) \in ℝ \lor P (M) = +∞ \lor P (M) = −∞) \land ((φ \land \neg M = 1) \land M \in ℕ)) \land i \in (1 ..^M)) \to P (i) < P (M)$
166	165	ralrimiva	$⊢ ((P (M) \in ℝ \lor P (M) = +∞ \lor P (M) = −∞) \land ((φ \land \neg M = 1) \land M \in ℕ)) \to \forall i \in (1 ..^M) P (i) < P (M)$
167	166	ex	$⊢ (P (M) \in ℝ \lor P (M) = +∞ \lor P (M) = −∞) \to (((φ \land \neg M = 1) \land M \in ℕ) \to \forall i \in (1 ..^M) P (i) < P (M))$
168	20 167	sylbi	$⊢ P (M) \in ℝ^{*} \to (((φ \land \neg M = 1) \land M \in ℕ) \to \forall i \in (1 ..^M) P (i) < P (M))$
169	19 168	mpcom	$⊢ ((φ \land \neg M = 1) \land M \in ℕ) \to \forall i \in (1 ..^M) P (i) < P (M)$
170	169	ex	$⊢ (φ \land \neg M = 1) \to (M \in ℕ \to \forall i \in (1 ..^M) P (i) < P (M))$
171	170	expcom	$⊢ \neg M = 1 \to (φ \to (M \in ℕ \to \forall i \in (1 ..^M) P (i) < P (M)))$
172	11 171	pm2.61i	$⊢ φ \to (M \in ℕ \to \forall i \in (1 ..^M) P (i) < P (M))$
173	1 172	mpd	$⊢ φ \to \forall i \in (1 ..^M) P (i) < P (M)$

Metamath Proof Explorer

Theorem iccpartiltu

Proof