uzwodc - Intuitionistic Logic Explorer

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

Theorem uzwodc 12733

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 6057	. . . . . . . 8 ⊢ (𝑝 = 𝑠 → (𝑝 − 1) = (𝑠 − 1))
3	2	oveq1d 6065	. . . . . . 7 ⊢ (𝑝 = 𝑠 → ((𝑝 − 1) + 𝑀) = ((𝑠 − 1) + 𝑀))
4	3	eleq1d 2301	. . . . . 6 ⊢ (𝑝 = 𝑠 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
5	4	elrab 2973	. . . . 5 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
6	1, 5	sylib 122	. . . 4 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → (𝑠 ∈ ℕ ∧ ((𝑠 − 1) + 𝑀) ∈ 𝑆))
7	6	simprd 114	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ((𝑠 − 1) + 𝑀) ∈ 𝑆)
8		breq2 4113	. . . . . . 7 ⊢ (𝑡 = ((𝑘 − 𝑀) + 1) → (𝑠 ≤ 𝑡 ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
9		simplr 529	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
10		oveq1 6057	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → (𝑝 − 1) = (((𝑘 − 𝑀) + 1) − 1))
11	10	oveq1d 6065	. . . . . . . . 9 ⊢ (𝑝 = ((𝑘 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑘 − 𝑀) + 1) − 1) + 𝑀))
12	11	eleq1d 2301	. . . . . . . 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 3239	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ (ℤ_≥‘𝑀))
17		eluzelz 9863	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
18	16, 17	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℤ)
19		simp2 1025	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑥 𝑥 ∈ 𝑆)
20		ssel2 3233	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (ℤ_≥‘𝑀))
21		eluzel2 9858	. . . . . . . . . . . . . . . 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 9705	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℤ)
28		eluzle 9866	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑘)
29	16, 28	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ≤ 𝑘)
30	18	zred 9700	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℝ)
31	26	zred 9700	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℝ)
32	30, 31	subge0d 8809	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (0 ≤ (𝑘 − 𝑀) ↔ 𝑀 ≤ 𝑘))
33	29, 32	mpbird 167	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 0 ≤ (𝑘 − 𝑀))
34		elnn0z 9590	. . . . . . . . . 10 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ ↔ ((𝑘 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑘 − 𝑀)))
35	27, 33, 34	sylanbrc 417	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℕ₀)
36		nn0p1nn 9535	. . . . . . . . 9 ⊢ ((𝑘 − 𝑀) ∈ ℕ₀ → ((𝑘 − 𝑀) + 1) ∈ ℕ)
37	35, 36	syl 14	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ ℕ)
38	27	zcnd 9701	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℂ)
39		1cnd 8290	. . . . . . . . . . . 12 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℂ)
40	38, 39	pncand 8585	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (((𝑘 − 𝑀) + 1) − 1) = (𝑘 − 𝑀))
41	40	oveq1d 6065	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = ((𝑘 − 𝑀) + 𝑀))
42	18	zcnd 9701	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ ℂ)
43	26	zcnd 9701	. . . . . . . . . . 11 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑀 ∈ ℂ)
44	42, 43	npcand 8588	. . . . . . . . . 10 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 𝑀) = 𝑘)
45	41, 44	eqtrd 2265	. . . . . . . . 9 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) = 𝑘)
46	45, 15	eqeltrd 2309	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((((𝑘 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
47	12, 37, 46	elrabd 2975	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑘 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
48	8, 9, 47	rspcdva 2926	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ≤ ((𝑘 − 𝑀) + 1))
49		elrabi 2970	. . . . . . . . 9 ⊢ (𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} → 𝑠 ∈ ℕ)
50	49	ad3antlr 493	. . . . . . . 8 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℕ)
51	50	nnred 9250	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 𝑠 ∈ ℝ)
52		1red 8289	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → 1 ∈ ℝ)
53	30, 31	resubcld 8654	. . . . . . 7 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑘 − 𝑀) ∈ ℝ)
54	51, 52, 53	lesubaddd 8816	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → ((𝑠 − 1) ≤ (𝑘 − 𝑀) ↔ 𝑠 ≤ ((𝑘 − 𝑀) + 1)))
55	48, 54	mpbird 167	. . . . 5 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ≤ (𝑘 − 𝑀))
56	51, 52	resubcld 8654	. . . . . 6 ⊢ (((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) ∧ 𝑘 ∈ 𝑆) → (𝑠 − 1) ∈ ℝ)
57		leaddsub 8712	. . . . . 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 2615	. . 3 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘)
61		breq1 4112	. . . . 5 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (𝑗 ≤ 𝑘 ↔ ((𝑠 − 1) + 𝑀) ≤ 𝑘))
62	61	ralbidv 2542	. . . 4 ⊢ (𝑗 = ((𝑠 − 1) + 𝑀) → (∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ↔ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘))
63	62	rspcev 2921	. . 3 ⊢ ((((𝑠 − 1) + 𝑀) ∈ 𝑆 ∧ ∀𝑘 ∈ 𝑆 ((𝑠 − 1) + 𝑀) ≤ 𝑘) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
64	7, 60, 63	syl2anc 411	. 2 ⊢ ((((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) ∧ ∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
65		ssrab2 3323	. . 3 ⊢ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ
66		eluzelz 9863	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑥 ∈ ℤ)
67	20, 66	syl 14	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℤ)
68	67, 22	zsubcld 9705	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℤ)
69		1zzd 9604	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℤ)
70	68, 69	zaddcld 9704	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℤ)
71		oveq1 6057	. . . . . . . . . . 11 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (𝑝 − 1) = (((𝑥 − 𝑀) + 1) − 1))
72	71	oveq1d 6065	. . . . . . . . . 10 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → ((𝑝 − 1) + 𝑀) = ((((𝑥 − 𝑀) + 1) − 1) + 𝑀))
73	72	eleq1d 2301	. . . . . . . . 9 ⊢ (𝑝 = ((𝑥 − 𝑀) + 1) → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆))
74		eluzle 9866	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝑥)
75	20, 74	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ≤ 𝑥)
76	67	zred 9700	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℝ)
77	22	zred 9700	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℝ)
78	76, 77	subge0d 8809	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (0 ≤ (𝑥 − 𝑀) ↔ 𝑀 ≤ 𝑥))
79	75, 78	mpbird 167	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 0 ≤ (𝑥 − 𝑀))
80		elnn0z 9590	. . . . . . . . . . 11 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ ↔ ((𝑥 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑥 − 𝑀)))
81	68, 79, 80	sylanbrc 417	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℕ₀)
82		nn0p1nn 9535	. . . . . . . . . 10 ⊢ ((𝑥 − 𝑀) ∈ ℕ₀ → ((𝑥 − 𝑀) + 1) ∈ ℕ)
83	81, 82	syl 14	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ ℕ)
84	68	zcnd 9701	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝑀) ∈ ℂ)
85		1cnd 8290	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℂ)
86	84, 85	pncand 8585	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → (((𝑥 − 𝑀) + 1) − 1) = (𝑥 − 𝑀))
87	86	oveq1d 6065	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
88	67	zcnd 9701	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ)
89	22	zcnd 9701	. . . . . . . . . . . 12 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ ℂ)
90	88, 89	npcand 8588	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
91	87, 90	eqtrd 2265	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) = 𝑥)
92		simpr 110	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
93	91, 92	eqeltrd 2309	. . . . . . . . 9 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((((𝑥 − 𝑀) + 1) − 1) + 𝑀) ∈ 𝑆)
94	73, 83, 93	elrabd 2975	. . . . . . . 8 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
95		eleq1 2295	. . . . . . . . 9 ⊢ (𝑞 = ((𝑥 − 𝑀) + 1) → (𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ↔ ((𝑥 − 𝑀) + 1) ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}))
96	95	spcegv 2905	. . . . . . . 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 2295	. . . . . . 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 9699	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑟 ∈ ℤ)
110		1zzd 9604	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 1 ∈ ℤ)
111	109, 110	zsubcld 9705	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℤ)
112	111, 107	zaddcld 9704	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ ℤ)
113		nnm1ge0 9664	. . . . . . . . 9 ⊢ (𝑟 ∈ ℕ → 0 ≤ (𝑟 − 1))
114	113	adantl 277	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 0 ≤ (𝑟 − 1))
115	107	zred 9700	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ∈ ℝ)
116	111	zred 9700	. . . . . . . . 9 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (𝑟 − 1) ∈ ℝ)
117	115, 116	addge02d 8808	. . . . . . . 8 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → (0 ≤ (𝑟 − 1) ↔ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
118	114, 117	mpbid 147	. . . . . . 7 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → 𝑀 ≤ ((𝑟 − 1) + 𝑀))
119		eluz2 9859	. . . . . . 7 ⊢ (((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ ((𝑟 − 1) + 𝑀) ∈ ℤ ∧ 𝑀 ≤ ((𝑟 − 1) + 𝑀)))
120	107, 112, 118, 119	syl3anbrc 1208	. . . . . 6 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → ((𝑟 − 1) + 𝑀) ∈ (ℤ_≥‘𝑀))
121	103, 104, 120	rspcdva 2926	. . . . 5 ⊢ (((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) ∧ 𝑟 ∈ ℕ) → DECID ((𝑟 − 1) + 𝑀) ∈ 𝑆)
122		oveq1 6057	. . . . . . . . . 10 ⊢ (𝑝 = 𝑟 → (𝑝 − 1) = (𝑟 − 1))
123	122	oveq1d 6065	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑝 − 1) + 𝑀) = ((𝑟 − 1) + 𝑀))
124	123	eleq1d 2301	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑝 − 1) + 𝑀) ∈ 𝑆 ↔ ((𝑟 − 1) + 𝑀) ∈ 𝑆))
125	124	elrab3 2974	. . . . . . 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 2615	. . 3 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆})
130		nnwodc 12732	. . 3 ⊢ (({𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ⊆ ℕ ∧ ∃𝑞 𝑞 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆} ∧ ∀𝑟 ∈ ℕ DECID 𝑟 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
131	65, 101, 129, 130	mp3an2i 1379	. 2 ⊢ ((𝑆 ⊆ (ℤ_≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑠 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}∀𝑡 ∈ {𝑝 ∈ ℕ ∣ ((𝑝 − 1) + 𝑀) ∈ 𝑆}𝑠 ≤ 𝑡)
132	64, 131	r19.29a 2686	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 2203 ∀wral 2520 ∃wrex 2521 {crab 2524 ⊆ wss 3211 class class class wbr 4109 ‘cfv 5352 (class class class)co 6050 ℝcr 8126 0cc0 8127 1c1 8128 + caddc 8130 ≤ cle 8309 − cmin 8444 ℕcn 9237 ℕ₀cn0 9496 ℤcz 9577 ℤ_≥cuz 9853

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 2205 ax-14 2206 ax-ext 2214 ax-sep 4228 ax-pow 4287 ax-pr 4322 ax-un 4554 ax-setind 4659 ax-cnex 8218 ax-resscn 8219 ax-1cn 8220 ax-1re 8221 ax-icn 8222 ax-addcl 8223 ax-addrcl 8224 ax-mulcl 8225 ax-addcom 8227 ax-addass 8229 ax-distr 8231 ax-i2m1 8232 ax-0lt1 8233 ax-0id 8235 ax-rnegex 8236 ax-cnre 8238 ax-pre-ltirr 8239 ax-pre-ltwlin 8240 ax-pre-lttrn 8241 ax-pre-apti 8242 ax-pre-ltadd 8243

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 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rmo 2528 df-rab 2529 df-v 2815 df-sbc 3043 df-csb 3139 df-dif 3213 df-un 3215 df-in 3217 df-ss 3224 df-pw 3671 df-sn 3695 df-pr 3696 df-op 3698 df-uni 3915 df-int 3950 df-iun 3993 df-br 4110 df-opab 4172 df-mpt 4173 df-id 4414 df-po 4417 df-iso 4418 df-xp 4755 df-rel 4756 df-cnv 4757 df-co 4758 df-dm 4759 df-rn 4760 df-res 4761 df-ima 4762 df-iota 5312 df-fun 5354 df-fn 5355 df-f 5356 df-f1 5357 df-fo 5358 df-f1o 5359 df-fv 5360 df-isom 5361 df-riota 6003 df-ov 6053 df-oprab 6054 df-mpo 6055 df-1st 6334 df-2nd 6335 df-sup 7275 df-inf 7276 df-pnf 8310 df-mnf 8311 df-xr 8312 df-ltxr 8313 df-le 8314 df-sub 8446 df-neg 8447 df-inn 9238 df-n0 9497 df-z 9578 df-uz 9854 df-fz 10343 df-fzo 10477

This theorem is referenced by: (None)

W3C validator