uzwodc - Intuitionistic Logic Explorer

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

Theorem uzwodc 12758

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 529	. . . . 5 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
2		oveq1 6065	. . . . . . . 8 ⊢ (𝑝 = 𝑠 → (𝑝 − 1) = (𝑠 − 1))
3	2	oveq1d 6073	. . . . . . 7 ⊢ (𝑝 = 𝑠 → ((𝑝 − 1) + 𝑀) = ((𝑠 − 1) + 𝑀))
4	3	eleq1d 2303	. . . . . 6 ⊢ (𝑝 = 𝑠 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
5	4	elrab 2976	. . . . 5 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
6	1, 5	sylib 122	. . . 4 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
7	6	simprd 114	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ((𝑠 − 1) + 𝑀) ∈ 𝑆)
8		breq2 4118	. . . . . . 7 ⊢ (𝑡 = ((𝑘 − 𝑀) + 1) → (𝑠 ≤ 𝑡 ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
9		simplr 529	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
10		oveq1 6065	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → (𝑝 − 1) = (((𝑘 − 𝑀) + 1) − 1))
11	10	oveq1d 6073	. . . . . . . . 9 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑘 − 𝑀) + 1) − 1) + 𝑀))
12	11	eleq1d 2303	. . . . . . . 8 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆))
13		simp1 1024	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑆 ⊆ (ℤ_≥‘𝑀))
14	13	ad3antrrr 492	. . . . . . . . . . . . 13 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑆 ⊆ (ℤ_≥‘𝑀))
15		simpr 110	. . . . . . . . . . . . 13 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ 𝑆)
16	14, 15	sseldd 3243	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ (ℤ_≥‘𝑀))
17		eluzelz 9881	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
18	16, 17	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℤ)
19		simp2 1025	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑥 𝑥 ∈ 𝑆)
20		ssel2 3237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (ℤ_≥‘𝑀))
21		eluzel2 9876	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
22	20, 21	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
23	22	ex 115	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (𝑥 ∈ 𝑆 → 𝑀 ∈ ℤ))
24	23	exlimdv 1868	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (∃𝑥 𝑥 ∈ 𝑆 → 𝑀 ∈ ℤ))
25	13, 19, 24	sylc 62	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
26	25	ad3antrrr 492	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℤ)
27	18, 26	zsubcld 9723	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℤ)
28		eluzle 9884	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑘)
29	16, 28	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ≤ 𝑘)
30	18	zred 9718	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℝ)
31	26	zred 9718	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℝ)
32	30, 31	subge0d 8826	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (0 ≤ (𝑘 − 𝑀) ↔ 𝑀 ≤ 𝑘))
33	29, 32	mpbird 167	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 0 ≤ (𝑘 − 𝑀))
34		elnn0z 9607	. . . . . . . . . 10 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ ↔ ((𝑘 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑘 − 𝑀)))
35	27, 33, 34	sylanbrc 417	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℕ₀)
36		nn0p1nn 9552	. . . . . . . . 9 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ → ((𝑘 − 𝑀) + 1) ∈ ℕ)
37	35, 36	syl 14	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ ℕ)
38	27	zcnd 9719	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℂ)
39		1cnd 8306	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℂ)
40	38, 39	pncand 8601	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (((𝑘 − 𝑀) + 1) − 1) = (𝑘 − 𝑀))
41	40	oveq1d 6073	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = ((𝑘 − 𝑀) + 𝑀))
42	18	zcnd 9719	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℂ)
43	26	zcnd 9719	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℂ)
44	42, 43	npcand 8604	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 𝑀) = 𝑘)
45	41, 44	eqtrd 2267	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = 𝑘)
46	45, 15	eqeltrd 2311	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
47	12, 37, 46	elrabd 2978	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
48	8, 9, 47	rspcdva 2928	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ≤ ((𝑘 − 𝑀) + 1))
49		elrabi 2973	. . . . . . . . 9 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} → 𝑠 ∈ ℕ)
50	49	ad3antlr 493	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℕ)
51	50	nnred 9267	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℝ)
52		1red 8305	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℝ)
53	30, 31	resubcld 8671	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℝ)
54	51, 52, 53	lesubaddd 8833	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑠 − 1) ≤ (𝑘 − 𝑀) ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
55	48, 54	mpbird 167	. . . . 5 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ≤ (𝑘 − 𝑀))
56	51, 52	resubcld 8671	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ∈ ℝ)
57		leaddsub 8729	. . . . . 6 ⊢ (((𝑠 − 1) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑠 − 1) + 𝑀) ≤ 𝑘 ↔ (𝑠 − 1) ≤ (𝑘 − 𝑀)))
58	56, 31, 30, 57	syl3anc 1274	. . . . 5 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (((𝑠 − 1) + 𝑀) ≤ 𝑘 ↔ (𝑠 − 1) ≤ (𝑘 − 𝑀)))
59	55, 58	mpbird 167	. . . 4 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑠 − 1) + 𝑀) ≤ 𝑘)
60	59	ralrimiva 2617	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘)
61		breq1 4117	. . . . 5 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (𝑗 ≤ 𝑘 ↔ ((𝑠 − 1) + 𝑀) ≤ 𝑘))
62	61	ralbidv 2544	. . . 4 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ↔ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘))
63	62	rspcev 2923	. . 3 ⊢ ((((𝑠 − 1) + 𝑀) ∈ 𝑆 ∧ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
64	7, 60, 63	syl2anc 411	. 2 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
65		ssrab2 3327	. . 3 ⊢ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ
66		eluzelz 9881	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑥 ∈ ℤ)
67	20, 66	syl 14	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℤ)
68	67, 22	zsubcld 9723	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℤ)
69		1zzd 9621	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℤ)
70	68, 69	zaddcld 9722	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℤ)
71		oveq1 6065	. . . . . . . . . . 11 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (𝑝 − 1) = (((𝑥 − 𝑀) + 1) − 1))
72	71	oveq1d 6073	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑥 − 𝑀) + 1) − 1) + 𝑀))
73	72	eleq1d 2303	. . . . . . . . 9 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆))
74		eluzle 9884	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑥)
75	20, 74	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ≤ 𝑥)
76	67	zred 9718	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℝ)
77	22	zred 9718	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℝ)
78	76, 77	subge0d 8826	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (0 ≤ (𝑥 − 𝑀) ↔ 𝑀 ≤ 𝑥))
79	75, 78	mpbird 167	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 0 ≤ (𝑥 − 𝑀))
80		elnn0z 9607	. . . . . . . . . . 11 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ ↔ ((𝑥 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑥 − 𝑀)))
81	68, 79, 80	sylanbrc 417	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℕ₀)
82		nn0p1nn 9552	. . . . . . . . . 10 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ → ((𝑥 − 𝑀) + 1) ∈ ℕ)
83	81, 82	syl 14	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℕ)
84	68	zcnd 9719	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℂ)
85		1cnd 8306	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℂ)
86	84, 85	pncand 8601	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (((𝑥 − 𝑀) + 1) − 1) = (𝑥 − 𝑀))
87	86	oveq1d 6073	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
88	67	zcnd 9719	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ)
89	22	zcnd 9719	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℂ)
90	88, 89	npcand 8604	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
91	87, 90	eqtrd 2267	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = 𝑥)
92		simpr 110	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
93	91, 92	eqeltrd 2311	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
94	73, 83, 93	elrabd 2978	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
95		eleq1 2297	. . . . . . . . 9 ⊢ (𝑞 = ((𝑥 − 𝑀) + 1) → (𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
96	95	spcegv 2907	. . . . . . . 8 ⊢ (((𝑥 − 𝑀) + 1) ∈ ℤ → (((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
97	70, 94, 96	sylc 62	. . . . . . 7 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
98	97	ex 115	. . . . . 6 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (𝑥 ∈ 𝑆 → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
99	98	exlimdv 1868	. . . . 5 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
100	99	imp 124	. . . 4 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
101	100	3adant3 1044	. . 3 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
102		eleq1 2297	. . . . . . 7 ⊢ (𝑥 = ((𝑟 − 1) + 𝑀) → (𝑥 ∈ 𝑆 ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
103	102	dcbid 846	. . . . . 6 ⊢ (𝑥 = ((𝑟 − 1) + 𝑀) → (DECID 𝑥 ∈ 𝑆 ↔ DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆))
104		simpl3 1029	. . . . . 6 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆)
105	24	imp 124	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
106	105	3adant3 1044	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
107	106	adantr 276	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ∈ ℤ)
108		simpr 110	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑟 ∈ ℕ)
109	108	nnzd 9717	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑟 ∈ ℤ)
110		1zzd 9621	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 1 ∈ ℤ)
111	109, 110	zsubcld 9723	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℤ)
112	111, 107	zaddcld 9722	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ ℤ)
113		nnm1ge0 9682	. . . . . . . . 9 ⊢ (𝑟 ∈ ℕ → 0 ≤ (𝑟 − 1))
114	113	adantl 277	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 0 ≤ (𝑟 − 1))
115	107	zred 9718	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ∈ ℝ)
116	111	zred 9718	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℝ)
117	115, 116	addge02d 8825	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (0 ≤ (𝑟 − 1) ↔ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
118	114, 117	mpbid 147	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ≤ ((𝑟 − 1) + 𝑀))
119		eluz2 9877	. . . . . . 7 ⊢ (((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ ((𝑟 − 1) + 𝑀) ∈ ℤ ∧ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
120	107, 112, 118, 119	syl3anbrc 1208	. . . . . 6 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀))
121	103, 104, 120	rspcdva 2928	. . . . 5 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆)
122		oveq1 6065	. . . . . . . . . 10 ⊢ (𝑝 = 𝑟 → (𝑝 − 1) = (𝑟 − 1))
123	122	oveq1d 6073	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑝 − 1) + 𝑀) = ((𝑟 − 1) + 𝑀))
124	123	eleq1d 2303	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
125	124	elrab3 2977	. . . . . . 7 ⊢ (𝑟 ∈ ℕ → (𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
126	125	dcbid 846	. . . . . 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 2617	. . 3 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
130		nnwodc 12757	. . 3 ⊢ (({𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ ∧ ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ∧ ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
131	65, 101, 129, 130	mp3an2i 1379	. 2 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
132	64, 131	r19.29a 2688	1 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 842 ∧ w3a 1005 = wceq 1398 ∃wex 1541 ∈ wcel 2205 ∀wral 2522 ∃wrex 2523 {crab 2526 ⊆ wss 3214 class class class wbr 4114 ‘cfv 5357 (class class class)co 6058 ℝcr 8142 0cc0 8143 1c1 8144 + caddc 8146 ≤ cle 8325 − cmin 8460 ℕcn 9254 ℕ₀cn0 9513 ℤcz 9594 ℤ_≥cuz 9871

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-sep 4233 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-addcom 8243 ax-addass 8245 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-0id 8251 ax-rnegex 8252 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-apti 8258 ax-pre-ltadd 8259

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rmo 2530 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-id 4419 df-po 4422 df-iso 4423 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-isom 5366 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-sup 7288 df-inf 7289 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8462 df-neg 8463 df-inn 9255 df-n0 9514 df-z 9595 df-uz 9872 df-fz 10362 df-fzo 10499

This theorem is referenced by: (None)

W3C validator