Step | Hyp | Ref
| Expression |
1 | | hoidmvlelem1.s |
. . . . . 6
⊢ 𝑆 = sup(𝑈, ℝ, < ) |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑆 = sup(𝑈, ℝ, < )) |
3 | | hoidmvlelem1.a |
. . . . . . 7
⊢ (𝜑 → 𝐴:𝑊⟶ℝ) |
4 | | hoidmvlelem1.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) |
5 | | snidg 4153 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (𝑋 ∖ 𝑌) → 𝑍 ∈ {𝑍}) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ {𝑍}) |
7 | | elun2 3743 |
. . . . . . . . 9
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
9 | | hoidmvlelem1.w |
. . . . . . . 8
⊢ 𝑊 = (𝑌 ∪ {𝑍}) |
10 | 8, 9 | syl6eleqr 2699 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑊) |
11 | 3, 10 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) |
12 | | hoidmvlelem1.b |
. . . . . . 7
⊢ (𝜑 → 𝐵:𝑊⟶ℝ) |
13 | 12, 10 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) |
14 | | hoidmvlelem1.u |
. . . . . . . 8
⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} |
15 | | ssrab2 3650 |
. . . . . . . 8
⊢ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍)) |
16 | 14, 15 | eqsstri 3598 |
. . . . . . 7
⊢ 𝑈 ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍)) |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑈 ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
18 | 11 | leidd 10473 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴‘𝑍) ≤ (𝐴‘𝑍)) |
19 | | hoidmvlelem1.ab |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴‘𝑍) < (𝐵‘𝑍)) |
20 | 11, 13, 19 | ltled 10064 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴‘𝑍) ≤ (𝐵‘𝑍)) |
21 | 11, 13, 11, 18, 20 | eliccd 38573 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴‘𝑍) ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
22 | 11 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℂ) |
23 | 22 | subidd 10259 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝑍) − (𝐴‘𝑍)) = 0) |
24 | 23 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 · ((𝐴‘𝑍) − (𝐴‘𝑍))) = (𝐺 · 0)) |
25 | | rge0ssre 12151 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ ℝ |
26 | | hoidmvlelem1.g |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) |
27 | | hoidmvlelem1.l |
. . . . . . . . . . . . . . . . 17
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
28 | | hoidmvlelem1.x |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑋 ∈ Fin) |
29 | | hoidmvlelem1.y |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
30 | 28, 29 | ssfid 8068 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑌 ∈ Fin) |
31 | | ssun1 3738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑌 ⊆ (𝑌 ∪ {𝑍}) |
32 | 31, 9 | sseqtr4i 3601 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑌 ⊆ 𝑊 |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑌 ⊆ 𝑊) |
34 | 3, 33 | fssresd 5984 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ↾ 𝑌):𝑌⟶ℝ) |
35 | 12, 33 | fssresd 5984 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 ↾ 𝑌):𝑌⟶ℝ) |
36 | 27, 30, 34, 35 | hoidmvcl 39472 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) ∈ (0[,)+∞)) |
37 | 26, 36 | syl5eqel 2692 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ (0[,)+∞)) |
38 | 25, 37 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ ℝ) |
39 | 38 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ ℂ) |
40 | 39 | mul01d 10114 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 · 0) = 0) |
41 | 24, 40 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 · ((𝐴‘𝑍) − (𝐴‘𝑍))) = 0) |
42 | | 1red 9934 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ) |
43 | | hoidmvlelem1.e |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
44 | 43 | rpred 11748 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ ℝ) |
45 | 42, 44 | readdcld 9948 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 + 𝐸) ∈ ℝ) |
46 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
47 | | 0lt1 10429 |
. . . . . . . . . . . . . . 15
⊢ 0 <
1 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 1) |
49 | 42, 43 | ltaddrpd 11781 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 < (1 + 𝐸)) |
50 | 46, 42, 45, 48, 49 | lttrd 10077 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (1 + 𝐸)) |
51 | 46, 45, 50 | ltled 10064 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (1 + 𝐸)) |
52 | | nnex 10903 |
. . . . . . . . . . . . . . 15
⊢ ℕ
∈ V |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ ∈
V) |
54 | | icossicc 12131 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
55 | | snfi 7923 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑍} ∈ Fin |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → {𝑍} ∈ Fin) |
57 | | unfi 8112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin) |
58 | 30, 56, 57 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin) |
59 | 9, 58 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑊 ∈ Fin) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin) |
61 | | hoidmvlelem1.c |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐶:ℕ⟶(ℝ
↑𝑚 𝑊)) |
62 | 61 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑊)) |
63 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑊) → (𝐶‘𝑗):𝑊⟶ℝ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ) |
65 | | hoidmvlelem1.h |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) |
66 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = ℎ → (𝑗 ∈ 𝑌 ↔ ℎ ∈ 𝑌)) |
67 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = ℎ → (𝑐‘𝑗) = (𝑐‘ℎ)) |
68 | 67 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = ℎ → ((𝑐‘𝑗) ≤ 𝑥 ↔ (𝑐‘ℎ) ≤ 𝑥)) |
69 | 68, 67 | ifbieq1d 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = ℎ → if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥) = if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥)) |
70 | 66, 67, 69 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = ℎ → if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)) = if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥))) |
71 | 70 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))) = (ℎ ∈ 𝑊 ↦ if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥))) |
72 | 71 | mpteq2i 4669 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ (ℝ
↑𝑚 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (ℎ ∈ 𝑊 ↦ if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥)))) |
73 | 72 | mpteq2i 4669 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ
↑𝑚 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (ℎ ∈ 𝑊 ↦ if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥))))) |
74 | 65, 73 | eqtri 2632 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (ℎ ∈ 𝑊 ↦ if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥))))) |
75 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴‘𝑍) ∈ ℝ) |
76 | | hoidmvlelem1.d |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐷:ℕ⟶(ℝ
↑𝑚 𝑊)) |
77 | 76 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑊)) |
78 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑊) → (𝐷‘𝑗):𝑊⟶ℝ) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ) |
80 | 74, 75, 60, 79 | hsphoif 39466 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)):𝑊⟶ℝ) |
81 | 27, 60, 64, 80 | hoidmvcl 39472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
82 | 54, 81 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
83 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)))) |
84 | 82, 83 | fmptd 6292 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)))):ℕ⟶(0[,]+∞)) |
85 | 53, 84 | sge0cl 39274 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) ∈ (0[,]+∞)) |
86 | 53, 84 | sge0xrcl 39278 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) ∈
ℝ*) |
87 | | pnfxr 9971 |
. . . . . . . . . . . . . . 15
⊢ +∞
∈ ℝ* |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → +∞ ∈
ℝ*) |
89 | | hoidmvlelem1.r |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) |
90 | 89 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈
ℝ*) |
91 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗𝜑 |
92 | 27, 60, 64, 79 | hoidmvcl 39472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,)+∞)) |
93 | 54, 92 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,]+∞)) |
94 | 4 | eldifbd 3553 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) |
95 | 10, 94 | eldifd 3551 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑍 ∈ (𝑊 ∖ 𝑌)) |
96 | 95 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊 ∖ 𝑌)) |
97 | 27, 60, 96, 9, 75, 74, 64, 79 | hsphoidmvle 39476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) |
98 | 91, 53, 82, 93, 97 | sge0lempt 39303 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
99 | 89 | ltpnfd 11831 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞) |
100 | 86, 90, 88, 98, 99 | xrlelttrd 11867 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) < +∞) |
101 | 86, 88, 100 | xrltned 38514 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) ≠ +∞) |
102 | | ge0xrre 38605 |
. . . . . . . . . . . . 13
⊢
(((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) ∈ (0[,]+∞) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) ≠ +∞) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) ∈ ℝ) |
103 | 85, 101, 102 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) ∈ ℝ) |
104 | 53, 84 | sge0ge0 39277 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)))))) |
105 | | mulge0 10425 |
. . . . . . . . . . . 12
⊢ ((((1 +
𝐸) ∈ ℝ ∧ 0
≤ (1 + 𝐸)) ∧
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) ∈ ℝ ∧ 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))))) → 0 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))))) |
106 | 45, 51, 103, 104, 105 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))))) |
107 | 41, 106 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 · ((𝐴‘𝑍) − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))))) |
108 | 21, 107 | jca 553 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴‘𝑍) ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · ((𝐴‘𝑍) − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)))))))) |
109 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐴‘𝑍) → (𝑧 − (𝐴‘𝑍)) = ((𝐴‘𝑍) − (𝐴‘𝑍))) |
110 | 109 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐴‘𝑍) → (𝐺 · (𝑧 − (𝐴‘𝑍))) = (𝐺 · ((𝐴‘𝑍) − (𝐴‘𝑍)))) |
111 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐴‘𝑍) → (𝐻‘𝑧) = (𝐻‘(𝐴‘𝑍))) |
112 | 111 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐴‘𝑍) → ((𝐻‘𝑧)‘(𝐷‘𝑗)) = ((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))) |
113 | 112 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐴‘𝑍) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)))) |
114 | 113 | mpteq2dv 4673 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐴‘𝑍) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))) |
115 | 114 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐴‘𝑍) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)))))) |
116 | 115 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐴‘𝑍) → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗))))))) |
117 | 110, 116 | breq12d 4596 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐴‘𝑍) → ((𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) ↔ (𝐺 · ((𝐴‘𝑍) − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)))))))) |
118 | 117 | elrab 3331 |
. . . . . . . . 9
⊢ ((𝐴‘𝑍) ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ↔ ((𝐴‘𝑍) ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · ((𝐴‘𝑍) − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘(𝐴‘𝑍))‘(𝐷‘𝑗)))))))) |
119 | 108, 118 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘𝑍) ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))}) |
120 | 119, 14 | syl6eleqr 2699 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘𝑍) ∈ 𝑈) |
121 | | ne0i 3880 |
. . . . . . 7
⊢ ((𝐴‘𝑍) ∈ 𝑈 → 𝑈 ≠ ∅) |
122 | 120, 121 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈 ≠ ∅) |
123 | 11, 13, 17, 122 | supicc 12191 |
. . . . 5
⊢ (𝜑 → sup(𝑈, ℝ, < ) ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
124 | 2, 123 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
125 | 2 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → (𝑆 − (𝐴‘𝑍)) = (sup(𝑈, ℝ, < ) − (𝐴‘𝑍))) |
126 | 125 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) = (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴‘𝑍)))) |
127 | 11, 13 | iccssred 38574 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴‘𝑍)[,](𝐵‘𝑍)) ⊆ ℝ) |
128 | 17, 127 | sstrd 3578 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ⊆ ℝ) |
129 | 11, 13 | jca 553 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ)) |
130 | | iccsupr 12137 |
. . . . . . . . . 10
⊢ ((((𝐴‘𝑍) ∈ ℝ ∧ (𝐵‘𝑍) ∈ ℝ) ∧ 𝑈 ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐴‘𝑍) ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 𝑧 ≤ 𝑦)) |
131 | 129, 17, 120, 130 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 𝑧 ≤ 𝑦)) |
132 | 131 | simp3d 1068 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 𝑧 ≤ 𝑦) |
133 | | eqid 2610 |
. . . . . . . 8
⊢ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} = {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} |
134 | 128, 122,
132, 11, 133 | supsubc 38510 |
. . . . . . 7
⊢ (𝜑 → (sup(𝑈, ℝ, < ) − (𝐴‘𝑍)) = sup({𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}, ℝ, < )) |
135 | 134 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (𝐺 · (sup(𝑈, ℝ, < ) − (𝐴‘𝑍))) = (𝐺 · sup({𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}, ℝ, < ))) |
136 | 46 | rexrd 9968 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ*) |
137 | | icogelb 12096 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐺 ∈ (0[,)+∞))
→ 0 ≤ 𝐺) |
138 | 136, 88, 37, 137 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐺) |
139 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑟 ∈ V |
140 | | eqeq1 2614 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑟 → (𝑤 = (𝑢 − (𝐴‘𝑍)) ↔ 𝑟 = (𝑢 − (𝐴‘𝑍)))) |
141 | 140 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑟 → (∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍)) ↔ ∃𝑢 ∈ 𝑈 𝑟 = (𝑢 − (𝐴‘𝑍)))) |
142 | 139, 141 | elab 3319 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ↔ ∃𝑢 ∈ 𝑈 𝑟 = (𝑢 − (𝐴‘𝑍))) |
143 | 142 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} → ∃𝑢 ∈ 𝑈 𝑟 = (𝑢 − (𝐴‘𝑍))) |
144 | 143 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → ∃𝑢 ∈ 𝑈 𝑟 = (𝑢 − (𝐴‘𝑍))) |
145 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢𝜑 |
146 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑢𝑟 |
147 | | nfre1 2988 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑢∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍)) |
148 | 147 | nfab 2755 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑢{𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} |
149 | 146, 148 | nfel 2763 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢 𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} |
150 | 145, 149 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑢(𝜑 ∧ 𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) |
151 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑢0 ≤ 𝑟 |
152 | 11 | rexrd 9968 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴‘𝑍) ∈
ℝ*) |
153 | 152 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐴‘𝑍) ∈
ℝ*) |
154 | 13 | rexrd 9968 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵‘𝑍) ∈
ℝ*) |
155 | 154 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐵‘𝑍) ∈
ℝ*) |
156 | 17 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
157 | | iccgelb 12101 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝑍) ∈ ℝ* ∧ (𝐵‘𝑍) ∈ ℝ* ∧ 𝑢 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) → (𝐴‘𝑍) ≤ 𝑢) |
158 | 153, 155,
156, 157 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐴‘𝑍) ≤ 𝑢) |
159 | 128 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ ℝ) |
160 | 11 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐴‘𝑍) ∈ ℝ) |
161 | 159, 160 | subge0d 10496 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (0 ≤ (𝑢 − (𝐴‘𝑍)) ↔ (𝐴‘𝑍) ≤ 𝑢)) |
162 | 158, 161 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 0 ≤ (𝑢 − (𝐴‘𝑍))) |
163 | 162 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑟 = (𝑢 − (𝐴‘𝑍))) → 0 ≤ (𝑢 − (𝐴‘𝑍))) |
164 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = (𝑢 − (𝐴‘𝑍)) → 𝑟 = (𝑢 − (𝐴‘𝑍))) |
165 | 164 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = (𝑢 − (𝐴‘𝑍)) → (𝑢 − (𝐴‘𝑍)) = 𝑟) |
166 | 165 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑟 = (𝑢 − (𝐴‘𝑍))) → (𝑢 − (𝐴‘𝑍)) = 𝑟) |
167 | 163, 166 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑟 = (𝑢 − (𝐴‘𝑍))) → 0 ≤ 𝑟) |
168 | 167 | 3exp 1256 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ 𝑈 → (𝑟 = (𝑢 − (𝐴‘𝑍)) → 0 ≤ 𝑟))) |
169 | 168 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → (𝑢 ∈ 𝑈 → (𝑟 = (𝑢 − (𝐴‘𝑍)) → 0 ≤ 𝑟))) |
170 | 150, 151,
169 | rexlimd 3008 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → (∃𝑢 ∈ 𝑈 𝑟 = (𝑢 − (𝐴‘𝑍)) → 0 ≤ 𝑟)) |
171 | 144, 170 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → 0 ≤ 𝑟) |
172 | 171 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}0 ≤ 𝑟) |
173 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑤 = (𝑢 − (𝐴‘𝑍))) → 𝑤 = (𝑢 − (𝐴‘𝑍))) |
174 | 159, 160 | resubcld 10337 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 − (𝐴‘𝑍)) ∈ ℝ) |
175 | 174 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑤 = (𝑢 − (𝐴‘𝑍))) → (𝑢 − (𝐴‘𝑍)) ∈ ℝ) |
176 | 173, 175 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑤 = (𝑢 − (𝐴‘𝑍))) → 𝑤 ∈ ℝ) |
177 | 176 | 3exp 1256 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ 𝑈 → (𝑤 = (𝑢 − (𝐴‘𝑍)) → 𝑤 ∈ ℝ))) |
178 | 177 | rexlimdv 3012 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍)) → 𝑤 ∈ ℝ)) |
179 | 178 | alrimiv 1842 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑤(∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍)) → 𝑤 ∈ ℝ)) |
180 | | abss 3634 |
. . . . . . . 8
⊢ ({𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ⊆ ℝ ↔ ∀𝑤(∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍)) → 𝑤 ∈ ℝ)) |
181 | 179, 180 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ⊆ ℝ) |
182 | 23 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝜑 → 0 = ((𝐴‘𝑍) − (𝐴‘𝑍))) |
183 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐴‘𝑍) → (𝑢 − (𝐴‘𝑍)) = ((𝐴‘𝑍) − (𝐴‘𝑍))) |
184 | 183 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝐴‘𝑍) → (0 = (𝑢 − (𝐴‘𝑍)) ↔ 0 = ((𝐴‘𝑍) − (𝐴‘𝑍)))) |
185 | 184 | rspcev 3282 |
. . . . . . . . . 10
⊢ (((𝐴‘𝑍) ∈ 𝑈 ∧ 0 = ((𝐴‘𝑍) − (𝐴‘𝑍))) → ∃𝑢 ∈ 𝑈 0 = (𝑢 − (𝐴‘𝑍))) |
186 | 120, 182,
185 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑢 ∈ 𝑈 0 = (𝑢 − (𝐴‘𝑍))) |
187 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
188 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑤 = 0 → (𝑤 = (𝑢 − (𝐴‘𝑍)) ↔ 0 = (𝑢 − (𝐴‘𝑍)))) |
189 | 188 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑤 = 0 → (∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍)) ↔ ∃𝑢 ∈ 𝑈 0 = (𝑢 − (𝐴‘𝑍)))) |
190 | 187, 189 | elab 3319 |
. . . . . . . . 9
⊢ (0 ∈
{𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ↔ ∃𝑢 ∈ 𝑈 0 = (𝑢 − (𝐴‘𝑍))) |
191 | 186, 190 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) |
192 | | ne0i 3880 |
. . . . . . . 8
⊢ (0 ∈
{𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} → {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ≠ ∅) |
193 | 191, 192 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ≠ ∅) |
194 | 13, 11 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ) |
195 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑠 ∈ V |
196 | | eqeq1 2614 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑠 → (𝑤 = (𝑢 − (𝐴‘𝑍)) ↔ 𝑠 = (𝑢 − (𝐴‘𝑍)))) |
197 | 196 | rexbidv 3034 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑠 → (∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍)) ↔ ∃𝑢 ∈ 𝑈 𝑠 = (𝑢 − (𝐴‘𝑍)))) |
198 | 195, 197 | elab 3319 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ↔ ∃𝑢 ∈ 𝑈 𝑠 = (𝑢 − (𝐴‘𝑍))) |
199 | 198 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} → ∃𝑢 ∈ 𝑈 𝑠 = (𝑢 − (𝐴‘𝑍))) |
200 | 199 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → ∃𝑢 ∈ 𝑈 𝑠 = (𝑢 − (𝐴‘𝑍))) |
201 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑢𝑠 |
202 | 201, 148 | nfel 2763 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑢 𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} |
203 | 145, 202 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢(𝜑 ∧ 𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) |
204 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑢 𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍)) |
205 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = (𝑢 − (𝐴‘𝑍))) → 𝑠 = (𝑢 − (𝐴‘𝑍))) |
206 | 160 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = (𝑢 − (𝐴‘𝑍))) → (𝐴‘𝑍) ∈ ℝ) |
207 | 13 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = (𝑢 − (𝐴‘𝑍))) → (𝐵‘𝑍) ∈ ℝ) |
208 | 156 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = (𝑢 − (𝐴‘𝑍))) → 𝑢 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
209 | 21 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = (𝑢 − (𝐴‘𝑍))) → (𝐴‘𝑍) ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
210 | 206, 207,
208, 209 | iccsuble 38592 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = (𝑢 − (𝐴‘𝑍))) → (𝑢 − (𝐴‘𝑍)) ≤ ((𝐵‘𝑍) − (𝐴‘𝑍))) |
211 | 205, 210 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑠 = (𝑢 − (𝐴‘𝑍))) → 𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍))) |
212 | 211 | 3exp 1256 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑢 ∈ 𝑈 → (𝑠 = (𝑢 − (𝐴‘𝑍)) → 𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍))))) |
213 | 212 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → (𝑢 ∈ 𝑈 → (𝑠 = (𝑢 − (𝐴‘𝑍)) → 𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍))))) |
214 | 203, 204,
213 | rexlimd 3008 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → (∃𝑢 ∈ 𝑈 𝑠 = (𝑢 − (𝐴‘𝑍)) → 𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍)))) |
215 | 200, 214 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → 𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍))) |
216 | 215 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍))) |
217 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑟 = ((𝐵‘𝑍) − (𝐴‘𝑍)) → (𝑠 ≤ 𝑟 ↔ 𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍)))) |
218 | 217 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑟 = ((𝐵‘𝑍) − (𝐴‘𝑍)) → (∀𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑠 ≤ 𝑟 ↔ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍)))) |
219 | 218 | rspcev 3282 |
. . . . . . . 8
⊢ ((((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ ∧ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑠 ≤ ((𝐵‘𝑍) − (𝐴‘𝑍))) → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑠 ≤ 𝑟) |
220 | 194, 216,
219 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑠 ≤ 𝑟) |
221 | | eqid 2610 |
. . . . . . . 8
⊢ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} = {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} |
222 | | biid 250 |
. . . . . . . 8
⊢ (((𝐺 ∈ ℝ ∧ 0 ≤
𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑠 ≤ 𝑟)) ↔ ((𝐺 ∈ ℝ ∧ 0 ≤ 𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑠 ≤ 𝑟))) |
223 | 221, 222 | supmul1 10869 |
. . . . . . 7
⊢ (((𝐺 ∈ ℝ ∧ 0 ≤
𝐺 ∧ ∀𝑟 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}0 ≤ 𝑟) ∧ ({𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ⊆ ℝ ∧ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ≠ ∅ ∧ ∃𝑟 ∈ ℝ ∀𝑠 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑠 ≤ 𝑟)) → (𝐺 · sup({𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < )) |
224 | 38, 138, 172, 181, 193, 220, 223 | syl33anc 1333 |
. . . . . 6
⊢ (𝜑 → (𝐺 · sup({𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}, ℝ, < )) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < )) |
225 | 126, 135,
224 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) = sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < )) |
226 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑐 ∈ V |
227 | | eqeq1 2614 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑐 → (𝑣 = (𝐺 · 𝑡) ↔ 𝑐 = (𝐺 · 𝑡))) |
228 | 227 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑐 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑐 = (𝐺 · 𝑡))) |
229 | 226, 228 | elab 3319 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑐 = (𝐺 · 𝑡)) |
230 | 229 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑐 = (𝐺 · 𝑡)) |
231 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))) |
232 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑡 ∈ V |
233 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑡 → (𝑤 = (𝑢 − (𝐴‘𝑍)) ↔ 𝑡 = (𝑢 − (𝐴‘𝑍)))) |
234 | 233 | rexbidv 3034 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑡 → (∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍)) ↔ ∃𝑢 ∈ 𝑈 𝑡 = (𝑢 − (𝐴‘𝑍)))) |
235 | 232, 234 | elab 3319 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ↔ ∃𝑢 ∈ 𝑈 𝑡 = (𝑢 − (𝐴‘𝑍))) |
236 | 235 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} → ∃𝑢 ∈ 𝑈 𝑡 = (𝑢 − (𝐴‘𝑍))) |
237 | 236 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢 ∈ 𝑈 𝑡 = (𝑢 − (𝐴‘𝑍))) |
238 | | simpl 472 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) → 𝑐 = (𝐺 · 𝑡)) |
239 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (𝑢 − (𝐴‘𝑍)) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴‘𝑍)))) |
240 | 239 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) → (𝐺 · 𝑡) = (𝐺 · (𝑢 − (𝐴‘𝑍)))) |
241 | 238, 240 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝐺 · 𝑡) ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) → 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) |
242 | 241 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝐺 · 𝑡) → (𝑡 = (𝑢 − (𝐴‘𝑍)) → 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))))) |
243 | 242 | reximdv 2999 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝐺 · 𝑡) → (∃𝑢 ∈ 𝑈 𝑡 = (𝑢 − (𝐴‘𝑍)) → ∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))))) |
244 | 243 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → (∃𝑢 ∈ 𝑈 𝑡 = (𝑢 − (𝐴‘𝑍)) → ∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))))) |
245 | 237, 244 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ∧ 𝑐 = (𝐺 · 𝑡)) → ∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) |
246 | 245 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} → (𝑐 = (𝐺 · 𝑡) → ∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))))) |
247 | 231, 246 | rexlimi 3006 |
. . . . . . . . . . 11
⊢
(∃𝑡 ∈
{𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) |
248 | 247 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑐 = (𝐺 · 𝑡) → ∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))))) |
249 | 230, 248 | mpd 15 |
. . . . . . . . 9
⊢ (𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} → ∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) |
250 | 249 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) |
251 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) → 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) |
252 | 38 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝐺 ∈ ℝ) |
253 | 252, 174 | remulcld 9949 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐺 · (𝑢 − (𝐴‘𝑍))) ∈ ℝ) |
254 | 45 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (1 + 𝐸) ∈ ℝ) |
255 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ℕ ∈ V) |
256 | 60 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin) |
257 | 64 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ) |
258 | 159 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢 ∈ ℝ) |
259 | 79 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ) |
260 | 74, 258, 256, 259 | hsphoif 39466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑢)‘(𝐷‘𝑗)):𝑊⟶ℝ) |
261 | 27, 256, 257, 260 | hoidmvcl 39472 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
262 | 54, 261 | sseldi 3566 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
263 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))) |
264 | 262, 263 | fmptd 6292 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))):ℕ⟶(0[,]+∞)) |
265 | 255, 264 | sge0cl 39274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) ∈ (0[,]+∞)) |
266 | 255, 264 | sge0xrcl 39278 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) ∈
ℝ*) |
267 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → +∞ ∈
ℝ*) |
268 | 90 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈
ℝ*) |
269 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗(𝜑 ∧ 𝑢 ∈ 𝑈) |
270 | 93 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,]+∞)) |
271 | 96 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊 ∖ 𝑌)) |
272 | 27, 256, 271, 9, 258, 74, 257, 259 | hsphoidmvle 39476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) |
273 | 269, 255,
262, 270, 272 | sge0lempt 39303 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
274 | 99 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞) |
275 | 266, 268,
267, 273, 274 | xrlelttrd 11867 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) < +∞) |
276 | 266, 267,
275 | xrltned 38514 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) ≠ +∞) |
277 | | ge0xrre 38605 |
. . . . . . . . . . . . . . . 16
⊢
(((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) ∈ (0[,]+∞) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) ≠ +∞) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) ∈ ℝ) |
278 | 265, 276,
277 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) ∈ ℝ) |
279 | 254, 278 | remulcld 9949 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))))) ∈ ℝ) |
280 | 127, 124 | sseldd 3569 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 ∈ ℝ) |
281 | 27, 30, 95, 9, 61, 76, 89, 65, 280 | sge0hsphoire 39479 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) |
282 | 45, 281 | remulcld 9949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℝ) |
283 | 282 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℝ) |
284 | 14 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))}) |
285 | 284 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ 𝑈 → 𝑢 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))}) |
286 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑢 → (𝑧 − (𝐴‘𝑍)) = (𝑢 − (𝐴‘𝑍))) |
287 | 286 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑢 → (𝐺 · (𝑧 − (𝐴‘𝑍))) = (𝐺 · (𝑢 − (𝐴‘𝑍)))) |
288 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑢 → (𝐻‘𝑧) = (𝐻‘𝑢)) |
289 | 288 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑢 → ((𝐻‘𝑧)‘(𝐷‘𝑗)) = ((𝐻‘𝑢)‘(𝐷‘𝑗))) |
290 | 289 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑢 → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))) |
291 | 290 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑢 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) |
292 | 291 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑢 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))))) |
293 | 292 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑢 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))))) |
294 | 287, 293 | breq12d 4596 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑢 → ((𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) ↔ (𝐺 · (𝑢 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))))))) |
295 | 294 | elrab 3331 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ↔ (𝑢 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑢 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))))))) |
296 | 285, 295 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ 𝑈 → (𝑢 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑢 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))))))) |
297 | 296 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑈 → (𝐺 · (𝑢 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))))) |
298 | 297 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐺 · (𝑢 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))))) |
299 | 281 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) |
300 | 51 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 0 ≤ (1 + 𝐸)) |
301 | 280 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ) |
302 | 74, 301, 60, 79 | hsphoif 39466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑆)‘(𝐷‘𝑗)):𝑊⟶ℝ) |
303 | 27, 60, 64, 302 | hoidmvcl 39472 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
304 | 54, 303 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
305 | 304 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
306 | 301 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ) |
307 | 128 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 ⊆ ℝ) |
308 | 122 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 ≠ ∅) |
309 | 132 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 𝑧 ≤ 𝑦) |
310 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈) |
311 | | suprub 10863 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑈 𝑧 ≤ 𝑦) ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < )) |
312 | 307, 308,
309, 310, 311 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < )) |
313 | 312, 1 | syl6breqr 4625 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ 𝑆) |
314 | 313 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → 𝑢 ≤ 𝑆) |
315 | 27, 256, 271, 9, 258, 306, 314, 74, 257, 259 | hsphoidmvle2 39475 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
316 | 269, 255,
262, 305, 315 | sge0lempt 39303 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) |
317 | 278, 299,
254, 300, 316 | lemul2ad 10843 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑢)‘(𝐷‘𝑗)))))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
318 | 253, 279,
283, 298, 317 | letrd 10073 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐺 · (𝑢 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
319 | 318 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) → (𝐺 · (𝑢 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
320 | 251, 319 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) → 𝑐 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
321 | 320 | 3exp 1256 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ 𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))) → 𝑐 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))))) |
322 | 321 | rexlimdv 3012 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))) → 𝑐 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
323 | 322 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))) → 𝑐 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
324 | 250, 323 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
325 | 324 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
326 | 230 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑐 = (𝐺 · 𝑡)) |
327 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝜑 |
328 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡𝑐 |
329 | | nfre1 2988 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡) |
330 | 329 | nfab 2755 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡{𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} |
331 | 328, 330 | nfel 2763 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} |
332 | 327, 331 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) |
333 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡 𝑐 ∈ ℝ |
334 | 236 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → ∃𝑢 ∈ 𝑈 𝑡 = (𝑢 − (𝐴‘𝑍))) |
335 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 = (𝐺 · 𝑡)) |
336 | 252 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) → 𝐺 ∈ ℝ) |
337 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) → 𝑡 = (𝑢 − (𝐴‘𝑍))) |
338 | 174 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) → (𝑢 − (𝐴‘𝑍)) ∈ ℝ) |
339 | 337, 338 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) → 𝑡 ∈ ℝ) |
340 | 336, 339 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) → (𝐺 · 𝑡) ∈ ℝ) |
341 | 340 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → (𝐺 · 𝑡) ∈ ℝ) |
342 | 335, 341 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) ∧ 𝑐 = (𝐺 · 𝑡)) → 𝑐 ∈ ℝ) |
343 | 342 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑡 = (𝑢 − (𝐴‘𝑍))) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)) |
344 | 343 | 3exp 1256 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑢 ∈ 𝑈 → (𝑡 = (𝑢 − (𝐴‘𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)))) |
345 | 344 | rexlimdv 3012 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∃𝑢 ∈ 𝑈 𝑡 = (𝑢 − (𝐴‘𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))) |
346 | 345 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → (∃𝑢 ∈ 𝑈 𝑡 = (𝑢 − (𝐴‘𝑍)) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))) |
347 | 334, 346 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}) → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)) |
348 | 347 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))) |
349 | 348 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) → (𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} → (𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ))) |
350 | 332, 333,
349 | rexlimd 3008 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑐 = (𝐺 · 𝑡) → 𝑐 ∈ ℝ)) |
351 | 326, 350 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ∈ ℝ) |
352 | 351 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ) |
353 | | dfss3 3558 |
. . . . . . . 8
⊢ ({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ∈ ℝ) |
354 | 352, 353 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ) |
355 | 40 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝜑 → 0 = (𝐺 · 0)) |
356 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑡 = 0 → (𝐺 · 𝑡) = (𝐺 · 0)) |
357 | 356 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑡 = 0 → (0 = (𝐺 · 𝑡) ↔ 0 = (𝐺 · 0))) |
358 | 357 | rspcev 3282 |
. . . . . . . . . 10
⊢ ((0
∈ {𝑤 ∣
∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))} ∧ 0 = (𝐺 · 0)) → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}0 = (𝐺 · 𝑡)) |
359 | 191, 355,
358 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}0 = (𝐺 · 𝑡)) |
360 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑣 = 0 → (𝑣 = (𝐺 · 𝑡) ↔ 0 = (𝐺 · 𝑡))) |
361 | 360 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑣 = 0 → (∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡) ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}0 = (𝐺 · 𝑡))) |
362 | 187, 361 | elab 3319 |
. . . . . . . . 9
⊢ (0 ∈
{𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} ↔ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}0 = (𝐺 · 𝑡)) |
363 | 359, 362 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) |
364 | | ne0i 3880 |
. . . . . . . 8
⊢ (0 ∈
{𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅) |
365 | 363, 364 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅) |
366 | 38, 194 | remulcld 9949 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍))) ∈ ℝ) |
367 | 194 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((𝐵‘𝑍) − (𝐴‘𝑍)) ∈ ℝ) |
368 | 138 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 0 ≤ 𝐺) |
369 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐵‘𝑍) ∈ ℝ) |
370 | | iccleub 12100 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴‘𝑍) ∈ ℝ* ∧ (𝐵‘𝑍) ∈ ℝ* ∧ 𝑢 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) → 𝑢 ≤ (𝐵‘𝑍)) |
371 | 153, 155,
156, 370 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ (𝐵‘𝑍)) |
372 | 159, 369,
160, 371 | lesub1dd 10522 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 − (𝐴‘𝑍)) ≤ ((𝐵‘𝑍) − (𝐴‘𝑍))) |
373 | 174, 367,
252, 368, 372 | lemul2ad 10843 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐺 · (𝑢 − (𝐴‘𝑍))) ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍)))) |
374 | 373 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) → (𝐺 · (𝑢 − (𝐴‘𝑍))) ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍)))) |
375 | 251, 374 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈 ∧ 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍)))) → 𝑐 ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍)))) |
376 | 375 | 3exp 1256 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑢 ∈ 𝑈 → (𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍)))))) |
377 | 376 | rexlimdv 3012 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍))))) |
378 | 377 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) → (∃𝑢 ∈ 𝑈 𝑐 = (𝐺 · (𝑢 − (𝐴‘𝑍))) → 𝑐 ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍))))) |
379 | 250, 378 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}) → 𝑐 ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍)))) |
380 | 379 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍)))) |
381 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍))) → (𝑐 ≤ 𝑦 ↔ 𝑐 ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍))))) |
382 | 381 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑦 = (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍))) → (∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ 𝑦 ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍))))) |
383 | 382 | rspcev 3282 |
. . . . . . . 8
⊢ (((𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍))) ∈ ℝ ∧ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ (𝐺 · ((𝐵‘𝑍) − (𝐴‘𝑍)))) → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ 𝑦) |
384 | 366, 380,
383 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ 𝑦) |
385 | | suprleub 10866 |
. . . . . . 7
⊢ ((({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} ⊆ ℝ ∧ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)} ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ 𝑦) ∧ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℝ) → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
386 | 354, 365,
384, 282, 385 | syl31anc 1321 |
. . . . . 6
⊢ (𝜑 → (sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ↔ ∀𝑐 ∈ {𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}𝑐 ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
387 | 325, 386 | mpbird 246 |
. . . . 5
⊢ (𝜑 → sup({𝑣 ∣ ∃𝑡 ∈ {𝑤 ∣ ∃𝑢 ∈ 𝑈 𝑤 = (𝑢 − (𝐴‘𝑍))}𝑣 = (𝐺 · 𝑡)}, ℝ, < ) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
388 | 225, 387 | eqbrtrd 4605 |
. . . 4
⊢ (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
389 | 124, 388 | jca 553 |
. . 3
⊢ (𝜑 → (𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
390 | | oveq1 6556 |
. . . . . 6
⊢ (𝑧 = 𝑆 → (𝑧 − (𝐴‘𝑍)) = (𝑆 − (𝐴‘𝑍))) |
391 | 390 | oveq2d 6565 |
. . . . 5
⊢ (𝑧 = 𝑆 → (𝐺 · (𝑧 − (𝐴‘𝑍))) = (𝐺 · (𝑆 − (𝐴‘𝑍)))) |
392 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑆 → (𝐻‘𝑧) = (𝐻‘𝑆)) |
393 | 392 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑧 = 𝑆 → ((𝐻‘𝑧)‘(𝐷‘𝑗)) = ((𝐻‘𝑆)‘(𝐷‘𝑗))) |
394 | 393 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑧 = 𝑆 → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
395 | 394 | mpteq2dv 4673 |
. . . . . . 7
⊢ (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) |
396 | 395 | fveq2d 6107 |
. . . . . 6
⊢ (𝑧 = 𝑆 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) |
397 | 396 | oveq2d 6565 |
. . . . 5
⊢ (𝑧 = 𝑆 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
398 | 391, 397 | breq12d 4596 |
. . . 4
⊢ (𝑧 = 𝑆 → ((𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) ↔ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
399 | 398 | elrab 3331 |
. . 3
⊢ (𝑆 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ↔ (𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
400 | 389, 399 | sylibr 223 |
. 2
⊢ (𝜑 → 𝑆 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))}) |
401 | 400, 14 | syl6eleqr 2699 |
1
⊢ (𝜑 → 𝑆 ∈ 𝑈) |