Step | Hyp | Ref
| Expression |
1 | | icccmp.13 |
. . . . . . 7
⊢ 𝐺 = sup(𝑆, ℝ, < ) |
2 | | icccmp.4 |
. . . . . . . . . 10
⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} |
3 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} ⊆ (𝐴[,]𝐵) |
4 | 2, 3 | eqsstri 3598 |
. . . . . . . . 9
⊢ 𝑆 ⊆ (𝐴[,]𝐵) |
5 | | icccmp.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
6 | | icccmp.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
7 | | iccssre 12126 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
8 | 5, 6, 7 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
9 | 4, 8 | syl5ss 3579 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
10 | | icccmp.1 |
. . . . . . . . . . 11
⊢ 𝐽 = (topGen‘ran
(,)) |
11 | | icccmp.2 |
. . . . . . . . . . 11
⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) |
12 | | icccmp.3 |
. . . . . . . . . . 11
⊢ 𝐷 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
13 | | icccmp.7 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
14 | | icccmp.8 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ 𝐽) |
15 | | icccmp.9 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
16 | 10, 11, 12, 2, 5, 6,
13, 14, 15 | icccmplem1 22433 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
17 | 16 | simpld 474 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
18 | | ne0i 3880 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑆 → 𝑆 ≠ ∅) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ≠ ∅) |
20 | 16 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) |
21 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝐵 → (𝑦 ≤ 𝑛 ↔ 𝑦 ≤ 𝐵)) |
22 | 21 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑛 = 𝐵 → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
23 | 22 | rspcev 3282 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧
∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) → ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) |
24 | 6, 20, 23 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) |
25 | | suprcl 10862 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) → sup(𝑆, ℝ, < ) ∈
ℝ) |
26 | 9, 19, 24, 25 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈
ℝ) |
27 | 1, 26 | syl5eqel 2692 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ℝ) |
28 | | icccmp.11 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
29 | 28 | rphalfcld 11760 |
. . . . . 6
⊢ (𝜑 → (𝐶 / 2) ∈
ℝ+) |
30 | 27, 29 | ltaddrpd 11781 |
. . . . 5
⊢ (𝜑 → 𝐺 < (𝐺 + (𝐶 / 2))) |
31 | 29 | rpred 11748 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 2) ∈ ℝ) |
32 | 27, 31 | readdcld 9948 |
. . . . . 6
⊢ (𝜑 → (𝐺 + (𝐶 / 2)) ∈ ℝ) |
33 | 27, 32 | ltnled 10063 |
. . . . 5
⊢ (𝜑 → (𝐺 < (𝐺 + (𝐶 / 2)) ↔ ¬ (𝐺 + (𝐶 / 2)) ≤ 𝐺)) |
34 | 30, 33 | mpbid 221 |
. . . 4
⊢ (𝜑 → ¬ (𝐺 + (𝐶 / 2)) ≤ 𝐺) |
35 | | icccmp.14 |
. . . . . . . . . 10
⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) |
36 | 32, 6 | ifcld 4081 |
. . . . . . . . . 10
⊢ (𝜑 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ∈ ℝ) |
37 | 35, 36 | syl5eqel 2692 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ℝ) |
38 | | suprub 10863 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) ∧ 𝐴 ∈ 𝑆) → 𝐴 ≤ sup(𝑆, ℝ, < )) |
39 | 9, 19, 24, 17, 38 | syl31anc 1321 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < )) |
40 | 39, 1 | syl6breqr 4625 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 𝐺) |
41 | 27, 32, 30 | ltled 10064 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ≤ (𝐺 + (𝐶 / 2))) |
42 | 5, 27, 32, 40, 41 | letrd 10073 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ (𝐺 + (𝐶 / 2))) |
43 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ ((𝐺 + (𝐶 / 2)) = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) → (𝐴 ≤ (𝐺 + (𝐶 / 2)) ↔ 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵))) |
44 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝐵 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵))) |
45 | 43, 44 | ifboth 4074 |
. . . . . . . . . . 11
⊢ ((𝐴 ≤ (𝐺 + (𝐶 / 2)) ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵)) |
46 | 42, 13, 45 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵)) |
47 | 46, 35 | syl6breqr 4625 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝑅) |
48 | | min2 11895 |
. . . . . . . . . . 11
⊢ (((𝐺 + (𝐶 / 2)) ∈ ℝ ∧ 𝐵 ∈ ℝ) →
if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ 𝐵) |
49 | 32, 6, 48 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ 𝐵) |
50 | 35, 49 | syl5eqbr 4618 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ≤ 𝐵) |
51 | | elicc2 12109 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑅 ∈ (𝐴[,]𝐵) ↔ (𝑅 ∈ ℝ ∧ 𝐴 ≤ 𝑅 ∧ 𝑅 ≤ 𝐵))) |
52 | 5, 6, 51 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ (𝐴[,]𝐵) ↔ (𝑅 ∈ ℝ ∧ 𝐴 ≤ 𝑅 ∧ 𝑅 ≤ 𝐵))) |
53 | 37, 47, 50, 52 | mpbir3and 1238 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ (𝐴[,]𝐵)) |
54 | 27, 28 | ltsubrpd 11780 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 − 𝐶) < 𝐺) |
55 | 54, 1 | syl6breq 4624 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 − 𝐶) < sup(𝑆, ℝ, < )) |
56 | 28 | rpred 11748 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℝ) |
57 | 27, 56 | resubcld 10337 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 − 𝐶) ∈ ℝ) |
58 | | suprlub 10864 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) ∧ (𝐺 − 𝐶) ∈ ℝ) → ((𝐺 − 𝐶) < sup(𝑆, ℝ, < ) ↔ ∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣)) |
59 | 9, 19, 24, 57, 58 | syl31anc 1321 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺 − 𝐶) < sup(𝑆, ℝ, < ) ↔ ∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣)) |
60 | 55, 59 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣) |
61 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑣 → (𝐴[,]𝑥) = (𝐴[,]𝑣)) |
62 | 61 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → ((𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝑣) ⊆ ∪ 𝑧)) |
63 | 62 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑣 → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧)) |
64 | 63, 2 | elrab2 3333 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑆 ↔ (𝑣 ∈ (𝐴[,]𝐵) ∧ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧)) |
65 | | unieq 4380 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ∪ 𝑧 = ∪
𝑤) |
66 | 65 | sseq2d 3596 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → ((𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝑣) ⊆ ∪ 𝑤)) |
67 | 66 | cbvrexv 3148 |
. . . . . . . . . . . . 13
⊢
(∃𝑧 ∈
(𝒫 𝑈 ∩
Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ ∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑤) |
68 | | simpr1 1060 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ∈ (𝒫 𝑈 ∩ Fin)) |
69 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ↔ (𝑤 ∈ 𝒫 𝑈 ∧ 𝑤 ∈ Fin)) |
70 | 68, 69 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∈ 𝒫 𝑈 ∧ 𝑤 ∈ Fin)) |
71 | 70 | simpld 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ∈ 𝒫 𝑈) |
72 | 71 | elpwid 4118 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ⊆ 𝑈) |
73 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝜑) |
74 | | icccmp.10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑉 ∈ 𝑈) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑉 ∈ 𝑈) |
76 | 75 | snssd 4281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → {𝑉} ⊆ 𝑈) |
77 | 72, 76 | unssd 3751 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ⊆ 𝑈) |
78 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑤 ∈ V |
79 | | snex 4835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑉} ∈ V |
80 | 78, 79 | unex 6854 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∪ {𝑉}) ∈ V |
81 | 80 | elpw 4114 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∪ {𝑉}) ∈ 𝒫 𝑈 ↔ (𝑤 ∪ {𝑉}) ⊆ 𝑈) |
82 | 77, 81 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ∈ 𝒫 𝑈) |
83 | 70 | simprd 478 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ∈ Fin) |
84 | | snfi 7923 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑉} ∈ Fin |
85 | | unfi 8112 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Fin ∧ {𝑉} ∈ Fin) → (𝑤 ∪ {𝑉}) ∈ Fin) |
86 | 83, 84, 85 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ∈ Fin) |
87 | 82, 86 | elind 3760 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ∈ (𝒫 𝑈 ∩ Fin)) |
88 | | simplr2 1097 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → (𝐴[,]𝑣) ⊆ ∪ 𝑤) |
89 | | ssun1 3738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ 𝑤
⊆ (∪ 𝑤 ∪ 𝑉) |
90 | 88, 89 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → (𝐴[,]𝑣) ⊆ (∪ 𝑤 ∪ 𝑉)) |
91 | 73, 5 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝐴 ∈ ℝ) |
92 | 73, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑅 ∈ ℝ) |
93 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (𝐴[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
94 | 91, 92, 93 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑡 ∈ (𝐴[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
95 | 94 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)) |
96 | 95 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑡 ∈ ℝ) |
97 | 96 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ∈ ℝ) |
98 | 95 | simp2d 1067 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝐴 ≤ 𝑡) |
99 | 98 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝐴 ≤ 𝑡) |
100 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ≤ 𝑣) |
101 | 73, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝐴[,]𝐵) ⊆ ℝ) |
102 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑣 ∈ (𝐴[,]𝐵)) |
103 | 101, 102 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑣 ∈ ℝ) |
104 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑡 ∈ (𝐴[,]𝑣) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣))) |
105 | 91, 103, 104 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑡 ∈ (𝐴[,]𝑣) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣))) |
106 | 105 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → (𝑡 ∈ (𝐴[,]𝑣) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣))) |
107 | 97, 99, 100, 106 | mpbir3and 1238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ∈ (𝐴[,]𝑣)) |
108 | 90, 107 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
109 | 108 | expr 641 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑡 ≤ 𝑣 → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉))) |
110 | 73 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝜑) |
111 | | icccmp.12 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) |
113 | 96 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ ℝ) |
114 | 110, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 − 𝐶) ∈ ℝ) |
115 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑣 ∈ ℝ) |
116 | | simplr3 1098 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 − 𝐶) < 𝑣) |
117 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑣 < 𝑡) |
118 | 114, 115,
113, 116, 117 | lttrd 10077 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 − 𝐶) < 𝑡) |
119 | 110, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑅 ∈ ℝ) |
120 | 27, 56 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐺 + 𝐶) ∈ ℝ) |
121 | 110, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 + 𝐶) ∈ ℝ) |
122 | 95 | simp3d 1068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑡 ≤ 𝑅) |
123 | 122 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ≤ 𝑅) |
124 | | min1 11894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐺 + (𝐶 / 2)) ∈ ℝ ∧ 𝐵 ∈ ℝ) →
if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ (𝐺 + (𝐶 / 2))) |
125 | 32, 6, 124 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ (𝐺 + (𝐶 / 2))) |
126 | 35, 125 | syl5eqbr 4618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑅 ≤ (𝐺 + (𝐶 / 2))) |
127 | | rphalflt 11736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐶 ∈ ℝ+
→ (𝐶 / 2) < 𝐶) |
128 | 28, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (𝐶 / 2) < 𝐶) |
129 | 31, 56, 27, 128 | ltadd2dd 10075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐺 + (𝐶 / 2)) < (𝐺 + 𝐶)) |
130 | 37, 32, 120, 126, 129 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑅 < (𝐺 + 𝐶)) |
131 | 110, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑅 < (𝐺 + 𝐶)) |
132 | 113, 119,
121, 123, 131 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 < (𝐺 + 𝐶)) |
133 | | rexr 9964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 − 𝐶) ∈ ℝ → (𝐺 − 𝐶) ∈
ℝ*) |
134 | | rexr 9964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 + 𝐶) ∈ ℝ → (𝐺 + 𝐶) ∈
ℝ*) |
135 | | elioo2 12087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐺 − 𝐶) ∈ ℝ* ∧ (𝐺 + 𝐶) ∈ ℝ*) → (𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶)) ↔ (𝑡 ∈ ℝ ∧ (𝐺 − 𝐶) < 𝑡 ∧ 𝑡 < (𝐺 + 𝐶)))) |
136 | 133, 134,
135 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐺 − 𝐶) ∈ ℝ ∧ (𝐺 + 𝐶) ∈ ℝ) → (𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶)) ↔ (𝑡 ∈ ℝ ∧ (𝐺 − 𝐶) < 𝑡 ∧ 𝑡 < (𝐺 + 𝐶)))) |
137 | 114, 121,
136 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶)) ↔ (𝑡 ∈ ℝ ∧ (𝐺 − 𝐶) < 𝑡 ∧ 𝑡 < (𝐺 + 𝐶)))) |
138 | 113, 118,
132, 137 | mpbir3and 1238 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶))) |
139 | 110, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝐺 ∈ ℝ) |
140 | 110, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝐶 ∈
ℝ+) |
141 | 140 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝐶 ∈ ℝ) |
142 | 12 | bl2ioo 22403 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐺(ball‘𝐷)𝐶) = ((𝐺 − 𝐶)(,)(𝐺 + 𝐶))) |
143 | 139, 141,
142 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺(ball‘𝐷)𝐶) = ((𝐺 − 𝐶)(,)(𝐺 + 𝐶))) |
144 | 138, 143 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ (𝐺(ball‘𝐷)𝐶)) |
145 | 112, 144 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ 𝑉) |
146 | | elun2 3743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 ∈ 𝑉 → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
148 | 147 | expr 641 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑣 < 𝑡 → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉))) |
149 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑣 ∈ ℝ) |
150 | | lelttric 10023 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑡 ≤ 𝑣 ∨ 𝑣 < 𝑡)) |
151 | 96, 149, 150 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑡 ≤ 𝑣 ∨ 𝑣 < 𝑡)) |
152 | 109, 148,
151 | mpjaod 395 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
153 | 152 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑡 ∈ (𝐴[,]𝑅) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉))) |
154 | 153 | ssrdv 3574 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝐴[,]𝑅) ⊆ (∪
𝑤 ∪ 𝑉)) |
155 | | uniun 4392 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ (𝑤
∪ {𝑉}) = (∪ 𝑤
∪ ∪ {𝑉}) |
156 | | unisng 4388 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈ 𝑈 → ∪ {𝑉} = 𝑉) |
157 | 75, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → ∪ {𝑉} = 𝑉) |
158 | 157 | uneq2d 3729 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (∪ 𝑤 ∪ ∪ {𝑉})
= (∪ 𝑤 ∪ 𝑉)) |
159 | 155, 158 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → ∪ (𝑤 ∪ {𝑉}) = (∪ 𝑤 ∪ 𝑉)) |
160 | 154, 159 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝐴[,]𝑅) ⊆ ∪
(𝑤 ∪ {𝑉})) |
161 | | unieq 4380 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑤 ∪ {𝑉}) → ∪ 𝑦 = ∪
(𝑤 ∪ {𝑉})) |
162 | 161 | sseq2d 3596 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑤 ∪ {𝑉}) → ((𝐴[,]𝑅) ⊆ ∪ 𝑦 ↔ (𝐴[,]𝑅) ⊆ ∪
(𝑤 ∪ {𝑉}))) |
163 | 162 | rspcev 3282 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∪ {𝑉}) ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑅) ⊆ ∪
(𝑤 ∪ {𝑉})) → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦) |
164 | 87, 160, 163 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦) |
165 | 164 | 3exp2 1277 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) → (𝑤 ∈ (𝒫 𝑈 ∩ Fin) → ((𝐴[,]𝑣) ⊆ ∪ 𝑤 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)))) |
166 | 165 | rexlimdv 3012 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) → (∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑤 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
167 | 67, 166 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
168 | 167 | expimpd 627 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∈ (𝐴[,]𝐵) ∧ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧) → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
169 | 64, 168 | syl5bi 231 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑣 ∈ 𝑆 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
170 | 169 | rexlimdv 3012 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
171 | 60, 170 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦) |
172 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑅 → (𝐴[,]𝑣) = (𝐴[,]𝑅)) |
173 | 172 | sseq1d 3595 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑅 → ((𝐴[,]𝑣) ⊆ ∪ 𝑦 ↔ (𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
174 | 173 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑣 = 𝑅 → (∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
175 | | unieq 4380 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → ∪ 𝑧 = ∪
𝑦) |
176 | 175 | sseq2d 3596 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → ((𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝑣) ⊆ ∪ 𝑦)) |
177 | 176 | cbvrexv 3148 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
(𝒫 𝑈 ∩
Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦) |
178 | 63, 177 | syl6bb 275 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦)) |
179 | 178 | cbvrabv 3172 |
. . . . . . . . . 10
⊢ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} = {𝑣 ∈ (𝐴[,]𝐵) ∣ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦} |
180 | 2, 179 | eqtri 2632 |
. . . . . . . . 9
⊢ 𝑆 = {𝑣 ∈ (𝐴[,]𝐵) ∣ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦} |
181 | 174, 180 | elrab2 3333 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑆 ↔ (𝑅 ∈ (𝐴[,]𝐵) ∧ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
182 | 53, 171, 181 | sylanbrc 695 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ 𝑆) |
183 | | suprub 10863 |
. . . . . . 7
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) ∧ 𝑅 ∈ 𝑆) → 𝑅 ≤ sup(𝑆, ℝ, < )) |
184 | 9, 19, 24, 182, 183 | syl31anc 1321 |
. . . . . 6
⊢ (𝜑 → 𝑅 ≤ sup(𝑆, ℝ, < )) |
185 | 184, 1 | syl6breqr 4625 |
. . . . 5
⊢ (𝜑 → 𝑅 ≤ 𝐺) |
186 | | iftrue 4042 |
. . . . . . 7
⊢ ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) = (𝐺 + (𝐶 / 2))) |
187 | 35, 186 | syl5eq 2656 |
. . . . . 6
⊢ ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → 𝑅 = (𝐺 + (𝐶 / 2))) |
188 | 187 | breq1d 4593 |
. . . . 5
⊢ ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → (𝑅 ≤ 𝐺 ↔ (𝐺 + (𝐶 / 2)) ≤ 𝐺)) |
189 | 185, 188 | syl5ibcom 234 |
. . . 4
⊢ (𝜑 → ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → (𝐺 + (𝐶 / 2)) ≤ 𝐺)) |
190 | 34, 189 | mtod 188 |
. . 3
⊢ (𝜑 → ¬ (𝐺 + (𝐶 / 2)) ≤ 𝐵) |
191 | | iffalse 4045 |
. . . 4
⊢ (¬
(𝐺 + (𝐶 / 2)) ≤ 𝐵 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) = 𝐵) |
192 | 35, 191 | syl5eq 2656 |
. . 3
⊢ (¬
(𝐺 + (𝐶 / 2)) ≤ 𝐵 → 𝑅 = 𝐵) |
193 | 190, 192 | syl 17 |
. 2
⊢ (𝜑 → 𝑅 = 𝐵) |
194 | 193, 182 | eqeltrrd 2689 |
1
⊢ (𝜑 → 𝐵 ∈ 𝑆) |