Step | Hyp | Ref
| Expression |
1 | | negn0 10459 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ≠ ∅) |
2 | | ublbneg 11773 |
. . . . 5
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) |
3 | | ssrab2 3687 |
. . . . . 6
⊢ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ⊆ ℝ |
4 | | infrenegsup 11006 |
. . . . . 6
⊢ (({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ⊆ ℝ ∧ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) → inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}}, ℝ, < )) |
5 | 3, 4 | mp3an1 1411 |
. . . . 5
⊢ (({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) → inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}}, ℝ, < )) |
6 | 1, 2, 5 | syl2an 494 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}}, ℝ, < )) |
7 | 6 | 3impa 1259 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) = -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}}, ℝ, < )) |
8 | | elrabi 3359 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}} → 𝑥 ∈ ℝ) |
9 | 8 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}}) → 𝑥 ∈ ℝ) |
10 | | ssel2 3598 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
11 | | negeq 10273 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → -𝑤 = -𝑥) |
12 | 11 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (-𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ↔ -𝑥 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴})) |
13 | 12 | elrab3 3364 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}} ↔ -𝑥 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴})) |
14 | | renegcl 10344 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → -𝑥 ∈
ℝ) |
15 | | negeq 10273 |
. . . . . . . . . . . 12
⊢ (𝑧 = -𝑥 → -𝑧 = --𝑥) |
16 | 15 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑧 = -𝑥 → (-𝑧 ∈ 𝐴 ↔ --𝑥 ∈ 𝐴)) |
17 | 16 | elrab3 3364 |
. . . . . . . . . 10
⊢ (-𝑥 ∈ ℝ → (-𝑥 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ↔ --𝑥 ∈ 𝐴)) |
18 | 14, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (-𝑥 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ↔ --𝑥 ∈ 𝐴)) |
19 | | recn 10026 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
20 | 19 | negnegd 10383 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → --𝑥 = 𝑥) |
21 | 20 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (--𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
22 | 13, 18, 21 | 3bitrd 294 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}} ↔ 𝑥 ∈ 𝐴)) |
23 | 22 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}} ↔ 𝑥 ∈ 𝐴)) |
24 | 9, 10, 23 | eqrdav 2621 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ → {𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}} = 𝐴) |
25 | 24 | supeq1d 8352 |
. . . . 5
⊢ (𝐴 ⊆ ℝ →
sup({𝑤 ∈ ℝ
∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < )) |
26 | 25 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}}, ℝ, < ) = sup(𝐴, ℝ, < )) |
27 | 26 | negeqd 10275 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → -sup({𝑤 ∈ ℝ ∣ -𝑤 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}}, ℝ, < ) = -sup(𝐴, ℝ, < )) |
28 | 7, 27 | eqtrd 2656 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < )) |
29 | | infrecl 11005 |
. . . . . 6
⊢ (({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ⊆ ℝ ∧ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) → inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
30 | 3, 29 | mp3an1 1411 |
. . . . 5
⊢ (({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) → inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
31 | 1, 2, 30 | syl2an 494 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
32 | 31 | 3impa 1259 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) ∈
ℝ) |
33 | | suprcl 10983 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈
ℝ) |
34 | | recn 10026 |
. . . 4
⊢
(inf({𝑧 ∈
ℝ ∣ -𝑧 ∈
𝐴}, ℝ, < ) ∈
ℝ → inf({𝑧
∈ ℝ ∣ -𝑧
∈ 𝐴}, ℝ, < )
∈ ℂ) |
35 | | recn 10026 |
. . . 4
⊢
(sup(𝐴, ℝ,
< ) ∈ ℝ → sup(𝐴, ℝ, < ) ∈
ℂ) |
36 | | negcon2 10334 |
. . . 4
⊢
((inf({𝑧 ∈
ℝ ∣ -𝑧 ∈
𝐴}, ℝ, < ) ∈
ℂ ∧ sup(𝐴,
ℝ, < ) ∈ ℂ) → (inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ))) |
37 | 34, 35, 36 | syl2an 494 |
. . 3
⊢
((inf({𝑧 ∈
ℝ ∣ -𝑧 ∈
𝐴}, ℝ, < ) ∈
ℝ ∧ sup(𝐴,
ℝ, < ) ∈ ℝ) → (inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ))) |
38 | 32, 33, 37 | syl2anc 693 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ) = -sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ, < ) = -inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ))) |
39 | 28, 38 | mpbid 222 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) = -inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < )) |