Step | Hyp | Ref
| Expression |
1 | | poimirlem2.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) |
2 | | dff1o3 6056 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈)) |
3 | 2 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈) |
4 | 1, 3 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun ◡𝑈) |
5 | | imadif 5887 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)}))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)}))) |
7 | | poimirlem2.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑉 ∈ (1...(𝑁 − 1))) |
8 | | fzp1elp1 12264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈ (1...(𝑁 − 1)) → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1))) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1))) |
10 | | poimir.0 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑁 ∈ ℕ) |
11 | 10 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ ℂ) |
12 | | npcan1 10334 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
14 | 13 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
15 | 9, 14 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑉 + 1) ∈ (1...𝑁)) |
16 | | fzsplit 12238 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) |
18 | 17 | difeq1d 3689 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)})) |
19 | | difundir 3839 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...(𝑉 + 1))
∪ (((𝑉 + 1) +
1)...𝑁)) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)})) |
20 | | elfzuz 12209 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈
(ℤ≥‘1)) |
21 | 7, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑉 ∈
(ℤ≥‘1)) |
22 | | fzsuc 12258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 ∈
(ℤ≥‘1) → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)})) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)})) |
24 | 23 | difeq1d 3689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)})) |
25 | | difun2 4000 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1...𝑉) ∪
{(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∖ {(𝑉 + 1)}) |
26 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈ ℤ) |
27 | 7, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑉 ∈ ℤ) |
28 | 27 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑉 ∈ ℝ) |
29 | 28 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑉 < (𝑉 + 1)) |
30 | 27 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑉 + 1) ∈ ℤ) |
31 | 30 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑉 + 1) ∈ ℝ) |
32 | 28, 31 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑉 < (𝑉 + 1) ↔ ¬ (𝑉 + 1) ≤ 𝑉)) |
33 | 29, 32 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ (𝑉 + 1) ≤ 𝑉) |
34 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 + 1) ∈ (1...𝑉) → (𝑉 + 1) ≤ 𝑉) |
35 | 33, 34 | nsyl 134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ¬ (𝑉 + 1) ∈ (1...𝑉)) |
36 | | difsn 4269 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝑉 + 1) ∈ (1...𝑉) → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉)) |
38 | 25, 37 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = (1...𝑉)) |
39 | 24, 38 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (1...𝑉)) |
40 | 31 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑉 + 1) < ((𝑉 + 1) + 1)) |
41 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 + 1) ∈ ℝ →
((𝑉 + 1) + 1) ∈
ℝ) |
42 | 31, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑉 + 1) + 1) ∈ ℝ) |
43 | 31, 42 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑉 + 1) < ((𝑉 + 1) + 1) ↔ ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1))) |
44 | 40, 43 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1)) |
45 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((𝑉 + 1) + 1) ≤ (𝑉 + 1)) |
46 | 44, 45 | nsyl 134 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁)) |
47 | | difsn 4269 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁)) |
49 | 39, 48 | uneq12d 3730 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)})) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) |
50 | 19, 49 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) |
51 | 18, 50 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) |
52 | 51 | imaeq2d 5385 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))) |
53 | 6, 52 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))) |
54 | | imaundi 5464 |
. . . . . . . . . . . . 13
⊢ (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
55 | 53, 54 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
56 | 55 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ 𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))) |
57 | | eldif 3550 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}))) |
58 | | elun 3715 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
59 | 56, 57, 58 | 3bitr3g 301 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))) |
60 | 59 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))) |
61 | | imassrn 5396 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ (1...𝑉)) ⊆ ran 𝑈 |
62 | | f1of 6050 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁)) |
63 | 1, 62 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁)) |
64 | | frn 5966 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁)) |
66 | 61, 65 | syl5ss 3579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (1...𝑁)) |
67 | 66 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (1...𝑁)) |
68 | | poimirlem2.2 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ) |
69 | | ffn 5958 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇:(1...𝑁)⟶ℤ → 𝑇 Fn (1...𝑁)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 Fn (1...𝑁)) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑇 Fn (1...𝑁)) |
72 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
V |
73 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
V → ((𝑈 “
(1...𝑉)) × {1}) Fn
(𝑈 “ (1...𝑉))) |
74 | 72, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) |
75 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
V |
76 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
V → ((𝑈 “
((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) |
77 | 75, 76 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) |
78 | 74, 77 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) |
79 | | imain 5888 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
80 | 4, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
81 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 < (𝑉 + 1) → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅) |
82 | 29, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅) |
83 | 82 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = (𝑈 “ ∅)) |
84 | | ima0 5400 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑈 “ ∅) =
∅ |
85 | 83, 84 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ∅) |
86 | 80, 85 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅) |
87 | | fnun 5911 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑈 “
(1...𝑉)) × {1}) Fn
(𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
88 | 78, 86, 87 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
89 | | imaundi 5464 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) |
90 | 10 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℤ) |
91 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
93 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
95 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
97 | 13, 96 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
98 | | fzss2 12252 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
100 | 99, 7 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑉 ∈ (1...𝑁)) |
101 | | fzsplit 12238 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) |
103 | 102 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))) |
104 | | f1ofo 6057 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁)) |
105 | 1, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑈:(1...𝑁)–onto→(1...𝑁)) |
106 | | foima 6033 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
108 | 103, 107 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = (1...𝑁)) |
109 | 89, 108 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) = (1...𝑁)) |
110 | 109 | fneq2d 5896 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
111 | 88, 110 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
112 | 111 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
113 | | fzfid 12634 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (1...𝑁) ∈ Fin) |
114 | | inidm 3784 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
115 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
116 | | fvun1 6179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛)) |
117 | 74, 77, 116 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛)) |
118 | 86, 117 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛)) |
119 | 72 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (𝑈 “ (1...𝑉)) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1) |
120 | 119 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1) |
121 | 118, 120 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1) |
123 | 71, 112, 113, 113, 114, 115, 122 | ofval 6804 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
124 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
V → ((𝑈 “
(1...(𝑉 + 1))) × {1})
Fn (𝑈 “ (1...(𝑉 + 1)))) |
125 | 72, 124 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) |
126 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
V → ((𝑈 “
(((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
127 | 75, 126 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) |
128 | 125, 127 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
129 | | imain 5888 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
130 | 4, 129 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
131 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 + 1) < ((𝑉 + 1) + 1) → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅) |
132 | 40, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅) |
133 | 132 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = (𝑈 “ ∅)) |
134 | 133, 84 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ∅) |
135 | 130, 134 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅) |
136 | | fnun 5911 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑈 “
(1...(𝑉 + 1))) × {1})
Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
137 | 128, 135,
136 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
138 | | imaundi 5464 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
139 | 17 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))) |
140 | 139, 107 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁)) |
141 | 138, 140 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁)) |
142 | 141 | fneq2d 5896 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
143 | 137, 142 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
144 | 143 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
145 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ∈ ℤ → 𝑉 ∈
(ℤ≥‘𝑉)) |
146 | 27, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘𝑉)) |
147 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑉 ∈
(ℤ≥‘𝑉) → (𝑉 + 1) ∈
(ℤ≥‘𝑉)) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑉 + 1) ∈
(ℤ≥‘𝑉)) |
149 | | fzss2 12252 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 + 1) ∈
(ℤ≥‘𝑉) → (1...𝑉) ⊆ (1...(𝑉 + 1))) |
150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...𝑉) ⊆ (1...(𝑉 + 1))) |
151 | | imass2 5420 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1...𝑉) ⊆
(1...(𝑉 + 1)) → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1)))) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1)))) |
153 | 152 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) |
154 | | fvun1 6179 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ∧ (((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛)) |
155 | 125, 127,
154 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛)) |
156 | 135, 155 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛)) |
157 | 72 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1) |
158 | 157 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1) |
159 | 156, 158 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
160 | 153, 159 | syldan 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
161 | 160 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
162 | 71, 144, 113, 113, 114, 115, 161 | ofval 6804 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
163 | 123, 162 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
164 | 67, 163 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
165 | | imassrn 5396 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ ran 𝑈 |
166 | 165, 65 | syl5ss 3579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (1...𝑁)) |
167 | 166 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (1...𝑁)) |
168 | 70 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑇 Fn (1...𝑁)) |
169 | 111 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
170 | | fzfid 12634 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (1...𝑁) ∈ Fin) |
171 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
172 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 + 1) ∈ ℤ →
(𝑉 + 1) ∈
(ℤ≥‘(𝑉 + 1))) |
173 | 30, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑉 + 1) ∈
(ℤ≥‘(𝑉 + 1))) |
174 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 + 1) ∈
(ℤ≥‘(𝑉 + 1)) → ((𝑉 + 1) + 1) ∈
(ℤ≥‘(𝑉 + 1))) |
175 | 173, 174 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑉 + 1) + 1) ∈
(ℤ≥‘(𝑉 + 1))) |
176 | | fzss1 12251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 + 1) + 1) ∈
(ℤ≥‘(𝑉 + 1)) → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁)) |
177 | 175, 176 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁)) |
178 | | imass2 5420 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁) → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁))) |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁))) |
180 | 179 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) |
181 | | fvun2 6180 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛)) |
182 | 74, 77, 181 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛)) |
183 | 86, 182 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛)) |
184 | 75 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0) |
185 | 184 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0) |
186 | 183, 185 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0) |
187 | 180, 186 | syldan 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0) |
188 | 187 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0) |
189 | 168, 169,
170, 170, 114, 171, 188 | ofval 6804 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
190 | 143 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
191 | | fvun2 6180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ∧ (((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛)) |
192 | 125, 127,
191 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛)) |
193 | 135, 192 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛)) |
194 | 75 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0) |
195 | 194 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0) |
196 | 193, 195 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0) |
197 | 196 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0) |
198 | 168, 190,
170, 170, 114, 171, 197 | ofval 6804 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
199 | 189, 198 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
200 | 167, 199 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
201 | 164, 200 | jaodan 822 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
202 | 201 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
203 | | poimirlem2.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) |
204 | 203 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) |
205 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
206 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 + 1) ∈ V |
207 | 205, 206 | ifex 4106 |
. . . . . . . . . . . . . . . 16
⊢ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V |
208 | 207 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V) |
209 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑉 − 1) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀)) |
210 | 209 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀)) |
211 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → 𝑦 = (𝑉 − 1)) |
212 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑉 − 1) → (𝑦 + 1) = ((𝑉 − 1) + 1)) |
213 | 27 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑉 ∈ ℂ) |
214 | | npcan1 10334 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ∈ ℂ → ((𝑉 − 1) + 1) = 𝑉) |
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑉 − 1) + 1) = 𝑉) |
216 | 212, 215 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 + 1) = 𝑉) |
217 | 210, 211,
216 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉)) |
218 | 217 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉)) |
219 | | poimirlem2.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉})) |
220 | 219 | eldifad 3552 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑀 ∈ (0...𝑁)) |
221 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈ ℤ) |
222 | 220, 221 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑀 ∈ ℤ) |
223 | | zltlem1 11307 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1))) |
224 | 222, 27, 223 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1))) |
225 | 222 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑀 ∈ ℝ) |
226 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑉 ∈ ℤ → (𝑉 − 1) ∈
ℤ) |
227 | 27, 226 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑉 − 1) ∈ ℤ) |
228 | 227 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑉 − 1) ∈ ℝ) |
229 | 225, 228 | lenltd 10062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑀 ≤ (𝑉 − 1) ↔ ¬ (𝑉 − 1) < 𝑀)) |
230 | 224, 229 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 < 𝑉 ↔ ¬ (𝑉 − 1) < 𝑀)) |
231 | 230 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ¬ (𝑉 − 1) < 𝑀) |
232 | 231 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉) |
233 | 232 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉) |
234 | 218, 233 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉) |
235 | 234 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉)) |
236 | 235 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉) |
237 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑉 → (1...𝑗) = (1...𝑉)) |
238 | 237 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑉 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑉))) |
239 | 238 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑉 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑉)) × {1})) |
240 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑉 → (𝑗 + 1) = (𝑉 + 1)) |
241 | 240 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑉 → ((𝑗 + 1)...𝑁) = ((𝑉 + 1)...𝑁)) |
242 | 241 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑉 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑉 + 1)...𝑁))) |
243 | 242 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑉 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) |
244 | 239, 243 | uneq12d 3730 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑉 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) |
245 | 244 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑉 → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
246 | 236, 245 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
247 | 208, 246 | csbied 3526 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
248 | | elfzm1b 12287 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1)))) |
249 | 27, 90, 248 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1)))) |
250 | 100, 249 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑉 − 1) ∈ (0...(𝑁 − 1))) |
251 | 250 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑉 − 1) ∈ (0...(𝑁 − 1))) |
252 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V |
253 | 252 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V) |
254 | 204, 247,
251, 253 | fvmptd 6197 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
255 | 254 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
256 | 255 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
257 | 207 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V) |
258 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑉 → (𝑦 < 𝑀 ↔ 𝑉 < 𝑀)) |
259 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑉 → 𝑦 = 𝑉) |
260 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑉 → (𝑦 + 1) = (𝑉 + 1)) |
261 | 258, 259,
260 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑉 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑉 < 𝑀, 𝑉, (𝑉 + 1))) |
262 | | ltnsym 10014 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀)) |
263 | 225, 28, 262 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀)) |
264 | 263 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ¬ 𝑉 < 𝑀) |
265 | 264 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = (𝑉 + 1)) |
266 | 261, 265 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 + 1)) |
267 | 266 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = (𝑉 + 1))) |
268 | 267 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = (𝑉 + 1)) |
269 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑉 + 1) → (1...𝑗) = (1...(𝑉 + 1))) |
270 | 269 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑉 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 + 1)))) |
271 | 270 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑉 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 + 1))) × {1})) |
272 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (𝑉 + 1) → (𝑗 + 1) = ((𝑉 + 1) + 1)) |
273 | 272 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑉 + 1) → ((𝑗 + 1)...𝑁) = (((𝑉 + 1) + 1)...𝑁)) |
274 | 273 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑉 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
275 | 274 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑉 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) |
276 | 271, 275 | uneq12d 3730 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑉 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) |
277 | 276 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑉 + 1) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))) |
278 | 268, 277 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))) |
279 | 257, 278 | csbied 3526 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))) |
280 | | 1eluzge0 11608 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
(ℤ≥‘0) |
281 | | fzss1 12251 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ∈
(ℤ≥‘0) → (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))) |
282 | 280, 281 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(1...(𝑁 − 1))
⊆ (0...(𝑁 −
1)) |
283 | 282, 7 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑉 ∈ (0...(𝑁 − 1))) |
284 | 283 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → 𝑉 ∈ (0...(𝑁 − 1))) |
285 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∘𝑓 +
(((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪
((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) ∈ V |
286 | 285 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) ∈ V) |
287 | 204, 279,
284, 286 | fvmptd 6197 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘𝑉) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))) |
288 | 287 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
289 | 288 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
290 | 202, 256,
289 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)) |
291 | 290 | ex 449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
292 | 60, 291 | sylbid 229 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
293 | 292 | expdimp 452 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
294 | 293 | necon1ad 2799 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}))) |
295 | | elimasni 5411 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → (𝑉 + 1)𝑈𝑛) |
296 | | eqcom 2617 |
. . . . . . . . 9
⊢ (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑈‘(𝑉 + 1)) = 𝑛) |
297 | | f1ofn 6051 |
. . . . . . . . . . 11
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁)) |
298 | 1, 297 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 Fn (1...𝑁)) |
299 | | fnbrfvb 6146 |
. . . . . . . . . 10
⊢ ((𝑈 Fn (1...𝑁) ∧ (𝑉 + 1) ∈ (1...𝑁)) → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛)) |
300 | 298, 15, 299 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛)) |
301 | 296, 300 | syl5bb 271 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑉 + 1)𝑈𝑛)) |
302 | 295, 301 | syl5ibr 235 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1)))) |
303 | 302 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1)))) |
304 | 294, 303 | syld 46 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))) |
305 | 304 | ralrimiva 2949 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))) |
306 | | fvex 6113 |
. . . . 5
⊢ (𝑈‘(𝑉 + 1)) ∈ V |
307 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘(𝑉 + 1)))) |
308 | 307 | imbi2d 329 |
. . . . . 6
⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))) |
309 | 308 | ralbidv 2969 |
. . . . 5
⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))) |
310 | 306, 309 | spcev 3273 |
. . . 4
⊢
(∀𝑛 ∈
(𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
311 | 305, 310 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
312 | | imadif 5887 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉}))) |
313 | 4, 312 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉}))) |
314 | 102 | difeq1d 3689 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...𝑁) ∖ {𝑉}) = (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉})) |
315 | | difundir 3839 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...𝑉) ∪
((𝑉 + 1)...𝑁)) ∖ {𝑉}) = (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉})) |
316 | 215, 21 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑉 − 1) + 1) ∈
(ℤ≥‘1)) |
317 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑉 − 1) ∈ ℤ
→ (𝑉 − 1) ∈
(ℤ≥‘(𝑉 − 1))) |
318 | 227, 317 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑉 − 1) ∈
(ℤ≥‘(𝑉 − 1))) |
319 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑉 − 1) ∈
(ℤ≥‘(𝑉 − 1)) → ((𝑉 − 1) + 1) ∈
(ℤ≥‘(𝑉 − 1))) |
320 | 318, 319 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑉 − 1) + 1) ∈
(ℤ≥‘(𝑉 − 1))) |
321 | 215, 320 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘(𝑉 − 1))) |
322 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑉 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑉 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉))) |
323 | 316, 321,
322 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉))) |
324 | 215 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑉) = (𝑉...𝑉)) |
325 | | fzsn 12254 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑉 ∈ ℤ → (𝑉...𝑉) = {𝑉}) |
326 | 27, 325 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑉...𝑉) = {𝑉}) |
327 | 324, 326 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑉) = {𝑉}) |
328 | 327 | uneq2d 3729 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)) = ((1...(𝑉 − 1)) ∪ {𝑉})) |
329 | 323, 328 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ {𝑉})) |
330 | 329 | difeq1d 3689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1...𝑉) ∖ {𝑉}) = (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉})) |
331 | | difun2 4000 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1...(𝑉 −
1)) ∪ {𝑉}) ∖
{𝑉}) = ((1...(𝑉 − 1)) ∖ {𝑉}) |
332 | 28 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑉 − 1) < 𝑉) |
333 | 228, 28 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑉 − 1) < 𝑉 ↔ ¬ 𝑉 ≤ (𝑉 − 1))) |
334 | 332, 333 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝑉 ≤ (𝑉 − 1)) |
335 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑉 ∈ (1...(𝑉 − 1)) → 𝑉 ≤ (𝑉 − 1)) |
336 | 334, 335 | nsyl 134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ¬ 𝑉 ∈ (1...(𝑉 − 1))) |
337 | | difsn 4269 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑉 ∈ (1...(𝑉 − 1)) → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1))) |
338 | 336, 337 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1))) |
339 | 331, 338 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = (1...(𝑉 − 1))) |
340 | 330, 339 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...𝑉) ∖ {𝑉}) = (1...(𝑉 − 1))) |
341 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈ ((𝑉 + 1)...𝑁) → (𝑉 + 1) ≤ 𝑉) |
342 | 33, 341 | nsyl 134 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ 𝑉 ∈ ((𝑉 + 1)...𝑁)) |
343 | | difsn 4269 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑉 ∈ ((𝑉 + 1)...𝑁) → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁)) |
344 | 342, 343 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁)) |
345 | 340, 344 | uneq12d 3730 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉})) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) |
346 | 315, 345 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) |
347 | 314, 346 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1...𝑁) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) |
348 | 347 | imaeq2d 5385 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))) |
349 | 313, 348 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))) |
350 | | imaundi 5464 |
. . . . . . . . . . . . 13
⊢ (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) |
351 | 349, 350 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
352 | 351 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ 𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))) |
353 | | eldif 3550 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉}))) |
354 | | elun 3715 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
355 | 352, 353,
354 | 3bitr3g 301 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))))) |
356 | 355 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))))) |
357 | | imassrn 5396 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ (1...(𝑉 − 1))) ⊆ ran 𝑈 |
358 | 357, 65 | syl5ss 3579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (1...𝑁)) |
359 | 358 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (1...𝑁)) |
360 | 70 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑇 Fn (1...𝑁)) |
361 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
V → ((𝑈 “
(1...(𝑉 − 1)))
× {1}) Fn (𝑈 “
(1...(𝑉 −
1)))) |
362 | 72, 361 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) |
363 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
V → ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) |
364 | 75, 363 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) |
365 | 362, 364 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) |
366 | | imain 5888 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁)))) |
367 | 4, 366 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁)))) |
368 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 − 1) < 𝑉 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅) |
369 | 332, 368 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅) |
370 | 369 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = (𝑈 “ ∅)) |
371 | 370, 84 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ∅) |
372 | 367, 371 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅) |
373 | | fnun 5911 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑈 “
(1...(𝑉 − 1)))
× {1}) Fn (𝑈 “
(1...(𝑉 − 1))) ∧
((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) ∧ ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁)))) |
374 | 365, 372,
373 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁)))) |
375 | | imaundi 5464 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) |
376 | | uzss 11584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑉 ∈
(ℤ≥‘(𝑉 − 1)) →
(ℤ≥‘𝑉) ⊆
(ℤ≥‘(𝑉 − 1))) |
377 | 321, 376 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 →
(ℤ≥‘𝑉) ⊆
(ℤ≥‘(𝑉 − 1))) |
378 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑉 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑉)) |
379 | 7, 378 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘𝑉)) |
380 | 377, 379 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘(𝑉 − 1))) |
381 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑉 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑉 − 1))) |
382 | 380, 381 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑉 − 1))) |
383 | 13, 382 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑉 − 1))) |
384 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑉 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁))) |
385 | 316, 383,
384 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁))) |
386 | 215 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑁) = (𝑉...𝑁)) |
387 | 386 | uneq2d 3729 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) |
388 | 385, 387 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) |
389 | 388 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))) |
390 | 389, 107 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = (1...𝑁)) |
391 | 375, 390 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) = (1...𝑁)) |
392 | 391 | fneq2d 5896 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) ↔ (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))) |
393 | 374, 392 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)) |
394 | 393 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)) |
395 | | fzfid 12634 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (1...𝑁) ∈ Fin) |
396 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
397 | | fvun1 6179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛)) |
398 | 362, 364,
397 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛)) |
399 | 372, 398 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛)) |
400 | 72 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1) |
401 | 400 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1) |
402 | 399, 401 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1) |
403 | 402 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1) |
404 | 360, 394,
395, 395, 114, 396, 403 | ofval 6804 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
405 | 111 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
406 | | fzss2 12252 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 ∈
(ℤ≥‘(𝑉 − 1)) → (1...(𝑉 − 1)) ⊆ (1...𝑉)) |
407 | 321, 406 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...(𝑉 − 1)) ⊆ (1...𝑉)) |
408 | | imass2 5420 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1...(𝑉 − 1))
⊆ (1...𝑉) →
(𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉))) |
409 | 407, 408 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉))) |
410 | 409 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (𝑈 “ (1...𝑉))) |
411 | 410, 121 | syldan 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1) |
412 | 411 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1) |
413 | 360, 405,
395, 395, 114, 396, 412 | ofval 6804 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
414 | 404, 413 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
415 | 359, 414 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
416 | | imassrn 5396 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ ran 𝑈 |
417 | 416, 65 | syl5ss 3579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (1...𝑁)) |
418 | 417 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (1...𝑁)) |
419 | 70 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑇 Fn (1...𝑁)) |
420 | 393 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)) |
421 | | fzfid 12634 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (1...𝑁) ∈ Fin) |
422 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
423 | | fzss1 12251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 + 1) ∈
(ℤ≥‘𝑉) → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁)) |
424 | 148, 423 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁)) |
425 | | imass2 5420 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁) → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁))) |
426 | 424, 425 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁))) |
427 | 426 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) |
428 | | fvun2 6180 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛)) |
429 | 362, 364,
428 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛)) |
430 | 372, 429 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛)) |
431 | 75 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (𝑈 “ (𝑉...𝑁)) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0) |
432 | 431 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0) |
433 | 430, 432 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0) |
434 | 427, 433 | syldan 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0) |
435 | 434 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0) |
436 | 419, 420,
421, 421, 114, 422, 435 | ofval 6804 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
437 | 111 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
438 | 186 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0) |
439 | 419, 437,
421, 421, 114, 422, 438 | ofval 6804 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
440 | 436, 439 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
441 | 418, 440 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
442 | 415, 441 | jaodan 822 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
443 | 442 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
444 | 203 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) |
445 | 207 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V) |
446 | 217 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉)) |
447 | | lttr 9993 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 − 1) ∈ ℝ ∧
𝑉 ∈ ℝ ∧
𝑀 ∈ ℝ) →
(((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀)) |
448 | 228, 28, 225, 447 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀)) |
449 | 332, 448 | mpand 707 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑉 < 𝑀 → (𝑉 − 1) < 𝑀)) |
450 | 449 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀) |
451 | 450 | iftrued 4044 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1)) |
452 | 451 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1)) |
453 | 446, 452 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 − 1)) |
454 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → 𝜑) |
455 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (𝑉 − 1) → (1...𝑗) = (1...(𝑉 − 1))) |
456 | 455 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑉 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 − 1)))) |
457 | 456 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑉 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1})) |
458 | 457 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1})) |
459 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = (𝑉 − 1) → (𝑗 + 1) = ((𝑉 − 1) + 1)) |
460 | 459, 215 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑗 + 1) = 𝑉) |
461 | 460 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑗 + 1)...𝑁) = (𝑉...𝑁)) |
462 | 461 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑉...𝑁))) |
463 | 462 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑉...𝑁)) × {0})) |
464 | 458, 463 | uneq12d 3730 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) |
465 | 464 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))) |
466 | 454, 465 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))) |
467 | 445, 453,
466 | csbied2 3527 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))) |
468 | 250 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) ∈ (0...(𝑁 − 1))) |
469 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∘𝑓 +
(((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪
((𝑈 “ (𝑉...𝑁)) × {0}))) ∈ V |
470 | 469 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) ∈ V) |
471 | 444, 467,
468, 470 | fvmptd 6197 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))) |
472 | 471 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛)) |
473 | 472 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛)) |
474 | 207 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V) |
475 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 < 𝑀 → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = 𝑉) |
476 | 261, 475 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉) |
477 | 476 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉)) |
478 | 477 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉) |
479 | 478, 245 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
480 | 474, 479 | csbied 3526 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
481 | 480 | adantll 746 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
482 | 283 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → 𝑉 ∈ (0...(𝑁 − 1))) |
483 | 252 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V) |
484 | 444, 481,
482, 483 | fvmptd 6197 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘𝑉) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
485 | 484 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
486 | 485 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
487 | 443, 473,
486 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)) |
488 | 487 | ex 449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
489 | 356, 488 | sylbid 229 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
490 | 489 | expdimp 452 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {𝑉}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
491 | 490 | necon1ad 2799 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {𝑉}))) |
492 | | elimasni 5411 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑉𝑈𝑛) |
493 | | eqcom 2617 |
. . . . . . . . 9
⊢ (𝑛 = (𝑈‘𝑉) ↔ (𝑈‘𝑉) = 𝑛) |
494 | | fnbrfvb 6146 |
. . . . . . . . . 10
⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑉 ∈ (1...𝑁)) → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛)) |
495 | 298, 100,
494 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛)) |
496 | 493, 495 | syl5bb 271 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 = (𝑈‘𝑉) ↔ 𝑉𝑈𝑛)) |
497 | 492, 496 | syl5ibr 235 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉))) |
498 | 497 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉))) |
499 | 491, 498 | syld 46 |
. . . . 5
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))) |
500 | 499 | ralrimiva 2949 |
. . . 4
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))) |
501 | | fvex 6113 |
. . . . 5
⊢ (𝑈‘𝑉) ∈ V |
502 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑚 = (𝑈‘𝑉) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘𝑉))) |
503 | 502 | imbi2d 329 |
. . . . . 6
⊢ (𝑚 = (𝑈‘𝑉) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))) |
504 | 503 | ralbidv 2969 |
. . . . 5
⊢ (𝑚 = (𝑈‘𝑉) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))) |
505 | 501, 504 | spcev 3273 |
. . . 4
⊢
(∀𝑛 ∈
(𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
506 | 500, 505 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
507 | | eldifsni 4261 |
. . . . 5
⊢ (𝑀 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑀 ≠ 𝑉) |
508 | 219, 507 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ≠ 𝑉) |
509 | 225, 28 | lttri2d 10055 |
. . . 4
⊢ (𝜑 → (𝑀 ≠ 𝑉 ↔ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀))) |
510 | 508, 509 | mpbid 221 |
. . 3
⊢ (𝜑 → (𝑀 < 𝑉 ∨ 𝑉 < 𝑀)) |
511 | 311, 506,
510 | mpjaodan 823 |
. 2
⊢ (𝜑 → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
512 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑚((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) |
513 | 512 | rmo2 3492 |
. . 3
⊢
(∃*𝑛 ∈
(𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
514 | | rmoeq1 3118 |
. . . 4
⊢ ((𝑈 “ (1...𝑁)) = (1...𝑁) → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))) |
515 | 107, 514 | syl 17 |
. . 3
⊢ (𝜑 → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))) |
516 | 513, 515 | syl5bbr 273 |
. 2
⊢ (𝜑 → (∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))) |
517 | 511, 516 | mpbid 221 |
1
⊢ (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)) |