Step | Hyp | Ref
| Expression |
1 | | cncficcgt0.fcn |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0}))) |
2 | | cncff 24056 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) → 𝐹:(𝐴[,]𝐵)⟶(ℝ ∖
{0})) |
3 | | ffun 6603 |
. . . . . . . 8
⊢ (𝐹:(𝐴[,]𝐵)⟶(ℝ ∖ {0}) → Fun
𝐹) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐹) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → Fun 𝐹) |
6 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → 𝑐 ∈ (𝐴[,]𝐵)) |
7 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶(ℝ ∖
{0})) |
8 | 7 | fdmd 6611 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = (𝐴[,]𝐵)) |
9 | 8 | eqcomd 2744 |
. . . . . . . 8
⊢ (𝜑 → (𝐴[,]𝐵) = dom 𝐹) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = dom 𝐹) |
11 | 6, 10 | eleqtrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → 𝑐 ∈ dom 𝐹) |
12 | | fvco 6866 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑐 ∈ dom 𝐹) → ((abs ∘ 𝐹)‘𝑐) = (abs‘(𝐹‘𝑐))) |
13 | 5, 11, 12 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) = (abs‘(𝐹‘𝑐))) |
14 | 7 | ffvelrnda 6961 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑐) ∈ (ℝ ∖
{0})) |
15 | 14 | eldifad 3899 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑐) ∈ ℝ) |
16 | 15 | recnd 11003 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑐) ∈ ℂ) |
17 | | eldifsni 4723 |
. . . . . . 7
⊢ ((𝐹‘𝑐) ∈ (ℝ ∖ {0}) → (𝐹‘𝑐) ≠ 0) |
18 | 14, 17 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑐) ≠ 0) |
19 | 16, 18 | absrpcld 15160 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (abs‘(𝐹‘𝑐)) ∈
ℝ+) |
20 | 13, 19 | eqeltrd 2839 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) ∈
ℝ+) |
21 | 20 | adantr 481 |
. . 3
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) → ((abs ∘ 𝐹)‘𝑐) ∈
ℝ+) |
22 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) |
23 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑥(𝐴[,]𝐵) |
24 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑥abs |
25 | | cncficcgt0.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) |
26 | | nfmpt1 5182 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) |
27 | 25, 26 | nfcxfr 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐹 |
28 | 24, 27 | nfco 5774 |
. . . . . . . 8
⊢
Ⅎ𝑥(abs
∘ 𝐹) |
29 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑐 |
30 | 28, 29 | nffv 6784 |
. . . . . . 7
⊢
Ⅎ𝑥((abs
∘ 𝐹)‘𝑐) |
31 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑥
≤ |
32 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑑 |
33 | 28, 32 | nffv 6784 |
. . . . . . 7
⊢
Ⅎ𝑥((abs
∘ 𝐹)‘𝑑) |
34 | 30, 31, 33 | nfbr 5121 |
. . . . . 6
⊢
Ⅎ𝑥((abs
∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑) |
35 | 23, 34 | nfralw 3151 |
. . . . 5
⊢
Ⅎ𝑥∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑) |
36 | 22, 35 | nfan 1902 |
. . . 4
⊢
Ⅎ𝑥((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) |
37 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑑 = 𝑥 → ((abs ∘ 𝐹)‘𝑑) = ((abs ∘ 𝐹)‘𝑥)) |
38 | 37 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑑 = 𝑥 → (((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑) ↔ ((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑥))) |
39 | 38 | rspccva 3560 |
. . . . . . 7
⊢
((∀𝑑 ∈
(𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑥)) |
40 | 39 | adantll 711 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑥)) |
41 | | absf 15049 |
. . . . . . . . . . 11
⊢
abs:ℂ⟶ℝ |
42 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
43 | | difss 4066 |
. . . . . . . . . . . . 13
⊢ (ℝ
∖ {0}) ⊆ ℝ |
44 | | ax-resscn 10928 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
45 | 43, 44 | sstri 3930 |
. . . . . . . . . . . 12
⊢ (ℝ
∖ {0}) ⊆ ℂ |
46 | 45 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ ∖ {0})
⊆ ℂ) |
47 | 7, 46 | fssd 6618 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
48 | | fcompt 7005 |
. . . . . . . . . 10
⊢
((abs:ℂ⟶ℝ ∧ 𝐹:(𝐴[,]𝐵)⟶ℂ) → (abs ∘ 𝐹) = (𝑧 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑧)))) |
49 | 42, 47, 48 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (abs ∘ 𝐹) = (𝑧 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑧)))) |
50 | | nfcv 2907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑧 |
51 | 27, 50 | nffv 6784 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝐹‘𝑧) |
52 | 24, 51 | nffv 6784 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(abs‘(𝐹‘𝑧)) |
53 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧(abs‘(𝐹‘𝑥)) |
54 | | fveq2 6774 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) |
55 | 54 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (abs‘(𝐹‘𝑧)) = (abs‘(𝐹‘𝑥))) |
56 | 52, 53, 55 | cbvmpt 5185 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑧))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑥))) |
57 | 56 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑧))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑥)))) |
58 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶)) |
59 | 58, 7 | feq1dd 42703 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶):(𝐴[,]𝐵)⟶(ℝ ∖
{0})) |
60 | 59 | fvmptelrn 6987 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ (ℝ ∖
{0})) |
61 | 58, 60 | fvmpt2d 6888 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) = 𝐶) |
62 | 61 | fveq2d 6778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (abs‘(𝐹‘𝑥)) = (abs‘𝐶)) |
63 | 62 | mpteq2dva 5174 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘𝐶))) |
64 | 49, 57, 63 | 3eqtrd 2782 |
. . . . . . . 8
⊢ (𝜑 → (abs ∘ 𝐹) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘𝐶))) |
65 | 45, 60 | sselid 3919 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ) |
66 | 65 | abscld 15148 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (abs‘𝐶) ∈ ℝ) |
67 | 64, 66 | fvmpt2d 6888 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑥) = (abs‘𝐶)) |
68 | 67 | ad4ant14 749 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑥) = (abs‘𝐶)) |
69 | 40, 68 | breqtrd 5100 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶)) |
70 | 69 | ex 413 |
. . . 4
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) → (𝑥 ∈ (𝐴[,]𝐵) → ((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶))) |
71 | 36, 70 | ralrimi 3141 |
. . 3
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) → ∀𝑥 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶)) |
72 | 30 | nfeq2 2924 |
. . . . 5
⊢
Ⅎ𝑥 𝑦 = ((abs ∘ 𝐹)‘𝑐) |
73 | | breq1 5077 |
. . . . 5
⊢ (𝑦 = ((abs ∘ 𝐹)‘𝑐) → (𝑦 ≤ (abs‘𝐶) ↔ ((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶))) |
74 | 72, 73 | ralbid 3161 |
. . . 4
⊢ (𝑦 = ((abs ∘ 𝐹)‘𝑐) → (∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶) ↔ ∀𝑥 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶))) |
75 | 74 | rspcev 3561 |
. . 3
⊢ ((((abs
∘ 𝐹)‘𝑐) ∈ ℝ+
∧ ∀𝑥 ∈
(𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶)) |
76 | 21, 71, 75 | syl2anc 584 |
. 2
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶)) |
77 | | cncficcgt0.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
78 | | cncficcgt0.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
79 | | cncficcgt0.aleb |
. . . 4
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
80 | | ssidd 3944 |
. . . . . . 7
⊢ (𝜑 → ℂ ⊆
ℂ) |
81 | | cncfss 24062 |
. . . . . . 7
⊢
(((ℝ ∖ {0}) ⊆ ℂ ∧ ℂ ⊆ ℂ)
→ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ⊆ ((𝐴[,]𝐵)–cn→ℂ)) |
82 | 46, 80, 81 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ⊆ ((𝐴[,]𝐵)–cn→ℂ)) |
83 | 82, 1 | sseldd 3922 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
84 | | abscncf 24064 |
. . . . . 6
⊢ abs
∈ (ℂ–cn→ℝ) |
85 | 84 | a1i 11 |
. . . . 5
⊢ (𝜑 → abs ∈
(ℂ–cn→ℝ)) |
86 | 83, 85 | cncfco 24070 |
. . . 4
⊢ (𝜑 → (abs ∘ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
87 | 77, 78, 79, 86 | evthicc 24623 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ (𝐴[,]𝐵)∀𝑏 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑏) ≤ ((abs ∘ 𝐹)‘𝑎) ∧ ∃𝑐 ∈ (𝐴[,]𝐵)∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑))) |
88 | 87 | simprd 496 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) |
89 | 76, 88 | r19.29a 3218 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶)) |