iccpartiltu - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > iccpartiltu		Structured version Unicode version

Theorem iccpartiltu 38454

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

**Hypotheses**
Ref	Expression
iccpartgtprec.m
iccpartgtprec.p	RePart

**Assertion**
Ref	Expression
iccpartiltu	..^

Distinct variable groups:

Proof of Theorem iccpartiltu Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	. 2
2		ral0 3903	. . . . 5
3		oveq2 6311	. . . . . . 7 ..^ ..^
4		fzo0 11944	. . . . . . 7 ..^
5	3, 4	syl6eq 2480	. . . . . 6 ..^
6		fveq2 5879	. . . . . . 7
7	6	breq2d 4433	. . . . . 6
8	5, 7	raleqbidv 3040	. . . . 5 ..^
9	2, 8	mpbiri 237	. . . 4 ..^
10	9	2a1d 28	. . 3 ..^
11		simpr 463	. . . . . . 7 $/\$ $/\$
12		iccpartgtprec.p	. . . . . . . . 9 RePart
13	12	adantr 467	. . . . . . . 8 $/\$ RePart
14	13	adantr 467	. . . . . . 7 $/\$ $/\$ RePart
15		nnnn0 10878	. . . . . . . . 9
16		nn0fz0 11892	. . . . . . . . 9
17	15, 16	sylib 200	. . . . . . . 8
18	17	adantl 468	. . . . . . 7 $/\$ $/\$
19	11, 14, 18	iccpartxr 38451	. . . . . 6 $/\$ $/\$
20		elxr 11418	. . . . . . 7 $\/$ $\/$
21		elfzoelz 11922	. . . . . . . . . . . . . 14 ..^
22	21	ad2antll 734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ..^
23		elfzo2 11925	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$
24		eluzelz 11170	. . . . . . . . . . . . . . . . . 18
25	24	peano2zd 11045	. . . . . . . . . . . . . . . . 17
26	25	3ad2ant1 1027	. . . . . . . . . . . . . . . 16 $/\$ $/\$
27		simp2 1007	. . . . . . . . . . . . . . . 16 $/\$ $/\$
28		zltp1le 10988	. . . . . . . . . . . . . . . . . 18 $/\$
29	24, 28	sylan 474	. . . . . . . . . . . . . . . . 17 $/\$
30	29	biimp3a 1365	. . . . . . . . . . . . . . . 16 $/\$ $/\$
31		eluz2 11167	. . . . . . . . . . . . . . . 16 $/\$ $/\$
32	26, 27, 30, 31	syl3anbrc 1190	. . . . . . . . . . . . . . 15 $/\$ $/\$
33	23, 32	sylbi 199	. . . . . . . . . . . . . 14 ..^
34	33	ad2antll 734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ..^
35		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
36	35	eqcomd 2431	. . . . . . . . . . . . . . . . . . 19
37	36	eleq1d 2492	. . . . . . . . . . . . . . . . . 18
38	37	biimpcd 228	. . . . . . . . . . . . . . . . 17
39	38	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ..^
40	39	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
41	40	com12 33	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
42	11	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ ..^
43	42	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ..^
44	43	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
45	44	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
46	14	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ ..^ RePart
47	46	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ..^ RePart
48	47	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ..^ $/\$ RePart
49	48	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ RePart
50		elfz2 11793	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
51		eluz2 11167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
52		1red 9660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
53		zre 10943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54	53	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
55		zre 10943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
56	55	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
57		letr 9729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
58	52, 54, 56, 57	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
59	58	expcomd 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
60	59	adantrd 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
61	60	3adant2 1025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
62	61	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
63	62	com12 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
64	63	3ad2ant3 1029	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	51, 64	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
66	65	3ad2ant1 1027	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	23, 66	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ $/\$ $/\$ $/\$ $/\$
68	50, 67	syl5bi 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^
69	68	imp 431	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
70	69	3adant3 1026	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$ $/\$
71		zre 10943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	71, 55	anim12ci 570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
73	72	3adant1 1024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
74		ltlen 9737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
75	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
76		nesym 2697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
77	76	anbi2i 699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
78	75, 77	syl6rbb 266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
79	78	biimpd 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
80	79	expd 438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
81	80	adantld 469	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
82	81	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
83	50, 82	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . 24
84	83	imp 431	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
85	84	3adant1 1024	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$ $/\$
86	70, 85	jca 535	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$ $/\$
87		elfzelz 11802	. . . . . . . . . . . . . . . . . . . . . . . 24
88		1zzd 10970	. . . . . . . . . . . . . . . . . . . . . . . 24
89		elfzel2 11800	. . . . . . . . . . . . . . . . . . . . . . . 24
90	87, 88, 89	3jca 1186	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
91	90	3ad2ant2 1028	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$ $/\$ $/\$ $/\$
92		elfzo 11924	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$ ..^ $/\$
94	86, 93	mpbird 236	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$ ..^
95	94	3exp 1205	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
96	95	ad2antll 734	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ ..^ ..^
97	96	imp 431	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ ..^ $/\$ ..^
98	97	impcom 432	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ ..^
99	45, 49, 98	iccpartipre 38453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
100	99	ex 436	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
101	41, 100	pm2.61i 168	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
102	43	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
103	47	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ..^ $/\$ RePart
104		1eluzge0 11204	. . . . . . . . . . . . . . . . . . . 20
105		fzoss1 11947	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
106	104, 105	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ ..^ ..^
107		elfzoel2 11921	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^
108		fzoval 11923	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
110	109	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
111	110	eleq2d 2493	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
112		elfzouz 11926	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
113		fzoss1 11947	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
114	112, 113	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^ ..^
115	114	sseld 3464	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^ ..^
116	111, 115	sylbid 219	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
117	116	imp 431	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ ..^
118	106, 117	sseldd 3466	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ ..^
119	118	ex 436	. . . . . . . . . . . . . . . . 17 ..^ ..^
120	119	ad2antll 734	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ..^ ..^
121	120	imp 431	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ..^ $/\$ ..^
122		iccpartimp 38449	. . . . . . . . . . . . . . 15 $/\$ RePart $/\$ ..^ $/\$
123	102, 103, 121, 122	syl3anc 1265	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
124	123	simprd 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
125	22, 34, 101, 124	smonoord 38436	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ..^
126	125	ex 436	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ..^
127		simpr 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ..^ ..^
128	42, 46, 127	iccpartipre 38453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ ..^
129		ltpnf 11424	. . . . . . . . . . . . 13
130	128, 129	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ ..^
131		breq2 4425	. . . . . . . . . . . 12
132	130, 131	syl5ibr 225	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ..^
133	42	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ..^
134	46	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ..^ RePart
135		elfzofz 11937	. . . . . . . . . . . . . . . . 17 ..^
136	135	ad2antll 734	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ..^
137		elfzubelfz 11813	. . . . . . . . . . . . . . . 16
138	136, 137	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ..^
139	133, 134, 138	iccpartgtprec 38452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ..^
140		breq2 4425	. . . . . . . . . . . . . . . 16
141	140	eqcoms 2435	. . . . . . . . . . . . . . 15
142	141	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ..^
143	139, 142	mpbird 236	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ..^
144	15	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
145	144	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ ..^
146		nnne0 10644	. . . . . . . . . . . . . . . . . . . . . 22
147	146	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
148		df-ne 2621	. . . . . . . . . . . . . . . . . . . . . . . 24
149	148	biimpri 210	. . . . . . . . . . . . . . . . . . . . . . 23
150	149	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
151	150	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
152	144, 147, 151	3jca 1186	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
153	152	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ ..^ $/\$ $/\$
154		nn0n0n1ge2 10934	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
155	153, 154	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ ..^
156	145, 155	jca 535	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ ..^ $/\$
157	156	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ ..^ $/\$
158		ige2m1fz 11886	. . . . . . . . . . . . . . . 16 $/\$
159	157, 158	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ ..^
160	133, 134, 159	iccpartxr 38451	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ ..^
161		nltmnf 11433	. . . . . . . . . . . . . 14
162	160, 161	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ ..^
163	143, 162	pm2.21dd 178	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ ..^
164	163	ex 436	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ..^
165	126, 132, 164	3jaoi 1328	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$ $/\$ ..^
166	165	impl 625	. . . . . . . . 9 $\/$ $\/$ $/\$ $/\$ $/\$ $/\$ ..^
167	166	ralrimiva 2840	. . . . . . . 8 $\/$ $\/$ $/\$ $/\$ $/\$ ..^
168	167	ex 436	. . . . . . 7 $\/$ $\/$ $/\$ $/\$ ..^
169	20, 168	sylbi 199	. . . . . 6 $/\$ $/\$ ..^
170	19, 169	mpcom 38	. . . . 5 $/\$ $/\$ ..^
171	170	ex 436	. . . 4 $/\$ ..^
172	171	expcom 437	. . 3 ..^
173	10, 172	pm2.61i 168	. 2 ..^
174	1, 173	mpd 15	1 ..^

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $\/$ w3o 982 $/\$ w3a 983

wceq 1438

wcel 1869

wne 2619

wral 2776

wss 3437

c0 3762 class class class wbr 4421

cfv 5599 (class class class)co 6303

cmap 7478

cr 9540

cc0 9541

c1 9542

caddc 9544

cpnf 9674

cmnf 9675

cxr 9676

clt 9677

cle 9678

cmin 9862

cn 10611

c2 10661

cn0 10871

cz 10939

cuz 11161

cfz 11786 ..^cfzo 11917 RePartciccp 38445

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-er 7369 df-map 7480 df-en 7576 df-dom 7577 df-sdom 7578 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-nn 10612 df-2 10670 df-n0 10872 df-z 10940 df-uz 11162 df-fz 11787 df-fzo 11918 df-iccp 38446

This theorem is referenced by: iccpartlt 38456 iccpartltu 38457 iccpartgt 38459

W3C validator