Step | Hyp | Ref
| Expression |
1 | | stoweidlem34.3 |
. 2
⊢
Ⅎ𝑡𝜑 |
2 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
3 | | ovex 6678 |
. . . . . . . . 9
⊢
(1...𝑁) ∈
V |
4 | 3 | rabex 4813 |
. . . . . . . 8
⊢ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)} ∈ V |
5 | | stoweidlem34.6 |
. . . . . . . . 9
⊢ 𝐽 = (𝑡 ∈ 𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)}) |
6 | 5 | fvmpt2 6291 |
. . . . . . . 8
⊢ ((𝑡 ∈ 𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)} ∈ V) → (𝐽‘𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)}) |
7 | 2, 4, 6 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐽‘𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)}) |
8 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)} ⊆ (1...𝑁) |
9 | 7, 8 | syl6eqss 3655 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐽‘𝑡) ⊆ (1...𝑁)) |
10 | | elfznn 12370 |
. . . . . . 7
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ) |
11 | 10 | ssriv 3607 |
. . . . . 6
⊢
(1...𝑁) ⊆
ℕ |
12 | 9, 11 | syl6ss 3615 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐽‘𝑡) ⊆ ℕ) |
13 | | nnssre 11024 |
. . . . 5
⊢ ℕ
⊆ ℝ |
14 | 12, 13 | syl6ss 3615 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐽‘𝑡) ⊆ ℝ) |
15 | | stoweidlem34.7 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℕ) |
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑁 ∈ ℕ) |
17 | | nnuz 11723 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
18 | 16, 17 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑁 ∈
(ℤ≥‘1)) |
19 | | eluzfz2 12349 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑁 ∈ (1...𝑁)) |
21 | | stoweidlem34.11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) < ((𝑁 − 1) · 𝐸)) |
22 | | 3re 11094 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 3 ∈
ℝ |
23 | | 3ne0 11115 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 3 ≠
0 |
24 | 22, 23 | rereccli 10790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 / 3)
∈ ℝ |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 / 3) ∈
ℝ) |
26 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℝ) |
27 | 16 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑁 ∈ ℝ) |
28 | | 1lt3 11196 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 <
3 |
29 | 22, 28 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3 ∈
ℝ ∧ 1 < 3) |
30 | | recgt1i 10920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((3
∈ ℝ ∧ 1 < 3) → (0 < (1 / 3) ∧ (1 / 3) <
1)) |
31 | 30 | simprd 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((3
∈ ℝ ∧ 1 < 3) → (1 / 3) < 1) |
32 | 29, 31 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 / 3) < 1) |
33 | 25, 26, 27, 32 | ltsub2dd 10640 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑁 − 1) < (𝑁 − (1 / 3))) |
34 | 27, 26 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑁 − 1) ∈ ℝ) |
35 | 27, 25 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑁 − (1 / 3)) ∈
ℝ) |
36 | | stoweidlem34.12 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
37 | 36 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸 ∈ ℝ) |
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐸 ∈ ℝ) |
39 | 36 | rpgt0d 11875 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 < 𝐸) |
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 < 𝐸) |
41 | | ltmul1 10873 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 − 1) ∈ ℝ ∧
(𝑁 − (1 / 3)) ∈
ℝ ∧ (𝐸 ∈
ℝ ∧ 0 < 𝐸))
→ ((𝑁 − 1) <
(𝑁 − (1 / 3)) ↔
((𝑁 − 1) ·
𝐸) < ((𝑁 − (1 / 3)) · 𝐸))) |
42 | 34, 35, 38, 40, 41 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸))) |
43 | 33, 42 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) |
44 | 21, 43 | jca 554 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸))) |
45 | | stoweidlem34.9 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
46 | 45 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) |
47 | 34, 38 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑁 − 1) · 𝐸) ∈ ℝ) |
48 | 35, 38 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) |
49 | | lttr 10114 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹‘𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹‘𝑡) < ((𝑁 − (1 / 3)) · 𝐸))) |
50 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘𝑡) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹‘𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))) |
51 | 50 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹‘𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))) |
52 | 49, 51 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹‘𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))) |
53 | 46, 47, 48, 52 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (((𝐹‘𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))) |
54 | 44, 53 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)) |
55 | | rabid 3116 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))) |
56 | 2, 54, 55 | sylanbrc 698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)}) |
57 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
58 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘0) |
59 | 57, 58 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘0)) |
60 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
61 | 15, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
62 | | stoweidlem34.8 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ∈ V) |
63 | | rabexg 4812 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V) |
65 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑁 → (𝑗 − (1 / 3)) = (𝑁 − (1 / 3))) |
66 | 65 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑁 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑁 − (1 / 3)) · 𝐸)) |
67 | 66 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑁 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))) |
68 | 67 | rabbidv 3189 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑁 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)}) |
69 | | stoweidlem34.4 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
70 | 68, 69 | fvmptg 6280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝑁) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)}) |
71 | 61, 64, 70 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷‘𝑁) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)}) |
72 | 71 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐷‘𝑁) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)}) |
73 | 56, 72 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝐷‘𝑁)) |
74 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗𝑁 |
75 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗(1...𝑁) |
76 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
77 | 69, 76 | nfcxfr 2762 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗𝐷 |
78 | 77, 74 | nffv 6198 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗(𝐷‘𝑁) |
79 | 78 | nfcri 2758 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗 𝑡 ∈ (𝐷‘𝑁) |
80 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑁 → (𝐷‘𝑗) = (𝐷‘𝑁)) |
81 | 80 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑁 → (𝑡 ∈ (𝐷‘𝑗) ↔ 𝑡 ∈ (𝐷‘𝑁))) |
82 | 74, 75, 79, 81 | elrabf 3360 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)} ↔ (𝑁 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑁))) |
83 | 20, 73, 82 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)}) |
84 | 83, 7 | eleqtrrd 2704 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑁 ∈ (𝐽‘𝑡)) |
85 | | ne0i 3921 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (𝐽‘𝑡) → (𝐽‘𝑡) ≠ ∅) |
86 | 84, 85 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐽‘𝑡) ≠ ∅) |
87 | | nnwo 11753 |
. . . . . . . . . . 11
⊢ (((𝐽‘𝑡) ⊆ ℕ ∧ (𝐽‘𝑡) ≠ ∅) → ∃𝑖 ∈ (𝐽‘𝑡)∀𝑘 ∈ (𝐽‘𝑡)𝑖 ≤ 𝑘) |
88 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝐽‘𝑡) |
89 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗𝑇 |
90 | | nfrab1 3122 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗{𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)} |
91 | 89, 90 | nfmpt 4746 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗(𝑡 ∈ 𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)}) |
92 | 5, 91 | nfcxfr 2762 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝐽 |
93 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝑡 |
94 | 92, 93 | nffv 6198 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(𝐽‘𝑡) |
95 | | nfv 1843 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗 𝑖 ≤ 𝑘 |
96 | 94, 95 | nfral 2945 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗∀𝑘 ∈ (𝐽‘𝑡)𝑖 ≤ 𝑘 |
97 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘 |
98 | | breq1 4656 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (𝑖 ≤ 𝑘 ↔ 𝑗 ≤ 𝑘)) |
99 | 98 | ralbidv 2986 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (∀𝑘 ∈ (𝐽‘𝑡)𝑖 ≤ 𝑘 ↔ ∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘)) |
100 | 88, 94, 96, 97, 99 | cbvrexf 3166 |
. . . . . . . . . . 11
⊢
(∃𝑖 ∈
(𝐽‘𝑡)∀𝑘 ∈ (𝐽‘𝑡)𝑖 ≤ 𝑘 ↔ ∃𝑗 ∈ (𝐽‘𝑡)∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘) |
101 | 87, 100 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝐽‘𝑡) ⊆ ℕ ∧ (𝐽‘𝑡) ≠ ∅) → ∃𝑗 ∈ (𝐽‘𝑡)∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘) |
102 | 12, 86, 101 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑗 ∈ (𝐽‘𝑡)∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘) |
103 | | stoweidlem34.2 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗𝜑 |
104 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗 𝑡 ∈ 𝑇 |
105 | 103, 104 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(𝜑 ∧ 𝑡 ∈ 𝑇) |
106 | 7 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑗 ∈ (𝐽‘𝑡) ↔ 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)})) |
107 | 106 | biimpa 501 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)}) |
108 | | rabid 3116 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)} ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑗))) |
109 | 107, 108 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑗))) |
110 | 109 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → 𝑡 ∈ (𝐷‘𝑗)) |
111 | 110 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ ∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘) → 𝑡 ∈ (𝐷‘𝑗)) |
112 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑡 ∈ (𝐷‘(𝑗 − 1))) |
113 | | simp1l 1085 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝜑) |
114 | | noel 3919 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ¬
𝑡 ∈
∅ |
115 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 = 1 → (𝑗 − 1) = (1 − 1)) |
116 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (1
− 1) = 0 |
117 | 115, 116 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 = 1 → (𝑗 − 1) = 0) |
118 | 117 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 = 1 → (𝐷‘(𝑗 − 1)) = (𝐷‘0)) |
119 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 3 ∈ ℝ) |
120 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 3 ≠ 0) |
121 | 26, 119, 120 | redivcld 10853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 / 3) ∈
ℝ) |
122 | 121 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → -(1 / 3) ∈
ℝ) |
123 | 122, 38 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (-(1 / 3) · 𝐸) ∈
ℝ) |
124 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ∈ ℝ) |
125 | | 3pos 11114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 0 <
3 |
126 | 22, 125 | recgt0ii 10929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ 0 < (1
/ 3) |
127 | | lt0neg2 10535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((1 / 3)
∈ ℝ → (0 < (1 / 3) ↔ -(1 / 3) < 0)) |
128 | 24, 127 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (0 <
(1 / 3) ↔ -(1 / 3) < 0) |
129 | 126, 128 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ -(1 / 3)
< 0 |
130 | | ltmul1 10873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((-(1 /
3) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (-(1 / 3) < 0
↔ (-(1 / 3) · 𝐸) < (0 · 𝐸))) |
131 | 122, 124,
38, 40, 130 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (-(1 / 3) < 0 ↔ (-(1 / 3)
· 𝐸) < (0
· 𝐸))) |
132 | 129, 131 | mpbii 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (-(1 / 3) · 𝐸) < (0 · 𝐸)) |
133 | | mul02lem2 10213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝐸 ∈ ℝ → (0
· 𝐸) =
0) |
134 | 38, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (0 · 𝐸) = 0) |
135 | 132, 134 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (-(1 / 3) · 𝐸) < 0) |
136 | | stoweidlem34.10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ (𝐹‘𝑡)) |
137 | 123, 124,
46, 135, 136 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (-(1 / 3) · 𝐸) < (𝐹‘𝑡)) |
138 | 123, 46 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((-(1 / 3) · 𝐸) < (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸))) |
139 | 137, 138 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ¬ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸)) |
140 | | nan 604 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 → ¬ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸))) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ¬ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸))) |
141 | 139, 140 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ¬ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸))) |
142 | | rabid 3116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸))) |
143 | 141, 142 | sylnibr 319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → ¬ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸)}) |
144 | 15 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
145 | | elnn0uz 11725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
146 | 144, 145 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
147 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑁)) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → 0 ∈ (0...𝑁)) |
149 | | rabexg 4812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V) |
150 | 62, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V) |
151 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑗 = 0 → (𝑗 − (1 / 3)) = (0 − (1 /
3))) |
152 | | df-neg 10269 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ -(1 / 3)
= (0 − (1 / 3)) |
153 | 151, 152 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 = 0 → (𝑗 − (1 / 3)) = -(1 /
3)) |
154 | 153 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑗 = 0 → ((𝑗 − (1 / 3)) · 𝐸) = (-(1 / 3) · 𝐸)) |
155 | 154 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑗 = 0 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸))) |
156 | 155 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑗 = 0 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸)}) |
157 | 156, 69 | fvmptg 6280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((0
∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V) → (𝐷‘0) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸)}) |
158 | 148, 150,
157 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝐷‘0) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (-(1 / 3) · 𝐸)}) |
159 | 143, 158 | neleqtrrd 2723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ¬ 𝑡 ∈ (𝐷‘0)) |
160 | 1, 159 | alrimi 2082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0)) |
161 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
Ⅎ𝑡(0...𝑁) |
162 | | nfrab1 3122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} |
163 | 161, 162 | nfmpt 4746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
164 | 69, 163 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
Ⅎ𝑡𝐷 |
165 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
Ⅎ𝑡0 |
166 | 164, 165 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
Ⅎ𝑡(𝐷‘0) |
167 | 166 | eq0f 3925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐷‘0) = ∅ ↔
∀𝑡 ¬ 𝑡 ∈ (𝐷‘0)) |
168 | 160, 167 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐷‘0) = ∅) |
169 | 118, 168 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 = 1) → (𝐷‘(𝑗 − 1)) = ∅) |
170 | 169 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 = 1) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ ∅)) |
171 | 114, 170 | mtbiri 317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 = 1) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) |
172 | 171 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑗 = 1 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) |
173 | 172 | con2d 129 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ 𝑗 = 1)) |
174 | 113, 112,
173 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 = 1) |
175 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ ¬ 𝑗 = 1) → 𝜑) |
176 | 106, 108 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑗 ∈ (𝐽‘𝑡) ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑗)))) |
177 | 176 | simprbda 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → 𝑗 ∈ (1...𝑁)) |
178 | 15, 17 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
179 | 178 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽‘𝑡)) → 𝑁 ∈
(ℤ≥‘1)) |
180 | | elfzp12 12419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁)))) |
181 | 179, 180 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽‘𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁)))) |
182 | 181 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁)))) |
183 | 177, 182 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))) |
184 | 183 | orcanai 952 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ ¬ 𝑗 = 1) → 𝑗 ∈ ((1 + 1)...𝑁)) |
185 | | fzssp1 12384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(1...(𝑁 − 1))
⊆ (1...((𝑁 − 1)
+ 1)) |
186 | 15 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑁 ∈ ℂ) |
187 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 1 ∈
ℂ) |
188 | 186, 187 | npcand 10396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
189 | 188 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
190 | 185, 189 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
191 | 190 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
192 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ((1 + 1)...𝑁)) |
193 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 1 ∈
ℤ |
194 | | zaddcl 11417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((1
∈ ℤ ∧ 1 ∈ ℤ) → (1 + 1) ∈
ℤ) |
195 | 193, 193,
194 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (1 + 1)
∈ ℤ |
196 | 195 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → (1 + 1) ∈
ℤ) |
197 | 15 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑁 ∈ ℤ) |
198 | 197 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → 𝑁 ∈ ℤ) |
199 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 ∈ ((1 + 1)...𝑁) → 𝑗 ∈ ℤ) |
200 | 199 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ℤ) |
201 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → 1 ∈ ℤ) |
202 | | fzsubel 12377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((1 +
1) ∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝑗
∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) |
203 | 196, 198,
200, 201, 202 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) |
204 | 192, 203 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1))) |
205 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℂ |
206 | 205, 205 | pncan3oi 10297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((1 + 1)
− 1) = 1 |
207 | 206 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((1 + 1)
− 1)...(𝑁 − 1))
= (1...(𝑁 −
1)) |
208 | 204, 207 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...(𝑁 − 1))) |
209 | 191, 208 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...𝑁)) |
210 | 175, 184,
209 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ ¬ 𝑗 = 1) → (𝑗 − 1) ∈ (1...𝑁)) |
211 | 210 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁))) |
212 | 211 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁))) |
213 | 174, 212 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (1...𝑁)) |
214 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = (𝑗 − 1) → (𝐷‘𝑖) = (𝐷‘(𝑗 − 1))) |
215 | 214 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = (𝑗 − 1) → (𝑡 ∈ (𝐷‘𝑖) ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) |
216 | 215 | elrab3 3364 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 − 1) ∈ (1...𝑁) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) |
217 | 213, 216 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) |
218 | 112, 217 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑖)}) |
219 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑖(1...𝑁) |
220 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑖 𝑡 ∈ (𝐷‘𝑗) |
221 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑗𝑖 |
222 | 77, 221 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑗(𝐷‘𝑖) |
223 | 222 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗 𝑡 ∈ (𝐷‘𝑖) |
224 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖)) |
225 | 224 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑖 → (𝑡 ∈ (𝐷‘𝑗) ↔ 𝑡 ∈ (𝐷‘𝑖))) |
226 | 75, 219, 220, 223, 225 | cbvrab 3198 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)} = {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑖)} |
227 | 218, 226 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)}) |
228 | 7 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝐽‘𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)}) |
229 | 227, 228 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (𝐽‘𝑡)) |
230 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (1...𝑁) → 𝑗 ∈ ℤ) |
231 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
ℝ) |
232 | 177, 230,
231 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → 𝑗 ∈ ℝ) |
233 | 232 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑗 ∈ ℝ) |
234 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℝ → (𝑗 − 1) ∈
ℝ) |
235 | 233, 234 | jccir 562 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ)) |
236 | | ltm1 10863 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℝ → (𝑗 − 1) < 𝑗) |
237 | 236 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ)
→ (𝑗 − 1) <
𝑗) |
238 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑗 − 1) ∈ ℝ ∧
𝑗 ∈ ℝ) →
((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1))) |
239 | 238 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ)
→ ((𝑗 − 1) <
𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1))) |
240 | 237, 239 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ)
→ ¬ 𝑗 ≤ (𝑗 − 1)) |
241 | 235, 240 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 ≤ (𝑗 − 1)) |
242 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = (𝑗 − 1) → (𝑗 ≤ 𝑘 ↔ 𝑗 ≤ (𝑗 − 1))) |
243 | 242 | notbid 308 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑗 − 1) → (¬ 𝑗 ≤ 𝑘 ↔ ¬ 𝑗 ≤ (𝑗 − 1))) |
244 | 243 | rspcev 3309 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑗 − 1) ∈ (𝐽‘𝑡) ∧ ¬ 𝑗 ≤ (𝑗 − 1)) → ∃𝑘 ∈ (𝐽‘𝑡) ¬ 𝑗 ≤ 𝑘) |
245 | 229, 241,
244 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ∃𝑘 ∈ (𝐽‘𝑡) ¬ 𝑗 ≤ 𝑘) |
246 | | rexnal 2995 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑘 ∈
(𝐽‘𝑡) ¬ 𝑗 ≤ 𝑘 ↔ ¬ ∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘) |
247 | 245, 246 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ ∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘) |
248 | 247 | 3expia 1267 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ ∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘)) |
249 | 248 | con2d 129 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → (∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) |
250 | 249 | imp 445 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ ∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) |
251 | 111, 250 | eldifd 3585 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ ∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘) → 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1)))) |
252 | 251 | exp31 630 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑗 ∈ (𝐽‘𝑡) → (∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘 → 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1)))))) |
253 | 105, 252 | reximdai 3012 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (∃𝑗 ∈ (𝐽‘𝑡)∀𝑘 ∈ (𝐽‘𝑡)𝑗 ≤ 𝑘 → ∃𝑗 ∈ (𝐽‘𝑡)𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) |
254 | 102, 253 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑗 ∈ (𝐽‘𝑡)𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1)))) |
255 | | df-rex 2918 |
. . . . . . . 8
⊢
(∃𝑗 ∈
(𝐽‘𝑡)𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))) ↔ ∃𝑗(𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) |
256 | 254, 255 | sylib 208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑗(𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) |
257 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (𝐽‘𝑡)) |
258 | | eldifn 3733 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) |
259 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑡 ∈ 𝑇) |
260 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝜑) |
261 | 177 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ (1...𝑁)) |
262 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) |
263 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 = 𝑘 → (𝑗 − (1 / 3)) = (𝑘 − (1 / 3))) |
264 | 263 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 = 𝑘 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑘 − (1 / 3)) · 𝐸)) |
265 | 264 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑘 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸))) |
266 | 265 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 𝑘 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)}) |
267 | 266 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) = (𝑘 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)}) |
268 | 69, 267 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐷 = (𝑘 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)}) |
269 | 268 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝐷 = (𝑘 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})) |
270 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = (𝑗 − 1) → (𝑘 − (1 / 3)) = ((𝑗 − 1) − (1 /
3))) |
271 | 270 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = (𝑗 − 1) → ((𝑘 − (1 / 3)) · 𝐸) = (((𝑗 − 1) − (1 / 3)) · 𝐸)) |
272 | 271 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (𝑗 − 1) → ((𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸))) |
273 | 272 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = (𝑗 − 1) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}) |
274 | 273 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑘 = (𝑗 − 1)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}) |
275 | | fzssp1 12384 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0...(𝑁 − 1))
⊆ (0...((𝑁 − 1)
+ 1)) |
276 | 188 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁)) |
277 | 275, 276 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
278 | 277 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
279 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁)) |
280 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 1 ∈ ℤ) |
281 | 197 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℤ) |
282 | 230 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℤ) |
283 | | fzsubel 12377 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((1
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝑗
∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))) |
284 | 280, 281,
282, 280, 283 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))) |
285 | 279, 284 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))) |
286 | 116 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (1 − 1) =
0) |
287 | 286 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → ((1 − 1)...(𝑁 − 1)) = (0...(𝑁 − 1))) |
288 | 285, 287 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...(𝑁 − 1))) |
289 | 278, 288 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...𝑁)) |
290 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑇 ∈ V) |
291 | | rabexg 4812 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V) |
292 | 290, 291 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V) |
293 | 269, 274,
289, 292 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (𝐷‘(𝑗 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}) |
294 | 293 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})) |
295 | 294 | notbid 308 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ ¬ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})) |
296 | 295 | biimpa 501 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}) |
297 | 260, 261,
262, 296 | syl21anc 1325 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}) |
298 | | rabid 3116 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸))) |
299 | 232 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ ℝ) |
300 | | recn 10026 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℝ → 𝑗 ∈
ℂ) |
301 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℝ → 1 ∈
ℂ) |
302 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℝ |
303 | 302, 22, 23 | 3pm3.2i 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) |
304 | | redivcl 10744 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1
∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (1 / 3) ∈
ℝ) |
305 | | recn 10026 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1 / 3)
∈ ℝ → (1 / 3) ∈ ℂ) |
306 | 303, 304,
305 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 / 3)
∈ ℂ |
307 | 306 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℝ → (1 / 3)
∈ ℂ) |
308 | 300, 301,
307 | subsub4d 10423 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) =
(𝑗 − (1 + (1 /
3)))) |
309 | | 3cn 11095 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 3 ∈
ℂ |
310 | 309, 205,
309, 23 | divdiri 10782 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((3 + 1)
/ 3) = ((3 / 3) + (1 / 3)) |
311 | | 3p1e4 11153 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (3 + 1) =
4 |
312 | 311 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((3 + 1)
/ 3) = (4 / 3) |
313 | 309, 23 | dividi 10758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (3 / 3) =
1 |
314 | 313 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((3 / 3)
+ (1 / 3)) = (1 + (1 / 3)) |
315 | 310, 312,
314 | 3eqtr3i 2652 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4 / 3) =
(1 + (1 / 3)) |
316 | 315 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℝ → (4 / 3) =
(1 + (1 / 3))) |
317 | 316 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℝ → (𝑗 − (4 / 3)) = (𝑗 − (1 + (1 /
3)))) |
318 | 308, 317 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) =
(𝑗 − (4 /
3))) |
319 | 318 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℝ → (((𝑗 − 1) − (1 / 3))
· 𝐸) = ((𝑗 − (4 / 3)) · 𝐸)) |
320 | 299, 319 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸)) |
321 | 320 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))) |
322 | 321 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)) ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))) |
323 | 298, 322 | syl5bb 272 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))) |
324 | 297, 323 | mtbid 314 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))) |
325 | | imnan 438 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ 𝑇 → ¬ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)) ↔ ¬ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))) |
326 | 324, 325 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡 ∈ 𝑇 → ¬ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))) |
327 | 259, 326 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)) |
328 | 258, 327 | sylanr2 685 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ¬ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)) |
329 | 232 | adantrr 753 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ ℝ) |
330 | | 4re 11097 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℝ |
331 | 330 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 4 ∈
ℝ) |
332 | 22 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ∈
ℝ) |
333 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ≠
0) |
334 | 331, 332,
333 | redivcld 10853 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (4 / 3) ∈
ℝ) |
335 | 329, 334 | resubcld 10458 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 − (4 / 3)) ∈
ℝ) |
336 | 37 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ) |
337 | | remulcl 10021 |
. . . . . . . . . . . . . . 15
⊢ (((𝑗 − (4 / 3)) ∈ ℝ
∧ 𝐸 ∈ ℝ)
→ ((𝑗 − (4 / 3))
· 𝐸) ∈
ℝ) |
338 | 337 | rexrd 10089 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 − (4 / 3)) ∈ ℝ
∧ 𝐸 ∈ ℝ)
→ ((𝑗 − (4 / 3))
· 𝐸) ∈
ℝ*) |
339 | 335, 336,
338 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) ∈
ℝ*) |
340 | 46 | rexrd 10089 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈
ℝ*) |
341 | 340 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹‘𝑡) ∈
ℝ*) |
342 | | xrltnle 10105 |
. . . . . . . . . . . . 13
⊢ ((((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*
∧ (𝐹‘𝑡) ∈ ℝ*)
→ (((𝑗 − (4 /
3)) · 𝐸) < (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))) |
343 | 339, 341,
342 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))) |
344 | 328, 343 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡)) |
345 | | simpl 473 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝜑 ∧ 𝑡 ∈ 𝑇)) |
346 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1)))) |
347 | 346 | eldifad 3586 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ (𝐷‘𝑗)) |
348 | | simplll 798 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑡 ∈ (𝐷‘𝑗)) → 𝜑) |
349 | 177 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑡 ∈ (𝐷‘𝑗)) → 𝑗 ∈ (1...𝑁)) |
350 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑡 ∈ (𝐷‘𝑗)) → 𝑡 ∈ (𝐷‘𝑗)) |
351 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑗 → (𝑘 − (1 / 3)) = (𝑗 − (1 / 3))) |
352 | 351 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑗 → ((𝑘 − (1 / 3)) · 𝐸) = ((𝑗 − (1 / 3)) · 𝐸)) |
353 | 352 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))) |
354 | 353 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑗 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
355 | 354 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑘 = 𝑗) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
356 | | 0p1e1 11132 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 + 1) =
1 |
357 | 356 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
358 | | 0z 11388 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℤ |
359 | | fzp1ss 12392 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
ℤ → ((0 + 1)...𝑁) ⊆ (0...𝑁)) |
360 | 358, 359 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0 +
1)...𝑁) ⊆ (0...𝑁) |
361 | 357, 360 | eqsstr3i 3636 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑁) ⊆
(0...𝑁) |
362 | 361 | sseli 3599 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (1...𝑁) → 𝑗 ∈ (0...𝑁)) |
363 | 362 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (0...𝑁)) |
364 | | rabexg 4812 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) |
365 | 290, 364 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) |
366 | 269, 355,
363, 365 | fvmptd 6288 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
367 | 366 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷‘𝑗) ↔ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})) |
368 | 367 | biimpa 501 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑡 ∈ (𝐷‘𝑗)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
369 | 348, 349,
350, 368 | syl21anc 1325 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑡 ∈ (𝐷‘𝑗)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
370 | | rabid 3116 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))) |
371 | 369, 370 | sylib 208 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑡 ∈ (𝐷‘𝑗)) → (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))) |
372 | 371 | simprd 479 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑡 ∈ (𝐷‘𝑗)) → (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) |
373 | 345, 257,
347, 372 | syl21anc 1325 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) |
374 | 344, 373 | jca 554 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))) |
375 | 15 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑁 ∈ ℕ) |
376 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ 𝑇) |
377 | 177 | adantrr 753 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (1...𝑁)) |
378 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗 𝑖 ∈ (0...𝑁) |
379 | 103, 378 | nfan 1828 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗(𝜑 ∧ 𝑖 ∈ (0...𝑁)) |
380 | | nfv 1843 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗(𝑋‘𝑖):𝑇⟶ℝ |
381 | 379, 380 | nfim 1825 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ) |
382 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (𝑗 ∈ (0...𝑁) ↔ 𝑖 ∈ (0...𝑁))) |
383 | 382 | anbi2d 740 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁)))) |
384 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (𝑋‘𝑗) = (𝑋‘𝑖)) |
385 | 384 | feq1d 6030 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → ((𝑋‘𝑗):𝑇⟶ℝ ↔ (𝑋‘𝑖):𝑇⟶ℝ)) |
386 | 383, 385 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑋‘𝑗):𝑇⟶ℝ) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ))) |
387 | | stoweidlem34.14 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑋‘𝑗):𝑇⟶ℝ) |
388 | 381, 386,
387 | chvar 2262 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ) |
389 | 388 | ad4ant14 1293 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ) |
390 | | simplll 798 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝜑) |
391 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁)) |
392 | | simpllr 799 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑡 ∈ 𝑇) |
393 | 103, 378,
104 | nf3an 1831 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) |
394 | | nfv 1843 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗((𝑋‘𝑖)‘𝑡) ≤ 1 |
395 | 393, 394 | nfim 1825 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → ((𝑋‘𝑖)‘𝑡) ≤ 1) |
396 | 382 | 3anbi2d 1404 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇))) |
397 | 384 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → ((𝑋‘𝑗)‘𝑡) = ((𝑋‘𝑖)‘𝑡)) |
398 | 397 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (((𝑋‘𝑗)‘𝑡) ≤ 1 ↔ ((𝑋‘𝑖)‘𝑡) ≤ 1)) |
399 | 396, 398 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → ((𝑋‘𝑗)‘𝑡) ≤ 1) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → ((𝑋‘𝑖)‘𝑡) ≤ 1))) |
400 | | stoweidlem34.16 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → ((𝑋‘𝑗)‘𝑡) ≤ 1) |
401 | 395, 399,
400 | chvar 2262 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → ((𝑋‘𝑖)‘𝑡) ≤ 1) |
402 | 390, 391,
392, 401 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑡) ≤ 1) |
403 | | simplll 798 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑) |
404 | | 0zd 11389 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ) |
405 | | elfzel2 12340 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (𝑗...𝑁) → 𝑁 ∈ ℤ) |
406 | 405 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ) |
407 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℤ) |
408 | 407 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ) |
409 | 404, 406,
408 | 3jca 1242 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈
ℤ)) |
410 | | 0red 10041 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℝ) |
411 | | elfzel1 12341 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℤ) |
412 | 411 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℝ) |
413 | 412 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ) |
414 | 407 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℝ) |
415 | 414 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ) |
416 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → 0 ∈ ℝ) |
417 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → 1 ∈ ℝ) |
418 | | 0le1 10551 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤
1 |
419 | 418 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → 0 ≤ 1) |
420 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (1...𝑁) → 1 ≤ 𝑗) |
421 | 177, 420 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → 1 ≤ 𝑗) |
422 | 416, 417,
232, 419, 421 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) → 0 ≤ 𝑗) |
423 | 422 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑗) |
424 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (𝑗...𝑁) → 𝑗 ≤ 𝑖) |
425 | 424 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ≤ 𝑖) |
426 | 410, 413,
415, 423, 425 | letrd 10194 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑖) |
427 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (𝑗...𝑁) → 𝑖 ≤ 𝑁) |
428 | 427 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ≤ 𝑁) |
429 | 426, 428 | jca 554 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)) |
430 | | elfz2 12333 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤
𝑖 ∧ 𝑖 ≤ 𝑁))) |
431 | 409, 429,
430 | sylanbrc 698 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁)) |
432 | 431 | adantlrr 757 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁)) |
433 | | simpll 790 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑 ∧ 𝑡 ∈ 𝑇)) |
434 | | simplrl 800 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽‘𝑡)) |
435 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1)))) |
436 | 435 | eldifad 3586 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷‘𝑗)) |
437 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁)) |
438 | | simpl1 1064 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑 ∧ 𝑡 ∈ 𝑇)) |
439 | 438 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ 𝑇) |
440 | 438, 46 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹‘𝑡) ∈ ℝ) |
441 | 412 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ) |
442 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈
ℝ) |
443 | 441, 442 | resubcld 10458 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ∈
ℝ) |
444 | | simpl1l 1112 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑) |
445 | 444, 37 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ) |
446 | 443, 445 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ) |
447 | 414 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ) |
448 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈
ℝ) |
449 | 447, 448 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈
ℝ) |
450 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ) |
451 | 449, 450 | remulcld 10070 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ) |
452 | 444, 451 | sylancom 701 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ) |
453 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷‘𝑗)) |
454 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽‘𝑡)) |
455 | 438, 454,
177 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (1...𝑁)) |
456 | 444, 455,
366 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
457 | 453, 456 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
458 | 457, 370 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))) |
459 | 458 | simprd 479 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) |
460 | 414 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ) |
461 | 424 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ≤ 𝑖) |
462 | 441, 460,
442, 461 | lesub1dd 10643 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3))) |
463 | 444, 449 | sylancom 701 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈
ℝ) |
464 | 36 | rpregt0d 11878 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
465 | 444, 464 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
466 | | lemul1 10875 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑗 − (1 / 3)) ∈ ℝ
∧ (𝑖 − (1 / 3))
∈ ℝ ∧ (𝐸
∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸))) |
467 | 443, 463,
465, 466 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸))) |
468 | 462, 467 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)) |
469 | 440, 446,
452, 459, 468 | letrd 10194 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)) |
470 | | rabid 3116 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸))) |
471 | 439, 469,
470 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)}) |
472 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁)) |
473 | | 0zd 11389 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ) |
474 | 405 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ) |
475 | 407 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ) |
476 | 473, 474,
475 | 3jca 1242 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈
ℤ)) |
477 | 429 | 3impa 1259 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)) |
478 | 476, 477,
430 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁)) |
479 | 438, 454,
472, 478 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁)) |
480 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁)) |
481 | | rabexg 4812 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V) |
482 | 62, 481 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V) |
483 | 482 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V) |
484 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑖 → (𝑗 − (1 / 3)) = (𝑖 − (1 / 3))) |
485 | 484 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑖 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑖 − (1 / 3)) · 𝐸)) |
486 | 485 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑖 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸))) |
487 | 486 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑖 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)}) |
488 | 487, 69 | fvmptg 6280 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝑖) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)}) |
489 | 480, 483,
488 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐷‘𝑖) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)}) |
490 | 444, 479,
489 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷‘𝑖) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)}) |
491 | 471, 490 | eleqtrrd 2704 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ (𝐷‘𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷‘𝑖)) |
492 | 433, 434,
436, 437, 491 | syl31anc 1329 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷‘𝑖)) |
493 | 103, 378,
223 | nf3an 1831 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑖)) |
494 | | nfv 1843 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁) |
495 | 493, 494 | nfim 1825 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑖)) → ((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁)) |
496 | 382, 225 | 3anbi23d 1402 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑗)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑖)))) |
497 | 397 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (((𝑋‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁))) |
498 | 496, 497 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑗)) → ((𝑋‘𝑗)‘𝑡) < (𝐸 / 𝑁)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑖)) → ((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁)))) |
499 | | stoweidlem34.17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑗)) → ((𝑋‘𝑗)‘𝑡) < (𝐸 / 𝑁)) |
500 | 495, 498,
499 | chvar 2262 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷‘𝑖)) → ((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁)) |
501 | 403, 432,
492, 500 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁)) |
502 | 36 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈
ℝ+) |
503 | | stoweidlem34.13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 < (1 / 3)) |
504 | 503 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 < (1 / 3)) |
505 | 375, 376,
377, 389, 402, 501, 502, 504 | stoweidlem11 40228 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸)) |
506 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑗 → (𝑙 ∈ (𝐽‘𝑡) ↔ 𝑗 ∈ (𝐽‘𝑡))) |
507 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑗 → (𝐷‘𝑙) = (𝐷‘𝑗)) |
508 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑗 → (𝑙 − 1) = (𝑗 − 1)) |
509 | 508 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑗 → (𝐷‘(𝑙 − 1)) = (𝐷‘(𝑗 − 1))) |
510 | 507, 509 | difeq12d 3729 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑗 → ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))) = ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1)))) |
511 | 510 | eleq2d 2687 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑗 → (𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) |
512 | 506, 511 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑗 → ((𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1)))))) |
513 | 512 | anbi2d 740 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑗 → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))))) |
514 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑗 → (𝑙 − (4 / 3)) = (𝑗 − (4 / 3))) |
515 | 514 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑗 → ((𝑙 − (4 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸)) |
516 | 515 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑗 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) ↔ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) |
517 | 513, 516 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑗 → ((((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)) ↔ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)))) |
518 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 𝑡 → (𝑠 ∈ 𝑇 ↔ 𝑡 ∈ 𝑇)) |
519 | 518 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑡 → ((𝜑 ∧ 𝑠 ∈ 𝑇) ↔ (𝜑 ∧ 𝑡 ∈ 𝑇))) |
520 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = 𝑡 → (𝐽‘𝑠) = (𝐽‘𝑡)) |
521 | 520 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 𝑡 → (𝑙 ∈ (𝐽‘𝑠) ↔ 𝑙 ∈ (𝐽‘𝑡))) |
522 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 𝑡 → (𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) |
523 | 521, 522 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑡 → ((𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1)))))) |
524 | 519, 523 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 𝑡 → (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))))) |
525 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑡 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑠) = ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)) |
526 | 525 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 𝑡 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑠) ↔ ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) |
527 | 524, 526 | imbi12d 334 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑡 → ((((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑠)) ↔ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)))) |
528 | | stoweidlem34.1 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡𝐹 |
529 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗 𝑠 ∈ 𝑇 |
530 | 103, 529 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗(𝜑 ∧ 𝑠 ∈ 𝑇) |
531 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑗𝑠 |
532 | 92, 531 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑗(𝐽‘𝑠) |
533 | 532 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗 𝑙 ∈ (𝐽‘𝑠) |
534 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑗𝑙 |
535 | 77, 534 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑗(𝐷‘𝑙) |
536 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑗(𝑙 − 1) |
537 | 77, 536 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑗(𝐷‘(𝑙 − 1)) |
538 | 535, 537 | nfdif 3731 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑗((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))) |
539 | 538 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))) |
540 | 533, 539 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗(𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1)))) |
541 | 530, 540 | nfan 1828 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) |
542 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡 𝑠 ∈ 𝑇 |
543 | 1, 542 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡(𝜑 ∧ 𝑠 ∈ 𝑇) |
544 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)}) |
545 | 5, 544 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑡𝐽 |
546 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑡𝑠 |
547 | 545, 546 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑡(𝐽‘𝑠) |
548 | 547 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡 𝑙 ∈ (𝐽‘𝑠) |
549 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡𝑙 |
550 | 164, 549 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑡(𝐷‘𝑙) |
551 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡(𝑙 − 1) |
552 | 164, 551 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑡(𝐷‘(𝑙 − 1)) |
553 | 550, 552 | nfdif 3731 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑡((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))) |
554 | 553 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))) |
555 | 548, 554 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡(𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1)))) |
556 | 543, 555 | nfan 1828 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) |
557 | | stoweidlem34.5 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
558 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑁 ∈ ℕ) |
559 | 62 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑇 ∈ V) |
560 | 3 | rabex 4813 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷‘𝑗)} ∈ V |
561 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
Ⅎ𝑡𝑗 |
562 | 164, 561 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑡(𝐷‘𝑗) |
563 | 562 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡 𝑠 ∈ (𝐷‘𝑗) |
564 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡(1...𝑁) |
565 | 563, 564 | nfrab 3123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑡{𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷‘𝑗)} |
566 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑠 → (𝑡 ∈ (𝐷‘𝑗) ↔ 𝑠 ∈ (𝐷‘𝑗))) |
567 | 566 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑠 → {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷‘𝑗)} = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷‘𝑗)}) |
568 | 546, 565,
567, 5 | fvmptf 6301 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ 𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷‘𝑗)} ∈ V) → (𝐽‘𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷‘𝑗)}) |
569 | 560, 568 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 ∈ 𝑇 → (𝐽‘𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷‘𝑗)}) |
570 | 569 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 ∈ 𝑇 → (𝑙 ∈ (𝐽‘𝑠) ↔ 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷‘𝑗)})) |
571 | 570 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑠 ∈ 𝑇 ∧ 𝑙 ∈ (𝐽‘𝑠)) → 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷‘𝑗)}) |
572 | 535 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑗 𝑠 ∈ (𝐷‘𝑙) |
573 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑙 → (𝐷‘𝑗) = (𝐷‘𝑙)) |
574 | 573 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑙 → (𝑠 ∈ (𝐷‘𝑗) ↔ 𝑠 ∈ (𝐷‘𝑙))) |
575 | 534, 75, 572, 574 | elrabf 3360 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷‘𝑗)} ↔ (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷‘𝑙))) |
576 | 571, 575 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑠 ∈ 𝑇 ∧ 𝑙 ∈ (𝐽‘𝑠)) → (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷‘𝑙))) |
577 | 576 | simpld 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ 𝑇 ∧ 𝑙 ∈ (𝐽‘𝑠)) → 𝑙 ∈ (1...𝑁)) |
578 | 577 | ad2ant2lr 784 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑙 ∈ (1...𝑁)) |
579 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1)))) |
580 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐹:𝑇⟶ℝ) |
581 | 36 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 ∈
ℝ+) |
582 | 503 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 < (1 / 3)) |
583 | 388 | ad4ant14 1293 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ) |
584 | | simp1ll 1124 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 𝜑) |
585 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑗0 ≤
((𝑋‘𝑖)‘𝑡) |
586 | 393, 585 | nfim 1825 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) |
587 | 397 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑖 → (0 ≤ ((𝑋‘𝑗)‘𝑡) ↔ 0 ≤ ((𝑋‘𝑖)‘𝑡))) |
588 | 396, 587 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑗)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡)))) |
589 | | stoweidlem34.15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑗)‘𝑡)) |
590 | 586, 588,
589 | chvar 2262 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) |
591 | 584, 590 | syld3an1 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) |
592 | | simp1ll 1124 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → 𝜑) |
593 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
594 | 557, 593 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑗𝐵 |
595 | 594, 221 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑗(𝐵‘𝑖) |
596 | 595 | nfcri 2758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑗 𝑡 ∈ (𝐵‘𝑖) |
597 | 103, 378,
596 | nf3an 1831 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑗(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) |
598 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑗(1 −
(𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡) |
599 | 597, 598 | nfim 1825 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) |
600 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑖 → (𝐵‘𝑗) = (𝐵‘𝑖)) |
601 | 600 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑖 → (𝑡 ∈ (𝐵‘𝑗) ↔ 𝑡 ∈ (𝐵‘𝑖))) |
602 | 382, 601 | 3anbi23d 1402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑖 → ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑗)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)))) |
603 | 397 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑖 → ((1 − (𝐸 / 𝑁)) < ((𝑋‘𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡))) |
604 | 602, 603 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑗)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)))) |
605 | | stoweidlem34.18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑗)‘𝑡)) |
606 | 599, 604,
605 | chvar 2262 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) |
607 | 592, 606 | syld3an1 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) |
608 | 528, 541,
556, 69, 557, 558, 559, 578, 579, 580, 581, 582, 583, 591, 607 | stoweidlem26 40243 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑠) ∧ 𝑠 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑠)) |
609 | 527, 608 | vtoclg 3266 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ 𝑇 → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) |
610 | 609 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) |
611 | 610 | pm2.43i 52 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑙 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)) |
612 | 517, 611 | vtoclg 3266 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (𝐽‘𝑡) → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) |
613 | 612 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) |
614 | 613 | pm2.43i 52 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)) |
615 | 505, 614 | jca 554 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) |
616 | 257, 374,
615 | 3jca 1242 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ (𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 ∈ (𝐽‘𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)))) |
617 | 616 | ex 450 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1)))) → (𝑗 ∈ (𝐽‘𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))) |
618 | 105, 617 | eximd 2085 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (∃𝑗(𝑗 ∈ (𝐽‘𝑡) ∧ 𝑡 ∈ ((𝐷‘𝑗) ∖ (𝐷‘(𝑗 − 1)))) → ∃𝑗(𝑗 ∈ (𝐽‘𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))) |
619 | 256, 618 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑗(𝑗 ∈ (𝐽‘𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)))) |
620 | | 3anass 1042 |
. . . . . . 7
⊢ ((𝑗 ∈ (𝐽‘𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) ↔ (𝑗 ∈ (𝐽‘𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))) |
621 | 620 | exbii 1774 |
. . . . . 6
⊢
(∃𝑗(𝑗 ∈ (𝐽‘𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽‘𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))) |
622 | 619, 621 | sylib 208 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑗(𝑗 ∈ (𝐽‘𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))) |
623 | | df-rex 2918 |
. . . . 5
⊢
(∃𝑗 ∈
(𝐽‘𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽‘𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))) |
624 | 622, 623 | sylibr 224 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑗 ∈ (𝐽‘𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)))) |
625 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑗ℝ |
626 | 94, 625 | ssrexf 3665 |
. . . 4
⊢ ((𝐽‘𝑡) ⊆ ℝ → (∃𝑗 ∈ (𝐽‘𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))) |
627 | 14, 624, 626 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)))) |
628 | 627 | ex 450 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝑇 → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡))))) |
629 | 1, 628 | ralrimi 2957 |
1
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)))) |