Proof of Theorem rexabslelem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp2 1137 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → 𝑦 ∈ ℝ) | 
| 2 |  | rexabslelem.1 | . . . . . . . 8
⊢
Ⅎ𝑥𝜑 | 
| 3 |  | nfv 1913 | . . . . . . . 8
⊢
Ⅎ𝑥 𝑦 ∈ ℝ | 
| 4 |  | nfra1 3283 | . . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 | 
| 5 | 2, 3, 4 | nf3an 1900 | . . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) | 
| 6 |  | rexabslelem.2 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 7 | 6 | 3ad2antl1 1185 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 8 | 6 | recnd 11290 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 9 | 8 | 3ad2antl1 1185 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 10 | 9 | abscld 15476 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ) | 
| 11 | 1 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) | 
| 12 | 7 | leabsd 15454 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ (abs‘𝐵)) | 
| 13 |  | rspa 3247 | . . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 (abs‘𝐵) ≤ 𝑦 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ≤ 𝑦) | 
| 14 | 13 | 3ad2antl3 1187 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ≤ 𝑦) | 
| 15 | 7, 10, 11, 12, 14 | letrd 11419 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑦) | 
| 16 | 15 | ex 412 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → (𝑥 ∈ 𝐴 → 𝐵 ≤ 𝑦)) | 
| 17 | 5, 16 | ralrimi 3256 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) | 
| 18 |  | brralrspcev 5202 | . . . . . 6
⊢ ((𝑦 ∈ ℝ ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) | 
| 19 | 1, 17, 18 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) | 
| 20 | 1 | renegcld 11691 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → -𝑦 ∈ ℝ) | 
| 21 | 6 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 22 |  | simplr 768 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) | 
| 23 |  | absle 15355 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((abs‘𝐵) ≤ 𝑦 ↔ (-𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦))) | 
| 24 | 21, 22, 23 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) ≤ 𝑦 ↔ (-𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦))) | 
| 25 | 24 | 3adantl3 1168 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) ≤ 𝑦 ↔ (-𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦))) | 
| 26 | 14, 25 | mpbid 232 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (-𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦)) | 
| 27 | 26 | simpld 494 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → -𝑦 ≤ 𝐵) | 
| 28 | 27 | ex 412 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → (𝑥 ∈ 𝐴 → -𝑦 ≤ 𝐵)) | 
| 29 | 5, 28 | ralrimi 3256 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → ∀𝑥 ∈ 𝐴 -𝑦 ≤ 𝐵) | 
| 30 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑧 = -𝑦 → (𝑧 ≤ 𝐵 ↔ -𝑦 ≤ 𝐵)) | 
| 31 | 30 | ralbidv 3177 | . . . . . . 7
⊢ (𝑧 = -𝑦 → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ↔ ∀𝑥 ∈ 𝐴 -𝑦 ≤ 𝐵)) | 
| 32 | 31 | rspcev 3621 | . . . . . 6
⊢ ((-𝑦 ∈ ℝ ∧
∀𝑥 ∈ 𝐴 -𝑦 ≤ 𝐵) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) | 
| 33 | 20, 29, 32 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) | 
| 34 | 19, 33 | jca 511 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵)) | 
| 35 | 34 | 3exp 1119 | . . 3
⊢ (𝜑 → (𝑦 ∈ ℝ → (∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 → (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵)))) | 
| 36 | 35 | rexlimdv 3152 | . 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 → (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵))) | 
| 37 |  | renegcl 11573 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ → -𝑧 ∈
ℝ) | 
| 38 | 37 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -𝑧 ∈
ℝ) | 
| 39 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑤 ∈
ℝ) | 
| 40 | 38, 39 | ifcld 4571 | . . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) | 
| 41 | 40 | ad5ant24 760 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) | 
| 42 |  | nfv 1913 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑤 ∈ ℝ | 
| 43 | 2, 42 | nfan 1898 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ ℝ) | 
| 44 |  | nfra1 3283 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 | 
| 45 | 43, 44 | nfan 1898 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) | 
| 46 |  | nfv 1913 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥 𝑧 ∈ ℝ | 
| 47 | 45, 46 | nfan 1898 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥(((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) | 
| 48 |  | nfra1 3283 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 | 
| 49 | 47, 48 | nfan 1898 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) | 
| 50 | 40 | ad5ant23 759 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) | 
| 51 | 50 | renegcld 11691 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) | 
| 52 |  | simpllr 775 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ ℝ) | 
| 53 | 6 | ad5ant15 758 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 54 |  | max2 13230 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ ℝ ∧ -𝑧 ∈ ℝ) → -𝑧 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) | 
| 55 | 39, 38, 54 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -𝑧 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) | 
| 56 | 38, 40 | lenegd 11843 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-𝑧 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ↔ -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ --𝑧)) | 
| 57 | 55, 56 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ --𝑧) | 
| 58 |  | recn 11246 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℝ → 𝑧 ∈
ℂ) | 
| 59 | 58 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℂ) | 
| 60 | 59 | negnegd 11612 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → --𝑧 = 𝑧) | 
| 61 | 57, 60 | breqtrd 5168 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝑧) | 
| 62 | 61 | ad5ant23 759 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝑧) | 
| 63 |  | rspa 3247 | . . . . . . . . . . . . . . . . . 18
⊢
((∀𝑥 ∈
𝐴 𝑧 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑧 ≤ 𝐵) | 
| 64 | 63 | adantll 714 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑧 ≤ 𝐵) | 
| 65 | 51, 52, 53, 62, 64 | letrd 11419 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵) | 
| 66 | 65 | adantl3r 750 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵) | 
| 67 | 6 | ad5ant15 758 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 68 |  | simp-4r 783 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑤 ∈ ℝ) | 
| 69 | 40 | ad5ant24 760 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) | 
| 70 |  | rspa 3247 | . . . . . . . . . . . . . . . . . 18
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑤 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑤) | 
| 71 | 70 | ad4ant24 754 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑤) | 
| 72 |  | max1 13228 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ℝ ∧ -𝑧 ∈ ℝ) → 𝑤 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) | 
| 73 | 39, 38, 72 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑤 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) | 
| 74 | 73 | ad5ant24 760 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑤 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) | 
| 75 | 67, 68, 69, 71, 74 | letrd 11419 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) | 
| 76 | 75 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) | 
| 77 | 66, 76 | jca 511 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → (-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵 ∧ 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤))) | 
| 78 | 6 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 79 | 78 | 3adant2 1131 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 80 | 40 | adantll 714 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) | 
| 81 | 80 | 3adant3 1132 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ ∧ 𝑥 ∈ 𝐴) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) | 
| 82 | 79, 81 | absled 15470 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ↔ (-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵 ∧ 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)))) | 
| 83 | 82 | ad5ant135 1369 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ↔ (-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵 ∧ 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)))) | 
| 84 | 77, 83 | mpbird 257 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) | 
| 85 | 84 | ex 412 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → (𝑥 ∈ 𝐴 → (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤))) | 
| 86 | 49, 85 | ralrimi 3256 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) | 
| 87 |  | brralrspcev 5202 | . . . . . . . . . . 11
⊢
((if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) | 
| 88 | 41, 86, 87 | syl2anc 584 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) | 
| 89 | 88 | exp31 419 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) → (𝑧 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦))) | 
| 90 | 89 | exp31 419 | . . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 → (𝑧 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦))))) | 
| 91 | 90 | rexlimdv 3152 | . . . . . . 7
⊢ (𝜑 → (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 → (𝑧 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦)))) | 
| 92 | 91 | imp 406 | . . . . . 6
⊢ ((𝜑 ∧ ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) → (𝑧 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦))) | 
| 93 | 92 | rexlimdv 3152 | . . . . 5
⊢ ((𝜑 ∧ ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) → (∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦)) | 
| 94 | 93 | imp 406 | . . . 4
⊢ (((𝜑 ∧ ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) | 
| 95 | 94 | anasss 466 | . . 3
⊢ ((𝜑 ∧ (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) | 
| 96 | 95 | ex 412 | . 2
⊢ (𝜑 → ((∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦)) | 
| 97 | 36, 96 | impbid 212 | 1
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 ↔ (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵))) |