| Step | Hyp | Ref
| Expression |
| 1 | | madjusmdet.n |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 2 | | nnuz 12921 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
| 3 | 1, 2 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
| 4 | | eluzfz2 13572 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
| 5 | 3, 4 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
| 6 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(1...𝑁) = (1...𝑁) |
| 7 | | madjusmdetlem2.s |
. . . . . . . . . . 11
⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) |
| 8 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁)) |
| 9 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘(SymGrp‘(1...𝑁))) = (Base‘(SymGrp‘(1...𝑁))) |
| 10 | 6, 7, 8, 9 | fzto1st 33123 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (1...𝑁) → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
| 11 | 5, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁)))) |
| 12 | 8, 9 | symgbasf1o 19392 |
. . . . . . . . 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 13618 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (𝑋 + 1) ∈ (1...𝑁)) |
| 16 | 1, 15 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (𝑋 + 1) ∈ (1...𝑁)) |
| 17 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → (𝑖 = 1 ↔ 𝑥 = 1)) |
| 18 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → (𝑖 ≤ 𝑁 ↔ 𝑥 ≤ 𝑁)) |
| 19 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → (𝑖 − 1) = (𝑥 − 1)) |
| 20 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑥 → 𝑖 = 𝑥) |
| 21 | 18, 19, 20 | ifbieq12d 4554 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑥 → if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖) = if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥)) |
| 22 | 17, 21 | ifbieq2d 4552 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑥 → if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥))) |
| 23 | 22 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥))) |
| 24 | 7, 23 | eqtri 2765 |
. . . . . . . 8
⊢ 𝑆 = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥))) |
| 25 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 = (𝑋 + 1)) |
| 26 | | 1red 11262 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 1 ∈
ℝ) |
| 27 | | fz1ssnn 13595 |
. . . . . . . . . . . . . . . . 17
⊢
(1...(𝑁 − 1))
⊆ ℕ |
| 28 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ (1...(𝑁 − 1))) |
| 29 | 27, 28 | sselid 3981 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ ℕ) |
| 30 | 29 | nnrpd 13075 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈
ℝ+) |
| 31 | 30 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑋 ∈
ℝ+) |
| 32 | 26, 31 | ltaddrp2d 13111 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 1 < (𝑋 + 1)) |
| 33 | 26, 32 | gtned 11396 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑋 + 1) ≠ 1) |
| 34 | 25, 33 | eqnetrd 3008 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≠ 1) |
| 35 | 34 | neneqd 2945 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → ¬ 𝑥 = 1) |
| 36 | 35 | iffalsed 4536 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥)) = if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥)) |
| 37 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
| 38 | 29 | nnnn0d 12587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈
ℕ0) |
| 39 | 37 | nnnn0d 12587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑁 ∈
ℕ0) |
| 40 | | elfzle2 13568 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ (1...(𝑁 − 1)) → 𝑋 ≤ (𝑁 − 1)) |
| 41 | 28, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ≤ (𝑁 − 1)) |
| 42 | | nn0ltlem1 12678 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑋 < 𝑁 ↔ 𝑋 ≤ (𝑁 − 1))) |
| 43 | 42 | biimpar 477 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑋 ≤ (𝑁 − 1)) → 𝑋 < 𝑁) |
| 44 | 38, 39, 41, 43 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 < 𝑁) |
| 45 | | nnltp1le 12674 |
. . . . . . . . . . . . . 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 5165 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≤ 𝑁) |
| 50 | 49 | iftrued 4533 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥) = (𝑥 − 1)) |
| 51 | 25 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑥 − 1) = ((𝑋 + 1) − 1)) |
| 52 | 29 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ ℂ) |
| 53 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 1 ∈
ℂ) |
| 54 | 52, 53 | pncand 11621 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → ((𝑋 + 1) − 1) = 𝑋) |
| 55 | 54 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → ((𝑋 + 1) − 1) = 𝑋) |
| 56 | 51, 55 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑥 − 1) = 𝑋) |
| 57 | 36, 50, 56 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝑁, if(𝑥 ≤ 𝑁, (𝑥 − 1), 𝑥)) = 𝑋) |
| 58 | 24, 57, 16, 28 | fvmptd2 7024 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (𝑆‘(𝑋 + 1)) = 𝑋) |
| 59 | | f1ocnvfv 7298 |
. . . . . . . 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 5146 |
. . . . . . . . 9
⊢ (𝑖 = 𝑥 → (𝑖 ≤ 𝐼 ↔ 𝑥 ≤ 𝐼)) |
| 66 | 65, 19, 20 | ifbieq12d 4554 |
. . . . . . . 8
⊢ (𝑖 = 𝑥 → if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖) = if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) |
| 67 | 17, 66 | ifbieq2d 4552 |
. . . . . . 7
⊢ (𝑖 = 𝑥 → if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥))) |
| 68 | 67 | cbvmptv 5255 |
. . . . . 6
⊢ (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥))) |
| 69 | 64, 68 | eqtri 2765 |
. . . . 5
⊢ 𝑃 = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥))) |
| 70 | 32, 25 | breqtrrd 5171 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 1 < 𝑥) |
| 71 | 26, 70 | gtned 11396 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≠ 1) |
| 72 | 71 | neneqd 2945 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → ¬ 𝑥 = 1) |
| 73 | 72 | iffalsed 4536 |
. . . . . . 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 13595 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
ℕ |
| 78 | | madjusmdet.i |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) |
| 79 | 77, 78 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ ℕ) |
| 80 | 79 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝐼 ∈ ℕ) |
| 81 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑋 < 𝐼) |
| 82 | | nnltp1le 12674 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ) → (𝑋 < 𝐼 ↔ (𝑋 + 1) ≤ 𝐼)) |
| 83 | 82 | biimpa 476 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ) ∧ 𝑋 < 𝐼) → (𝑋 + 1) ≤ 𝐼) |
| 84 | 76, 80, 81, 83 | syl21anc 838 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → (𝑋 + 1) ≤ 𝐼) |
| 85 | 75, 84 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≤ 𝐼) |
| 86 | 85 | iftrued 4533 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥) = (𝑥 − 1)) |
| 87 | 56 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → (𝑥 − 1) = 𝑋) |
| 88 | 74, 86, 87 | 3eqtrd 2781 |
. . . . 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 7024 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → (𝑃‘(𝑋 + 1)) = 𝑋) |
| 92 | 63, 91 | eqtr2d 2778 |
. . 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 5167 |
. . . . . . . . . 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 1772 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ ¬ 𝑋 < 𝐼) → ¬ 𝑥 ≤ 𝐼) |
| 103 | 102 | an32s 652 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → ¬ 𝑥 ≤ 𝐼) |
| 104 | 103 | iffalsed 4536 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥) = 𝑥) |
| 105 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 = (𝑋 + 1)) |
| 106 | 94, 104, 105 | 3eqtrd 2781 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥 ≤ 𝐼, (𝑥 − 1), 𝑥)) = (𝑋 + 1)) |
| 107 | 16 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑋 + 1) ∈ (1...𝑁)) |
| 108 | 69, 106, 107, 107 | fvmptd2 7024 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑃‘(𝑋 + 1)) = (𝑋 + 1)) |
| 109 | 93, 108 | eqtr2d 2778 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑋 + 1) = (𝑃‘(◡𝑆‘𝑋))) |
| 110 | 92, 109 | ifeqda 4562 |
. 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 32792 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
| 116 | 3, 115 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
| 117 | | difss 4136 |
. . . . . 6
⊢
((1...𝑁) ∖
{𝑁}) ⊆ (1...𝑁) |
| 118 | 116, 117 | eqsstrrdi 4029 |
. . . . 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 4021 |
. . . 4
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ dom ◡𝑆) |
| 122 | 121 | sselda 3983 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ dom ◡𝑆) |
| 123 | | fvco 7007 |
. . 3
⊢ ((Fun
◡𝑆 ∧ 𝑋 ∈ dom ◡𝑆) → ((𝑃 ∘ ◡𝑆)‘𝑋) = (𝑃‘(◡𝑆‘𝑋))) |
| 124 | 114, 122,
123 | syl2an2r 685 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → ((𝑃 ∘ ◡𝑆)‘𝑋) = (𝑃‘(◡𝑆‘𝑋))) |
| 125 | 110, 124 | eqtr4d 2780 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = ((𝑃 ∘ ◡𝑆)‘𝑋)) |