Step | Hyp | Ref
| Expression |
1 | | icccmp.13 |
. . . . . . 7
⊢ 𝐺 = sup(𝑆, ℝ, < ) |
2 | | icccmp.4 |
. . . . . . . . . 10
⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} |
3 | 2 | ssrab3 4020 |
. . . . . . . . 9
⊢ 𝑆 ⊆ (𝐴[,]𝐵) |
4 | | icccmp.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
5 | | icccmp.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
6 | | iccssre 13158 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
7 | 4, 5, 6 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
8 | 3, 7 | sstrid 3937 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
9 | | icccmp.1 |
. . . . . . . . . . 11
⊢ 𝐽 = (topGen‘ran
(,)) |
10 | | icccmp.2 |
. . . . . . . . . . 11
⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) |
11 | | icccmp.3 |
. . . . . . . . . . 11
⊢ 𝐷 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
12 | | icccmp.7 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
13 | | icccmp.8 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ 𝐽) |
14 | | icccmp.9 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
15 | 9, 10, 11, 2, 4, 5,
12, 13, 14 | icccmplem1 23981 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
16 | 15 | simpld 495 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
17 | 16 | ne0d 4275 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ≠ ∅) |
18 | 15 | simprd 496 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) |
19 | | brralrspcev 5139 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧
∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) → ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) |
20 | 5, 18, 19 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) |
21 | 8, 17, 20 | suprcld 11936 |
. . . . . . 7
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈
ℝ) |
22 | 1, 21 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ℝ) |
23 | | icccmp.11 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
24 | 23 | rphalfcld 12781 |
. . . . . 6
⊢ (𝜑 → (𝐶 / 2) ∈
ℝ+) |
25 | 22, 24 | ltaddrpd 12802 |
. . . . 5
⊢ (𝜑 → 𝐺 < (𝐺 + (𝐶 / 2))) |
26 | 24 | rpred 12769 |
. . . . . . 7
⊢ (𝜑 → (𝐶 / 2) ∈ ℝ) |
27 | 22, 26 | readdcld 11003 |
. . . . . 6
⊢ (𝜑 → (𝐺 + (𝐶 / 2)) ∈ ℝ) |
28 | 22, 27 | ltnled 11120 |
. . . . 5
⊢ (𝜑 → (𝐺 < (𝐺 + (𝐶 / 2)) ↔ ¬ (𝐺 + (𝐶 / 2)) ≤ 𝐺)) |
29 | 25, 28 | mpbid 231 |
. . . 4
⊢ (𝜑 → ¬ (𝐺 + (𝐶 / 2)) ≤ 𝐺) |
30 | | icccmp.14 |
. . . . . . . . . 10
⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) |
31 | 27, 5 | ifcld 4511 |
. . . . . . . . . 10
⊢ (𝜑 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ∈ ℝ) |
32 | 30, 31 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ℝ) |
33 | 8, 17, 20, 16 | suprubd 11935 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < )) |
34 | 33, 1 | breqtrrdi 5121 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 𝐺) |
35 | 22, 27, 25 | ltled 11121 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ≤ (𝐺 + (𝐶 / 2))) |
36 | 4, 22, 27, 34, 35 | letrd 11130 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ (𝐺 + (𝐶 / 2))) |
37 | | breq2 5083 |
. . . . . . . . . . . 12
⊢ ((𝐺 + (𝐶 / 2)) = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) → (𝐴 ≤ (𝐺 + (𝐶 / 2)) ↔ 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵))) |
38 | | breq2 5083 |
. . . . . . . . . . . 12
⊢ (𝐵 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵))) |
39 | 37, 38 | ifboth 4504 |
. . . . . . . . . . 11
⊢ ((𝐴 ≤ (𝐺 + (𝐶 / 2)) ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵)) |
40 | 36, 12, 39 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≤ if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵)) |
41 | 40, 30 | breqtrrdi 5121 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝑅) |
42 | | min2 12921 |
. . . . . . . . . . 11
⊢ (((𝐺 + (𝐶 / 2)) ∈ ℝ ∧ 𝐵 ∈ ℝ) →
if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ 𝐵) |
43 | 27, 5, 42 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ 𝐵) |
44 | 30, 43 | eqbrtrid 5114 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ≤ 𝐵) |
45 | | elicc2 13141 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑅 ∈ (𝐴[,]𝐵) ↔ (𝑅 ∈ ℝ ∧ 𝐴 ≤ 𝑅 ∧ 𝑅 ≤ 𝐵))) |
46 | 4, 5, 45 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ (𝐴[,]𝐵) ↔ (𝑅 ∈ ℝ ∧ 𝐴 ≤ 𝑅 ∧ 𝑅 ≤ 𝐵))) |
47 | 32, 41, 44, 46 | mpbir3and 1341 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ (𝐴[,]𝐵)) |
48 | 22, 23 | ltsubrpd 12801 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 − 𝐶) < 𝐺) |
49 | 48, 1 | breqtrdi 5120 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 − 𝐶) < sup(𝑆, ℝ, < )) |
50 | 23 | rpred 12769 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℝ) |
51 | 22, 50 | resubcld 11401 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 − 𝐶) ∈ ℝ) |
52 | | suprlub 11937 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑛) ∧ (𝐺 − 𝐶) ∈ ℝ) → ((𝐺 − 𝐶) < sup(𝑆, ℝ, < ) ↔ ∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣)) |
53 | 8, 17, 20, 51, 52 | syl31anc 1372 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐺 − 𝐶) < sup(𝑆, ℝ, < ) ↔ ∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣)) |
54 | 49, 53 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣) |
55 | | oveq2 7277 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑣 → (𝐴[,]𝑥) = (𝐴[,]𝑣)) |
56 | 55 | sseq1d 3957 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → ((𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝑣) ⊆ ∪ 𝑧)) |
57 | 56 | rexbidv 3228 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑣 → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧)) |
58 | 57, 2 | elrab2 3629 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝑆 ↔ (𝑣 ∈ (𝐴[,]𝐵) ∧ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧)) |
59 | | unieq 4856 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ∪ 𝑧 = ∪
𝑤) |
60 | 59 | sseq2d 3958 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → ((𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝑣) ⊆ ∪ 𝑤)) |
61 | 60 | cbvrexvw 3382 |
. . . . . . . . . . . . 13
⊢
(∃𝑧 ∈
(𝒫 𝑈 ∩
Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ ∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑤) |
62 | | simpr1 1193 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ∈ (𝒫 𝑈 ∩ Fin)) |
63 | | elin 3908 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ↔ (𝑤 ∈ 𝒫 𝑈 ∧ 𝑤 ∈ Fin)) |
64 | 62, 63 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∈ 𝒫 𝑈 ∧ 𝑤 ∈ Fin)) |
65 | 64 | simpld 495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ∈ 𝒫 𝑈) |
66 | 65 | elpwid 4550 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ⊆ 𝑈) |
67 | | simpll 764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝜑) |
68 | | icccmp.10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑉 ∈ 𝑈) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑉 ∈ 𝑈) |
70 | 69 | snssd 4748 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → {𝑉} ⊆ 𝑈) |
71 | 66, 70 | unssd 4125 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ⊆ 𝑈) |
72 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑤 ∈ V |
73 | | snex 5358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑉} ∈ V |
74 | 72, 73 | unex 7588 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∪ {𝑉}) ∈ V |
75 | 74 | elpw 4543 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∪ {𝑉}) ∈ 𝒫 𝑈 ↔ (𝑤 ∪ {𝑉}) ⊆ 𝑈) |
76 | 71, 75 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ∈ 𝒫 𝑈) |
77 | 64 | simprd 496 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑤 ∈ Fin) |
78 | | snfi 8815 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑉} ∈ Fin |
79 | | unfi 8935 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Fin ∧ {𝑉} ∈ Fin) → (𝑤 ∪ {𝑉}) ∈ Fin) |
80 | 77, 78, 79 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ∈ Fin) |
81 | 76, 80 | elind 4133 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑤 ∪ {𝑉}) ∈ (𝒫 𝑈 ∩ Fin)) |
82 | | simplr2 1215 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → (𝐴[,]𝑣) ⊆ ∪ 𝑤) |
83 | | ssun1 4111 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ 𝑤
⊆ (∪ 𝑤 ∪ 𝑉) |
84 | 82, 83 | sstrdi 3938 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → (𝐴[,]𝑣) ⊆ (∪ 𝑤 ∪ 𝑉)) |
85 | 67, 4 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝐴 ∈ ℝ) |
86 | 67, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑅 ∈ ℝ) |
87 | | elicc2 13141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (𝐴[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
88 | 85, 86, 87 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑡 ∈ (𝐴[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
89 | 88 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)) |
90 | 89 | simp1d 1141 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑡 ∈ ℝ) |
91 | 90 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ∈ ℝ) |
92 | 89 | simp2d 1142 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝐴 ≤ 𝑡) |
93 | 92 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝐴 ≤ 𝑡) |
94 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ≤ 𝑣) |
95 | 67, 7 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝐴[,]𝐵) ⊆ ℝ) |
96 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑣 ∈ (𝐴[,]𝐵)) |
97 | 95, 96 | sseldd 3927 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → 𝑣 ∈ ℝ) |
98 | | elicc2 13141 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑡 ∈ (𝐴[,]𝑣) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣))) |
99 | 85, 97, 98 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑡 ∈ (𝐴[,]𝑣) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣))) |
100 | 99 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → (𝑡 ∈ (𝐴[,]𝑣) ↔ (𝑡 ∈ ℝ ∧ 𝐴 ≤ 𝑡 ∧ 𝑡 ≤ 𝑣))) |
101 | 91, 93, 94, 100 | mpbir3and 1341 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ∈ (𝐴[,]𝑣)) |
102 | 84, 101 | sseldd 3927 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑡 ≤ 𝑣)) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
103 | 102 | expr 457 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑡 ≤ 𝑣 → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉))) |
104 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝜑) |
105 | | icccmp.12 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) |
107 | 90 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ ℝ) |
108 | 104, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 − 𝐶) ∈ ℝ) |
109 | 97 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑣 ∈ ℝ) |
110 | | simplr3 1216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 − 𝐶) < 𝑣) |
111 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑣 < 𝑡) |
112 | 108, 109,
107, 110, 111 | lttrd 11134 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 − 𝐶) < 𝑡) |
113 | 104, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑅 ∈ ℝ) |
114 | 22, 50 | readdcld 11003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐺 + 𝐶) ∈ ℝ) |
115 | 104, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺 + 𝐶) ∈ ℝ) |
116 | 89 | simp3d 1143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑡 ≤ 𝑅) |
117 | 116 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ≤ 𝑅) |
118 | | min1 12920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐺 + (𝐶 / 2)) ∈ ℝ ∧ 𝐵 ∈ ℝ) →
if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ (𝐺 + (𝐶 / 2))) |
119 | 27, 5, 118 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ≤ (𝐺 + (𝐶 / 2))) |
120 | 30, 119 | eqbrtrid 5114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑅 ≤ (𝐺 + (𝐶 / 2))) |
121 | | rphalflt 12756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐶 ∈ ℝ+
→ (𝐶 / 2) < 𝐶) |
122 | 23, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (𝐶 / 2) < 𝐶) |
123 | 26, 50, 22, 122 | ltadd2dd 11132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐺 + (𝐶 / 2)) < (𝐺 + 𝐶)) |
124 | 32, 27, 114, 120, 123 | lelttrd 11131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑅 < (𝐺 + 𝐶)) |
125 | 104, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑅 < (𝐺 + 𝐶)) |
126 | 107, 113,
115, 117, 125 | lelttrd 11131 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 < (𝐺 + 𝐶)) |
127 | | rexr 11020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 − 𝐶) ∈ ℝ → (𝐺 − 𝐶) ∈
ℝ*) |
128 | | rexr 11020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 + 𝐶) ∈ ℝ → (𝐺 + 𝐶) ∈
ℝ*) |
129 | | elioo2 13117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐺 − 𝐶) ∈ ℝ* ∧ (𝐺 + 𝐶) ∈ ℝ*) → (𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶)) ↔ (𝑡 ∈ ℝ ∧ (𝐺 − 𝐶) < 𝑡 ∧ 𝑡 < (𝐺 + 𝐶)))) |
130 | 127, 128,
129 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐺 − 𝐶) ∈ ℝ ∧ (𝐺 + 𝐶) ∈ ℝ) → (𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶)) ↔ (𝑡 ∈ ℝ ∧ (𝐺 − 𝐶) < 𝑡 ∧ 𝑡 < (𝐺 + 𝐶)))) |
131 | 108, 115,
130 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶)) ↔ (𝑡 ∈ ℝ ∧ (𝐺 − 𝐶) < 𝑡 ∧ 𝑡 < (𝐺 + 𝐶)))) |
132 | 107, 112,
126, 131 | mpbir3and 1341 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ ((𝐺 − 𝐶)(,)(𝐺 + 𝐶))) |
133 | 104, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝐺 ∈ ℝ) |
134 | 104, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝐶 ∈
ℝ+) |
135 | 134 | rpred 12769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝐶 ∈ ℝ) |
136 | 11 | bl2ioo 23951 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐺(ball‘𝐷)𝐶) = ((𝐺 − 𝐶)(,)(𝐺 + 𝐶))) |
137 | 133, 135,
136 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → (𝐺(ball‘𝐷)𝐶) = ((𝐺 − 𝐶)(,)(𝐺 + 𝐶))) |
138 | 132, 137 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ (𝐺(ball‘𝐷)𝐶)) |
139 | 106, 138 | sseldd 3927 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ 𝑉) |
140 | | elun2 4116 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 ∈ 𝑉 → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ (𝑡 ∈ (𝐴[,]𝑅) ∧ 𝑣 < 𝑡)) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
142 | 141 | expr 457 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑣 < 𝑡 → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉))) |
143 | 97 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑣 ∈ ℝ) |
144 | | lelttric 11080 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑡 ≤ 𝑣 ∨ 𝑣 < 𝑡)) |
145 | 90, 143, 144 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → (𝑡 ≤ 𝑣 ∨ 𝑣 < 𝑡)) |
146 | 103, 142,
145 | mpjaod 857 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) ∧ 𝑡 ∈ (𝐴[,]𝑅)) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉)) |
147 | 146 | ex 413 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝑡 ∈ (𝐴[,]𝑅) → 𝑡 ∈ (∪ 𝑤 ∪ 𝑉))) |
148 | 147 | ssrdv 3932 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝐴[,]𝑅) ⊆ (∪
𝑤 ∪ 𝑉)) |
149 | | uniun 4870 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ (𝑤
∪ {𝑉}) = (∪ 𝑤
∪ ∪ {𝑉}) |
150 | | unisng 4866 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈ 𝑈 → ∪ {𝑉} = 𝑉) |
151 | 69, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → ∪ {𝑉} = 𝑉) |
152 | 151 | uneq2d 4102 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (∪ 𝑤 ∪ ∪ {𝑉})
= (∪ 𝑤 ∪ 𝑉)) |
153 | 149, 152 | eqtrid 2792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → ∪ (𝑤 ∪ {𝑉}) = (∪ 𝑤 ∪ 𝑉)) |
154 | 148, 153 | sseqtrrd 3967 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → (𝐴[,]𝑅) ⊆ ∪
(𝑤 ∪ {𝑉})) |
155 | | unieq 4856 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑤 ∪ {𝑉}) → ∪ 𝑦 = ∪
(𝑤 ∪ {𝑉})) |
156 | 155 | sseq2d 3958 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑤 ∪ {𝑉}) → ((𝐴[,]𝑅) ⊆ ∪ 𝑦 ↔ (𝐴[,]𝑅) ⊆ ∪
(𝑤 ∪ {𝑉}))) |
157 | 156 | rspcev 3561 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∪ {𝑉}) ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑅) ⊆ ∪
(𝑤 ∪ {𝑉})) → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦) |
158 | 81, 154, 157 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ (𝐴[,]𝑣) ⊆ ∪ 𝑤 ∧ (𝐺 − 𝐶) < 𝑣)) → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦) |
159 | 158 | 3exp2 1353 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) → (𝑤 ∈ (𝒫 𝑈 ∩ Fin) → ((𝐴[,]𝑣) ⊆ ∪ 𝑤 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)))) |
160 | 159 | rexlimdv 3214 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) → (∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑤 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
161 | 61, 160 | syl5bi 241 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (𝐴[,]𝐵)) → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
162 | 161 | expimpd 454 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∈ (𝐴[,]𝐵) ∧ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧) → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
163 | 58, 162 | syl5bi 241 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑣 ∈ 𝑆 → ((𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦))) |
164 | 163 | rexlimdv 3214 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑣 ∈ 𝑆 (𝐺 − 𝐶) < 𝑣 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
165 | 54, 164 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦) |
166 | | oveq2 7277 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑅 → (𝐴[,]𝑣) = (𝐴[,]𝑅)) |
167 | 166 | sseq1d 3957 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑅 → ((𝐴[,]𝑣) ⊆ ∪ 𝑦 ↔ (𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
168 | 167 | rexbidv 3228 |
. . . . . . . . 9
⊢ (𝑣 = 𝑅 → (∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
169 | | unieq 4856 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → ∪ 𝑧 = ∪
𝑦) |
170 | 169 | sseq2d 3958 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → ((𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝑣) ⊆ ∪ 𝑦)) |
171 | 170 | cbvrexvw 3382 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
(𝒫 𝑈 ∩
Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑧 ↔ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦) |
172 | 57, 171 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦)) |
173 | 172 | cbvrabv 3425 |
. . . . . . . . . 10
⊢ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} = {𝑣 ∈ (𝐴[,]𝐵) ∣ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦} |
174 | 2, 173 | eqtri 2768 |
. . . . . . . . 9
⊢ 𝑆 = {𝑣 ∈ (𝐴[,]𝐵) ∣ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑣) ⊆ ∪ 𝑦} |
175 | 168, 174 | elrab2 3629 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑆 ↔ (𝑅 ∈ (𝐴[,]𝐵) ∧ ∃𝑦 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑅) ⊆ ∪ 𝑦)) |
176 | 47, 165, 175 | sylanbrc 583 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ 𝑆) |
177 | 8, 17, 20, 176 | suprubd 11935 |
. . . . . 6
⊢ (𝜑 → 𝑅 ≤ sup(𝑆, ℝ, < )) |
178 | 177, 1 | breqtrrdi 5121 |
. . . . 5
⊢ (𝜑 → 𝑅 ≤ 𝐺) |
179 | | iftrue 4471 |
. . . . . . 7
⊢ ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) = (𝐺 + (𝐶 / 2))) |
180 | 30, 179 | eqtrid 2792 |
. . . . . 6
⊢ ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → 𝑅 = (𝐺 + (𝐶 / 2))) |
181 | 180 | breq1d 5089 |
. . . . 5
⊢ ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → (𝑅 ≤ 𝐺 ↔ (𝐺 + (𝐶 / 2)) ≤ 𝐺)) |
182 | 178, 181 | syl5ibcom 244 |
. . . 4
⊢ (𝜑 → ((𝐺 + (𝐶 / 2)) ≤ 𝐵 → (𝐺 + (𝐶 / 2)) ≤ 𝐺)) |
183 | 29, 182 | mtod 197 |
. . 3
⊢ (𝜑 → ¬ (𝐺 + (𝐶 / 2)) ≤ 𝐵) |
184 | | iffalse 4474 |
. . . 4
⊢ (¬
(𝐺 + (𝐶 / 2)) ≤ 𝐵 → if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) = 𝐵) |
185 | 30, 184 | eqtrid 2792 |
. . 3
⊢ (¬
(𝐺 + (𝐶 / 2)) ≤ 𝐵 → 𝑅 = 𝐵) |
186 | 183, 185 | syl 17 |
. 2
⊢ (𝜑 → 𝑅 = 𝐵) |
187 | 186, 176 | eqeltrrd 2842 |
1
⊢ (𝜑 → 𝐵 ∈ 𝑆) |