Step | Hyp | Ref
| Expression |
1 | | iseqf1o.1 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
2 | | iseqf1o.2 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
3 | | iseqf1o.3 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
4 | | iseqf1o.4 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
5 | | iseqf1o.6 |
. . . . . 6
⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
6 | | iseqf1o.7 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) |
7 | | iseqf1olemstep.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) |
8 | | iseqf1olemstep.j |
. . . . . 6
⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
9 | | iseqf1olemstep.const |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥) |
10 | | iseqf1olemnk |
. . . . . 6
⊢ (𝜑 → 𝐾 ≠ (◡𝐽‘𝐾)) |
11 | | iseqf1olemqres.q |
. . . . . 6
⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢))) |
12 | | iseqf1olemqsumk.p |
. . . . . 6
⊢ 𝑃 = (𝑥 ∈ (ℤ≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀))) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | seq3f1olemqsumkj 10443 |
. . . . 5
⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾))) |
14 | 13 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾))) |
15 | | f1ocnv 5453 |
. . . . . . . . . . . 12
⊢ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
16 | 8, 15 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
17 | | f1of 5440 |
. . . . . . . . . . 11
⊢ (◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) |
18 | 16, 17 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → ◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) |
19 | 18, 7 | ffvelrnd 5630 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐽‘𝐾) ∈ (𝑀...𝑁)) |
20 | | elfzelz 9970 |
. . . . . . . . 9
⊢ ((◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (◡𝐽‘𝐾) ∈ ℤ) |
21 | 19, 20 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (◡𝐽‘𝐾) ∈ ℤ) |
22 | 21 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → (◡𝐽‘𝐾) ∈ ℤ) |
23 | 22 | peano2zd 9326 |
. . . . . 6
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → ((◡𝐽‘𝐾) + 1) ∈ ℤ) |
24 | | elfzel2 9968 |
. . . . . . . 8
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ) |
25 | 7, 24 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℤ) |
26 | 25 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ ℤ) |
27 | | simpr 109 |
. . . . . . 7
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → (◡𝐽‘𝐾) < 𝑁) |
28 | | zltp1le 9255 |
. . . . . . . 8
⊢ (((◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((◡𝐽‘𝐾) < 𝑁 ↔ ((◡𝐽‘𝐾) + 1) ≤ 𝑁)) |
29 | 22, 26, 28 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → ((◡𝐽‘𝐾) < 𝑁 ↔ ((◡𝐽‘𝐾) + 1) ≤ 𝑁)) |
30 | 27, 29 | mpbid 146 |
. . . . . 6
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → ((◡𝐽‘𝐾) + 1) ≤ 𝑁) |
31 | | eluz2 9482 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘((◡𝐽‘𝐾) + 1)) ↔ (((◡𝐽‘𝐾) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((◡𝐽‘𝐾) + 1) ≤ 𝑁)) |
32 | 23, 26, 30, 31 | syl3anbrc 1176 |
. . . . 5
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈
(ℤ≥‘((◡𝐽‘𝐾) + 1))) |
33 | 7 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝐾 ∈ (𝑀...𝑁)) |
34 | 8 | ad2antrr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
35 | | elfzel1 9969 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) |
36 | 7, 35 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
37 | 36 | ad2antrr 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℤ) |
38 | 33, 24 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑁 ∈ ℤ) |
39 | | elfzelz 9970 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ∈ ℤ) |
40 | 39 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℤ) |
41 | 37, 38, 40 | 3jca 1172 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ)) |
42 | 36 | zred 9323 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℝ) |
43 | 42 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℝ) |
44 | 21 | zred 9323 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝐽‘𝐾) ∈ ℝ) |
45 | | peano2re 8044 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐽‘𝐾) ∈ ℝ → ((◡𝐽‘𝐾) + 1) ∈ ℝ) |
46 | 44, 45 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((◡𝐽‘𝐾) + 1) ∈ ℝ) |
47 | 46 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → ((◡𝐽‘𝐾) + 1) ∈ ℝ) |
48 | 40 | zred 9323 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℝ) |
49 | | elfzelz 9970 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ) |
50 | 7, 49 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ ℤ) |
51 | 50 | zred 9323 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ ℝ) |
52 | | elfzle1 9972 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾) |
53 | 7, 52 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ≤ 𝐾) |
54 | 4, 7, 8, 9 | iseqf1olemkle 10429 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ≤ (◡𝐽‘𝐾)) |
55 | 42, 51, 44, 53, 54 | letrd 8032 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ≤ (◡𝐽‘𝐾)) |
56 | 44 | lep1d 8836 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝐽‘𝐾) ≤ ((◡𝐽‘𝐾) + 1)) |
57 | 42, 44, 46, 55, 56 | letrd 8032 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ≤ ((◡𝐽‘𝐾) + 1)) |
58 | 57 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ ((◡𝐽‘𝐾) + 1)) |
59 | | elfzle1 9972 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁) → ((◡𝐽‘𝐾) + 1) ≤ 𝑣) |
60 | 59 | adantl 275 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → ((◡𝐽‘𝐾) + 1) ≤ 𝑣) |
61 | 43, 47, 48, 58, 60 | letrd 8032 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ 𝑣) |
62 | | elfzle2 9973 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ≤ 𝑁) |
63 | 62 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ≤ 𝑁) |
64 | 61, 63 | jca 304 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)) |
65 | | elfz2 9961 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))) |
66 | 41, 64, 65 | sylanbrc 415 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ (𝑀...𝑁)) |
67 | 33, 34, 66, 11 | iseqf1olemqval 10432 |
. . . . . . . 8
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → (𝑄‘𝑣) = if(𝑣 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑣 = 𝐾, 𝐾, (𝐽‘(𝑣 − 1))), (𝐽‘𝑣))) |
68 | 44 | ad3antrrr 489 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(◡𝐽‘𝐾))) → (◡𝐽‘𝐾) ∈ ℝ) |
69 | 68, 45 | syl 14 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(◡𝐽‘𝐾))) → ((◡𝐽‘𝐾) + 1) ∈ ℝ) |
70 | 48 | adantr 274 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(◡𝐽‘𝐾))) → 𝑣 ∈ ℝ) |
71 | 68 | ltp1d 8835 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(◡𝐽‘𝐾))) → (◡𝐽‘𝐾) < ((◡𝐽‘𝐾) + 1)) |
72 | 60 | adantr 274 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(◡𝐽‘𝐾))) → ((◡𝐽‘𝐾) + 1) ≤ 𝑣) |
73 | 68, 69, 70, 71, 72 | ltletrd 8331 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(◡𝐽‘𝐾))) → (◡𝐽‘𝐾) < 𝑣) |
74 | | elfzle2 9973 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ (𝐾...(◡𝐽‘𝐾)) → 𝑣 ≤ (◡𝐽‘𝐾)) |
75 | 74 | adantl 275 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(◡𝐽‘𝐾))) → 𝑣 ≤ (◡𝐽‘𝐾)) |
76 | 70, 68, 75 | lensymd 8030 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(◡𝐽‘𝐾))) → ¬ (◡𝐽‘𝐾) < 𝑣) |
77 | 73, 76 | pm2.65da 656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → ¬ 𝑣 ∈ (𝐾...(◡𝐽‘𝐾))) |
78 | 77 | iffalsed 3535 |
. . . . . . . 8
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → if(𝑣 ∈ (𝐾...(◡𝐽‘𝐾)), if(𝑣 = 𝐾, 𝐾, (𝐽‘(𝑣 − 1))), (𝐽‘𝑣)) = (𝐽‘𝑣)) |
79 | 67, 78 | eqtrd 2203 |
. . . . . . 7
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → (𝑄‘𝑣) = (𝐽‘𝑣)) |
80 | 79 | fveq2d 5498 |
. . . . . 6
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → (𝐺‘(𝑄‘𝑣)) = (𝐺‘(𝐽‘𝑣))) |
81 | 33, 34, 11 | iseqf1olemqf1o 10438 |
. . . . . . 7
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → 𝑄:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
82 | 6 | ralrimiva 2543 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆) |
83 | 82 | ad2antrr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆) |
84 | 83 | r19.21bi 2558 |
. . . . . . 7
⊢ ((((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) |
85 | 33, 81, 66, 84, 12 | iseqf1olemfvp 10442 |
. . . . . 6
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝑄‘𝑣))) |
86 | 33, 34, 66, 84, 12 | iseqf1olemfvp 10442 |
. . . . . 6
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝐽‘𝑣))) |
87 | 80, 85, 86 | 3eqtr4rd 2214 |
. . . . 5
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (⦋𝑄 / 𝑓⦌𝑃‘𝑣)) |
88 | 36 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℤ) |
89 | | eluzelz 9485 |
. . . . . . . 8
⊢ (𝑥 ∈
(ℤ≥‘((◡𝐽‘𝐾) + 1)) → 𝑥 ∈ ℤ) |
90 | 89 | adantl 275 |
. . . . . . 7
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℤ) |
91 | 42 | ad2antrr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℝ) |
92 | 46 | ad2antrr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → ((◡𝐽‘𝐾) + 1) ∈ ℝ) |
93 | 90 | zred 9323 |
. . . . . . . 8
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℝ) |
94 | 57 | ad2antrr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → 𝑀 ≤ ((◡𝐽‘𝐾) + 1)) |
95 | | eluzle 9488 |
. . . . . . . . 9
⊢ (𝑥 ∈
(ℤ≥‘((◡𝐽‘𝐾) + 1)) → ((◡𝐽‘𝐾) + 1) ≤ 𝑥) |
96 | 95 | adantl 275 |
. . . . . . . 8
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → ((◡𝐽‘𝐾) + 1) ≤ 𝑥) |
97 | 91, 92, 93, 94, 96 | letrd 8032 |
. . . . . . 7
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → 𝑀 ≤ 𝑥) |
98 | | eluz2 9482 |
. . . . . . 7
⊢ (𝑥 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)) |
99 | 88, 90, 97, 98 | syl3anbrc 1176 |
. . . . . 6
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → 𝑥 ∈ (ℤ≥‘𝑀)) |
100 | 7 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → 𝐾 ∈ (𝑀...𝑁)) |
101 | 8 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
102 | 6 | adantlr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆) |
103 | 100, 101,
11, 102, 12 | iseqf1olemjpcl 10440 |
. . . . . 6
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
104 | 99, 103 | syldan 280 |
. . . . 5
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
105 | 7, 8, 11, 6, 12 | iseqf1olemqpcl 10441 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
106 | 105 | adantlr 474 |
. . . . . 6
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
107 | 99, 106 | syldan 280 |
. . . . 5
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘((◡𝐽‘𝐾) + 1))) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
108 | 1 | adantlr 474 |
. . . . 5
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
109 | 32, 87, 104, 107, 108 | seq3fveq 10416 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → (seq((◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq((◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)) |
110 | 14, 109 | oveq12d 5869 |
. . 3
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) + (seq((◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) + (seq((◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))) |
111 | 3 | adantlr 474 |
. . . 4
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
112 | | eluz2 9482 |
. . . . . 6
⊢ ((◡𝐽‘𝐾) ∈ (ℤ≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ (◡𝐽‘𝐾) ∈ ℤ ∧ 𝐾 ≤ (◡𝐽‘𝐾))) |
113 | 50, 21, 54, 112 | syl3anbrc 1176 |
. . . . 5
⊢ (𝜑 → (◡𝐽‘𝐾) ∈ (ℤ≥‘𝐾)) |
114 | 113 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → (◡𝐽‘𝐾) ∈ (ℤ≥‘𝐾)) |
115 | | simpr 109 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → 𝑥 ∈ (ℤ≥‘𝐾)) |
116 | 7 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁)) |
117 | | elfzuz 9966 |
. . . . . . . 8
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
118 | 116, 117 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (ℤ≥‘𝑀)) |
119 | | uztrn 9492 |
. . . . . . 7
⊢ ((𝑥 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
120 | 115, 118,
119 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
121 | 7, 8, 11, 6, 12 | iseqf1olemjpcl 10440 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
122 | 120, 121 | syldan 280 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
123 | 122 | adantlr 474 |
. . . 4
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
124 | 108, 111,
32, 114, 123 | seq3split 10424 |
. . 3
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) + (seq((◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁))) |
125 | 120, 105 | syldan 280 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
126 | 125 | adantlr 474 |
. . . 4
⊢ (((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆) |
127 | 108, 111,
32, 114, 126 | seq3split 10424 |
. . 3
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) + (seq((◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))) |
128 | 110, 124,
127 | 3eqtr4d 2213 |
. 2
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)) |
129 | 13 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾))) |
130 | | simpr 109 |
. . . 4
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) = 𝑁) → (◡𝐽‘𝐾) = 𝑁) |
131 | 130 | fveq2d 5498 |
. . 3
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)) |
132 | 130 | fveq2d 5498 |
. . 3
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)) |
133 | 129, 131,
132 | 3eqtr3d 2211 |
. 2
⊢ ((𝜑 ∧ (◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)) |
134 | | elfzle2 9973 |
. . . 4
⊢ ((◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (◡𝐽‘𝐾) ≤ 𝑁) |
135 | 19, 134 | syl 14 |
. . 3
⊢ (𝜑 → (◡𝐽‘𝐾) ≤ 𝑁) |
136 | | zleloe 9248 |
. . . 4
⊢ (((◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((◡𝐽‘𝐾) ≤ 𝑁 ↔ ((◡𝐽‘𝐾) < 𝑁 ∨ (◡𝐽‘𝐾) = 𝑁))) |
137 | 21, 25, 136 | syl2anc 409 |
. . 3
⊢ (𝜑 → ((◡𝐽‘𝐾) ≤ 𝑁 ↔ ((◡𝐽‘𝐾) < 𝑁 ∨ (◡𝐽‘𝐾) = 𝑁))) |
138 | 135, 137 | mpbid 146 |
. 2
⊢ (𝜑 → ((◡𝐽‘𝐾) < 𝑁 ∨ (◡𝐽‘𝐾) = 𝑁)) |
139 | 128, 133,
138 | mpjaodan 793 |
1
⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)) |