Proof of Theorem rexabslelem
Step | Hyp | Ref
| Expression |
1 | | simp2 1062 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → 𝑦 ∈ ℝ) |
2 | | rexabslelem.1 |
. . . . . . . 8
⊢
Ⅎ𝑥𝜑 |
3 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 ∈ ℝ |
4 | | nfra1 2941 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 |
5 | 2, 3, 4 | nf3an 1831 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) |
6 | | rexabslelem.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
7 | 6 | 3ad2antl1 1223 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
8 | 6 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
9 | 8 | 3ad2antl1 1223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
10 | 9 | abscld 14175 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ) |
11 | 1 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
12 | 7 | leabsd 14153 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ (abs‘𝐵)) |
13 | | rspa 2930 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 (abs‘𝐵) ≤ 𝑦 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ≤ 𝑦) |
14 | 13 | 3ad2antl3 1225 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ≤ 𝑦) |
15 | 7, 10, 11, 12, 14 | letrd 10194 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑦) |
16 | 15 | ex 450 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → (𝑥 ∈ 𝐴 → 𝐵 ≤ 𝑦)) |
17 | 5, 16 | ralrimi 2957 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
18 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (𝐵 ≤ 𝑤 ↔ 𝐵 ≤ 𝑦)) |
19 | 18 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)) |
20 | 19 | rspcev 3309 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) |
21 | 1, 17, 20 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) |
22 | 1 | renegcld 10457 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → -𝑦 ∈ ℝ) |
23 | 6 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
24 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
25 | | absle 14055 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((abs‘𝐵) ≤ 𝑦 ↔ (-𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦))) |
26 | 23, 24, 25 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) ≤ 𝑦 ↔ (-𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦))) |
27 | 26 | 3adantl3 1219 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) ≤ 𝑦 ↔ (-𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦))) |
28 | 14, 27 | mpbid 222 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → (-𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦)) |
29 | 28 | simpld 475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → -𝑦 ≤ 𝐵) |
30 | 29 | ex 450 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → (𝑥 ∈ 𝐴 → -𝑦 ≤ 𝐵)) |
31 | 5, 30 | ralrimi 2957 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → ∀𝑥 ∈ 𝐴 -𝑦 ≤ 𝐵) |
32 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑧 = -𝑦 → (𝑧 ≤ 𝐵 ↔ -𝑦 ≤ 𝐵)) |
33 | 32 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑧 = -𝑦 → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ↔ ∀𝑥 ∈ 𝐴 -𝑦 ≤ 𝐵)) |
34 | 33 | rspcev 3309 |
. . . . . 6
⊢ ((-𝑦 ∈ ℝ ∧
∀𝑥 ∈ 𝐴 -𝑦 ≤ 𝐵) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) |
35 | 22, 31, 34 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) |
36 | 21, 35 | jca 554 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) → (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵)) |
37 | 36 | 3exp 1264 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ → (∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 → (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵)))) |
38 | 37 | rexlimdv 3030 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 → (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵))) |
39 | | renegcl 10344 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ → -𝑧 ∈
ℝ) |
40 | 39 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -𝑧 ∈
ℝ) |
41 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑤 ∈
ℝ) |
42 | 40, 41 | ifcld 4131 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) |
43 | 42 | ad5ant24 1305 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) |
44 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑤 ∈ ℝ |
45 | 2, 44 | nfan 1828 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ ℝ) |
46 | | nfra1 2941 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 |
47 | 45, 46 | nfan 1828 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) |
48 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥 𝑧 ∈ ℝ |
49 | 47, 48 | nfan 1828 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) |
50 | | nfra1 2941 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 |
51 | 49, 50 | nfan 1828 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) |
52 | 42 | ad5ant23 1304 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) |
53 | 52 | renegcld 10457 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) |
54 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ ℝ) |
55 | 6 | ad5ant15 1303 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
56 | | max2 12018 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ ℝ ∧ -𝑧 ∈ ℝ) → -𝑧 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) |
57 | 41, 40, 56 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → -𝑧 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) |
58 | 40, 42 | lenegd 10606 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-𝑧 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ↔ -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ --𝑧)) |
59 | 57, 58 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ --𝑧) |
60 | | recn 10026 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℝ → 𝑧 ∈
ℂ) |
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℂ) |
62 | 61 | negnegd 10383 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → --𝑧 = 𝑧) |
63 | 59, 62 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝑧) |
64 | 63 | ad5ant23 1304 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝑧) |
65 | | rspa 2930 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑥 ∈
𝐴 𝑧 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑧 ≤ 𝐵) |
66 | 65 | adantll 750 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑧 ≤ 𝐵) |
67 | 53, 54, 55, 64, 66 | letrd 10194 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵) |
68 | 67 | ad5ant1345 1316 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → -if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵) |
69 | 6 | ad5ant15 1303 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
70 | | simp-4r 807 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑤 ∈ ℝ) |
71 | 42 | ad5ant24 1305 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) |
72 | | rspa 2930 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑤 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑤) |
73 | 72 | ad4ant24 1298 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑤) |
74 | | max1 12016 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ℝ ∧ -𝑧 ∈ ℝ) → 𝑤 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) |
75 | 41, 40, 74 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑤 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) |
76 | 75 | ad5ant24 1305 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑤 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) |
77 | 69, 70, 71, 73, 76 | letrd 10194 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) |
78 | 77 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) |
79 | 68, 78 | jca 554 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → (-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵 ∧ 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤))) |
80 | 6 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
81 | 80 | 3adant2 1080 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
82 | 42 | adantll 750 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) |
83 | 82 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ ∧ 𝑥 ∈ 𝐴) → if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ) |
84 | 81, 83 | absled 14169 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ↔ (-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵 ∧ 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)))) |
85 | 84 | ad5ant135 1314 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ↔ (-if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ≤ 𝐵 ∧ 𝐵 ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)))) |
86 | 79, 85 | mpbird 247 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) |
87 | 86 | ex 450 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → (𝑥 ∈ 𝐴 → (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤))) |
88 | 51, 87 | ralrimi 2957 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) |
89 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑦 = if(𝑤 ≤ -𝑧, -𝑧, 𝑤) → ((abs‘𝐵) ≤ 𝑦 ↔ (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤))) |
90 | 89 | ralbidv 2986 |
. . . . . . . . . . . 12
⊢ (𝑦 = if(𝑤 ≤ -𝑧, -𝑧, 𝑤) → (∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 ↔ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤))) |
91 | 90 | rspcev 3309 |
. . . . . . . . . . 11
⊢
((if(𝑤 ≤ -𝑧, -𝑧, 𝑤) ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ if(𝑤 ≤ -𝑧, -𝑧, 𝑤)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) |
92 | 43, 88, 91 | syl2anc 693 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ) ∧
∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) |
93 | 92 | exp31 630 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) → (𝑧 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦))) |
94 | 93 | exp31 630 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 → (𝑧 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦))))) |
95 | 94 | rexlimdv 3030 |
. . . . . . 7
⊢ (𝜑 → (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 → (𝑧 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦)))) |
96 | 95 | imp 445 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) → (𝑧 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦))) |
97 | 96 | rexlimdv 3030 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) → (∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦)) |
98 | 97 | imp 445 |
. . . 4
⊢ (((𝜑 ∧ ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤) ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) |
99 | 98 | anasss 679 |
. . 3
⊢ ((𝜑 ∧ (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦) |
100 | 99 | ex 450 |
. 2
⊢ (𝜑 → ((∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦)) |
101 | 38, 100 | impbid 202 |
1
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 ↔ (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵))) |