| Step | Hyp | Ref
| Expression |
| 1 | | metakunt16.4 |
. 2
⊢ 𝐹 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) |
| 2 | | metakunt16.2 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ ℕ) |
| 3 | 2 | nnzd 12640 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ ℤ) |
| 4 | 3 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → 𝐼 ∈ ℤ) |
| 5 | | metakunt16.1 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 6 | 5 | nnzd 12640 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → 𝑀 ∈ ℤ) |
| 8 | | 1zzd 12648 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → 1 ∈
ℤ) |
| 9 | 7, 8 | zsubcld 12727 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → (𝑀 − 1) ∈ ℤ) |
| 10 | 8, 4 | zsubcld 12727 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → (1 − 𝐼) ∈
ℤ) |
| 11 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → 𝑥 ∈ (𝐼...(𝑀 − 1))) |
| 12 | | elfz3 13574 |
. . . 4
⊢ ((1
− 𝐼) ∈ ℤ
→ (1 − 𝐼) ∈
((1 − 𝐼)...(1 −
𝐼))) |
| 13 | 10, 12 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → (1 − 𝐼) ∈ ((1 − 𝐼)...(1 − 𝐼))) |
| 14 | 4 | zcnd 12723 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → 𝐼 ∈ ℂ) |
| 15 | | 1cnd 11256 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → 1 ∈
ℂ) |
| 16 | 14, 15 | pncan3d 11623 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → (𝐼 + (1 − 𝐼)) = 1) |
| 17 | 16 | eqcomd 2743 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → 1 = (𝐼 + (1 − 𝐼))) |
| 18 | 5 | nncnd 12282 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 19 | 18 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → 𝑀 ∈ ℂ) |
| 20 | 19, 15, 14 | npncand 11644 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → ((𝑀 − 1) + (1 − 𝐼)) = (𝑀 − 𝐼)) |
| 21 | 20 | eqcomd 2743 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → (𝑀 − 𝐼) = ((𝑀 − 1) + (1 − 𝐼))) |
| 22 | 4, 9, 10, 10, 11, 13, 17, 21 | fzadd2d 41979 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼...(𝑀 − 1))) → (𝑥 + (1 − 𝐼)) ∈ (1...(𝑀 − 𝐼))) |
| 23 | 3 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝐼 ∈ ℤ) |
| 24 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝑀 ∈ ℤ) |
| 25 | | 1zzd 12648 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 1 ∈
ℤ) |
| 26 | 24, 25 | zsubcld 12727 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (𝑀 − 1) ∈ ℤ) |
| 27 | | elfznn 13593 |
. . . . . 6
⊢ (𝑦 ∈ (1...(𝑀 − 𝐼)) → 𝑦 ∈ ℕ) |
| 28 | 27 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝑦 ∈ ℕ) |
| 29 | | nnz 12634 |
. . . . 5
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 30 | 28, 29 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝑦 ∈ ℤ) |
| 31 | 25, 23 | zsubcld 12727 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (1 − 𝐼) ∈ ℤ) |
| 32 | 30, 31 | zsubcld 12727 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (𝑦 − (1 − 𝐼)) ∈ ℤ) |
| 33 | 23 | zred 12722 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝐼 ∈ ℝ) |
| 34 | 33 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝐼 ∈ ℂ) |
| 35 | | 1cnd 11256 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 1 ∈
ℂ) |
| 36 | 34, 35 | pncan3d 11623 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (𝐼 + (1 − 𝐼)) = 1) |
| 37 | 27 | nnge1d 12314 |
. . . . . 6
⊢ (𝑦 ∈ (1...(𝑀 − 𝐼)) → 1 ≤ 𝑦) |
| 38 | 37 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 1 ≤ 𝑦) |
| 39 | 36, 38 | eqbrtrd 5165 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (𝐼 + (1 − 𝐼)) ≤ 𝑦) |
| 40 | | 1red 11262 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 1 ∈
ℝ) |
| 41 | 40, 33 | resubcld 11691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (1 − 𝐼) ∈ ℝ) |
| 42 | 28 | nnred 12281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝑦 ∈ ℝ) |
| 43 | 33, 41, 42 | 3jca 1129 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (𝐼 ∈ ℝ ∧ (1 − 𝐼) ∈ ℝ ∧ 𝑦 ∈
ℝ)) |
| 44 | | leaddsub 11739 |
. . . . 5
⊢ ((𝐼 ∈ ℝ ∧ (1 −
𝐼) ∈ ℝ ∧
𝑦 ∈ ℝ) →
((𝐼 + (1 − 𝐼)) ≤ 𝑦 ↔ 𝐼 ≤ (𝑦 − (1 − 𝐼)))) |
| 45 | 43, 44 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → ((𝐼 + (1 − 𝐼)) ≤ 𝑦 ↔ 𝐼 ≤ (𝑦 − (1 − 𝐼)))) |
| 46 | 39, 45 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝐼 ≤ (𝑦 − (1 − 𝐼))) |
| 47 | | elfzle2 13568 |
. . . . . 6
⊢ (𝑦 ∈ (1...(𝑀 − 𝐼)) → 𝑦 ≤ (𝑀 − 𝐼)) |
| 48 | 47 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝑦 ≤ (𝑀 − 𝐼)) |
| 49 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝑀 ∈ ℂ) |
| 50 | 23 | zcnd 12723 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝐼 ∈ ℂ) |
| 51 | 49, 35, 50 | npncand 11644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → ((𝑀 − 1) + (1 − 𝐼)) = (𝑀 − 𝐼)) |
| 52 | 48, 51 | breqtrrd 5171 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → 𝑦 ≤ ((𝑀 − 1) + (1 − 𝐼))) |
| 53 | 31 | zred 12722 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (1 − 𝐼) ∈ ℝ) |
| 54 | 26 | zred 12722 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (𝑀 − 1) ∈ ℝ) |
| 55 | 42, 53, 54 | lesubaddd 11860 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → ((𝑦 − (1 − 𝐼)) ≤ (𝑀 − 1) ↔ 𝑦 ≤ ((𝑀 − 1) + (1 − 𝐼)))) |
| 56 | 52, 55 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (𝑦 − (1 − 𝐼)) ≤ (𝑀 − 1)) |
| 57 | 23, 26, 32, 46, 56 | elfzd 13555 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑀 − 𝐼))) → (𝑦 − (1 − 𝐼)) ∈ (𝐼...(𝑀 − 1))) |
| 58 | | 1cnd 11256 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → 1 ∈
ℂ) |
| 59 | 34 | adantrl 716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → 𝐼 ∈ ℂ) |
| 60 | 58, 59 | subcld 11620 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → (1 − 𝐼) ∈ ℂ) |
| 61 | | elfzelz 13564 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐼...(𝑀 − 1)) → 𝑥 ∈ ℤ) |
| 62 | 61 | ad2antrl 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → 𝑥 ∈ ℤ) |
| 63 | | zcn 12618 |
. . . . . 6
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 64 | 62, 63 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → 𝑥 ∈ ℂ) |
| 65 | 28 | adantrl 716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → 𝑦 ∈ ℕ) |
| 66 | | nncn 12274 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
| 67 | 65, 66 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → 𝑦 ∈ ℂ) |
| 68 | 60, 64, 67 | addrsub 11680 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → (((1 − 𝐼) + 𝑥) = 𝑦 ↔ 𝑥 = (𝑦 − (1 − 𝐼)))) |
| 69 | 68 | bicomd 223 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → (𝑥 = (𝑦 − (1 − 𝐼)) ↔ ((1 − 𝐼) + 𝑥) = 𝑦)) |
| 70 | 60, 64 | addcomd 11463 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → ((1 − 𝐼) + 𝑥) = (𝑥 + (1 − 𝐼))) |
| 71 | 70 | eqeq1d 2739 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → (((1 − 𝐼) + 𝑥) = 𝑦 ↔ (𝑥 + (1 − 𝐼)) = 𝑦)) |
| 72 | | eqcom 2744 |
. . . . 5
⊢ ((𝑥 + (1 − 𝐼)) = 𝑦 ↔ 𝑦 = (𝑥 + (1 − 𝐼))) |
| 73 | 72 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → ((𝑥 + (1 − 𝐼)) = 𝑦 ↔ 𝑦 = (𝑥 + (1 − 𝐼)))) |
| 74 | 71, 73 | bitrd 279 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → (((1 − 𝐼) + 𝑥) = 𝑦 ↔ 𝑦 = (𝑥 + (1 − 𝐼)))) |
| 75 | 69, 74 | bitrd 279 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ∧ 𝑦 ∈ (1...(𝑀 − 𝐼)))) → (𝑥 = (𝑦 − (1 − 𝐼)) ↔ 𝑦 = (𝑥 + (1 − 𝐼)))) |
| 76 | 1, 22, 57, 75 | f1o2d 7687 |
1
⊢ (𝜑 → 𝐹:(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀 − 𝐼))) |