Step | Hyp | Ref
| Expression |
1 | | icccmp.13 |
. . . . . . 7
⊢ 𝐺 = sup(𝑆, ℝ, < ) |
2 | | icccmp.4 |
. . . . . . . . . 10
⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} |
3 | | ssrab2 3908 |
. . . . . . . . . 10
⊢ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} ⊆ (𝐴[,]𝐵) |
4 | 2, 3 | eqsstri 3854 |
. . . . . . . . 9
⊢ 𝑆 ⊆ (𝐴[,]𝐵) |
5 | | icccmp.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
6 | | icccmp.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
7 | | iccssre 12567 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
8 | 5, 6, 7 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
9 | 4, 8 | syl5ss 3832 |
. . . . . . . 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 23033 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
17 | 16 | simpld 490 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
18 | 17 | ne0d 4150 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ≠ ∅) |
19 | 16 | simprd 491 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) |
20 | | brralrspcev 4946 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧
∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) → ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) |
21 | 6, 19, 20 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) |
22 | | suprcl 11337 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) → sup(𝑆, ℝ, < ) ∈
ℝ) |
23 | 9, 18, 21, 22 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈
ℝ) |
24 | 1, 23 | syl5eqel 2863 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ℝ) |
25 | | icccmp.11 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
26 | 25 | rphalfcld 12193 |
. . . . . 6
⊢ (𝜑 → (𝐶 / 2) ∈
ℝ+) |
27 | 24, 26 | ltaddrpd 12214 |
. . . . 5
⊢ (𝜑 → 𝐺 < (𝐺 + (𝐶 / 2))) |
28 | 26 | rpred 12181 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 2) ∈ ℝ) |
29 | 24, 28 | readdcld 10406 |
. . . . . 6
⊢ (𝜑 → (𝐺 + (𝐶 / 2)) ∈ ℝ) |
30 | 24, 29 | ltnled 10523 |
. . . . 5
⊢ (𝜑 → (𝐺 < (𝐺 + (𝐶 / 2)) ↔ ¬ (𝐺 + (𝐶 / 2)) ≤ 𝐺)) |
31 | 27, 30 | mpbid 224 |
. . . 4
⊢ (𝜑 → ¬ (𝐺 + (𝐶 / 2)) ≤ 𝐺) |
32 | | icccmp.14 |
. . . . . . . . . 10
⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) |
33 | 29, 6 | ifcld 4352 |
. . . . . . . . . 10
⊢ (𝜑 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ∈ ℝ) |
34 | 32, 33 | syl5eqel 2863 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ℝ) |
35 | | suprub 11338 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) ∧ 𝐴 ∈ 𝑆) → 𝐴 ≤ sup(𝑆, ℝ, < )) |
36 | 9, 18, 21, 17, 35 | syl31anc 1441 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < )) |
37 | 36, 1 | syl6breqr 4928 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 𝐺) |
38 | 24, 29, 27 | ltled 10524 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ≤ (𝐺 + (𝐶 / 2))) |
39 | 5, 24, 29, 37, 38 | letrd 10533 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ (𝐺 + (𝐶 / 2))) |
40 | | breq2 4890 |
. . . . . . . . . . . 12
⊢ ((𝐺 + (𝐶 / 2)) = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) → (𝐴 ≤ (𝐺 + (𝐶 / 2)) ↔ 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵))) |
41 | | breq2 4890 |
. . . . . . . . . . . 12
⊢ (𝐵 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵))) |
42 | 40, 41 | ifboth 4345 |
. . . . . . . . . . 11
⊢ ((𝐴 ≤ (𝐺 + (𝐶 / 2)) ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵)) |
43 | 39, 13, 42 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵)) |
44 | 43, 32 | syl6breqr 4928 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝑅) |
45 | | min2 12333 |
. . . . . . . . . . 11
⊢ (((𝐺 + (𝐶 / 2)) ∈ ℝ ∧ 𝐵 ∈ ℝ) →
if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ 𝐵) |
46 | 29, 6, 45 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ 𝐵) |
47 | 32, 46 | syl5eqbr 4921 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ≤ 𝐵) |
48 | | elicc2 12550 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑅 ∈ (𝐴[,]𝐵) ↔ (𝑅 ∈ ℝ ∧ 𝐴 ≤ 𝑅 ∧ 𝑅 ≤ 𝐵))) |
49 | 5, 6, 48 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ (𝐴[,]𝐵) ↔ (𝑅 ∈ ℝ ∧ 𝐴 ≤ 𝑅 ∧ 𝑅 ≤ 𝐵))) |
50 | 34, 44, 47, 49 | mpbir3and 1399 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ (𝐴[,]𝐵)) |
51 | 24, 25 | ltsubrpd 12213 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 − 𝐶) < 𝐺) |
52 | 51, 1 | syl6breq 4927 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 − 𝐶) < sup(𝑆, ℝ, < )) |
53 | 25 | rpred 12181 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℝ) |
54 | 24, 53 | resubcld 10803 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 − 𝐶) ∈ ℝ) |
55 | | suprlub 11341 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) ∧ (𝐺 − 𝐶) ∈ ℝ) → ((𝐺 − 𝐶) < sup(𝑆, ℝ, < ) ↔ ∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣)) |
56 | 9, 18, 21, 54, 55 | syl31anc 1441 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺 − 𝐶) < sup(𝑆, ℝ, < ) ↔ ∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣)) |
57 | 52, 56 | mpbid 224 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣) |
58 | | oveq2 6930 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑣 → (𝐴[,]𝑥) = (𝐴[,]𝑣)) |
59 | 58 | sseq1d 3851 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → ((𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝑣) ⊆ ∪ 𝑧)) |
60 | 59 | rexbidv 3237 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑣 → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧)) |
61 | 60, 2 | elrab2 3576 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑆 ↔ (𝑣 ∈ (𝐴[,]𝐵) ∧ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧)) |
62 | | unieq 4679 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ∪ 𝑧 = ∪
𝑤) |
63 | 62 | sseq2d 3852 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → ((𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝑣) ⊆ ∪ 𝑤)) |
64 | 63 | cbvrexv 3368 |
. . . . . . . . . . . . 13
⊢
(∃𝑧 ∈
(𝒫 𝑈 ∩
Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ ∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑤) |
65 | | simpr1 1205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ∈ (𝒫 𝑈 ∩ Fin)) |
66 | | elin 4019 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ↔ (𝑤 ∈ 𝒫 𝑈 ∧ 𝑤 ∈ Fin)) |
67 | 65, 66 | sylib 210 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∈ 𝒫 𝑈 ∧ 𝑤 ∈ Fin)) |
68 | 67 | simpld 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ∈ 𝒫 𝑈) |
69 | 68 | elpwid 4391 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ⊆ 𝑈) |
70 | | simpll 757 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝜑) |
71 | | icccmp.10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑉 ∈ 𝑈) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑉 ∈ 𝑈) |
73 | 72 | snssd 4571 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → {𝑉} ⊆ 𝑈) |
74 | 69, 73 | unssd 4012 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ⊆ 𝑈) |
75 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑤 ∈ V |
76 | | snex 5140 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑉} ∈ V |
77 | 75, 76 | unex 7233 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∪ {𝑉}) ∈ V |
78 | 77 | elpw 4385 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∪ {𝑉}) ∈ 𝒫 𝑈 ↔ (𝑤 ∪ {𝑉}) ⊆ 𝑈) |
79 | 74, 78 | sylibr 226 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ∈ 𝒫 𝑈) |
80 | 67 | simprd 491 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ∈ Fin) |
81 | | snfi 8326 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑉} ∈ Fin |
82 | | unfi 8515 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Fin ∧ {𝑉} ∈ Fin) → (𝑤 ∪ {𝑉}) ∈ Fin) |
83 | 80, 81, 82 | sylancl 580 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ∈ Fin) |
84 | 79, 83 | elind 4021 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ∈ (𝒫 𝑈 ∩ Fin)) |
85 | | simplr2 1234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → (𝐴[,]𝑣) ⊆ ∪ 𝑤) |
86 | | ssun1 3999 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ 𝑤
⊆ (∪ 𝑤 ∪ 𝑉) |
87 | 85, 86 | syl6ss 3833 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → (𝐴[,]𝑣) ⊆ (∪ 𝑤 ∪ 𝑉)) |
88 | 70, 5 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝐴 ∈ ℝ) |
89 | 70, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑅 ∈ ℝ) |
90 | | elicc2 12550 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (𝐴[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
91 | 88, 89, 90 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑡 ∈ (𝐴[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
92 | 91 | biimpa 470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)) |
93 | 92 | simp1d 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑡 ∈ ℝ) |
94 | 93 | adantrr 707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ∈ ℝ) |
95 | 92 | simp2d 1134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝐴 ≤ 𝑡) |
96 | 95 | adantrr 707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝐴 ≤ 𝑡) |
97 | | simprr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ≤ 𝑣) |
98 | 70, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝐴[,]𝐵) ⊆ ℝ) |
99 | | simplr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑣 ∈ (𝐴[,]𝐵)) |
100 | 98, 99 | sseldd 3822 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑣 ∈ ℝ) |
101 | | elicc2 12550 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑡 ∈ (𝐴[,]𝑣) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣))) |
102 | 88, 100, 101 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑡 ∈ (𝐴[,]𝑣) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣))) |
103 | 102 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → (𝑡 ∈ (𝐴[,]𝑣) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣))) |
104 | 94, 96, 97, 103 | mpbir3and 1399 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ∈ (𝐴[,]𝑣)) |
105 | 87, 104 | sseldd 3822 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
106 | 105 | expr 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑡 ≤ 𝑣 → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉))) |
107 | 70 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝜑) |
108 | | icccmp.12 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) |
110 | 93 | adantrr 707 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ ℝ) |
111 | 107, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 − 𝐶) ∈ ℝ) |
112 | 100 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑣 ∈ ℝ) |
113 | | simplr3 1236 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 − 𝐶) < 𝑣) |
114 | | simprr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑣 < 𝑡) |
115 | 111, 112,
110, 113, 114 | lttrd 10537 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 − 𝐶) < 𝑡) |
116 | 107, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑅 ∈ ℝ) |
117 | 24, 53 | readdcld 10406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐺 + 𝐶) ∈ ℝ) |
118 | 107, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 + 𝐶) ∈ ℝ) |
119 | 92 | simp3d 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑡 ≤ 𝑅) |
120 | 119 | adantrr 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ≤ 𝑅) |
121 | | min1 12332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐺 + (𝐶 / 2)) ∈ ℝ ∧ 𝐵 ∈ ℝ) →
if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ (𝐺 + (𝐶 / 2))) |
122 | 29, 6, 121 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ (𝐺 + (𝐶 / 2))) |
123 | 32, 122 | syl5eqbr 4921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑅 ≤ (𝐺 + (𝐶 / 2))) |
124 | | rphalflt 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐶 ∈ ℝ+
→ (𝐶 / 2) < 𝐶) |
125 | 25, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (𝐶 / 2) < 𝐶) |
126 | 28, 53, 24, 125 | ltadd2dd 10535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐺 + (𝐶 / 2)) < (𝐺 + 𝐶)) |
127 | 34, 29, 117, 123, 126 | lelttrd 10534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑅 < (𝐺 + 𝐶)) |
128 | 107, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑅 < (𝐺 + 𝐶)) |
129 | 110, 116,
118, 120, 128 | lelttrd 10534 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 < (𝐺 + 𝐶)) |
130 | | rexr 10422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 − 𝐶) ∈ ℝ → (𝐺 − 𝐶) ∈
ℝ*) |
131 | | rexr 10422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 + 𝐶) ∈ ℝ → (𝐺 + 𝐶) ∈
ℝ*) |
132 | | elioo2 12528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐺 − 𝐶) ∈ ℝ* ∧ (𝐺 + 𝐶) ∈ ℝ*) → (𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶)) ↔ (𝑡 ∈ ℝ ∧ (𝐺 − 𝐶) < 𝑡 ∧ 𝑡 < (𝐺 + 𝐶)))) |
133 | 130, 131,
132 | syl2an 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐺 − 𝐶) ∈ ℝ ∧ (𝐺 + 𝐶) ∈ ℝ) → (𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶)) ↔ (𝑡 ∈ ℝ ∧ (𝐺 − 𝐶) < 𝑡 ∧ 𝑡 < (𝐺 + 𝐶)))) |
134 | 111, 118,
133 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶)) ↔ (𝑡 ∈ ℝ ∧ (𝐺 − 𝐶) < 𝑡 ∧ 𝑡 < (𝐺 + 𝐶)))) |
135 | 110, 115,
129, 134 | mpbir3and 1399 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶))) |
136 | 107, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝐺 ∈ ℝ) |
137 | 107, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝐶 ∈
ℝ+) |
138 | 137 | rpred 12181 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝐶 ∈ ℝ) |
139 | 12 | bl2ioo 23003 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐺(ball‘𝐷)𝐶) = ((𝐺 − 𝐶)(,)(𝐺 + 𝐶))) |
140 | 136, 138,
139 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺(ball‘𝐷)𝐶) = ((𝐺 − 𝐶)(,)(𝐺 + 𝐶))) |
141 | 135, 140 | eleqtrrd 2862 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ (𝐺(ball‘𝐷)𝐶)) |
142 | 109, 141 | sseldd 3822 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ 𝑉) |
143 | | elun2 4004 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 ∈ 𝑉 → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
145 | 144 | expr 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑣 < 𝑡 → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉))) |
146 | 100 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑣 ∈ ℝ) |
147 | | lelttric 10483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑡 ≤ 𝑣 ∨ 𝑣 < 𝑡)) |
148 | 93, 146, 147 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑡 ≤ 𝑣 ∨ 𝑣 < 𝑡)) |
149 | 106, 145,
148 | mpjaod 849 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
150 | 149 | ex 403 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑡 ∈ (𝐴[,]𝑅) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉))) |
151 | 150 | ssrdv 3827 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝐴[,]𝑅) ⊆ (∪
𝑤 ∪ 𝑉)) |
152 | | uniun 4692 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ (𝑤
∪ {𝑉}) = (∪ 𝑤
∪ ∪ {𝑉}) |
153 | | unisng 4686 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈ 𝑈 → ∪ {𝑉} = 𝑉) |
154 | 72, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → ∪ {𝑉} = 𝑉) |
155 | 154 | uneq2d 3990 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (∪ 𝑤 ∪ ∪ {𝑉})
= (∪ 𝑤 ∪ 𝑉)) |
156 | 152, 155 | syl5eq 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → ∪ (𝑤 ∪ {𝑉}) = (∪ 𝑤 ∪ 𝑉)) |
157 | 151, 156 | sseqtr4d 3861 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝐴[,]𝑅) ⊆ ∪
(𝑤 ∪ {𝑉})) |
158 | | unieq 4679 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑤 ∪ {𝑉}) → ∪ 𝑦 = ∪
(𝑤 ∪ {𝑉})) |
159 | 158 | sseq2d 3852 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑤 ∪ {𝑉}) → ((𝐴[,]𝑅) ⊆ ∪ 𝑦 ↔ (𝐴[,]𝑅) ⊆ ∪
(𝑤 ∪ {𝑉}))) |
160 | 159 | rspcev 3511 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∪ {𝑉}) ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑅) ⊆ ∪
(𝑤 ∪ {𝑉})) → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦) |
161 | 84, 157, 160 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦) |
162 | 161 | 3exp2 1416 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) → (𝑤 ∈ (𝒫 𝑈 ∩ Fin) → ((𝐴[,]𝑣) ⊆ ∪ 𝑤 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)))) |
163 | 162 | rexlimdv 3212 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) → (∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑤 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
164 | 64, 163 | syl5bi 234 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
165 | 164 | expimpd 447 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∈ (𝐴[,]𝐵) ∧ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧) → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
166 | 61, 165 | syl5bi 234 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑣 ∈ 𝑆 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
167 | 166 | rexlimdv 3212 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
168 | 57, 167 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦) |
169 | | oveq2 6930 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑅 → (𝐴[,]𝑣) = (𝐴[,]𝑅)) |
170 | 169 | sseq1d 3851 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑅 → ((𝐴[,]𝑣) ⊆ ∪ 𝑦 ↔ (𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
171 | 170 | rexbidv 3237 |
. . . . . . . . 9
⊢ (𝑣 = 𝑅 → (∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
172 | | unieq 4679 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → ∪ 𝑧 = ∪
𝑦) |
173 | 172 | sseq2d 3852 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → ((𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝑣) ⊆ ∪ 𝑦)) |
174 | 173 | cbvrexv 3368 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
(𝒫 𝑈 ∩
Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦) |
175 | 60, 174 | syl6bb 279 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦)) |
176 | 175 | cbvrabv 3396 |
. . . . . . . . . 10
⊢ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} = {𝑣 ∈ (𝐴[,]𝐵) ∣ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦} |
177 | 2, 176 | eqtri 2802 |
. . . . . . . . 9
⊢ 𝑆 = {𝑣 ∈ (𝐴[,]𝐵) ∣ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦} |
178 | 171, 177 | elrab2 3576 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑆 ↔ (𝑅 ∈ (𝐴[,]𝐵) ∧ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
179 | 50, 168, 178 | sylanbrc 578 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ 𝑆) |
180 | | suprub 11338 |
. . . . . . 7
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) ∧ 𝑅 ∈ 𝑆) → 𝑅 ≤ sup(𝑆, ℝ, < )) |
181 | 9, 18, 21, 179, 180 | syl31anc 1441 |
. . . . . 6
⊢ (𝜑 → 𝑅 ≤ sup(𝑆, ℝ, < )) |
182 | 181, 1 | syl6breqr 4928 |
. . . . 5
⊢ (𝜑 → 𝑅 ≤ 𝐺) |
183 | | iftrue 4313 |
. . . . . . 7
⊢ ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) = (𝐺 + (𝐶 / 2))) |
184 | 32, 183 | syl5eq 2826 |
. . . . . 6
⊢ ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → 𝑅 = (𝐺 + (𝐶 / 2))) |
185 | 184 | breq1d 4896 |
. . . . 5
⊢ ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → (𝑅 ≤ 𝐺 ↔ (𝐺 + (𝐶 / 2)) ≤ 𝐺)) |
186 | 182, 185 | syl5ibcom 237 |
. . . 4
⊢ (𝜑 → ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → (𝐺 + (𝐶 / 2)) ≤ 𝐺)) |
187 | 31, 186 | mtod 190 |
. . 3
⊢ (𝜑 → ¬ (𝐺 + (𝐶 / 2)) ≤ 𝐵) |
188 | | iffalse 4316 |
. . . 4
⊢ (¬
(𝐺 + (𝐶 / 2)) ≤ 𝐵 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) = 𝐵) |
189 | 32, 188 | syl5eq 2826 |
. . 3
⊢ (¬
(𝐺 + (𝐶 / 2)) ≤ 𝐵 → 𝑅 = 𝐵) |
190 | 187, 189 | syl 17 |
. 2
⊢ (𝜑 → 𝑅 = 𝐵) |
191 | 190, 179 | eqeltrrd 2860 |
1
⊢ (𝜑 → 𝐵 ∈ 𝑆) |