Theorem suprzubdc 11881

Description: The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)

Hypotheses

Ref	Expression
suprzubdc.ss	⊢ (𝜑 → 𝐴 ⊆ ℤ)
suprzubdc.dc	⊢ (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)
suprzubdc.ub	⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
suprzubdc.b	⊢ (𝜑 → 𝐵 ∈ 𝐴)

Assertion

Ref	Expression
suprzubdc	⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))

Distinct variable groups:   𝑦,𝐴,𝑥   𝑦,𝐵

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑥)

Proof of Theorem suprzubdc

Dummy variables 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		suprzubdc.ub	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
2		breq2 3985	. . . . 5 ⊢ (𝑥 = 𝑢 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑢))
3	2	ralbidv 2465	. . . 4 ⊢ (𝑥 = 𝑢 → (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢))
4	3	cbvrexv 2692	. . 3 ⊢ (∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∃𝑢 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)
5	1, 4	sylib 121	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)
6		dfin5 3122	. . . . . . 7 ⊢ (ℤ ∩ 𝐴) = {𝑧 ∈ ℤ ∣ 𝑧 ∈ 𝐴}
7		suprzubdc.ss	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
8		sseqin2 3340	. . . . . . . 8 ⊢ (𝐴 ⊆ ℤ ↔ (ℤ ∩ 𝐴) = 𝐴)
9	7, 8	sylib 121	. . . . . . 7 ⊢ (𝜑 → (ℤ ∩ 𝐴) = 𝐴)
10	6, 9	eqtr3id 2212	. . . . . 6 ⊢ (𝜑 → {𝑧 ∈ ℤ ∣ 𝑧 ∈ 𝐴} = 𝐴)
11	10	supeq1d 6948	. . . . 5 ⊢ (𝜑 → sup({𝑧 ∈ ℤ ∣ 𝑧 ∈ 𝐴}, ℝ, < ) = sup(𝐴, ℝ, < ))
12	11	adantr 274	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → sup({𝑧 ∈ ℤ ∣ 𝑧 ∈ 𝐴}, ℝ, < ) = sup(𝐴, ℝ, < ))
13		suprzubdc.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
14	7, 13	sseldd 3142	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℤ)
15	14	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → 𝐵 ∈ ℤ)
16		eleq1 2228	. . . . 5 ⊢ (𝑧 = 𝐵 → (𝑧 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
17	13	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → 𝐵 ∈ 𝐴)
18		eleq1w 2226	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
19	18	dcbid 828	. . . . . 6 ⊢ (𝑥 = 𝑧 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑧 ∈ 𝐴))
20		suprzubdc.dc	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)
21	20	ad2antrr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘𝐵)) → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)
22		eluzelz 9471	. . . . . . 7 ⊢ (𝑧 ∈ (ℤ≥‘𝐵) → 𝑧 ∈ ℤ)
23	22	adantl 275	. . . . . 6 ⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘𝐵)) → 𝑧 ∈ ℤ)
24	19, 21, 23	rspcdva 2834	. . . . 5 ⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘𝐵)) → DECID 𝑧 ∈ 𝐴)
25		simprl 521	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → 𝑢 ∈ ℤ)
26	25	peano2zd 9312	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → (𝑢 + 1) ∈ ℤ)
27	15	zred 9309	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → 𝐵 ∈ ℝ)
28	25	zred 9309	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → 𝑢 ∈ ℝ)
29	26	zred 9309	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → (𝑢 + 1) ∈ ℝ)
30		breq1 3984	. . . . . . . . 9 ⊢ (𝑦 = 𝐵 → (𝑦 ≤ 𝑢 ↔ 𝐵 ≤ 𝑢))
31		simprr 522	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)
32	30, 31, 17	rspcdva 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → 𝐵 ≤ 𝑢)
33	28	lep1d 8822	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → 𝑢 ≤ (𝑢 + 1))
34	27, 28, 29, 32, 33	letrd 8018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → 𝐵 ≤ (𝑢 + 1))
35		eluz2 9468	. . . . . . 7 ⊢ ((𝑢 + 1) ∈ (ℤ≥‘𝐵) ↔ (𝐵 ∈ ℤ ∧ (𝑢 + 1) ∈ ℤ ∧ 𝐵 ≤ (𝑢 + 1)))
36	15, 26, 34, 35	syl3anbrc 1171	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → (𝑢 + 1) ∈ (ℤ≥‘𝐵))
37		eluzle 9474	. . . . . . . . . 10 ⊢ (𝑧 ∈ (ℤ≥‘(𝑢 + 1)) → (𝑢 + 1) ≤ 𝑧)
38	37	ad2antlr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → (𝑢 + 1) ≤ 𝑧)
39	25	ad2antrr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → 𝑢 ∈ ℤ)
40		eluzelz 9471	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (ℤ≥‘(𝑢 + 1)) → 𝑧 ∈ ℤ)
41	40	ad2antlr 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℤ)
42		zltp1le 9241	. . . . . . . . . 10 ⊢ ((𝑢 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑢 < 𝑧 ↔ (𝑢 + 1) ≤ 𝑧))
43	39, 41, 42	syl2anc 409	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → (𝑢 < 𝑧 ↔ (𝑢 + 1) ≤ 𝑧))
44	38, 43	mpbird 166	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → 𝑢 < 𝑧)
45	41	zred 9309	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ)
46	28	ad2antrr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → 𝑢 ∈ ℝ)
47		breq1 3984	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑦 ≤ 𝑢 ↔ 𝑧 ≤ 𝑢))
48	31	ad2antrr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)
49		simpr 109	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
50	47, 48, 49	rspcdva 2834	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → 𝑧 ≤ 𝑢)
51	45, 46, 50	lensymd 8016	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) ∧ 𝑧 ∈ 𝐴) → ¬ 𝑢 < 𝑧)
52	44, 51	pm2.65da 651	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) ∧ 𝑧 ∈ (ℤ≥‘(𝑢 + 1))) → ¬ 𝑧 ∈ 𝐴)
53	52	ralrimiva 2538	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → ∀𝑧 ∈ (ℤ≥‘(𝑢 + 1)) ¬ 𝑧 ∈ 𝐴)
54		fveq2 5485	. . . . . . . 8 ⊢ (𝑣 = (𝑢 + 1) → (ℤ≥‘𝑣) = (ℤ≥‘(𝑢 + 1)))
55	54	raleqdv 2666	. . . . . . 7 ⊢ (𝑣 = (𝑢 + 1) → (∀𝑧 ∈ (ℤ≥‘𝑣) ¬ 𝑧 ∈ 𝐴 ↔ ∀𝑧 ∈ (ℤ≥‘(𝑢 + 1)) ¬ 𝑧 ∈ 𝐴))
56	55	rspcev 2829	. . . . . 6 ⊢ (((𝑢 + 1) ∈ (ℤ≥‘𝐵) ∧ ∀𝑧 ∈ (ℤ≥‘(𝑢 + 1)) ¬ 𝑧 ∈ 𝐴) → ∃𝑣 ∈ (ℤ≥‘𝐵)∀𝑧 ∈ (ℤ≥‘𝑣) ¬ 𝑧 ∈ 𝐴)
57	36, 53, 56	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → ∃𝑣 ∈ (ℤ≥‘𝐵)∀𝑧 ∈ (ℤ≥‘𝑣) ¬ 𝑧 ∈ 𝐴)
58	15, 16, 17, 24, 57	zsupcl 11876	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → sup({𝑧 ∈ ℤ ∣ 𝑧 ∈ 𝐴}, ℝ, < ) ∈ (ℤ≥‘𝐵))
59	12, 58	eqeltrrd 2243	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → sup(𝐴, ℝ, < ) ∈ (ℤ≥‘𝐵))
60		eluzle 9474	. . 3 ⊢ (sup(𝐴, ℝ, < ) ∈ (ℤ≥‘𝐵) → 𝐵 ≤ sup(𝐴, ℝ, < ))
61	59, 60	syl 14	. 2 ⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑢)) → 𝐵 ≤ sup(𝐴, ℝ, < ))
62	5, 61	rexlimddv 2587	1 ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 824   = wceq 1343   ∈ wcel 2136  ∀wral 2443  ∃wrex 2444  {crab 2447   ∩ cin 3114   ⊆ wss 3115   class class class wbr 3981  ‘cfv 5187  (class class class)co 5841  supcsup 6943  ℝcr 7748  1c1 7750   + caddc 7752   < clt 7929   ≤ cle 7930  ℤcz 9187  ℤ_≥cuz 9462

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-sep 4099  ax-pow 4152  ax-pr 4186  ax-un 4410  ax-setind 4513  ax-cnex 7840  ax-resscn 7841  ax-1cn 7842  ax-1re 7843  ax-icn 7844  ax-addcl 7845  ax-addrcl 7846  ax-mulcl 7847  ax-addcom 7849  ax-addass 7851  ax-distr 7853  ax-i2m1 7854  ax-0lt1 7855  ax-0id 7857  ax-rnegex 7858  ax-cnre 7860  ax-pre-ltirr 7861  ax-pre-ltwlin 7862  ax-pre-lttrn 7863  ax-pre-apti 7864  ax-pre-ltadd 7865

This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 969  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ne 2336  df-nel 2431  df-ral 2448  df-rex 2449  df-reu 2450  df-rmo 2451  df-rab 2452  df-v 2727  df-sbc 2951  df-csb 3045  df-dif 3117  df-un 3119  df-in 3121  df-ss 3128  df-pw 3560  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-int 3824  df-iun 3867  df-br 3982  df-opab 4043  df-mpt 4044  df-id 4270  df-xp 4609  df-rel 4610  df-cnv 4611  df-co 4612  df-dm 4613  df-rn 4614  df-res 4615  df-ima 4616  df-iota 5152  df-fun 5189  df-fn 5190  df-f 5191  df-fv 5195  df-riota 5797  df-ov 5844  df-oprab 5845  df-mpo 5846  df-1st 6105  df-2nd 6106  df-sup 6945  df-pnf 7931  df-mnf 7932  df-xr 7933  df-ltxr 7934  df-le 7935  df-sub 8067  df-neg 8068  df-inn 8854  df-n0 9111  df-z 9188  df-uz 9463  df-fz 9941  df-fzo 10074

This theorem is referenced by:  pcprendvds  12218  pcpremul  12221