Step | Hyp | Ref
| Expression |
1 | | stoweidlem59.8 |
. . . . . . . . . 10
⊢ 𝑌 = {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} |
2 | | nfrab1 3099 |
. . . . . . . . . 10
⊢
Ⅎ𝑦{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} |
3 | 1, 2 | nfcxfr 2749 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝑌 |
4 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝑌 |
5 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑧(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) |
6 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)) |
7 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑦‘𝑡) = (𝑧‘𝑡)) |
8 | 7 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑧‘𝑡) < (𝐸 / 𝑁))) |
9 | 8 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁))) |
10 | 7 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))) |
11 | 10 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))) |
12 | 9, 11 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))) |
13 | 3, 4, 5, 6, 12 | cbvrab 3171 |
. . . . . . . 8
⊢ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} = {𝑧 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))} |
14 | | stoweidlem59.10 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ Comp) |
15 | | cmptop 21008 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ Top) |
17 | | stoweidlem59.3 |
. . . . . . . . . . . 12
⊢ 𝐾 = (topGen‘ran
(,)) |
18 | | retop 22375 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) ∈ Top |
19 | 17, 18 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐾 ∈ Top |
20 | | cnfex 38210 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V) |
21 | 16, 19, 20 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 Cn 𝐾) ∈ V) |
22 | | stoweidlem59.11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
23 | | stoweidlem59.5 |
. . . . . . . . . . 11
⊢ 𝐶 = (𝐽 Cn 𝐾) |
24 | 22, 23 | syl6sseq 3614 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
25 | 21, 24 | ssexd 4733 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ V) |
26 | 1, 25 | rabexd 4741 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ V) |
27 | 13, 26 | rabexd 4741 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) |
28 | 27 | ralrimivw 2950 |
. . . . . 6
⊢ (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) |
29 | | stoweidlem59.9 |
. . . . . . 7
⊢ 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) |
30 | 29 | fnmpt 5933 |
. . . . . 6
⊢
(∀𝑗 ∈
(0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V → 𝐻 Fn (0...𝑁)) |
31 | 28, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐻 Fn (0...𝑁)) |
32 | | fzfi 12633 |
. . . . 5
⊢
(0...𝑁) ∈
Fin |
33 | | fnfi 8123 |
. . . . 5
⊢ ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin) |
34 | 31, 32, 33 | sylancl 693 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ Fin) |
35 | | rnfi 8132 |
. . . 4
⊢ (𝐻 ∈ Fin → ran 𝐻 ∈ Fin) |
36 | 34, 35 | syl 17 |
. . 3
⊢ (𝜑 → ran 𝐻 ∈ Fin) |
37 | | fnchoice 38211 |
. . 3
⊢ (ran
𝐻 ∈ Fin →
∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) |
38 | 36, 37 | syl 17 |
. 2
⊢ (𝜑 → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) |
39 | | simprl 790 |
. . . . 5
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ Fn ran 𝐻) |
40 | | ovex 6577 |
. . . . . . . 8
⊢
(0...𝑁) ∈
V |
41 | 40 | mptex 6390 |
. . . . . . 7
⊢ (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) ∈ V |
42 | 29, 41 | eqeltri 2684 |
. . . . . 6
⊢ 𝐻 ∈ V |
43 | 42 | rnex 6992 |
. . . . 5
⊢ ran 𝐻 ∈ V |
44 | | fnex 6386 |
. . . . 5
⊢ ((ℎ Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ℎ ∈ V) |
45 | 39, 43, 44 | sylancl 693 |
. . . 4
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ ∈ V) |
46 | | coexg 7010 |
. . . 4
⊢ ((ℎ ∈ V ∧ 𝐻 ∈ V) → (ℎ ∘ 𝐻) ∈ V) |
47 | 45, 42, 46 | sylancl 693 |
. . 3
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻) ∈ V) |
48 | | dffn3 5967 |
. . . . . . 7
⊢ (ℎ Fn ran 𝐻 ↔ ℎ:ran 𝐻⟶ran ℎ) |
49 | 39, 48 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶ran ℎ) |
50 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑤𝜑 |
51 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤 ℎ Fn ran 𝐻 |
52 | | nfra1 2925 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) |
53 | 51, 52 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑤(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) |
54 | 50, 53 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑤(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) |
55 | | simplrr 797 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) |
56 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻) |
57 | | fvelrnb 6153 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤)) |
58 | | nfv 1830 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎(𝐻‘𝑗) = 𝑤 |
59 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) |
60 | 29, 59 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗𝐻 |
61 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗𝑎 |
62 | 60, 61 | nffv 6110 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗(𝐻‘𝑎) |
63 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗𝑤 |
64 | 62, 63 | nfeq 2762 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗(𝐻‘𝑎) = 𝑤 |
65 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑎 → (𝐻‘𝑗) = (𝐻‘𝑎)) |
66 | 65 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑎 → ((𝐻‘𝑗) = 𝑤 ↔ (𝐻‘𝑎) = 𝑤)) |
67 | 58, 64, 66 | cbvrex 3144 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑗 ∈
(0...𝑁)(𝐻‘𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤) |
68 | 57, 67 | syl6bbr 277 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤)) |
69 | 31, 68 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤)) |
70 | 69 | biimpa 500 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤) |
71 | | simp3 1056 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) = 𝑤) |
72 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁)) |
73 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) |
74 | 29 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) |
75 | 72, 73, 74 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) |
76 | | stoweidlem59.6 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
77 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡(0...𝑁) |
78 | | nfrab1 3099 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} |
79 | 77, 78 | nfmpt 4674 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
80 | 76, 79 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡𝐷 |
81 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡𝑗 |
82 | 80, 81 | nffv 6110 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡(𝐷‘𝑗) |
83 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡𝑇 |
84 | | stoweidlem59.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
85 | | nfrab1 3099 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} |
86 | 77, 85 | nfmpt 4674 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
87 | 84, 86 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑡𝐵 |
88 | 87, 81 | nffv 6110 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡(𝐵‘𝑗) |
89 | 83, 88 | nfdif 3693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡(𝑇 ∖ (𝐵‘𝑗)) |
90 | | stoweidlem59.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡𝜑 |
91 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡 𝑗 ∈ (0...𝑁) |
92 | 90, 91 | nfan 1816 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡(𝜑 ∧ 𝑗 ∈ (0...𝑁)) |
93 | | stoweidlem59.4 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑇 = ∪
𝐽 |
94 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐽 ∈ Comp) |
95 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐴 ⊆ 𝐶) |
96 | | stoweidlem59.12 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
97 | 96 | 3adant1r 1311 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
98 | | stoweidlem59.13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
99 | 98 | 3adant1r 1311 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
100 | | stoweidlem59.14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴) |
101 | 100 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴) |
102 | | stoweidlem59.15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡)) |
103 | 102 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡)) |
104 | | uniexg 6853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐽 ∈ Comp → ∪ 𝐽
∈ V) |
105 | 14, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ∪ 𝐽
∈ V) |
106 | 93, 105 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑇 ∈ V) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V) |
108 | | rabexg 4739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) |
110 | 84 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
111 | 72, 109, 110 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
112 | | stoweidlem59.1 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑡𝐹 |
113 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} |
114 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ) |
115 | 114 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ) |
116 | | 3re 10971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 3 ∈
ℝ |
117 | | 3ne0 10992 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 3 ≠
0 |
118 | 116, 117 | rereccli 10669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 / 3)
∈ ℝ |
119 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℝ ∧ (1 / 3)
∈ ℝ) → (𝑗 +
(1 / 3)) ∈ ℝ) |
120 | 115, 118,
119 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ) |
121 | 120 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ) |
122 | | stoweidlem59.17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
123 | 122 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐸 ∈ ℝ) |
124 | 123 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ) |
125 | 121, 124 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ) |
126 | | stoweidlem59.16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐹 ∈ 𝐶) |
127 | 126, 23 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
128 | 127 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
129 | 112, 17, 93, 113, 125, 128 | rfcnpre3 38215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ (Clsd‘𝐽)) |
130 | 111, 129 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ∈ (Clsd‘𝐽)) |
131 | | rabexg 4739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) |
132 | 107, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) |
133 | 76 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
134 | 72, 132, 133 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
135 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} |
136 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℝ ∧ (1 / 3)
∈ ℝ) → (𝑗
− (1 / 3)) ∈ ℝ) |
137 | 115, 118,
136 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈
ℝ) |
138 | 137 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈
ℝ) |
139 | 138, 124 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ) |
140 | 112, 17, 93, 135, 139, 128 | rfcnpre4 38216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽)) |
141 | 134, 140 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) ∈ (Clsd‘𝐽)) |
142 | 139 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ) |
143 | 125 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ) |
144 | 17, 93, 23, 126 | fcnre 38207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
145 | 144 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝐹:𝑇⟶ℝ) |
146 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ⊆ 𝑇 |
147 | 111, 146 | syl6eqss 3618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ⊆ 𝑇) |
148 | 147 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ 𝑇) |
149 | 145, 148 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐹‘𝑡) ∈ ℝ) |
150 | 118, 136 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈
ℝ) |
151 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → 𝑗 ∈
ℝ) |
152 | 118, 119 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈
ℝ) |
153 | | 3pos 10991 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 0 <
3 |
154 | 116, 153 | recgt0ii 10808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ 0 < (1
/ 3) |
155 | 118, 154 | elrpii 11711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (1 / 3)
∈ ℝ+ |
156 | | ltsubrp 11742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑗 ∈ ℝ ∧ (1 / 3)
∈ ℝ+) → (𝑗 − (1 / 3)) < 𝑗) |
157 | 155, 156 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗) |
158 | | ltaddrp 11743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑗 ∈ ℝ ∧ (1 / 3)
∈ ℝ+) → 𝑗 < (𝑗 + (1 / 3))) |
159 | 155, 158 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3))) |
160 | 150, 151,
152, 157, 159 | lttrd 10077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3))) |
161 | 115, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3))) |
162 | 161 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3))) |
163 | 122 | rpregt0d 11754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
164 | 163 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
165 | | ltmul1 10752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑗 − (1 / 3)) ∈ ℝ
∧ (𝑗 + (1 / 3)) ∈
ℝ ∧ (𝐸 ∈
ℝ ∧ 0 < 𝐸))
→ ((𝑗 − (1 / 3))
< (𝑗 + (1 / 3)) ↔
((𝑗 − (1 / 3))
· 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))) |
166 | 138, 121,
164, 165 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))) |
167 | 162, 166 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)) |
168 | 167 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)) |
169 | 111 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) ↔ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})) |
170 | 169 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
171 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡))) |
172 | 170, 171 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡))) |
173 | 172 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)) |
174 | 142, 143,
149, 168, 173 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡)) |
175 | 142, 149 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))) |
176 | 174, 175 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) |
177 | 176 | intnand 953 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))) |
178 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))) |
179 | 177, 178 | sylnibr 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
180 | 134 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
181 | 179, 180 | neleqtrrd 2710 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ (𝐷‘𝑗)) |
182 | 181 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) → ¬ 𝑡 ∈ (𝐷‘𝑗))) |
183 | 92, 182 | ralrimi 2940 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗)) |
184 | | disj 3969 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗)) |
185 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑎(𝐵‘𝑗) |
186 | 82 | nfcri 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑡 𝑎 ∈ (𝐷‘𝑗) |
187 | 186 | nfn 1768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡 ¬ 𝑎 ∈ (𝐷‘𝑗) |
188 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑎 ¬ 𝑡 ∈ (𝐷‘𝑗) |
189 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 = 𝑡 → (𝑎 ∈ (𝐷‘𝑗) ↔ 𝑡 ∈ (𝐷‘𝑗))) |
190 | 189 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ¬ 𝑡 ∈ (𝐷‘𝑗))) |
191 | 185, 88, 187, 188, 190 | cbvralf 3141 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑎 ∈
(𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗)) |
192 | 184, 191 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗)) |
193 | 183, 192 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅) |
194 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑇 ∖ (𝐵‘𝑗)) = (𝑇 ∖ (𝐵‘𝑗)) |
195 | | stoweidlem59.19 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑁 ∈ ℕ) |
196 | 195 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
197 | 122, 196 | rpdivcld 11765 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐸 / 𝑁) ∈
ℝ+) |
198 | 197 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈
ℝ+) |
199 | 123, 195 | nndivred 10946 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ) |
200 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1 / 3) ∈
ℝ) |
201 | 195 | nnge1d 10940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 1 ≤ 𝑁) |
202 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 1 ∈
ℝ |
203 | | 0lt1 10429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 <
1 |
204 | 202, 203 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (1 ∈
ℝ ∧ 0 < 1) |
205 | 204 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (1 ∈ ℝ ∧ 0
< 1)) |
206 | 195 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ∈ ℝ) |
207 | 195 | nngt0d 10941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 0 < 𝑁) |
208 | | lediv2 10792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1))) |
209 | 205, 206,
207, 163, 208 | syl121anc 1323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1))) |
210 | 201, 209 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1)) |
211 | 122 | rpcnd 11750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐸 ∈ ℂ) |
212 | 211 | div1d 10672 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐸 / 1) = 𝐸) |
213 | 210, 212 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐸 / 𝑁) ≤ 𝐸) |
214 | | stoweidlem59.18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐸 < (1 / 3)) |
215 | 199, 123,
200, 213, 214 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐸 / 𝑁) < (1 / 3)) |
216 | 215 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) < (1 / 3)) |
217 | 82, 89, 92, 17, 93, 23, 94, 95, 97, 99, 101, 103, 130, 141, 193, 194, 198, 216 | stoweidlem58 38951 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) |
218 | | df-rex 2902 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑥 ∈
𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) |
219 | 217, 218 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) |
220 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝐴) |
221 | | simprr1 1102 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)) |
222 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = 𝑥 → (𝑦‘𝑡) = (𝑥‘𝑡)) |
223 | 222 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = 𝑥 → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (𝑥‘𝑡))) |
224 | 222 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) ≤ 1 ↔ (𝑥‘𝑡) ≤ 1)) |
225 | 223, 224 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = 𝑥 → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1))) |
226 | 225 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1))) |
227 | 226, 1 | elrab2 3333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1))) |
228 | 220, 221,
227 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝑌) |
229 | | simprr2 1103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁)) |
230 | | simprr3 1104 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)) |
231 | 229, 230 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) |
232 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑦𝑥 |
233 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)) |
234 | 222 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑥‘𝑡) < (𝐸 / 𝑁))) |
235 | 234 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁))) |
236 | 222 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) |
237 | 236 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) |
238 | 235, 237 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) |
239 | 232, 3, 233, 238 | elrabf 3329 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑥 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) |
240 | 228, 231,
239 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) |
241 | 240 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})) |
242 | 241 | eximdv 1833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})) |
243 | 219, 242 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) |
244 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅) |
245 | 244 | exlimiv 1845 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅) |
246 | 243, 245 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅) |
247 | 75, 246 | eqnetrd 2849 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅) |
248 | 247 | 3adant3 1074 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) ≠ ∅) |
249 | 71, 248 | eqnetrrd 2850 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → 𝑤 ≠ ∅) |
250 | 249 | 3exp 1256 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))) |
251 | 250 | rexlimdv 3012 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅)) |
252 | 251 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅)) |
253 | 70, 252 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅) |
254 | 253 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅) |
255 | | rsp 2913 |
. . . . . . . . . . 11
⊢
(∀𝑤 ∈
ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) |
256 | 55, 56, 254, 255 | syl3c 64 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (ℎ‘𝑤) ∈ 𝑤) |
257 | 256 | ex 449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (ℎ‘𝑤) ∈ 𝑤)) |
258 | 54, 257 | ralrimi 2940 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤) |
259 | | chfnrn 6236 |
. . . . . . . 8
⊢ ((ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤) → ran ℎ ⊆ ∪ ran
𝐻) |
260 | 39, 258, 259 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ ∪ ran
𝐻) |
261 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝜑 |
262 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦ℎ |
263 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(0...𝑁) |
264 | | nfrab1 3099 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} |
265 | 263, 264 | nfmpt 4674 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) |
266 | 29, 265 | nfcxfr 2749 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝐻 |
267 | 266 | nfrn 5289 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦ran
𝐻 |
268 | 262, 267 | nffn 5901 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 ℎ Fn ran 𝐻 |
269 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) |
270 | 267, 269 | nfral 2929 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) |
271 | 268, 270 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) |
272 | 261, 271 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) |
273 | 267 | nfuni 4378 |
. . . . . . . . 9
⊢
Ⅎ𝑦∪ ran 𝐻 |
274 | | fnunirn 6415 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran
𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧))) |
275 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗𝑧 |
276 | 60, 275 | nffv 6110 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗(𝐻‘𝑧) |
277 | 276 | nfcri 2745 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗 𝑦 ∈ (𝐻‘𝑧) |
278 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧 𝑦 ∈ (𝐻‘𝑗) |
279 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑗 → (𝐻‘𝑧) = (𝐻‘𝑗)) |
280 | 279 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑗 → (𝑦 ∈ (𝐻‘𝑧) ↔ 𝑦 ∈ (𝐻‘𝑗))) |
281 | 277, 278,
280 | cbvrex 3144 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑧 ∈
(0...𝑁)𝑦 ∈ (𝐻‘𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)) |
282 | 274, 281 | syl6bb 275 |
. . . . . . . . . . . . . 14
⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran
𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))) |
283 | 31, 282 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ ∪ ran
𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))) |
284 | 283 | biimpa 500 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)) |
285 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗𝜑 |
286 | 60 | nfrn 5289 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗ran
𝐻 |
287 | 286 | nfuni 4378 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗∪ ran 𝐻 |
288 | 287 | nfcri 2745 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗 𝑦 ∈ ∪ ran 𝐻 |
289 | 285, 288 | nfan 1816 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗(𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) |
290 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗 𝑦 ∈ 𝑌 |
291 | | simp1l 1078 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝜑) |
292 | | simp2 1055 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑗 ∈ (0...𝑁)) |
293 | | simp3 1056 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ (𝐻‘𝑗)) |
294 | 75 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻‘𝑗) ↔ 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})) |
295 | 294 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) |
296 | | rabid 3095 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)))) |
297 | 295, 296 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)))) |
298 | 297 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) |
299 | 291, 292,
293, 298 | syl21anc 1317 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) |
300 | 299 | 3exp 1256 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌))) |
301 | 289, 290,
300 | rexlimd 3008 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) → (∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌)) |
302 | 284, 301 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) → 𝑦 ∈ 𝑌) |
303 | 302 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑦 ∈ ∪ ran
𝐻) → 𝑦 ∈ 𝑌) |
304 | 303 | ex 449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑦 ∈ ∪ ran
𝐻 → 𝑦 ∈ 𝑌)) |
305 | 272, 273,
3, 304 | ssrd 3573 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran
𝐻 ⊆ 𝑌) |
306 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ⊆ 𝐴 |
307 | 1, 306 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑌 ⊆ 𝐴 |
308 | 305, 307 | syl6ss 3580 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran
𝐻 ⊆ 𝐴) |
309 | 260, 308 | sstrd 3578 |
. . . . . 6
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ 𝐴) |
310 | 49, 309 | fssd 5970 |
. . . . 5
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶𝐴) |
311 | | dffn3 5967 |
. . . . . . 7
⊢ (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻) |
312 | 31, 311 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐻:(0...𝑁)⟶ran 𝐻) |
313 | 312 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻) |
314 | | fco 5971 |
. . . . 5
⊢ ((ℎ:ran 𝐻⟶𝐴 ∧ 𝐻:(0...𝑁)⟶ran 𝐻) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴) |
315 | 310, 313,
314 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴) |
316 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑗ℎ |
317 | 316, 286 | nffn 5901 |
. . . . . . 7
⊢
Ⅎ𝑗 ℎ Fn ran 𝐻 |
318 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) |
319 | 286, 318 | nfral 2929 |
. . . . . . 7
⊢
Ⅎ𝑗∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) |
320 | 317, 319 | nfan 1816 |
. . . . . 6
⊢
Ⅎ𝑗(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) |
321 | 285, 320 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑗(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) |
322 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑) |
323 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁)) |
324 | 31 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝐻 Fn (0...𝑁)) |
325 | | fvco2 6183 |
. . . . . . . . . . . 12
⊢ ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗))) |
326 | 324, 325 | sylancom 698 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗))) |
327 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) |
328 | | fnfun 5902 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 Fn (0...𝑁) → Fun 𝐻) |
329 | 31, 328 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun 𝐻) |
330 | 329 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻) |
331 | | fndm 5904 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐻 Fn (0...𝑁) → dom 𝐻 = (0...𝑁)) |
332 | 31, 331 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐻 = (0...𝑁)) |
333 | 332 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁)) |
334 | 72, 333 | eleqtrrd 2691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻) |
335 | 334 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻) |
336 | | fvelrn 6260 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐻 ∧ 𝑗 ∈ dom 𝐻) → (𝐻‘𝑗) ∈ ran 𝐻) |
337 | 330, 335,
336 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ∈ ran 𝐻) |
338 | 327, 337 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻)) |
339 | 247 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅) |
340 | | neeq1 2844 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐻‘𝑗) → (𝑤 ≠ ∅ ↔ (𝐻‘𝑗) ≠ ∅)) |
341 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝐻‘𝑗) → (ℎ‘𝑤) = (ℎ‘(𝐻‘𝑗))) |
342 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝐻‘𝑗) → 𝑤 = (𝐻‘𝑗)) |
343 | 341, 342 | eleq12d 2682 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐻‘𝑗) → ((ℎ‘𝑤) ∈ 𝑤 ↔ (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))) |
344 | 340, 343 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐻‘𝑗) → ((𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ↔ ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))) |
345 | 344 | rspccva 3281 |
. . . . . . . . . . . 12
⊢
((∀𝑤 ∈
ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻) → ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))) |
346 | 338, 339,
345 | sylc 63 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)) |
347 | 326, 346 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) |
348 | 262, 266 | nfco 5209 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(ℎ ∘ 𝐻) |
349 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝑗 |
350 | 348, 349 | nffv 6110 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) |
351 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ (0...𝑁)) |
352 | 266, 349 | nffv 6110 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝐻‘𝑗) |
353 | 350, 352 | nfel 2763 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) |
354 | 351, 353 | nfan 1816 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) |
355 | 350, 3 | nfel 2763 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 |
356 | 354, 355 | nfim 1813 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌) |
357 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ (𝐻‘𝑗) ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))) |
358 | 357 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) ↔ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)))) |
359 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)) |
360 | 358, 359 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))) |
361 | 350, 356,
360, 298 | vtoclgf 3237 |
. . . . . . . . . . 11
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)) |
362 | 361 | anabsi7 856 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌) |
363 | 322, 323,
347, 362 | syl21anc 1317 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌) |
364 | 1 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}) |
365 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝐴 |
366 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝑇 |
367 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦0 |
368 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦
≤ |
369 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝑡 |
370 | 350, 369 | nffv 6110 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) |
371 | 367, 368,
370 | nfbr 4629 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦0 ≤
(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) |
372 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦1 |
373 | 370, 368,
372 | nfbr 4629 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1 |
374 | 371, 373 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(0 ≤
(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) |
375 | 366, 374 | nfral 2929 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) |
376 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡𝑦 |
377 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡ℎ |
378 | | nfra1 2925 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) |
379 | | nfra1 2925 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) |
380 | 378, 379 | nfan 1816 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) |
381 | | nfra1 2925 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) |
382 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡𝐴 |
383 | 381, 382 | nfrab 3100 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} |
384 | 1, 383 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡𝑌 |
385 | 380, 384 | nfrab 3100 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} |
386 | 77, 385 | nfmpt 4674 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) |
387 | 29, 386 | nfcxfr 2749 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝐻 |
388 | 377, 387 | nfco 5209 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(ℎ ∘ 𝐻) |
389 | 388, 81 | nffv 6110 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡((ℎ ∘ 𝐻)‘𝑗) |
390 | 376, 389 | nfeq 2762 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡 𝑦 = ((ℎ ∘ 𝐻)‘𝑗) |
391 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) |
392 | 391 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) |
393 | 391 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)) |
394 | 392, 393 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) |
395 | 390, 394 | ralbid 2966 |
. . . . . . . . . . 11
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) |
396 | 350, 365,
375, 395 | elrabf 3329 |
. . . . . . . . . 10
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) |
397 | 364, 396 | bitri 263 |
. . . . . . . . 9
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) |
398 | 363, 397 | sylib 207 |
. . . . . . . 8
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) |
399 | 398 | simprd 478 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)) |
400 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝐷‘𝑗) |
401 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦
< |
402 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝐸 / 𝑁) |
403 | 370, 401,
402 | nfbr 4629 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) |
404 | 400, 403 | nfral 2929 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) |
405 | 354, 404 | nfim 1813 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)) |
406 | 391 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))) |
407 | 390, 406 | ralbid 2966 |
. . . . . . . . . . 11
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))) |
408 | 358, 407 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))) |
409 | 297 | simprd 478 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))) |
410 | 409 | simpld 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)) |
411 | 350, 405,
408, 410 | vtoclgf 3237 |
. . . . . . . . 9
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))) |
412 | 411 | anabsi7 856 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)) |
413 | 322, 323,
347, 412 | syl21anc 1317 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)) |
414 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝐵‘𝑗) |
415 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(1
− (𝐸 / 𝑁)) |
416 | 415, 401,
370 | nfbr 4629 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(1 −
(𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) |
417 | 414, 416 | nfral 2929 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) |
418 | 354, 417 | nfim 1813 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) |
419 | 391 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) |
420 | 390, 419 | ralbid 2966 |
. . . . . . . . . . 11
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) |
421 | 358, 420 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))) |
422 | 409 | simprd 478 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) |
423 | 350, 418,
421, 422 | vtoclgf 3237 |
. . . . . . . . 9
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) |
424 | 423 | anabsi7 856 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) |
425 | 322, 323,
347, 424 | syl21anc 1317 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) |
426 | 399, 413,
425 | 3jca 1235 |
. . . . . 6
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) |
427 | 426 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))) |
428 | 321, 427 | ralrimi 2940 |
. . . 4
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) |
429 | 315, 428 | jca 553 |
. . 3
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))) |
430 | | feq1 5939 |
. . . . 5
⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)) |
431 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑗𝑥 |
432 | 316, 60 | nfco 5209 |
. . . . . . 7
⊢
Ⅎ𝑗(ℎ ∘ 𝐻) |
433 | 431, 432 | nfeq 2762 |
. . . . . 6
⊢
Ⅎ𝑗 𝑥 = (ℎ ∘ 𝐻) |
434 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝑥 |
435 | 434, 388 | nfeq 2762 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑥 = (ℎ ∘ 𝐻) |
436 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥‘𝑗) = ((ℎ ∘ 𝐻)‘𝑗)) |
437 | 436 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥‘𝑗)‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) |
438 | 437 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑥 = (ℎ ∘ 𝐻) → (0 ≤ ((𝑥‘𝑗)‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) |
439 | 437 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)) |
440 | 438, 439 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = (ℎ ∘ 𝐻) → ((0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) |
441 | 435, 440 | ralbid 2966 |
. . . . . . 7
⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) |
442 | 437 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))) |
443 | 435, 442 | ralbid 2966 |
. . . . . . 7
⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))) |
444 | 437 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑥 = (ℎ ∘ 𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) |
445 | 435, 444 | ralbid 2966 |
. . . . . . 7
⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) |
446 | 441, 443,
445 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑥 = (ℎ ∘ 𝐻) → ((∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))) |
447 | 433, 446 | ralbid 2966 |
. . . . 5
⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))) |
448 | 430, 447 | anbi12d 743 |
. . . 4
⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))) ↔ ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))) |
449 | 448 | spcegv 3267 |
. . 3
⊢ ((ℎ ∘ 𝐻) ∈ V → (((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))) |
450 | 47, 429, 449 | sylc 63 |
. 2
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)))) |
451 | 38, 450 | exlimddv 1850 |
1
⊢ (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)))) |