| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | renegcl 11572 | . . 3
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) | 
| 2 |  | zmin 12986 | . . 3
⊢ (-𝐴 ∈ ℝ →
∃!𝑧 ∈ ℤ
(-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤))) | 
| 3 | 1, 2 | syl 17 | . 2
⊢ (𝐴 ∈ ℝ →
∃!𝑧 ∈ ℤ
(-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤))) | 
| 4 |  | znegcl 12652 | . . . 4
⊢ (𝑥 ∈ ℤ → -𝑥 ∈
ℤ) | 
| 5 |  | znegcl 12652 | . . . . 5
⊢ (𝑧 ∈ ℤ → -𝑧 ∈
ℤ) | 
| 6 |  | zcn 12618 | . . . . . 6
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℂ) | 
| 7 |  | zcn 12618 | . . . . . 6
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) | 
| 8 |  | negcon2 11562 | . . . . . 6
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑧 = -𝑥 ↔ 𝑥 = -𝑧)) | 
| 9 | 6, 7, 8 | syl2an 596 | . . . . 5
⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑧 = -𝑥 ↔ 𝑥 = -𝑧)) | 
| 10 | 5, 9 | reuhyp 5420 | . . . 4
⊢ (𝑧 ∈ ℤ →
∃!𝑥 ∈ ℤ
𝑧 = -𝑥) | 
| 11 |  | breq2 5147 | . . . . 5
⊢ (𝑧 = -𝑥 → (-𝐴 ≤ 𝑧 ↔ -𝐴 ≤ -𝑥)) | 
| 12 |  | breq1 5146 | . . . . . . 7
⊢ (𝑧 = -𝑥 → (𝑧 ≤ 𝑤 ↔ -𝑥 ≤ 𝑤)) | 
| 13 | 12 | imbi2d 340 | . . . . . 6
⊢ (𝑧 = -𝑥 → ((-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤) ↔ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) | 
| 14 | 13 | ralbidv 3178 | . . . . 5
⊢ (𝑧 = -𝑥 → (∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤) ↔ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) | 
| 15 | 11, 14 | anbi12d 632 | . . . 4
⊢ (𝑧 = -𝑥 → ((-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤)) ↔ (-𝐴 ≤ -𝑥 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) | 
| 16 | 4, 10, 15 | reuxfr1 3758 | . . 3
⊢
(∃!𝑧 ∈
ℤ (-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤)) ↔ ∃!𝑥 ∈ ℤ (-𝐴 ≤ -𝑥 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) | 
| 17 |  | zre 12617 | . . . . . . 7
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℝ) | 
| 18 |  | leneg 11766 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 ≤ 𝐴 ↔ -𝐴 ≤ -𝑥)) | 
| 19 | 17, 18 | sylan 580 | . . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑥 ≤ 𝐴 ↔ -𝐴 ≤ -𝑥)) | 
| 20 | 19 | ancoms 458 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑥 ≤ 𝐴 ↔ -𝐴 ≤ -𝑥)) | 
| 21 |  | znegcl 12652 | . . . . . . . . . 10
⊢ (𝑤 ∈ ℤ → -𝑤 ∈
ℤ) | 
| 22 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑦 = -𝑤 → (𝑦 ≤ 𝐴 ↔ -𝑤 ≤ 𝐴)) | 
| 23 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑦 = -𝑤 → (𝑦 ≤ 𝑥 ↔ -𝑤 ≤ 𝑥)) | 
| 24 | 22, 23 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑦 = -𝑤 → ((𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) ↔ (-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥))) | 
| 25 | 24 | rspcv 3618 | . . . . . . . . . 10
⊢ (-𝑤 ∈ ℤ →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → (-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥))) | 
| 26 | 21, 25 | syl 17 | . . . . . . . . 9
⊢ (𝑤 ∈ ℤ →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → (-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥))) | 
| 27 |  | zre 12617 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℤ → 𝑤 ∈
ℝ) | 
| 28 |  | lenegcon1 11767 | . . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (-𝑤 ≤ 𝐴 ↔ -𝐴 ≤ 𝑤)) | 
| 29 | 28 | adantrr 717 | . . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → (-𝑤 ≤ 𝐴 ↔ -𝐴 ≤ 𝑤)) | 
| 30 |  | lenegcon1 11767 | . . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (-𝑤 ≤ 𝑥 ↔ -𝑥 ≤ 𝑤)) | 
| 31 | 17, 30 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-𝑤 ≤ 𝑥 ↔ -𝑥 ≤ 𝑤)) | 
| 32 | 31 | adantrl 716 | . . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → (-𝑤 ≤ 𝑥 ↔ -𝑥 ≤ 𝑤)) | 
| 33 | 29, 32 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) →
((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) ↔ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) | 
| 34 | 27, 33 | sylan 580 | . . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℤ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) →
((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) ↔ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) | 
| 35 | 34 | biimpd 229 | . . . . . . . . . . 11
⊢ ((𝑤 ∈ ℤ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) →
((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) | 
| 36 | 35 | ex 412 | . . . . . . . . . 10
⊢ (𝑤 ∈ ℤ → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) | 
| 37 | 36 | com23 86 | . . . . . . . . 9
⊢ (𝑤 ∈ ℤ → ((-𝑤 ≤ 𝐴 → -𝑤 ≤ 𝑥) → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) | 
| 38 | 26, 37 | syld 47 | . . . . . . . 8
⊢ (𝑤 ∈ ℤ →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) | 
| 39 | 38 | com13 88 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → (𝑤 ∈ ℤ → (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) | 
| 40 | 39 | ralrimdv 3152 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) → ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) | 
| 41 |  | znegcl 12652 | . . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → -𝑦 ∈
ℤ) | 
| 42 |  | breq2 5147 | . . . . . . . . . . . 12
⊢ (𝑤 = -𝑦 → (-𝐴 ≤ 𝑤 ↔ -𝐴 ≤ -𝑦)) | 
| 43 |  | breq2 5147 | . . . . . . . . . . . 12
⊢ (𝑤 = -𝑦 → (-𝑥 ≤ 𝑤 ↔ -𝑥 ≤ -𝑦)) | 
| 44 | 42, 43 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑤 = -𝑦 → ((-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) ↔ (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) | 
| 45 | 44 | rspcv 3618 | . . . . . . . . . 10
⊢ (-𝑦 ∈ ℤ →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) | 
| 46 | 41, 45 | syl 17 | . . . . . . . . 9
⊢ (𝑦 ∈ ℤ →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) | 
| 47 |  | zre 12617 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) | 
| 48 |  | leneg 11766 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑦 ≤ 𝐴 ↔ -𝐴 ≤ -𝑦)) | 
| 49 | 48 | adantrr 717 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → (𝑦 ≤ 𝐴 ↔ -𝐴 ≤ -𝑦)) | 
| 50 |  | leneg 11766 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 ≤ 𝑥 ↔ -𝑥 ≤ -𝑦)) | 
| 51 | 17, 50 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑦 ≤ 𝑥 ↔ -𝑥 ≤ -𝑦)) | 
| 52 | 51 | adantrl 716 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → (𝑦 ≤ 𝑥 ↔ -𝑥 ≤ -𝑦)) | 
| 53 | 49, 52 | imbi12d 344 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → ((𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) ↔ (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) | 
| 54 | 47, 53 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ ℤ ∧ (𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ)) → ((𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) ↔ (-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦))) | 
| 55 | 54 | exbiri 811 | . . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦) → (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) | 
| 56 | 55 | com23 86 | . . . . . . . . 9
⊢ (𝑦 ∈ ℤ → ((-𝐴 ≤ -𝑦 → -𝑥 ≤ -𝑦) → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) | 
| 57 | 46, 56 | syld 47 | . . . . . . . 8
⊢ (𝑦 ∈ ℤ →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) | 
| 58 | 57 | com13 88 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → (𝑦 ∈ ℤ → (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) | 
| 59 | 58 | ralrimdv 3152 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑤 ∈ ℤ
(-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤) → ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥))) | 
| 60 | 40, 59 | impbid 212 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) →
(∀𝑦 ∈ ℤ
(𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥) ↔ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤))) | 
| 61 | 20, 60 | anbi12d 632 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)) ↔ (-𝐴 ≤ -𝑥 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) | 
| 62 | 61 | reubidva 3396 | . . 3
⊢ (𝐴 ∈ ℝ →
(∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)) ↔ ∃!𝑥 ∈ ℤ (-𝐴 ≤ -𝑥 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → -𝑥 ≤ 𝑤)))) | 
| 63 | 16, 62 | bitr4id 290 | . 2
⊢ (𝐴 ∈ ℝ →
(∃!𝑧 ∈ ℤ
(-𝐴 ≤ 𝑧 ∧ ∀𝑤 ∈ ℤ (-𝐴 ≤ 𝑤 → 𝑧 ≤ 𝑤)) ↔ ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥)))) | 
| 64 | 3, 63 | mpbid 232 | 1
⊢ (𝐴 ∈ ℝ →
∃!𝑥 ∈ ℤ
(𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥))) |