uzwodc - Intuitionistic Logic Explorer

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

Theorem uzwodc 12473

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 5974	. . . . . . . 8 ⊢ (𝑝 = 𝑠 → (𝑝 − 1) = (𝑠 − 1))
3	2	oveq1d 5982	. . . . . . 7 ⊢ (𝑝 = 𝑠 → ((𝑝 − 1) + 𝑀) = ((𝑠 − 1) + 𝑀))
4	3	eleq1d 2276	. . . . . 6 ⊢ (𝑝 = 𝑠 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
5	4	elrab 2936	. . . . 5 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
6	1, 5	sylib 122	. . . 4 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
7	6	simprd 114	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ((𝑠 − 1) + 𝑀) ∈ 𝑆)
8		breq2 4063	. . . . . . 7 ⊢ (𝑡 = ((𝑘 − 𝑀) + 1) → (𝑠 ≤ 𝑡 ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
9		simplr 528	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
10		oveq1 5974	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → (𝑝 − 1) = (((𝑘 − 𝑀) + 1) − 1))
11	10	oveq1d 5982	. . . . . . . . 9 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑘 − 𝑀) + 1) − 1) + 𝑀))
12	11	eleq1d 2276	. . . . . . . 8 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆))
13		simp1 1000	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑆 ⊆ (ℤ_≥‘𝑀))
14	13	ad3antrrr 492	. . . . . . . . . . . . 13 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑆 ⊆ (ℤ_≥‘𝑀))
15		simpr 110	. . . . . . . . . . . . 13 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ 𝑆)
16	14, 15	sseldd 3202	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ (ℤ_≥‘𝑀))
17		eluzelz 9692	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
18	16, 17	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℤ)
19		simp2 1001	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑥 𝑥 ∈ 𝑆)
20		ssel2 3196	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (ℤ_≥‘𝑀))
21		eluzel2 9688	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
22	20, 21	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
23	22	ex 115	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (𝑥 ∈ 𝑆 → 𝑀 ∈ ℤ))
24	23	exlimdv 1843	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (∃𝑥 𝑥 ∈ 𝑆 → 𝑀 ∈ ℤ))
25	13, 19, 24	sylc 62	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
26	25	ad3antrrr 492	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℤ)
27	18, 26	zsubcld 9535	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℤ)
28		eluzle 9695	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑘)
29	16, 28	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ≤ 𝑘)
30	18	zred 9530	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℝ)
31	26	zred 9530	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℝ)
32	30, 31	subge0d 8643	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (0 ≤ (𝑘 − 𝑀) ↔ 𝑀 ≤ 𝑘))
33	29, 32	mpbird 167	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 0 ≤ (𝑘 − 𝑀))
34		elnn0z 9420	. . . . . . . . . 10 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ ↔ ((𝑘 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑘 − 𝑀)))
35	27, 33, 34	sylanbrc 417	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℕ₀)
36		nn0p1nn 9369	. . . . . . . . 9 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ → ((𝑘 − 𝑀) + 1) ∈ ℕ)
37	35, 36	syl 14	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ ℕ)
38	27	zcnd 9531	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℂ)
39		1cnd 8123	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℂ)
40	38, 39	pncand 8419	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (((𝑘 − 𝑀) + 1) − 1) = (𝑘 − 𝑀))
41	40	oveq1d 5982	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = ((𝑘 − 𝑀) + 𝑀))
42	18	zcnd 9531	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℂ)
43	26	zcnd 9531	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℂ)
44	42, 43	npcand 8422	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 𝑀) = 𝑘)
45	41, 44	eqtrd 2240	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = 𝑘)
46	45, 15	eqeltrd 2284	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
47	12, 37, 46	elrabd 2938	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
48	8, 9, 47	rspcdva 2889	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ≤ ((𝑘 − 𝑀) + 1))
49		elrabi 2933	. . . . . . . . 9 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} → 𝑠 ∈ ℕ)
50	49	ad3antlr 493	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℕ)
51	50	nnred 9084	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℝ)
52		1red 8122	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℝ)
53	30, 31	resubcld 8488	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℝ)
54	51, 52, 53	lesubaddd 8650	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑠 − 1) ≤ (𝑘 − 𝑀) ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
55	48, 54	mpbird 167	. . . . 5 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ≤ (𝑘 − 𝑀))
56	51, 52	resubcld 8488	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ∈ ℝ)
57		leaddsub 8546	. . . . . 6 ⊢ (((𝑠 − 1) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑠 − 1) + 𝑀) ≤ 𝑘 ↔ (𝑠 − 1) ≤ (𝑘 − 𝑀)))
58	56, 31, 30, 57	syl3anc 1250	. . . . 5 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (((𝑠 − 1) + 𝑀) ≤ 𝑘 ↔ (𝑠 − 1) ≤ (𝑘 − 𝑀)))
59	55, 58	mpbird 167	. . . 4 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑠 − 1) + 𝑀) ≤ 𝑘)
60	59	ralrimiva 2581	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘)
61		breq1 4062	. . . . 5 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (𝑗 ≤ 𝑘 ↔ ((𝑠 − 1) + 𝑀) ≤ 𝑘))
62	61	ralbidv 2508	. . . 4 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ↔ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘))
63	62	rspcev 2884	. . 3 ⊢ ((((𝑠 − 1) + 𝑀) ∈ 𝑆 ∧ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
64	7, 60, 63	syl2anc 411	. 2 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
65		ssrab2 3286	. . 3 ⊢ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ
66		eluzelz 9692	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑥 ∈ ℤ)
67	20, 66	syl 14	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℤ)
68	67, 22	zsubcld 9535	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℤ)
69		1zzd 9434	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℤ)
70	68, 69	zaddcld 9534	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℤ)
71		oveq1 5974	. . . . . . . . . . 11 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (𝑝 − 1) = (((𝑥 − 𝑀) + 1) − 1))
72	71	oveq1d 5982	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑥 − 𝑀) + 1) − 1) + 𝑀))
73	72	eleq1d 2276	. . . . . . . . 9 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆))
74		eluzle 9695	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑥)
75	20, 74	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ≤ 𝑥)
76	67	zred 9530	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℝ)
77	22	zred 9530	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℝ)
78	76, 77	subge0d 8643	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (0 ≤ (𝑥 − 𝑀) ↔ 𝑀 ≤ 𝑥))
79	75, 78	mpbird 167	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 0 ≤ (𝑥 − 𝑀))
80		elnn0z 9420	. . . . . . . . . . 11 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ ↔ ((𝑥 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑥 − 𝑀)))
81	68, 79, 80	sylanbrc 417	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℕ₀)
82		nn0p1nn 9369	. . . . . . . . . 10 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ → ((𝑥 − 𝑀) + 1) ∈ ℕ)
83	81, 82	syl 14	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℕ)
84	68	zcnd 9531	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℂ)
85		1cnd 8123	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℂ)
86	84, 85	pncand 8419	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (((𝑥 − 𝑀) + 1) − 1) = (𝑥 − 𝑀))
87	86	oveq1d 5982	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
88	67	zcnd 9531	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ)
89	22	zcnd 9531	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℂ)
90	88, 89	npcand 8422	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
91	87, 90	eqtrd 2240	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = 𝑥)
92		simpr 110	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
93	91, 92	eqeltrd 2284	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
94	73, 83, 93	elrabd 2938	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
95		eleq1 2270	. . . . . . . . 9 ⊢ (𝑞 = ((𝑥 − 𝑀) + 1) → (𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
96	95	spcegv 2868	. . . . . . . 8 ⊢ (((𝑥 − 𝑀) + 1) ∈ ℤ → (((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
97	70, 94, 96	sylc 62	. . . . . . 7 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
98	97	ex 115	. . . . . 6 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (𝑥 ∈ 𝑆 → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
99	98	exlimdv 1843	. . . . 5 ⊢ (𝑆 ⊆ (ℤ_≥‘𝑀) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
100	99	imp 124	. . . 4 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
101	100	3adant3 1020	. . 3 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
102		eleq1 2270	. . . . . . 7 ⊢ (𝑥 = ((𝑟 − 1) + 𝑀) → (𝑥 ∈ 𝑆 ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
103	102	dcbid 840	. . . . . 6 ⊢ (𝑥 = ((𝑟 − 1) + 𝑀) → (DECID 𝑥 ∈ 𝑆 ↔ DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆))
104		simpl3 1005	. . . . . 6 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆)
105	24	imp 124	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
106	105	3adant3 1020	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → 𝑀 ∈ ℤ)
107	106	adantr 276	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ∈ ℤ)
108		simpr 110	. . . . . . . . . 10 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑟 ∈ ℕ)
109	108	nnzd 9529	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑟 ∈ ℤ)
110		1zzd 9434	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 1 ∈ ℤ)
111	109, 110	zsubcld 9535	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℤ)
112	111, 107	zaddcld 9534	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ ℤ)
113		nnm1ge0 9494	. . . . . . . . 9 ⊢ (𝑟 ∈ ℕ → 0 ≤ (𝑟 − 1))
114	113	adantl 277	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 0 ≤ (𝑟 − 1))
115	107	zred 9530	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ∈ ℝ)
116	111	zred 9530	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℝ)
117	115, 116	addge02d 8642	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (0 ≤ (𝑟 − 1) ↔ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
118	114, 117	mpbid 147	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ≤ ((𝑟 − 1) + 𝑀))
119		eluz2 9689	. . . . . . 7 ⊢ (((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ ((𝑟 − 1) + 𝑀) ∈ ℤ ∧ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
120	107, 112, 118, 119	syl3anbrc 1184	. . . . . 6 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀))
121	103, 104, 120	rspcdva 2889	. . . . 5 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆)
122		oveq1 5974	. . . . . . . . . 10 ⊢ (𝑝 = 𝑟 → (𝑝 − 1) = (𝑟 − 1))
123	122	oveq1d 5982	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑝 − 1) + 𝑀) = ((𝑟 − 1) + 𝑀))
124	123	eleq1d 2276	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
125	124	elrab3 2937	. . . . . . 7 ⊢ (𝑟 ∈ ℕ → (𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
126	125	dcbid 840	. . . . . 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 2581	. . 3 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
130		nnwodc 12472	. . 3 ⊢ (({𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ ∧ ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ∧ ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
131	65, 101, 129, 130	mp3an2i 1355	. 2 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
132	64, 131	r19.29a 2651	1 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 836 ∧ w3a 981 = wceq 1373 ∃wex 1516 ∈ wcel 2178 ∀wral 2486 ∃wrex 2487 {crab 2490 ⊆ wss 3174 class class class wbr 4059 ‘cfv 5290 (class class class)co 5967 ℝcr 7959 0cc0 7960 1c1 7961 + caddc 7963 ≤ cle 8143 − cmin 8278 ℕcn 9071 ℕ₀cn0 9330 ℤcz 9407 ℤ_≥cuz 9683

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-sep 4178 ax-pow 4234 ax-pr 4269 ax-un 4498 ax-setind 4603 ax-cnex 8051 ax-resscn 8052 ax-1cn 8053 ax-1re 8054 ax-icn 8055 ax-addcl 8056 ax-addrcl 8057 ax-mulcl 8058 ax-addcom 8060 ax-addass 8062 ax-distr 8064 ax-i2m1 8065 ax-0lt1 8066 ax-0id 8068 ax-rnegex 8069 ax-cnre 8071 ax-pre-ltirr 8072 ax-pre-ltwlin 8073 ax-pre-lttrn 8074 ax-pre-apti 8075 ax-pre-ltadd 8076

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-nel 2474 df-ral 2491 df-rex 2492 df-reu 2493 df-rmo 2494 df-rab 2495 df-v 2778 df-sbc 3006 df-csb 3102 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-int 3900 df-iun 3943 df-br 4060 df-opab 4122 df-mpt 4123 df-id 4358 df-po 4361 df-iso 4362 df-xp 4699 df-rel 4700 df-cnv 4701 df-co 4702 df-dm 4703 df-rn 4704 df-res 4705 df-ima 4706 df-iota 5251 df-fun 5292 df-fn 5293 df-f 5294 df-f1 5295 df-fo 5296 df-f1o 5297 df-fv 5298 df-isom 5299 df-riota 5922 df-ov 5970 df-oprab 5971 df-mpo 5972 df-1st 6249 df-2nd 6250 df-sup 7112 df-inf 7113 df-pnf 8144 df-mnf 8145 df-xr 8146 df-ltxr 8147 df-le 8148 df-sub 8280 df-neg 8281 df-inn 9072 df-n0 9331 df-z 9408 df-uz 9684 df-fz 10166 df-fzo 10300

This theorem is referenced by: (None)

W3C validator