Proof of Theorem stoweid
| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑇 = ∅) → 𝑇 = ∅) |
| 2 | | stoweid.10 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
| 3 | 2 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
| 4 | | 1re 11261 |
. . . . . 6
⊢ 1 ∈
ℝ |
| 5 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 1 → 𝑥 = 1) |
| 6 | 5 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝑡 ∈ 𝑇 ↦ 𝑥) = (𝑡 ∈ 𝑇 ↦ 1)) |
| 7 | 6 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 1 → ((𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴)) |
| 8 | 7 | rspccv 3619 |
. . . . . 6
⊢
(∀𝑥 ∈
ℝ (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴 → (1 ∈ ℝ → (𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴)) |
| 9 | 3, 4, 8 | mpisyl 21 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) |
| 10 | 9 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑇 = ∅) → (𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) |
| 11 | 1, 10 | stoweidlem9 46024 |
. . 3
⊢ ((𝜑 ∧ 𝑇 = ∅) → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4))) |
| 12 | | stoweid.1 |
. . . 4
⊢
Ⅎ𝑡𝐹 |
| 13 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑓𝜑 |
| 14 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑓 ¬ 𝑇 = ∅ |
| 15 | 13, 14 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑓(𝜑 ∧ ¬ 𝑇 = ∅) |
| 16 | | stoweid.2 |
. . . . 5
⊢
Ⅎ𝑡𝜑 |
| 17 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑡 ¬ 𝑇 = ∅ |
| 18 | 16, 17 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑡(𝜑 ∧ ¬ 𝑇 = ∅) |
| 19 | | eqid 2737 |
. . . 4
⊢ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − inf(ran 𝐹, ℝ, < ))) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − inf(ran 𝐹, ℝ, < ))) |
| 20 | | stoweid.3 |
. . . 4
⊢ 𝐾 = (topGen‘ran
(,)) |
| 21 | | stoweid.5 |
. . . 4
⊢ 𝑇 = ∪
𝐽 |
| 22 | | stoweid.4 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Comp) |
| 23 | 22 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑇 = ∅) → 𝐽 ∈ Comp) |
| 24 | | stoweid.6 |
. . . 4
⊢ 𝐶 = (𝐽 Cn 𝐾) |
| 25 | | stoweid.7 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| 26 | 25 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑇 = ∅) → 𝐴 ⊆ 𝐶) |
| 27 | | stoweid.8 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 28 | 27 | 3adant1r 1178 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑇 = ∅) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 29 | | stoweid.9 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 30 | 29 | 3adant1r 1178 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑇 = ∅) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 31 | 2 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑇 = ∅) ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
| 32 | | stoweid.11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃ℎ ∈ 𝐴 (ℎ‘𝑟) ≠ (ℎ‘𝑡)) |
| 33 | 32 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑇 = ∅) ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃ℎ ∈ 𝐴 (ℎ‘𝑟) ≠ (ℎ‘𝑡)) |
| 34 | | stoweid.12 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝐶) |
| 35 | 34 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑇 = ∅) → 𝐹 ∈ 𝐶) |
| 36 | | stoweid.13 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 37 | | 4re 12350 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
| 38 | | 4pos 12373 |
. . . . . . . . 9
⊢ 0 <
4 |
| 39 | 37, 38 | elrpii 13037 |
. . . . . . . 8
⊢ 4 ∈
ℝ+ |
| 40 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 4 ∈
ℝ+) |
| 41 | 40 | rpreccld 13087 |
. . . . . 6
⊢ (𝜑 → (1 / 4) ∈
ℝ+) |
| 42 | 36, 41 | ifcld 4572 |
. . . . 5
⊢ (𝜑 → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ∈
ℝ+) |
| 43 | 42 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑇 = ∅) → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ∈
ℝ+) |
| 44 | | neqne 2948 |
. . . . 5
⊢ (¬
𝑇 = ∅ → 𝑇 ≠ ∅) |
| 45 | 44 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑇 = ∅) → 𝑇 ≠ ∅) |
| 46 | 36 | rpred 13077 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℝ) |
| 47 | | 4ne0 12374 |
. . . . . . . . 9
⊢ 4 ≠
0 |
| 48 | 37, 47 | rereccli 12032 |
. . . . . . . 8
⊢ (1 / 4)
∈ ℝ |
| 49 | 48 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1 / 4) ∈
ℝ) |
| 50 | 46, 49 | ifcld 4572 |
. . . . . 6
⊢ (𝜑 → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ∈ ℝ) |
| 51 | | 3re 12346 |
. . . . . . . 8
⊢ 3 ∈
ℝ |
| 52 | | 3ne0 12372 |
. . . . . . . 8
⊢ 3 ≠
0 |
| 53 | 51, 52 | rereccli 12032 |
. . . . . . 7
⊢ (1 / 3)
∈ ℝ |
| 54 | 53 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1 / 3) ∈
ℝ) |
| 55 | 36 | rpxrd 13078 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ*) |
| 56 | 41 | rpxrd 13078 |
. . . . . . 7
⊢ (𝜑 → (1 / 4) ∈
ℝ*) |
| 57 | | xrmin2 13220 |
. . . . . . 7
⊢ ((𝐸 ∈ ℝ*
∧ (1 / 4) ∈ ℝ*) → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ≤ (1 / 4)) |
| 58 | 55, 56, 57 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ≤ (1 / 4)) |
| 59 | | 3lt4 12440 |
. . . . . . . 8
⊢ 3 <
4 |
| 60 | | 3pos 12371 |
. . . . . . . . 9
⊢ 0 <
3 |
| 61 | 51, 37, 60, 38 | ltrecii 12184 |
. . . . . . . 8
⊢ (3 < 4
↔ (1 / 4) < (1 / 3)) |
| 62 | 59, 61 | mpbi 230 |
. . . . . . 7
⊢ (1 / 4)
< (1 / 3) |
| 63 | 62 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1 / 4) < (1 /
3)) |
| 64 | 50, 49, 54, 58, 63 | lelttrd 11419 |
. . . . 5
⊢ (𝜑 → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) < (1 / 3)) |
| 65 | 64 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑇 = ∅) → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) < (1 / 3)) |
| 66 | 12, 15, 18, 19, 20, 21, 23, 24, 26, 28, 30, 31, 33, 35, 43, 45, 65 | stoweidlem62 46077 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑇 = ∅) → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4))) |
| 67 | 11, 66 | pm2.61dan 813 |
. 2
⊢ (𝜑 → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4))) |
| 68 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑡 𝑓 ∈ 𝐴 |
| 69 | 16, 68 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑡(𝜑 ∧ 𝑓 ∈ 𝐴) |
| 70 | | xrmin1 13219 |
. . . . . . 7
⊢ ((𝐸 ∈ ℝ*
∧ (1 / 4) ∈ ℝ*) → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ≤ 𝐸) |
| 71 | 55, 56, 70 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ≤ 𝐸) |
| 72 | 71 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ≤ 𝐸) |
| 73 | 25 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝐴 ⊆ 𝐶) |
| 74 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝑓 ∈ 𝐴) |
| 75 | 73, 74 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝑓 ∈ 𝐶) |
| 76 | 20, 21, 24, 75 | fcnre 45030 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝑓:𝑇⟶ℝ) |
| 77 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
| 78 | 76, 77 | jca 511 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝑓:𝑇⟶ℝ ∧ 𝑡 ∈ 𝑇)) |
| 79 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((𝑓:𝑇⟶ℝ ∧ 𝑡 ∈ 𝑇) → (𝑓‘𝑡) ∈ ℝ) |
| 80 | | recn 11245 |
. . . . . . . . 9
⊢ ((𝑓‘𝑡) ∈ ℝ → (𝑓‘𝑡) ∈ ℂ) |
| 81 | 78, 79, 80 | 3syl 18 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝑓‘𝑡) ∈ ℂ) |
| 82 | 34 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝐹 ∈ 𝐶) |
| 83 | 20, 21, 24, 82 | fcnre 45030 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝐹:𝑇⟶ℝ) |
| 84 | 83, 77 | jca 511 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐹:𝑇⟶ℝ ∧ 𝑡 ∈ 𝑇)) |
| 85 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((𝐹:𝑇⟶ℝ ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) |
| 86 | | recn 11245 |
. . . . . . . . 9
⊢ ((𝐹‘𝑡) ∈ ℝ → (𝐹‘𝑡) ∈ ℂ) |
| 87 | 84, 85, 86 | 3syl 18 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℂ) |
| 88 | 81, 87 | subcld 11620 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((𝑓‘𝑡) − (𝐹‘𝑡)) ∈ ℂ) |
| 89 | 88 | abscld 15475 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) ∈ ℝ) |
| 90 | 4, 37, 47 | 3pm3.2i 1340 |
. . . . . . . . 9
⊢ (1 ∈
ℝ ∧ 4 ∈ ℝ ∧ 4 ≠ 0) |
| 91 | | redivcl 11986 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ 4 ∈ ℝ ∧ 4 ≠ 0) → (1 / 4) ∈
ℝ) |
| 92 | 90, 91 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (1 / 4) ∈
ℝ) |
| 93 | 46, 92 | ifcld 4572 |
. . . . . . 7
⊢ (𝜑 → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ∈ ℝ) |
| 94 | 93 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ∈ ℝ) |
| 95 | 46 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝐸 ∈ ℝ) |
| 96 | | ltletr 11353 |
. . . . . 6
⊢
(((abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) ∈ ℝ ∧ if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ∈ ℝ ∧ 𝐸 ∈ ℝ) →
(((abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ∧ if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ≤ 𝐸) → (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)) |
| 97 | 89, 94, 95, 96 | syl3anc 1373 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (((abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ∧ if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) ≤ 𝐸) → (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)) |
| 98 | 72, 97 | mpan2d 694 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) → (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)) |
| 99 | 69, 98 | ralimdaa 3260 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → (∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) → ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)) |
| 100 | 99 | reximdva 3168 |
. 2
⊢ (𝜑 → (∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < if(𝐸 ≤ (1 / 4), 𝐸, (1 / 4)) → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)) |
| 101 | 67, 100 | mpd 15 |
1
⊢ (𝜑 → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸) |