Step | Hyp | Ref
| Expression |
1 | | renegcl 10797 |
. . 3
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) |
2 | | zmin 12193 |
. . 3
⊢ (-𝐴 ∈ ℝ →
∃!𝑧 ∈ ℤ
(-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝐴 ∈ ℝ →
∃!𝑧 ∈ ℤ
(-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤))) |
4 | | zre 11833 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℝ) |
5 | | leneg 10991 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 ≤ 𝐴 ↔ -𝐴 ≤ -𝑥)) |
6 | 4, 5 | sylan 580 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑥 ≤ 𝐴 ↔ -𝐴 ≤ -𝑥)) |
7 | 6 | ancoms 459 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑥 ≤ 𝐴 ↔ -𝐴 ≤ -𝑥)) |
8 | | znegcl 11866 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℤ → -𝑤 ∈
ℤ) |
9 | | breq1 4965 |
. . . . . . . . . . . 12
⊢ (𝑦 = -𝑤 → (𝑦 ≤ 𝐴 ↔ -𝑤 ≤ 𝐴)) |
10 | | breq1 4965 |
. . . . . . . . . . . 12
⊢ (𝑦 = -𝑤 → (𝑦 ≤ 𝑥 ↔ -𝑤 ≤ 𝑥)) |
11 | 9, 10 | imbi12d 346 |
. . . . . . . . . . 11
⊢ (𝑦 = -𝑤 → ((𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) ↔ (-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥))) |
12 | 11 | rspcv 3555 |
. . . . . . . . . 10
⊢ (-𝑤 ∈ ℤ →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → (-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥))) |
13 | 8, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℤ →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → (-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥))) |
14 | | zre 11833 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℤ → 𝑤 ∈
ℝ) |
15 | | lenegcon1 10992 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (-𝑤 ≤ 𝐴 ↔ -𝐴 ≤ 𝑤)) |
16 | 15 | adantrr 713 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → (-𝑤 ≤ 𝐴 ↔ -𝐴 ≤ 𝑤)) |
17 | | lenegcon1 10992 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (-𝑤 ≤ 𝑥 ↔ -𝑥 ≤ 𝑤)) |
18 | 4, 17 | sylan2 592 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-𝑤 ≤ 𝑥 ↔ -𝑥 ≤ 𝑤)) |
19 | 18 | adantrl 712 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → (-𝑤 ≤ 𝑥 ↔ -𝑥 ≤ 𝑤)) |
20 | 16, 19 | imbi12d 346 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) →
((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) ↔ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) |
21 | 14, 20 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℤ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) →
((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) ↔ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) |
22 | 21 | biimpd 230 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℤ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) →
((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) |
23 | 22 | ex 413 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℤ → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) |
24 | 23 | com23 86 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℤ → ((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) |
25 | 13, 24 | syld 47 |
. . . . . . . 8
⊢ (𝑤 ∈ ℤ →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) |
26 | 25 | com13 88 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → (𝑤 ∈ ℤ → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) |
27 | 26 | ralrimdv 3155 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) |
28 | | znegcl 11866 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → -𝑦 ∈
ℤ) |
29 | | breq2 4966 |
. . . . . . . . . . . 12
⊢ (𝑤 = -𝑦 → (-𝐴 ≤ 𝑤 ↔ -𝐴 ≤ -𝑦)) |
30 | | breq2 4966 |
. . . . . . . . . . . 12
⊢ (𝑤 = -𝑦 → (-𝑥 ≤ 𝑤 ↔ -𝑥 ≤ -𝑦)) |
31 | 29, 30 | imbi12d 346 |
. . . . . . . . . . 11
⊢ (𝑤 = -𝑦 → ((-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) ↔ (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) |
32 | 31 | rspcv 3555 |
. . . . . . . . . 10
⊢ (-𝑦 ∈ ℤ →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) |
33 | 28, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) |
34 | | zre 11833 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) |
35 | | leneg 10991 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑦 ≤ 𝐴 ↔ -𝐴 ≤ -𝑦)) |
36 | 35 | adantrr 713 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → (𝑦 ≤ 𝐴 ↔ -𝐴 ≤ -𝑦)) |
37 | | leneg 10991 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 ≤ 𝑥 ↔ -𝑥 ≤ -𝑦)) |
38 | 4, 37 | sylan2 592 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑦 ≤ 𝑥 ↔ -𝑥 ≤ -𝑦)) |
39 | 38 | adantrl 712 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → (𝑦 ≤ 𝑥 ↔ -𝑥 ≤ -𝑦)) |
40 | 36, 39 | imbi12d 346 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → ((𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) ↔ (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) |
41 | 34, 40 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℤ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → ((𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) ↔ (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) |
42 | 41 | exbiri 807 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦) → (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) |
43 | 42 | com23 86 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → ((-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦) → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) |
44 | 33, 43 | syld 47 |
. . . . . . . 8
⊢ (𝑦 ∈ ℤ →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) |
45 | 44 | com13 88 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → (𝑦 ∈ ℤ → (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) |
46 | 45 | ralrimdv 3155 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥))) |
47 | 27, 46 | impbid 213 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) ↔ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) |
48 | 7, 47 | anbi12d 630 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)) ↔ (-𝐴 ≤ -𝑥 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) |
49 | 48 | reubidva 3347 |
. . 3
⊢ (𝐴 ∈ ℝ →
(∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)) ↔ ∃!𝑥 ∈ ℤ (-𝐴 ≤ -𝑥 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) |
50 | | znegcl 11866 |
. . . 4
⊢ (𝑥 ∈ ℤ → -𝑥 ∈
ℤ) |
51 | | znegcl 11866 |
. . . . 5
⊢ (𝑧 ∈ ℤ → -𝑧 ∈
ℤ) |
52 | | zcn 11834 |
. . . . . 6
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℂ) |
53 | | zcn 11834 |
. . . . . 6
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
54 | | negcon2 10787 |
. . . . . 6
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑧 = -𝑥 ↔ 𝑥 = -𝑧)) |
55 | 52, 53, 54 | syl2an 595 |
. . . . 5
⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑧 = -𝑥 ↔ 𝑥 = -𝑧)) |
56 | 51, 55 | reuhyp 5212 |
. . . 4
⊢ (𝑧 ∈ ℤ →
∃!𝑥 ∈ ℤ
𝑧 = -𝑥) |
57 | | breq2 4966 |
. . . . 5
⊢ (𝑧 = -𝑥 → (-𝐴 ≤ 𝑧 ↔ -𝐴 ≤ -𝑥)) |
58 | | breq1 4965 |
. . . . . . 7
⊢ (𝑧 = -𝑥 → (𝑧 ≤ 𝑤 ↔ -𝑥 ≤ 𝑤)) |
59 | 58 | imbi2d 342 |
. . . . . 6
⊢ (𝑧 = -𝑥 → ((-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤) ↔ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) |
60 | 59 | ralbidv 3164 |
. . . . 5
⊢ (𝑧 = -𝑥 → (∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤) ↔ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) |
61 | 57, 60 | anbi12d 630 |
. . . 4
⊢ (𝑧 = -𝑥 → ((-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤)) ↔ (-𝐴 ≤ -𝑥 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) |
62 | 50, 56, 61 | reuxfr1 3677 |
. . 3
⊢
(∃!𝑧 ∈
ℤ (-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤)) ↔ ∃!𝑥 ∈ ℤ (-𝐴 ≤ -𝑥 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) |
63 | 49, 62 | syl6rbbr 291 |
. 2
⊢ (𝐴 ∈ ℝ →
(∃!𝑧 ∈ ℤ
(-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤)) ↔ ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) |
64 | 3, 63 | mpbid 233 |
1
⊢ (𝐴 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥))) |