Step | Hyp | Ref
| Expression |
1 | | cncficcgt0.fcn |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0}))) |
2 | | cncff 22696 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) → 𝐹:(𝐴[,]𝐵)⟶(ℝ ∖
{0})) |
3 | | ffun 6048 |
. . . . . . . 8
⊢ (𝐹:(𝐴[,]𝐵)⟶(ℝ ∖ {0}) → Fun
𝐹) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐹) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → Fun 𝐹) |
6 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → 𝑐 ∈ (𝐴[,]𝐵)) |
7 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶(ℝ ∖
{0})) |
8 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:(𝐴[,]𝐵)⟶(ℝ ∖ {0}) → dom
𝐹 = (𝐴[,]𝐵)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = (𝐴[,]𝐵)) |
10 | 9 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝜑 → (𝐴[,]𝐵) = dom 𝐹) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = dom 𝐹) |
12 | 6, 11 | eleqtrd 2703 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → 𝑐 ∈ dom 𝐹) |
13 | | fvco 6274 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑐 ∈ dom 𝐹) → ((abs ∘ 𝐹)‘𝑐) = (abs‘(𝐹‘𝑐))) |
14 | 5, 12, 13 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) = (abs‘(𝐹‘𝑐))) |
15 | 7 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑐) ∈ (ℝ ∖
{0})) |
16 | 15 | eldifad 3586 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑐) ∈ ℝ) |
17 | 16 | recnd 10068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑐) ∈ ℂ) |
18 | | eldifsni 4320 |
. . . . . . 7
⊢ ((𝐹‘𝑐) ∈ (ℝ ∖ {0}) → (𝐹‘𝑐) ≠ 0) |
19 | 15, 18 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑐) ≠ 0) |
20 | 17, 19 | absrpcld 14187 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → (abs‘(𝐹‘𝑐)) ∈
ℝ+) |
21 | 14, 20 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) ∈
ℝ+) |
22 | 21 | adantr 481 |
. . 3
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) → ((abs ∘ 𝐹)‘𝑐) ∈
ℝ+) |
23 | | nfv 1843 |
. . . . 5
⊢
Ⅎ𝑥(𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) |
24 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥(𝐴[,]𝐵) |
25 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥abs |
26 | | cncficcgt0.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) |
27 | | nfmpt1 4747 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) |
28 | 26, 27 | nfcxfr 2762 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐹 |
29 | 25, 28 | nfco 5287 |
. . . . . . . 8
⊢
Ⅎ𝑥(abs
∘ 𝐹) |
30 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑐 |
31 | 29, 30 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑥((abs
∘ 𝐹)‘𝑐) |
32 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥
≤ |
33 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑑 |
34 | 29, 33 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑥((abs
∘ 𝐹)‘𝑑) |
35 | 31, 32, 34 | nfbr 4699 |
. . . . . 6
⊢
Ⅎ𝑥((abs
∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑) |
36 | 24, 35 | nfral 2945 |
. . . . 5
⊢
Ⅎ𝑥∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑) |
37 | 23, 36 | nfan 1828 |
. . . 4
⊢
Ⅎ𝑥((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) |
38 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑑 = 𝑥 → ((abs ∘ 𝐹)‘𝑑) = ((abs ∘ 𝐹)‘𝑥)) |
39 | 38 | breq2d 4665 |
. . . . . . . 8
⊢ (𝑑 = 𝑥 → (((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑) ↔ ((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑥))) |
40 | 39 | rspccva 3308 |
. . . . . . 7
⊢
((∀𝑑 ∈
(𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑥)) |
41 | 40 | adantll 750 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑥)) |
42 | | absf 14077 |
. . . . . . . . . . 11
⊢
abs:ℂ⟶ℝ |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
44 | | difss 3737 |
. . . . . . . . . . . . 13
⊢ (ℝ
∖ {0}) ⊆ ℝ |
45 | | ax-resscn 9993 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
46 | 44, 45 | sstri 3612 |
. . . . . . . . . . . 12
⊢ (ℝ
∖ {0}) ⊆ ℂ |
47 | 46 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ ∖ {0})
⊆ ℂ) |
48 | 7, 47 | fssd 6057 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
49 | | fcompt 6400 |
. . . . . . . . . 10
⊢
((abs:ℂ⟶ℝ ∧ 𝐹:(𝐴[,]𝐵)⟶ℂ) → (abs ∘ 𝐹) = (𝑧 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑧)))) |
50 | 43, 48, 49 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (abs ∘ 𝐹) = (𝑧 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑧)))) |
51 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑧 |
52 | 28, 51 | nffv 6198 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝐹‘𝑧) |
53 | 25, 52 | nffv 6198 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(abs‘(𝐹‘𝑧)) |
54 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧(abs‘(𝐹‘𝑥)) |
55 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) |
56 | 55 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (abs‘(𝐹‘𝑧)) = (abs‘(𝐹‘𝑥))) |
57 | 53, 54, 56 | cbvmpt 4749 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑧))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑥))) |
58 | 57 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑧))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑥)))) |
59 | 26 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶)) |
60 | 59, 7 | feq1dd 39347 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶):(𝐴[,]𝐵)⟶(ℝ ∖
{0})) |
61 | 60 | mptex2 6384 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ (ℝ ∖
{0})) |
62 | 59, 61 | fvmpt2d 6293 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) = 𝐶) |
63 | 62 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (abs‘(𝐹‘𝑥)) = (abs‘𝐶)) |
64 | 63 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘(𝐹‘𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘𝐶))) |
65 | 50, 58, 64 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → (abs ∘ 𝐹) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (abs‘𝐶))) |
66 | 46, 61 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ) |
67 | 66 | abscld 14175 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (abs‘𝐶) ∈ ℝ) |
68 | 65, 67 | fvmpt2d 6293 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑥) = (abs‘𝐶)) |
69 | 68 | ad4ant14 1293 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑥) = (abs‘𝐶)) |
70 | 41, 69 | breqtrd 4679 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶)) |
71 | 70 | ex 450 |
. . . 4
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) → (𝑥 ∈ (𝐴[,]𝐵) → ((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶))) |
72 | 37, 71 | ralrimi 2957 |
. . 3
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) → ∀𝑥 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶)) |
73 | 31 | nfeq2 2780 |
. . . . 5
⊢
Ⅎ𝑥 𝑦 = ((abs ∘ 𝐹)‘𝑐) |
74 | | breq1 4656 |
. . . . 5
⊢ (𝑦 = ((abs ∘ 𝐹)‘𝑐) → (𝑦 ≤ (abs‘𝐶) ↔ ((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶))) |
75 | 73, 74 | ralbid 2983 |
. . . 4
⊢ (𝑦 = ((abs ∘ 𝐹)‘𝑐) → (∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶) ↔ ∀𝑥 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶))) |
76 | 75 | rspcev 3309 |
. . 3
⊢ ((((abs
∘ 𝐹)‘𝑐) ∈ ℝ+
∧ ∀𝑥 ∈
(𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ (abs‘𝐶)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶)) |
77 | 22, 72, 76 | syl2anc 693 |
. 2
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴[,]𝐵)) ∧ ∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶)) |
78 | | cncficcgt0.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
79 | | cncficcgt0.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
80 | | cncficcgt0.aleb |
. . . 4
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
81 | | ssid 3624 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
82 | 81 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ⊆
ℂ) |
83 | | cncfss 22702 |
. . . . . . 7
⊢
(((ℝ ∖ {0}) ⊆ ℂ ∧ ℂ ⊆ ℂ)
→ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ⊆ ((𝐴[,]𝐵)–cn→ℂ)) |
84 | 47, 82, 83 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ⊆ ((𝐴[,]𝐵)–cn→ℂ)) |
85 | 84, 1 | sseldd 3604 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
86 | | abscncf 22704 |
. . . . . 6
⊢ abs
∈ (ℂ–cn→ℝ) |
87 | 86 | a1i 11 |
. . . . 5
⊢ (𝜑 → abs ∈
(ℂ–cn→ℝ)) |
88 | 85, 87 | cncfco 22710 |
. . . 4
⊢ (𝜑 → (abs ∘ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
89 | 78, 79, 80, 88 | evthicc 23228 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ (𝐴[,]𝐵)∀𝑏 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑏) ≤ ((abs ∘ 𝐹)‘𝑎) ∧ ∃𝑐 ∈ (𝐴[,]𝐵)∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑))) |
90 | 89 | simprd 479 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)∀𝑑 ∈ (𝐴[,]𝐵)((abs ∘ 𝐹)‘𝑐) ≤ ((abs ∘ 𝐹)‘𝑑)) |
91 | 77, 90 | r19.29a 3078 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶)) |