uzwodc - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > uzwodc		GIF version

Theorem uzwodc 12204

Description: Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.)

**Assertion**
Ref	Expression
uzwodc	⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)

Distinct variable groups: 𝑗,𝑀,𝑘 𝑥,𝑀,𝑘 𝑆,𝑗,𝑘 𝑥,𝑆

Proof of Theorem uzwodc Dummy variables 𝑠 𝑝 𝑡 𝑞 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 528	. . . . 5 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
2		oveq1 5929	. . . . . . . 8 ⊢ (𝑝 = 𝑠 → (𝑝 − 1) = (𝑠 − 1))
3	2	oveq1d 5937	. . . . . . 7 ⊢ (𝑝 = 𝑠 → ((𝑝 − 1) + 𝑀) = ((𝑠 − 1) + 𝑀))
4	3	eleq1d 2265	. . . . . 6 ⊢ (𝑝 = 𝑠 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
5	4	elrab 2920	. . . . 5 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
6	1, 5	sylib 122	. . . 4 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
7	6	simprd 114	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ((𝑠 − 1) + 𝑀) ∈ 𝑆)
8		breq2 4037	. . . . . . 7 ⊢ (𝑡 = ((𝑘 − 𝑀) + 1) → (𝑠 ≤ 𝑡 ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
9		simplr 528	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
10		oveq1 5929	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → (𝑝 − 1) = (((𝑘 − 𝑀) + 1) − 1))
11	10	oveq1d 5937	. . . . . . . . 9 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑘 − 𝑀) + 1) − 1) + 𝑀))
12	11	eleq1d 2265	. . . . . . . 8 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆))
13		simp1 999	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑆 ⊆ (ℤ_≥‘𝑀))
14	13	ad3antrrr 492	. . . . . . . . . . . . 13 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑆 ⊆ (ℤ_≥‘𝑀))
15		simpr 110	. . . . . . . . . . . . 13 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ 𝑆)
16	14, 15	sseldd 3184	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ (ℤ_≥‘𝑀))
17		eluzelz 9610	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
18	16, 17	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℤ)
19		simp2 1000	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑥 𝑥 ∈ 𝑆)
20		ssel2 3178	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (ℤ_≥‘𝑀))
21		eluzel2 9606	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
22	20, 21	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
23	22	ex 115	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (𝑥 ∈ 𝑆 → 𝑀 ∈ ℤ))
24	23	exlimdv 1833	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (∃𝑥 𝑥 ∈ 𝑆 → 𝑀 ∈ ℤ))
25	13, 19, 24	sylc 62	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
26	25	ad3antrrr 492	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℤ)
27	18, 26	zsubcld 9453	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℤ)
28		eluzle 9613	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑘)
29	16, 28	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ≤ 𝑘)
30	18	zred 9448	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℝ)
31	26	zred 9448	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℝ)
32	30, 31	subge0d 8562	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (0 ≤ (𝑘 − 𝑀) ↔ 𝑀 ≤ 𝑘))
33	29, 32	mpbird 167	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 0 ≤ (𝑘 − 𝑀))
34		elnn0z 9339	. . . . . . . . . 10 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ ↔ ((𝑘 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑘 − 𝑀)))
35	27, 33, 34	sylanbrc 417	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℕ₀)
36		nn0p1nn 9288	. . . . . . . . 9 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ → ((𝑘 − 𝑀) + 1) ∈ ℕ)
37	35, 36	syl 14	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ ℕ)
38	27	zcnd 9449	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℂ)
39		1cnd 8042	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℂ)
40	38, 39	pncand 8338	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (((𝑘 − 𝑀) + 1) − 1) = (𝑘 − 𝑀))
41	40	oveq1d 5937	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = ((𝑘 − 𝑀) + 𝑀))
42	18	zcnd 9449	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℂ)
43	26	zcnd 9449	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℂ)
44	42, 43	npcand 8341	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 𝑀) = 𝑘)
45	41, 44	eqtrd 2229	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = 𝑘)
46	45, 15	eqeltrd 2273	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
47	12, 37, 46	elrabd 2922	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
48	8, 9, 47	rspcdva 2873	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ≤ ((𝑘 − 𝑀) + 1))
49		elrabi 2917	. . . . . . . . 9 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} → 𝑠 ∈ ℕ)
50	49	ad3antlr 493	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℕ)
51	50	nnred 9003	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℝ)
52		1red 8041	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℝ)
53	30, 31	resubcld 8407	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℝ)
54	51, 52, 53	lesubaddd 8569	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑠 − 1) ≤ (𝑘 − 𝑀) ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
55	48, 54	mpbird 167	. . . . 5 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ≤ (𝑘 − 𝑀))
56	51, 52	resubcld 8407	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ∈ ℝ)
57		leaddsub 8465	. . . . . 6 ⊢ (((𝑠 − 1) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑠 − 1) + 𝑀) ≤ 𝑘 ↔ (𝑠 − 1) ≤ (𝑘 − 𝑀)))
58	56, 31, 30, 57	syl3anc 1249	. . . . 5 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (((𝑠 − 1) + 𝑀) ≤ 𝑘 ↔ (𝑠 − 1) ≤ (𝑘 − 𝑀)))
59	55, 58	mpbird 167	. . . 4 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑠 − 1) + 𝑀) ≤ 𝑘)
60	59	ralrimiva 2570	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘)
61		breq1 4036	. . . . 5 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (𝑗 ≤ 𝑘 ↔ ((𝑠 − 1) + 𝑀) ≤ 𝑘))
62	61	ralbidv 2497	. . . 4 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ↔ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘))
63	62	rspcev 2868	. . 3 ⊢ ((((𝑠 − 1) + 𝑀) ∈ 𝑆 ∧ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
64	7, 60, 63	syl2anc 411	. 2 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
65		ssrab2 3268	. . 3 ⊢ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ
66		eluzelz 9610	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑥 ∈ ℤ)
67	20, 66	syl 14	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℤ)
68	67, 22	zsubcld 9453	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℤ)
69		1zzd 9353	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℤ)
70	68, 69	zaddcld 9452	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℤ)
71		oveq1 5929	. . . . . . . . . . 11 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (𝑝 − 1) = (((𝑥 − 𝑀) + 1) − 1))
72	71	oveq1d 5937	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑥 − 𝑀) + 1) − 1) + 𝑀))
73	72	eleq1d 2265	. . . . . . . . 9 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆))
74		eluzle 9613	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑥)
75	20, 74	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ≤ 𝑥)
76	67	zred 9448	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℝ)
77	22	zred 9448	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℝ)
78	76, 77	subge0d 8562	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (0 ≤ (𝑥 − 𝑀) ↔ 𝑀 ≤ 𝑥))
79	75, 78	mpbird 167	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 0 ≤ (𝑥 − 𝑀))
80		elnn0z 9339	. . . . . . . . . . 11 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ ↔ ((𝑥 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑥 − 𝑀)))
81	68, 79, 80	sylanbrc 417	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℕ₀)
82		nn0p1nn 9288	. . . . . . . . . 10 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ → ((𝑥 − 𝑀) + 1) ∈ ℕ)
83	81, 82	syl 14	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℕ)
84	68	zcnd 9449	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℂ)
85		1cnd 8042	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℂ)
86	84, 85	pncand 8338	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (((𝑥 − 𝑀) + 1) − 1) = (𝑥 − 𝑀))
87	86	oveq1d 5937	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
88	67	zcnd 9449	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ)
89	22	zcnd 9449	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℂ)
90	88, 89	npcand 8341	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
91	87, 90	eqtrd 2229	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = 𝑥)
92		simpr 110	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
93	91, 92	eqeltrd 2273	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
94	73, 83, 93	elrabd 2922	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
95		eleq1 2259	. . . . . . . . 9 ⊢ (𝑞 = ((𝑥 − 𝑀) + 1) → (𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
96	95	spcegv 2852	. . . . . . . 8 ⊢ (((𝑥 − 𝑀) + 1) ∈ ℤ → (((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
97	70, 94, 96	sylc 62	. . . . . . 7 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
98	97	ex 115	. . . . . 6 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (𝑥 ∈ 𝑆 → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
99	98	exlimdv 1833	. . . . 5 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
100	99	imp 124	. . . 4 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
101	100	3adant3 1019	. . 3 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
102		eleq1 2259	. . . . . . 7 ⊢ (𝑥 = ((𝑟 − 1) + 𝑀) → (𝑥 ∈ 𝑆 ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
103	102	dcbid 839	. . . . . 6 ⊢ (𝑥 = ((𝑟 − 1) + 𝑀) → (DECID 𝑥 ∈ 𝑆 ↔ DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆))
104		simpl3 1004	. . . . . 6 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆)
105	24	imp 124	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
106	105	3adant3 1019	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
107	106	adantr 276	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ∈ ℤ)
108		simpr 110	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑟 ∈ ℕ)
109	108	nnzd 9447	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑟 ∈ ℤ)
110		1zzd 9353	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 1 ∈ ℤ)
111	109, 110	zsubcld 9453	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℤ)
112	111, 107	zaddcld 9452	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ ℤ)
113		nnm1ge0 9412	. . . . . . . . 9 ⊢ (𝑟 ∈ ℕ → 0 ≤ (𝑟 − 1))
114	113	adantl 277	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 0 ≤ (𝑟 − 1))
115	107	zred 9448	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ∈ ℝ)
116	111	zred 9448	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℝ)
117	115, 116	addge02d 8561	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (0 ≤ (𝑟 − 1) ↔ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
118	114, 117	mpbid 147	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ≤ ((𝑟 − 1) + 𝑀))
119		eluz2 9607	. . . . . . 7 ⊢ (((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ ((𝑟 − 1) + 𝑀) ∈ ℤ ∧ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
120	107, 112, 118, 119	syl3anbrc 1183	. . . . . 6 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀))
121	103, 104, 120	rspcdva 2873	. . . . 5 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆)
122		oveq1 5929	. . . . . . . . . 10 ⊢ (𝑝 = 𝑟 → (𝑝 − 1) = (𝑟 − 1))
123	122	oveq1d 5937	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑝 − 1) + 𝑀) = ((𝑟 − 1) + 𝑀))
124	123	eleq1d 2265	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
125	124	elrab3 2921	. . . . . . 7 ⊢ (𝑟 ∈ ℕ → (𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
126	125	dcbid 839	. . . . . 6 ⊢ (𝑟 ∈ ℕ → (DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆))
127	126	adantl 277	. . . . 5 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆))
128	121, 127	mpbird 167	. . . 4 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
129	128	ralrimiva 2570	. . 3 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
130		nnwodc 12203	. . 3 ⊢ (({𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ ∧ ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ∧ ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
131	65, 101, 129, 130	mp3an2i 1353	. 2 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
132	64, 131	r19.29a 2640	1 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 835 ∧ w3a 980 = wceq 1364 ∃wex 1506 ∈ wcel 2167 ∀wral 2475 ∃wrex 2476 {crab 2479 ⊆ wss 3157 class class class wbr 4033 ‘cfv 5258 (class class class)co 5922 ℝcr 7878 0cc0 7879 1c1 7880 + caddc 7882 ≤ cle 8062 − cmin 8197 ℕcn 8990 ℕ₀cn0 9249 ℤcz 9326 ℤ_≥cuz 9601

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4151 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-addcom 7979 ax-addass 7981 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-0id 7987 ax-rnegex 7988 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-id 4328 df-po 4331 df-iso 4332 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-isom 5267 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-sup 7050 df-inf 7051 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-inn 8991 df-n0 9250 df-z 9327 df-uz 9602 df-fz 10084 df-fzo 10218

This theorem is referenced by: (None)

W3C validator