uzwodc - Intuitionistic Logic Explorer

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

Theorem uzwodc 12558

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 6008	. . . . . . . 8 ⊢ (𝑝 = 𝑠 → (𝑝 − 1) = (𝑠 − 1))
3	2	oveq1d 6016	. . . . . . 7 ⊢ (𝑝 = 𝑠 → ((𝑝 − 1) + 𝑀) = ((𝑠 − 1) + 𝑀))
4	3	eleq1d 2298	. . . . . 6 ⊢ (𝑝 = 𝑠 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
5	4	elrab 2959	. . . . 5 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
6	1, 5	sylib 122	. . . 4 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
7	6	simprd 114	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ((𝑠 − 1) + 𝑀) ∈ 𝑆)
8		breq2 4087	. . . . . . 7 ⊢ (𝑡 = ((𝑘 − 𝑀) + 1) → (𝑠 ≤ 𝑡 ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
9		simplr 528	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
10		oveq1 6008	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → (𝑝 − 1) = (((𝑘 − 𝑀) + 1) − 1))
11	10	oveq1d 6016	. . . . . . . . 9 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑘 − 𝑀) + 1) − 1) + 𝑀))
12	11	eleq1d 2298	. . . . . . . 8 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆))
13		simp1 1021	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑆 ⊆ (ℤ_≥‘𝑀))
14	13	ad3antrrr 492	. . . . . . . . . . . . 13 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑆 ⊆ (ℤ_≥‘𝑀))
15		simpr 110	. . . . . . . . . . . . 13 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ 𝑆)
16	14, 15	sseldd 3225	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ (ℤ_≥‘𝑀))
17		eluzelz 9731	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
18	16, 17	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℤ)
19		simp2 1022	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑥 𝑥 ∈ 𝑆)
20		ssel2 3219	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (ℤ_≥‘𝑀))
21		eluzel2 9727	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
22	20, 21	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
23	22	ex 115	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (𝑥 ∈ 𝑆 → 𝑀 ∈ ℤ))
24	23	exlimdv 1865	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (∃𝑥 𝑥 ∈ 𝑆 → 𝑀 ∈ ℤ))
25	13, 19, 24	sylc 62	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
26	25	ad3antrrr 492	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℤ)
27	18, 26	zsubcld 9574	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℤ)
28		eluzle 9734	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑘)
29	16, 28	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ≤ 𝑘)
30	18	zred 9569	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℝ)
31	26	zred 9569	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℝ)
32	30, 31	subge0d 8682	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (0 ≤ (𝑘 − 𝑀) ↔ 𝑀 ≤ 𝑘))
33	29, 32	mpbird 167	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 0 ≤ (𝑘 − 𝑀))
34		elnn0z 9459	. . . . . . . . . 10 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ ↔ ((𝑘 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑘 − 𝑀)))
35	27, 33, 34	sylanbrc 417	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℕ₀)
36		nn0p1nn 9408	. . . . . . . . 9 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ → ((𝑘 − 𝑀) + 1) ∈ ℕ)
37	35, 36	syl 14	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ ℕ)
38	27	zcnd 9570	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℂ)
39		1cnd 8162	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℂ)
40	38, 39	pncand 8458	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (((𝑘 − 𝑀) + 1) − 1) = (𝑘 − 𝑀))
41	40	oveq1d 6016	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = ((𝑘 − 𝑀) + 𝑀))
42	18	zcnd 9570	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℂ)
43	26	zcnd 9570	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℂ)
44	42, 43	npcand 8461	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 𝑀) = 𝑘)
45	41, 44	eqtrd 2262	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = 𝑘)
46	45, 15	eqeltrd 2306	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
47	12, 37, 46	elrabd 2961	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
48	8, 9, 47	rspcdva 2912	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ≤ ((𝑘 − 𝑀) + 1))
49		elrabi 2956	. . . . . . . . 9 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} → 𝑠 ∈ ℕ)
50	49	ad3antlr 493	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℕ)
51	50	nnred 9123	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℝ)
52		1red 8161	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℝ)
53	30, 31	resubcld 8527	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℝ)
54	51, 52, 53	lesubaddd 8689	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑠 − 1) ≤ (𝑘 − 𝑀) ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
55	48, 54	mpbird 167	. . . . 5 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ≤ (𝑘 − 𝑀))
56	51, 52	resubcld 8527	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ∈ ℝ)
57		leaddsub 8585	. . . . . 6 ⊢ (((𝑠 − 1) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑠 − 1) + 𝑀) ≤ 𝑘 ↔ (𝑠 − 1) ≤ (𝑘 − 𝑀)))
58	56, 31, 30, 57	syl3anc 1271	. . . . 5 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (((𝑠 − 1) + 𝑀) ≤ 𝑘 ↔ (𝑠 − 1) ≤ (𝑘 − 𝑀)))
59	55, 58	mpbird 167	. . . 4 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑠 − 1) + 𝑀) ≤ 𝑘)
60	59	ralrimiva 2603	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘)
61		breq1 4086	. . . . 5 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (𝑗 ≤ 𝑘 ↔ ((𝑠 − 1) + 𝑀) ≤ 𝑘))
62	61	ralbidv 2530	. . . 4 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ↔ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘))
63	62	rspcev 2907	. . 3 ⊢ ((((𝑠 − 1) + 𝑀) ∈ 𝑆 ∧ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
64	7, 60, 63	syl2anc 411	. 2 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
65		ssrab2 3309	. . 3 ⊢ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ
66		eluzelz 9731	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑥 ∈ ℤ)
67	20, 66	syl 14	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℤ)
68	67, 22	zsubcld 9574	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℤ)
69		1zzd 9473	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℤ)
70	68, 69	zaddcld 9573	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℤ)
71		oveq1 6008	. . . . . . . . . . 11 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (𝑝 − 1) = (((𝑥 − 𝑀) + 1) − 1))
72	71	oveq1d 6016	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑥 − 𝑀) + 1) − 1) + 𝑀))
73	72	eleq1d 2298	. . . . . . . . 9 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆))
74		eluzle 9734	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑥)
75	20, 74	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ≤ 𝑥)
76	67	zred 9569	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℝ)
77	22	zred 9569	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℝ)
78	76, 77	subge0d 8682	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (0 ≤ (𝑥 − 𝑀) ↔ 𝑀 ≤ 𝑥))
79	75, 78	mpbird 167	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 0 ≤ (𝑥 − 𝑀))
80		elnn0z 9459	. . . . . . . . . . 11 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ ↔ ((𝑥 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑥 − 𝑀)))
81	68, 79, 80	sylanbrc 417	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℕ₀)
82		nn0p1nn 9408	. . . . . . . . . 10 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ → ((𝑥 − 𝑀) + 1) ∈ ℕ)
83	81, 82	syl 14	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℕ)
84	68	zcnd 9570	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℂ)
85		1cnd 8162	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℂ)
86	84, 85	pncand 8458	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (((𝑥 − 𝑀) + 1) − 1) = (𝑥 − 𝑀))
87	86	oveq1d 6016	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
88	67	zcnd 9570	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ)
89	22	zcnd 9570	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℂ)
90	88, 89	npcand 8461	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
91	87, 90	eqtrd 2262	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = 𝑥)
92		simpr 110	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
93	91, 92	eqeltrd 2306	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
94	73, 83, 93	elrabd 2961	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
95		eleq1 2292	. . . . . . . . 9 ⊢ (𝑞 = ((𝑥 − 𝑀) + 1) → (𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
96	95	spcegv 2891	. . . . . . . 8 ⊢ (((𝑥 − 𝑀) + 1) ∈ ℤ → (((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
97	70, 94, 96	sylc 62	. . . . . . 7 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
98	97	ex 115	. . . . . 6 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (𝑥 ∈ 𝑆 → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
99	98	exlimdv 1865	. . . . 5 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
100	99	imp 124	. . . 4 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
101	100	3adant3 1041	. . 3 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
102		eleq1 2292	. . . . . . 7 ⊢ (𝑥 = ((𝑟 − 1) + 𝑀) → (𝑥 ∈ 𝑆 ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
103	102	dcbid 843	. . . . . 6 ⊢ (𝑥 = ((𝑟 − 1) + 𝑀) → (DECID 𝑥 ∈ 𝑆 ↔ DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆))
104		simpl3 1026	. . . . . 6 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆)
105	24	imp 124	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
106	105	3adant3 1041	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
107	106	adantr 276	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ∈ ℤ)
108		simpr 110	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑟 ∈ ℕ)
109	108	nnzd 9568	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑟 ∈ ℤ)
110		1zzd 9473	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 1 ∈ ℤ)
111	109, 110	zsubcld 9574	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℤ)
112	111, 107	zaddcld 9573	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ ℤ)
113		nnm1ge0 9533	. . . . . . . . 9 ⊢ (𝑟 ∈ ℕ → 0 ≤ (𝑟 − 1))
114	113	adantl 277	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 0 ≤ (𝑟 − 1))
115	107	zred 9569	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ∈ ℝ)
116	111	zred 9569	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℝ)
117	115, 116	addge02d 8681	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (0 ≤ (𝑟 − 1) ↔ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
118	114, 117	mpbid 147	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ≤ ((𝑟 − 1) + 𝑀))
119		eluz2 9728	. . . . . . 7 ⊢ (((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ ((𝑟 − 1) + 𝑀) ∈ ℤ ∧ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
120	107, 112, 118, 119	syl3anbrc 1205	. . . . . 6 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀))
121	103, 104, 120	rspcdva 2912	. . . . 5 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆)
122		oveq1 6008	. . . . . . . . . 10 ⊢ (𝑝 = 𝑟 → (𝑝 − 1) = (𝑟 − 1))
123	122	oveq1d 6016	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑝 − 1) + 𝑀) = ((𝑟 − 1) + 𝑀))
124	123	eleq1d 2298	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
125	124	elrab3 2960	. . . . . . 7 ⊢ (𝑟 ∈ ℕ → (𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
126	125	dcbid 843	. . . . . 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 2603	. . 3 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
130		nnwodc 12557	. . 3 ⊢ (({𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ ∧ ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ∧ ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
131	65, 101, 129, 130	mp3an2i 1376	. 2 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
132	64, 131	r19.29a 2674	1 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 839 ∧ w3a 1002 = wceq 1395 ∃wex 1538 ∈ wcel 2200 ∀wral 2508 ∃wrex 2509 {crab 2512 ⊆ wss 3197 class class class wbr 4083 ‘cfv 5318 (class class class)co 6001 ℝcr 7998 0cc0 7999 1c1 8000 + caddc 8002 ≤ cle 8182 − cmin 8317 ℕcn 9110 ℕ₀cn0 9369 ℤcz 9446 ℤ_≥cuz 9722

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4202 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629 ax-cnex 8090 ax-resscn 8091 ax-1cn 8092 ax-1re 8093 ax-icn 8094 ax-addcl 8095 ax-addrcl 8096 ax-mulcl 8097 ax-addcom 8099 ax-addass 8101 ax-distr 8103 ax-i2m1 8104 ax-0lt1 8105 ax-0id 8107 ax-rnegex 8108 ax-cnre 8110 ax-pre-ltirr 8111 ax-pre-ltwlin 8112 ax-pre-lttrn 8113 ax-pre-apti 8114 ax-pre-ltadd 8115

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-id 4384 df-po 4387 df-iso 4388 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-isom 5327 df-riota 5954 df-ov 6004 df-oprab 6005 df-mpo 6006 df-1st 6286 df-2nd 6287 df-sup 7151 df-inf 7152 df-pnf 8183 df-mnf 8184 df-xr 8185 df-ltxr 8186 df-le 8187 df-sub 8319 df-neg 8320 df-inn 9111 df-n0 9370 df-z 9447 df-uz 9723 df-fz 10205 df-fzo 10339

This theorem is referenced by: (None)

W3C validator