Proof of Theorem stoweidlem51
Step | Hyp | Ref
| Expression |
1 | | stoweidlem51.5 |
. . . 4
⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
2 | | ssrab2 3908 |
. . . 4
⊢ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ⊆ 𝐴 |
3 | 1, 2 | eqsstri 3854 |
. . 3
⊢ 𝑌 ⊆ 𝐴 |
4 | | stoweidlem51.6 |
. . . 4
⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) |
5 | | stoweidlem51.7 |
. . . 4
⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀) |
6 | | 1zzd 11760 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
7 | | stoweidlem51.10 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
8 | 7 | nnzd 11833 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | 6, 8, 8 | 3jca 1119 |
. . . . 5
⊢ (𝜑 → (1 ∈ ℤ ∧
𝑀 ∈ ℤ ∧
𝑀 ∈
ℤ)) |
10 | 7 | nnge1d 11423 |
. . . . . 6
⊢ (𝜑 → 1 ≤ 𝑀) |
11 | 7 | nnred 11391 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) |
12 | 11 | leidd 10941 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
13 | 10, 12 | jca 507 |
. . . . 5
⊢ (𝜑 → (1 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)) |
14 | | elfz2 12650 |
. . . . 5
⊢ (𝑀 ∈ (1...𝑀) ↔ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (1 ≤
𝑀 ∧ 𝑀 ≤ 𝑀))) |
15 | 9, 13, 14 | sylanbrc 578 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (1...𝑀)) |
16 | | stoweidlem51.12 |
. . . 4
⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌) |
17 | | stoweidlem51.2 |
. . . . 5
⊢
Ⅎ𝑡𝜑 |
18 | | eqid 2778 |
. . . . 5
⊢ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) = (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) |
19 | | stoweidlem51.20 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
20 | | stoweidlem51.19 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
21 | 17, 1, 18, 19, 20 | stoweidlem16 41164 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌) |
22 | | stoweidlem51.21 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ V) |
23 | 4, 5, 15, 16, 21, 22 | fmulcl 40725 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑌) |
24 | 3, 23 | sseldi 3819 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
25 | 1 | eleq2i 2851 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑌 ↔ 𝑋 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}) |
26 | | nfcv 2934 |
. . . . . . . . . . 11
⊢
Ⅎℎ1 |
27 | | nfrab1 3309 |
. . . . . . . . . . . . . 14
⊢
Ⅎℎ{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
28 | 1, 27 | nfcxfr 2932 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ𝑌 |
29 | | nfcv 2934 |
. . . . . . . . . . . . 13
⊢
Ⅎℎ(𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) |
30 | 28, 28, 29 | nfmpt2 7001 |
. . . . . . . . . . . 12
⊢
Ⅎℎ(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) |
31 | 4, 30 | nfcxfr 2932 |
. . . . . . . . . . 11
⊢
Ⅎℎ𝑃 |
32 | | nfcv 2934 |
. . . . . . . . . . 11
⊢
Ⅎℎ𝑈 |
33 | 26, 31, 32 | nfseq 13129 |
. . . . . . . . . 10
⊢
Ⅎℎseq1(𝑃, 𝑈) |
34 | | nfcv 2934 |
. . . . . . . . . 10
⊢
Ⅎℎ𝑀 |
35 | 33, 34 | nffv 6456 |
. . . . . . . . 9
⊢
Ⅎℎ(seq1(𝑃, 𝑈)‘𝑀) |
36 | 5, 35 | nfcxfr 2932 |
. . . . . . . 8
⊢
Ⅎℎ𝑋 |
37 | | nfcv 2934 |
. . . . . . . 8
⊢
Ⅎℎ𝐴 |
38 | | nfcv 2934 |
. . . . . . . . 9
⊢
Ⅎℎ𝑇 |
39 | | nfcv 2934 |
. . . . . . . . . . 11
⊢
Ⅎℎ0 |
40 | | nfcv 2934 |
. . . . . . . . . . 11
⊢
Ⅎℎ
≤ |
41 | | nfcv 2934 |
. . . . . . . . . . . 12
⊢
Ⅎℎ𝑡 |
42 | 36, 41 | nffv 6456 |
. . . . . . . . . . 11
⊢
Ⅎℎ(𝑋‘𝑡) |
43 | 39, 40, 42 | nfbr 4933 |
. . . . . . . . . 10
⊢
Ⅎℎ0 ≤ (𝑋‘𝑡) |
44 | 42, 40, 26 | nfbr 4933 |
. . . . . . . . . 10
⊢
Ⅎℎ(𝑋‘𝑡) ≤ 1 |
45 | 43, 44 | nfan 1946 |
. . . . . . . . 9
⊢
Ⅎℎ(0 ≤
(𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1) |
46 | 38, 45 | nfral 3127 |
. . . . . . . 8
⊢
Ⅎℎ∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1) |
47 | | nfcv 2934 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡1 |
48 | | nfra1 3123 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) |
49 | | nfcv 2934 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝐴 |
50 | 48, 49 | nfrab 3310 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
51 | 1, 50 | nfcxfr 2932 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝑌 |
52 | | nfmpt1 4982 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) |
53 | 51, 51, 52 | nfmpt2 7001 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) |
54 | 4, 53 | nfcxfr 2932 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡𝑃 |
55 | | nfcv 2934 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡𝑈 |
56 | 47, 54, 55 | nfseq 13129 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡seq1(𝑃, 𝑈) |
57 | | nfcv 2934 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝑀 |
58 | 56, 57 | nffv 6456 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(seq1(𝑃, 𝑈)‘𝑀) |
59 | 5, 58 | nfcxfr 2932 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑋 |
60 | 59 | nfeq2 2949 |
. . . . . . . . 9
⊢
Ⅎ𝑡 ℎ = 𝑋 |
61 | | fveq1 6445 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑋 → (ℎ‘𝑡) = (𝑋‘𝑡)) |
62 | 61 | breq2d 4898 |
. . . . . . . . . 10
⊢ (ℎ = 𝑋 → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ (𝑋‘𝑡))) |
63 | 61 | breq1d 4896 |
. . . . . . . . . 10
⊢ (ℎ = 𝑋 → ((ℎ‘𝑡) ≤ 1 ↔ (𝑋‘𝑡) ≤ 1)) |
64 | 62, 63 | anbi12d 624 |
. . . . . . . . 9
⊢ (ℎ = 𝑋 → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
65 | 60, 64 | ralbid 3165 |
. . . . . . . 8
⊢ (ℎ = 𝑋 → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
66 | 36, 37, 46, 65 | elrabf 3568 |
. . . . . . 7
⊢ (𝑋 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
67 | 25, 66 | bitri 267 |
. . . . . 6
⊢ (𝑋 ∈ 𝑌 ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
68 | 23, 67 | sylib 210 |
. . . . 5
⊢ (𝜑 → (𝑋 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
69 | 68 | simprd 491 |
. . . 4
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1)) |
70 | | stoweidlem51.1 |
. . . . 5
⊢
Ⅎ𝑖𝜑 |
71 | | stoweidlem51.8 |
. . . . 5
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡))) |
72 | | stoweidlem51.9 |
. . . . 5
⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀)) |
73 | | stoweidlem51.11 |
. . . . 5
⊢ (𝜑 → 𝑊:(1...𝑀)⟶𝑉) |
74 | | stoweidlem51.14 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆ ∪ ran
𝑊) |
75 | | stoweidlem51.15 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆ 𝑇) |
76 | | nfv 1957 |
. . . . . . 7
⊢
Ⅎ𝑡 𝑖 ∈ (1...𝑀) |
77 | 17, 76 | nfan 1946 |
. . . . . 6
⊢
Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (1...𝑀)) |
78 | 16 | ffvelrnda 6623 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝑌) |
79 | | fveq1 6445 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝑈‘𝑖) → (ℎ‘𝑡) = ((𝑈‘𝑖)‘𝑡)) |
80 | 79 | breq2d 4898 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = (𝑈‘𝑖) → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ ((𝑈‘𝑖)‘𝑡))) |
81 | 79 | breq1d 4896 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = (𝑈‘𝑖) → ((ℎ‘𝑡) ≤ 1 ↔ ((𝑈‘𝑖)‘𝑡) ≤ 1)) |
82 | 80, 81 | anbi12d 624 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = (𝑈‘𝑖) → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ ((𝑈‘𝑖)‘𝑡) ∧ ((𝑈‘𝑖)‘𝑡) ≤ 1))) |
83 | 82 | ralbidv 3168 |
. . . . . . . . . . . . . 14
⊢ (ℎ = (𝑈‘𝑖) → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑈‘𝑖)‘𝑡) ∧ ((𝑈‘𝑖)‘𝑡) ≤ 1))) |
84 | 83, 1 | elrab2 3576 |
. . . . . . . . . . . . 13
⊢ ((𝑈‘𝑖) ∈ 𝑌 ↔ ((𝑈‘𝑖) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ ((𝑈‘𝑖)‘𝑡) ∧ ((𝑈‘𝑖)‘𝑡) ≤ 1))) |
85 | 84 | simplbi 493 |
. . . . . . . . . . . 12
⊢ ((𝑈‘𝑖) ∈ 𝑌 → (𝑈‘𝑖) ∈ 𝐴) |
86 | 78, 85 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖) ∈ 𝐴) |
87 | | eleq1 2847 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑈‘𝑖) → (𝑓 ∈ 𝐴 ↔ (𝑈‘𝑖) ∈ 𝐴)) |
88 | 87 | anbi2d 622 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑈‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ (𝑈‘𝑖) ∈ 𝐴))) |
89 | | feq1 6272 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑈‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈‘𝑖):𝑇⟶ℝ)) |
90 | 88, 89 | imbi12d 336 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑈‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝐴) → (𝑈‘𝑖):𝑇⟶ℝ))) |
91 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ 𝐴 → ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ)) |
92 | 90, 91 | vtoclga 3474 |
. . . . . . . . . . . 12
⊢ ((𝑈‘𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝐴) → (𝑈‘𝑖):𝑇⟶ℝ)) |
93 | 92 | anabsi7 661 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈‘𝑖) ∈ 𝐴) → (𝑈‘𝑖):𝑇⟶ℝ) |
94 | 86, 93 | syldan 585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑈‘𝑖):𝑇⟶ℝ) |
95 | 94 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → (𝑈‘𝑖):𝑇⟶ℝ) |
96 | 73 | ffvelrnda 6623 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊‘𝑖) ∈ 𝑉) |
97 | | simpl 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝜑) |
98 | 97, 96 | jca 507 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑊‘𝑖) ∈ 𝑉)) |
99 | | stoweidlem51.3 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑤𝜑 |
100 | | stoweidlem51.4 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤𝑉 |
101 | 100 | nfel2 2950 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑤(𝑊‘𝑖) ∈ 𝑉 |
102 | 99, 101 | nfan 1946 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑤(𝜑 ∧ (𝑊‘𝑖) ∈ 𝑉) |
103 | | nfv 1957 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑤(𝑊‘𝑖) ⊆ 𝑇 |
104 | 102, 103 | nfim 1943 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑤((𝜑 ∧ (𝑊‘𝑖) ∈ 𝑉) → (𝑊‘𝑖) ⊆ 𝑇) |
105 | | eleq1 2847 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑊‘𝑖) → (𝑤 ∈ 𝑉 ↔ (𝑊‘𝑖) ∈ 𝑉)) |
106 | 105 | anbi2d 622 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑊‘𝑖) → ((𝜑 ∧ 𝑤 ∈ 𝑉) ↔ (𝜑 ∧ (𝑊‘𝑖) ∈ 𝑉))) |
107 | | sseq1 3845 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑊‘𝑖) → (𝑤 ⊆ 𝑇 ↔ (𝑊‘𝑖) ⊆ 𝑇)) |
108 | 106, 107 | imbi12d 336 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑊‘𝑖) → (((𝜑 ∧ 𝑤 ∈ 𝑉) → 𝑤 ⊆ 𝑇) ↔ ((𝜑 ∧ (𝑊‘𝑖) ∈ 𝑉) → (𝑊‘𝑖) ⊆ 𝑇))) |
109 | | stoweidlem51.13 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉) → 𝑤 ⊆ 𝑇) |
110 | 104, 108,
109 | vtoclg1f 3466 |
. . . . . . . . . . 11
⊢ ((𝑊‘𝑖) ∈ 𝑉 → ((𝜑 ∧ (𝑊‘𝑖) ∈ 𝑉) → (𝑊‘𝑖) ⊆ 𝑇)) |
111 | 96, 98, 110 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊‘𝑖) ⊆ 𝑇) |
112 | 111 | sselda 3821 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → 𝑡 ∈ 𝑇) |
113 | 95, 112 | ffvelrnd 6624 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → ((𝑈‘𝑖)‘𝑡) ∈ ℝ) |
114 | | stoweidlem51.22 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
115 | 114 | rpred 12181 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℝ) |
116 | 115 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → 𝐸 ∈ ℝ) |
117 | 11 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → 𝑀 ∈ ℝ) |
118 | 7 | nnne0d 11425 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≠ 0) |
119 | 118 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → 𝑀 ≠ 0) |
120 | 116, 117,
119 | redivcld 11203 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → (𝐸 / 𝑀) ∈ ℝ) |
121 | | stoweidlem51.17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊‘𝑖)((𝑈‘𝑖)‘𝑡) < (𝐸 / 𝑀)) |
122 | 121 | r19.21bi 3114 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → ((𝑈‘𝑖)‘𝑡) < (𝐸 / 𝑀)) |
123 | | 1red 10377 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
124 | | 0lt1 10897 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
125 | 124 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 1) |
126 | 7 | nngt0d 11424 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑀) |
127 | 114 | rpregt0d 12187 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
128 | | lediv2 11267 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 1))) |
129 | 123, 125,
11, 126, 127, 128 | syl221anc 1449 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 ≤ 𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 1))) |
130 | 10, 129 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 / 𝑀) ≤ (𝐸 / 1)) |
131 | 114 | rpcnd 12183 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℂ) |
132 | 131 | div1d 11143 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 / 1) = 𝐸) |
133 | 130, 132 | breqtrd 4912 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 / 𝑀) ≤ 𝐸) |
134 | 133 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → (𝐸 / 𝑀) ≤ 𝐸) |
135 | 113, 120,
116, 122, 134 | ltletrd 10536 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊‘𝑖)) → ((𝑈‘𝑖)‘𝑡) < 𝐸) |
136 | 135 | ex 403 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑡 ∈ (𝑊‘𝑖) → ((𝑈‘𝑖)‘𝑡) < 𝐸)) |
137 | 77, 136 | ralrimi 3139 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊‘𝑖)((𝑈‘𝑖)‘𝑡) < 𝐸) |
138 | 70, 17, 1, 4, 5, 71,
72, 7, 73, 16, 74, 75, 137, 22, 19, 20, 114 | stoweidlem48 41196 |
. . . 4
⊢ (𝜑 → ∀𝑡 ∈ 𝐷 (𝑋‘𝑡) < 𝐸) |
139 | | stoweidlem51.18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑀)) < ((𝑈‘𝑖)‘𝑡)) |
140 | | stoweidlem51.23 |
. . . . 5
⊢ (𝜑 → 𝐸 < (1 / 3)) |
141 | 3 | sseli 3817 |
. . . . . 6
⊢ (𝑓 ∈ 𝑌 → 𝑓 ∈ 𝐴) |
142 | 141, 19 | sylan2 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ) |
143 | | stoweidlem51.16 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝑇) |
144 | 70, 17, 51, 4, 5, 71, 72, 7, 16, 139, 114, 140, 142, 21, 22, 143 | stoweidlem42 41190 |
. . . 4
⊢ (𝜑 → ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑋‘𝑡)) |
145 | 69, 138, 144 | 3jca 1119 |
. . 3
⊢ (𝜑 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑋‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑋‘𝑡))) |
146 | 24, 145 | jca 507 |
. 2
⊢ (𝜑 → (𝑋 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑋‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑋‘𝑡)))) |
147 | | eleq1 2847 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴)) |
148 | 59 | nfeq2 2949 |
. . . . . 6
⊢
Ⅎ𝑡 𝑥 = 𝑋 |
149 | | fveq1 6445 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥‘𝑡) = (𝑋‘𝑡)) |
150 | 149 | breq2d 4898 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (0 ≤ (𝑥‘𝑡) ↔ 0 ≤ (𝑋‘𝑡))) |
151 | 149 | breq1d 4896 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ((𝑥‘𝑡) ≤ 1 ↔ (𝑋‘𝑡) ≤ 1)) |
152 | 150, 151 | anbi12d 624 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ((0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ↔ (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
153 | 148, 152 | ralbid 3165 |
. . . . 5
⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
154 | 149 | breq1d 4896 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ((𝑥‘𝑡) < 𝐸 ↔ (𝑋‘𝑡) < 𝐸)) |
155 | 148, 154 | ralbid 3165 |
. . . . 5
⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ↔ ∀𝑡 ∈ 𝐷 (𝑋‘𝑡) < 𝐸)) |
156 | 149 | breq2d 4898 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ((1 − 𝐸) < (𝑥‘𝑡) ↔ (1 − 𝐸) < (𝑋‘𝑡))) |
157 | 148, 156 | ralbid 3165 |
. . . . 5
⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡) ↔ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑋‘𝑡))) |
158 | 153, 155,
157 | 3anbi123d 1509 |
. . . 4
⊢ (𝑥 = 𝑋 → ((∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑋‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑋‘𝑡)))) |
159 | 147, 158 | anbi12d 624 |
. . 3
⊢ (𝑥 = 𝑋 → ((𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡))) ↔ (𝑋 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑋‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑋‘𝑡))))) |
160 | 159 | spcegv 3496 |
. 2
⊢ (𝑋 ∈ 𝐴 → ((𝑋 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑋‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑋‘𝑡))) → ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡))))) |
161 | 24, 146, 160 | sylc 65 |
1
⊢ (𝜑 → ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))) |