Step | Hyp | Ref
| Expression |
1 | | lttri3 7999 |
. . . . . 6
⊢ ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓))) |
2 | 1 | adantl 275 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓))) |
3 | | suprzclex.ex |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
4 | 2, 3 | supclti 6975 |
. . . 4
⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈
ℝ) |
5 | 4 | ltm1d 8848 |
. . 3
⊢ (𝜑 → (sup(𝐴, ℝ, < ) − 1) < sup(𝐴, ℝ, <
)) |
6 | | suprzclex.ss |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℤ) |
7 | | zssre 9219 |
. . . . 5
⊢ ℤ
⊆ ℝ |
8 | 6, 7 | sstrdi 3159 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
9 | | peano2rem 8186 |
. . . . 5
⊢
(sup(𝐴, ℝ,
< ) ∈ ℝ → (sup(𝐴, ℝ, < ) − 1) ∈
ℝ) |
10 | 4, 9 | syl 14 |
. . . 4
⊢ (𝜑 → (sup(𝐴, ℝ, < ) − 1) ∈
ℝ) |
11 | 3, 8, 10 | suprlubex 8868 |
. . 3
⊢ (𝜑 → ((sup(𝐴, ℝ, < ) − 1) < sup(𝐴, ℝ, < ) ↔
∃𝑧 ∈ 𝐴 (sup(𝐴, ℝ, < ) − 1) < 𝑧)) |
12 | 5, 11 | mpbid 146 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ 𝐴 (sup(𝐴, ℝ, < ) − 1) < 𝑧) |
13 | 6 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → 𝐴 ⊆ ℤ) |
14 | 13 | sselda 3147 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℤ) |
15 | 7, 14 | sselid 3145 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ) |
16 | 4 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → sup(𝐴, ℝ, < ) ∈
ℝ) |
17 | 16 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → sup(𝐴, ℝ, < ) ∈
ℝ) |
18 | | simprl 526 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → 𝑧 ∈ 𝐴) |
19 | 13, 18 | sseldd 3148 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → 𝑧 ∈ ℤ) |
20 | | zre 9216 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
21 | 19, 20 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → 𝑧 ∈ ℝ) |
22 | | peano2re 8055 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → (𝑧 + 1) ∈
ℝ) |
23 | 21, 22 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → (𝑧 + 1) ∈ ℝ) |
24 | 23 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → (𝑧 + 1) ∈ ℝ) |
25 | 3 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
26 | 8 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → 𝐴 ⊆ ℝ) |
27 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ 𝐴) |
28 | 25, 26, 27 | suprubex 8867 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ≤ sup(𝐴, ℝ, < )) |
29 | | simprr 527 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → (sup(𝐴, ℝ, < ) − 1) < 𝑧) |
30 | | 1red 7935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → 1 ∈
ℝ) |
31 | 16, 30, 21 | ltsubaddd 8460 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → ((sup(𝐴, ℝ, < ) − 1)
< 𝑧 ↔ sup(𝐴, ℝ, < ) < (𝑧 + 1))) |
32 | 29, 31 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → sup(𝐴, ℝ, < ) < (𝑧 + 1)) |
33 | 32 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → sup(𝐴, ℝ, < ) < (𝑧 + 1)) |
34 | 15, 17, 24, 28, 33 | lelttrd 8044 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → 𝑤 < (𝑧 + 1)) |
35 | 19 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → 𝑧 ∈ ℤ) |
36 | | zleltp1 9267 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑤 ≤ 𝑧 ↔ 𝑤 < (𝑧 + 1))) |
37 | 14, 35, 36 | syl2anc 409 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → (𝑤 ≤ 𝑧 ↔ 𝑤 < (𝑧 + 1))) |
38 | 34, 37 | mpbird 166 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ≤ 𝑧) |
39 | 38 | ralrimiva 2543 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → ∀𝑤 ∈ 𝐴 𝑤 ≤ 𝑧) |
40 | | breq2 3993 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑤 → (𝑦 < 𝑧 ↔ 𝑦 < 𝑤)) |
41 | 40 | cbvrexv 2697 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
𝐴 𝑦 < 𝑧 ↔ ∃𝑤 ∈ 𝐴 𝑦 < 𝑤) |
42 | 41 | imbi2i 225 |
. . . . . . . . . . 11
⊢ ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑤 ∈ 𝐴 𝑦 < 𝑤)) |
43 | 42 | ralbii 2476 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑤 ∈ 𝐴 𝑦 < 𝑤)) |
44 | 43 | anbi2i 454 |
. . . . . . . . 9
⊢
((∀𝑦 ∈
𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑤 ∈ 𝐴 𝑦 < 𝑤))) |
45 | 44 | rexbii 2477 |
. . . . . . . 8
⊢
(∃𝑥 ∈
ℝ (∀𝑦 ∈
𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑤 ∈ 𝐴 𝑦 < 𝑤))) |
46 | 3, 45 | sylib 121 |
. . . . . . 7
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑤 ∈ 𝐴 𝑦 < 𝑤))) |
47 | 46 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑤 ∈ 𝐴 𝑦 < 𝑤))) |
48 | 13, 7 | sstrdi 3159 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → 𝐴 ⊆ ℝ) |
49 | 47, 48, 21 | suprleubex 8870 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → (sup(𝐴, ℝ, < ) ≤ 𝑧 ↔ ∀𝑤 ∈ 𝐴 𝑤 ≤ 𝑧)) |
50 | 39, 49 | mpbird 166 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → sup(𝐴, ℝ, < ) ≤ 𝑧) |
51 | 47, 48, 18 | suprubex 8867 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → 𝑧 ≤ sup(𝐴, ℝ, < )) |
52 | 16, 21 | letri3d 8035 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → (sup(𝐴, ℝ, < ) = 𝑧 ↔ (sup(𝐴, ℝ, < ) ≤ 𝑧 ∧ 𝑧 ≤ sup(𝐴, ℝ, < )))) |
53 | 50, 51, 52 | mpbir2and 939 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → sup(𝐴, ℝ, < ) = 𝑧) |
54 | 53, 18 | eqeltrd 2247 |
. 2
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ (sup(𝐴, ℝ, < ) − 1) < 𝑧)) → sup(𝐴, ℝ, < ) ∈ 𝐴) |
55 | 12, 54 | rexlimddv 2592 |
1
⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ 𝐴) |