Step | Hyp | Ref
| Expression |
1 | | infssuzledc.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | | infssuzledc.s |
. . . 4
⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓} |
3 | | infssuzledc.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
4 | | infssuzledc.dc |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓) |
5 | 1, 2, 3, 4 | infssuzex 11904 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑤 ∈ 𝑆 𝑤 < 𝑦))) |
6 | | ssrab2 3232 |
. . . . . . 7
⊢ {𝑛 ∈
(ℤ≥‘𝑀) ∣ 𝜓} ⊆
(ℤ≥‘𝑀) |
7 | 2, 6 | eqsstri 3179 |
. . . . . 6
⊢ 𝑆 ⊆
(ℤ≥‘𝑀) |
8 | | uzssz 9506 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
9 | 7, 8 | sstri 3156 |
. . . . 5
⊢ 𝑆 ⊆
ℤ |
10 | | zssre 9219 |
. . . . 5
⊢ ℤ
⊆ ℝ |
11 | 9, 10 | sstri 3156 |
. . . 4
⊢ 𝑆 ⊆
ℝ |
12 | 11 | a1i 9 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
13 | 5, 12 | infrenegsupex 9553 |
. 2
⊢ (𝜑 → inf(𝑆, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < )) |
14 | 1, 2, 3, 4 | infssuzex 11904 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦))) |
15 | 14, 12 | infsupneg 9555 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}𝑦 < 𝑧))) |
16 | | negeq 8112 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑢 → -𝑤 = -𝑢) |
17 | 16 | eleq1d 2239 |
. . . . . . . . 9
⊢ (𝑤 = 𝑢 → (-𝑤 ∈ 𝑆 ↔ -𝑢 ∈ 𝑆)) |
18 | 17 | elrab 2886 |
. . . . . . . 8
⊢ (𝑢 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆} ↔ (𝑢 ∈ ℝ ∧ -𝑢 ∈ 𝑆)) |
19 | 9 | sseli 3143 |
. . . . . . . . . 10
⊢ (-𝑢 ∈ 𝑆 → -𝑢 ∈ ℤ) |
20 | 19 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℝ ∧ -𝑢 ∈ 𝑆) → -𝑢 ∈ ℤ) |
21 | | simpl 108 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℝ ∧ -𝑢 ∈ 𝑆) → 𝑢 ∈ ℝ) |
22 | 21 | recnd 7948 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ℝ ∧ -𝑢 ∈ 𝑆) → 𝑢 ∈ ℂ) |
23 | | znegclb 9245 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ℂ → (𝑢 ∈ ℤ ↔ -𝑢 ∈
ℤ)) |
24 | 22, 23 | syl 14 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℝ ∧ -𝑢 ∈ 𝑆) → (𝑢 ∈ ℤ ↔ -𝑢 ∈ ℤ)) |
25 | 20, 24 | mpbird 166 |
. . . . . . . 8
⊢ ((𝑢 ∈ ℝ ∧ -𝑢 ∈ 𝑆) → 𝑢 ∈ ℤ) |
26 | 18, 25 | sylbi 120 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆} → 𝑢 ∈ ℤ) |
27 | 26 | ssriv 3151 |
. . . . . 6
⊢ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆} ⊆ ℤ |
28 | 27 | a1i 9 |
. . . . 5
⊢ (𝜑 → {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆} ⊆ ℤ) |
29 | 15, 28 | suprzclex 9310 |
. . . 4
⊢ (𝜑 → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}) |
30 | | nfrab1 2649 |
. . . . . 6
⊢
Ⅎ𝑤{𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆} |
31 | | nfcv 2312 |
. . . . . 6
⊢
Ⅎ𝑤ℝ |
32 | | nfcv 2312 |
. . . . . 6
⊢
Ⅎ𝑤
< |
33 | 30, 31, 32 | nfsup 6969 |
. . . . 5
⊢
Ⅎ𝑤sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) |
34 | 33 | nfneg 8116 |
. . . . . 6
⊢
Ⅎ𝑤-sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) |
35 | 34 | nfel1 2323 |
. . . . 5
⊢
Ⅎ𝑤-sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) ∈ 𝑆 |
36 | | negeq 8112 |
. . . . . 6
⊢ (𝑤 = sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) → -𝑤 = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < )) |
37 | 36 | eleq1d 2239 |
. . . . 5
⊢ (𝑤 = sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) → (-𝑤 ∈ 𝑆 ↔ -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) ∈ 𝑆)) |
38 | 33, 31, 35, 37 | elrabf 2884 |
. . . 4
⊢
(sup({𝑤 ∈
ℝ ∣ -𝑤 ∈
𝑆}, ℝ, < ) ∈
{𝑤 ∈ ℝ ∣
-𝑤 ∈ 𝑆} ↔ (sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) ∈ ℝ ∧
-sup({𝑤 ∈ ℝ
∣ -𝑤 ∈ 𝑆}, ℝ, < ) ∈ 𝑆)) |
39 | 29, 38 | sylib 121 |
. . 3
⊢ (𝜑 → (sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) ∈ ℝ ∧
-sup({𝑤 ∈ ℝ
∣ -𝑤 ∈ 𝑆}, ℝ, < ) ∈ 𝑆)) |
40 | 39 | simprd 113 |
. 2
⊢ (𝜑 → -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝑆}, ℝ, < ) ∈ 𝑆) |
41 | 13, 40 | eqeltrd 2247 |
1
⊢ (𝜑 → inf(𝑆, ℝ, < ) ∈ 𝑆) |