Step | Hyp | Ref
| Expression |
1 | | madjusmdet.n |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | nnuz 12918 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
3 | 1, 2 | eleqtrdi 2848 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
4 | | eluzfz2 13568 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
6 | | eqid 2734 |
. . . . . . . . . . 11
⊢
(1...𝑁) = (1...𝑁) |
7 | | madjusmdetlem2.s |
. . . . . . . . . . 11
⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) |
8 | | eqid 2734 |
. . . . . . . . . . 11
⊢
(SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁)) |
9 | | eqid 2734 |
. . . . . . . . . . 11
⊢
(Base‘(SymGrp‘(1...𝑁))) = (Base‘(SymGrp‘(1...𝑁))) |
10 | 6, 7, 8, 9 | fzto1st 33105 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (1...𝑁) → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
11 | 5, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
12 | 8, 9 | symgbasf1o 19406 |
. . . . . . . . 9
⊢ (𝑆 ∈
(Base‘(SymGrp‘(1...𝑁))) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁)) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁)) |
14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁)) |
15 | | fznatpl1 13614 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (𝑋 + 1) ∈ (1...𝑁)) |
16 | 1, 15 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (𝑋 + 1) ∈ (1...𝑁)) |
17 | | eqeq1 2738 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝑖 = 1 ↔ 𝑥 = 1)) |
18 | | breq1 5150 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → (𝑖 ≤ 𝑁 ↔ 𝑥 ≤ 𝑁)) |
19 | | oveq1 7437 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → (𝑖 − 1) = (𝑥 − 1)) |
20 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → 𝑖 = 𝑥) |
21 | 18, 19, 20 | ifbieq12d 4558 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖) = if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥)) |
22 | 17, 21 | ifbieq2d 4556 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑥 → if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥))) |
23 | 22 | cbvmptv 5260 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥))) |
24 | 7, 23 | eqtri 2762 |
. . . . . . . 8
⊢ 𝑆 = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥))) |
25 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 = (𝑋 + 1)) |
26 | | 1red 11259 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 1 ∈
ℝ) |
27 | | fz1ssnn 13591 |
. . . . . . . . . . . . . . . . 17
⊢
(1...(𝑁 − 1))
⊆ ℕ |
28 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ (1...(𝑁 − 1))) |
29 | 27, 28 | sselid 3992 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ ℕ) |
30 | 29 | nnrpd 13072 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈
ℝ+) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑋 ∈
ℝ+) |
32 | 26, 31 | ltaddrp2d 13108 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 1 < (𝑋 + 1)) |
33 | 26, 32 | gtned 11393 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑋 + 1) ≠ 1) |
34 | 25, 33 | eqnetrd 3005 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≠ 1) |
35 | 34 | neneqd 2942 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → ¬ 𝑥 = 1) |
36 | 35 | iffalsed 4541 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥)) = if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥)) |
37 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
38 | 29 | nnnn0d 12584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈
ℕ0) |
39 | 37 | nnnn0d 12584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑁 ∈
ℕ0) |
40 | | elfzle2 13564 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ (1...(𝑁 − 1)) → 𝑋 ≤ (𝑁 − 1)) |
41 | 28, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ≤ (𝑁 − 1)) |
42 | | nn0ltlem1 12675 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑋 < 𝑁 ↔ 𝑋 ≤ (𝑁 − 1))) |
43 | 42 | biimpar 477 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑋 ≤ (𝑁 − 1)) → 𝑋 < 𝑁) |
44 | 38, 39, 41, 43 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 < 𝑁) |
45 | | nnltp1le 12671 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑋 < 𝑁 ↔ (𝑋 + 1) ≤ 𝑁)) |
46 | 45 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑋 < 𝑁) → (𝑋 + 1) ≤ 𝑁) |
47 | 29, 37, 44, 46 | syl21anc 838 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (𝑋 + 1) ≤ 𝑁) |
48 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑋 + 1) ≤ 𝑁) |
49 | 25, 48 | eqbrtrd 5169 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≤ 𝑁) |
50 | 49 | iftrued 4538 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥) = (𝑥 − 1)) |
51 | 25 | oveq1d 7445 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑥 − 1) = ((𝑋 + 1) − 1)) |
52 | 29 | nncnd 12279 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ ℂ) |
53 | | 1cnd 11253 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 1 ∈
ℂ) |
54 | 52, 53 | pncand 11618 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → ((𝑋 + 1) − 1) = 𝑋) |
55 | 54 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → ((𝑋 + 1) − 1) = 𝑋) |
56 | 51, 55 | eqtrd 2774 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑥 − 1) = 𝑋) |
57 | 36, 50, 56 | 3eqtrd 2778 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥)) = 𝑋) |
58 | 24, 57, 16, 28 | fvmptd2 7023 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (𝑆‘(𝑋 + 1)) = 𝑋) |
59 | | f1ocnvfv 7297 |
. . . . . . . 8
⊢ ((𝑆:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (𝑋 + 1) ∈ (1...𝑁)) → ((𝑆‘(𝑋 + 1)) = 𝑋 → (◡𝑆‘𝑋) = (𝑋 + 1))) |
60 | 59 | imp 406 |
. . . . . . 7
⊢ (((𝑆:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (𝑋 + 1) ∈ (1...𝑁)) ∧ (𝑆‘(𝑋 + 1)) = 𝑋) → (◡𝑆‘𝑋) = (𝑋 + 1)) |
61 | 14, 16, 58, 60 | syl21anc 838 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (◡𝑆‘𝑋) = (𝑋 + 1)) |
62 | 61 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (𝑃‘(◡𝑆‘𝑋)) = (𝑃‘(𝑋 + 1))) |
63 | 62 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → (𝑃‘(◡𝑆‘𝑋)) = (𝑃‘(𝑋 + 1))) |
64 | | madjusmdetlem2.p |
. . . . . 6
⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) |
65 | | breq1 5150 |
. . . . . . . . 9
⊢ (𝑖 = 𝑥 → (𝑖 ≤ 𝐼 ↔ 𝑥 ≤ 𝐼)) |
66 | 65, 19, 20 | ifbieq12d 4558 |
. . . . . . . 8
⊢ (𝑖 = 𝑥 → if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖) = if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) |
67 | 17, 66 | ifbieq2d 4556 |
. . . . . . 7
⊢ (𝑖 = 𝑥 → if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥))) |
68 | 67 | cbvmptv 5260 |
. . . . . 6
⊢ (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥))) |
69 | 64, 68 | eqtri 2762 |
. . . . 5
⊢ 𝑃 = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥))) |
70 | 32, 25 | breqtrrd 5175 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 1 < 𝑥) |
71 | 26, 70 | gtned 11393 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≠ 1) |
72 | 71 | neneqd 2942 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → ¬ 𝑥 = 1) |
73 | 72 | iffalsed 4541 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) = if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) |
74 | 73 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) = if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) |
75 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 = (𝑋 + 1)) |
76 | 29 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑋 ∈ ℕ) |
77 | | fz1ssnn 13591 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
ℕ |
78 | | madjusmdet.i |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) |
79 | 77, 78 | sselid 3992 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ ℕ) |
80 | 79 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝐼 ∈ ℕ) |
81 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑋 < 𝐼) |
82 | | nnltp1le 12671 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ) → (𝑋 < 𝐼 ↔ (𝑋 + 1) ≤ 𝐼)) |
83 | 82 | biimpa 476 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ) ∧ 𝑋 < 𝐼) → (𝑋 + 1) ≤ 𝐼) |
84 | 76, 80, 81, 83 | syl21anc 838 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → (𝑋 + 1) ≤ 𝐼) |
85 | 75, 84 | eqbrtrd 5169 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≤ 𝐼) |
86 | 85 | iftrued 4538 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥) = (𝑥 − 1)) |
87 | 56 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → (𝑥 − 1) = 𝑋) |
88 | 74, 86, 87 | 3eqtrd 2778 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) = 𝑋) |
89 | 16 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → (𝑋 + 1) ∈ (1...𝑁)) |
90 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → 𝑋 ∈ (1...(𝑁 − 1))) |
91 | 69, 88, 89, 90 | fvmptd2 7023 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → (𝑃‘(𝑋 + 1)) = 𝑋) |
92 | 63, 91 | eqtr2d 2775 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → 𝑋 = (𝑃‘(◡𝑆‘𝑋))) |
93 | 62 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑃‘(◡𝑆‘𝑋)) = (𝑃‘(𝑋 + 1))) |
94 | 73 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) = if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) |
95 | 29 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥 ≤ 𝐼) → 𝑋 ∈ ℕ) |
96 | 79 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥 ≤ 𝐼) → 𝐼 ∈ ℕ) |
97 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥 ≤ 𝐼) → 𝑥 = (𝑋 + 1)) |
98 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥 ≤ 𝐼) → 𝑥 ≤ 𝐼) |
99 | 97, 98 | eqbrtrrd 5171 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥 ≤ 𝐼) → (𝑋 + 1) ≤ 𝐼) |
100 | 82 | biimpar 477 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ) ∧ (𝑋 + 1) ≤ 𝐼) → 𝑋 < 𝐼) |
101 | 95, 96, 99, 100 | syl21anc 838 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥 ≤ 𝐼) → 𝑋 < 𝐼) |
102 | 101 | stoic1a 1768 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ ¬ 𝑋 < 𝐼) → ¬ 𝑥 ≤ 𝐼) |
103 | 102 | an32s 652 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → ¬ 𝑥 ≤ 𝐼) |
104 | 103 | iffalsed 4541 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥) = 𝑥) |
105 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 = (𝑋 + 1)) |
106 | 94, 104, 105 | 3eqtrd 2778 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) = (𝑋 + 1)) |
107 | 16 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑋 + 1) ∈ (1...𝑁)) |
108 | 69, 106, 107, 107 | fvmptd2 7023 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑃‘(𝑋 + 1)) = (𝑋 + 1)) |
109 | 93, 108 | eqtr2d 2775 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑋 + 1) = (𝑃‘(◡𝑆‘𝑋))) |
110 | 92, 109 | ifeqda 4566 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = (𝑃‘(◡𝑆‘𝑋))) |
111 | | f1ocnv 6860 |
. . . . 5
⊢ (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → ◡𝑆:(1...𝑁)–1-1-onto→(1...𝑁)) |
112 | 11, 12, 111 | 3syl 18 |
. . . 4
⊢ (𝜑 → ◡𝑆:(1...𝑁)–1-1-onto→(1...𝑁)) |
113 | | f1ofun 6850 |
. . . 4
⊢ (◡𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑆) |
114 | 112, 113 | syl 17 |
. . 3
⊢ (𝜑 → Fun ◡𝑆) |
115 | | fzdif2 32798 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
116 | 3, 115 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
117 | | difss 4145 |
. . . . . 6
⊢
((1...𝑁) ∖
{𝑁}) ⊆ (1...𝑁) |
118 | 116, 117 | eqsstrrdi 4050 |
. . . . 5
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
119 | | f1odm 6852 |
. . . . . 6
⊢ (◡𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → dom ◡𝑆 = (1...𝑁)) |
120 | 112, 119 | syl 17 |
. . . . 5
⊢ (𝜑 → dom ◡𝑆 = (1...𝑁)) |
121 | 118, 120 | sseqtrrd 4036 |
. . . 4
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ dom ◡𝑆) |
122 | 121 | sselda 3994 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ dom ◡𝑆) |
123 | | fvco 7006 |
. . 3
⊢ ((Fun
◡𝑆 ∧ 𝑋 ∈ dom ◡𝑆) → ((𝑃 ∘ ◡𝑆)‘𝑋) = (𝑃‘(◡𝑆‘𝑋))) |
124 | 114, 122,
123 | syl2an2r 685 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → ((𝑃 ∘ ◡𝑆)‘𝑋) = (𝑃‘(◡𝑆‘𝑋))) |
125 | 110, 124 | eqtr4d 2777 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = ((𝑃 ∘ ◡𝑆)‘𝑋)) |