Step | Hyp | Ref
| Expression |
1 | | metakunt15.4 |
. 2
⊢ 𝐹 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) |
2 | | 1zzd 12037 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → 1 ∈
ℤ) |
3 | | metakunt15.2 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℕ) |
4 | 3 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ ℤ) |
5 | 4 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → 𝐼 ∈ ℤ) |
6 | 5, 2 | zsubcld 12116 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → (𝐼 − 1) ∈ ℤ) |
7 | | metakunt15.1 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
8 | 7 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | 8 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → 𝑀 ∈ ℤ) |
10 | 9, 5 | zsubcld 12116 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → (𝑀 − 𝐼) ∈ ℤ) |
11 | | simpr 489 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → 𝑥 ∈ (1...(𝐼 − 1))) |
12 | | elfz3 12951 |
. . . 4
⊢ ((𝑀 − 𝐼) ∈ ℤ → (𝑀 − 𝐼) ∈ ((𝑀 − 𝐼)...(𝑀 − 𝐼))) |
13 | 10, 12 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → (𝑀 − 𝐼) ∈ ((𝑀 − 𝐼)...(𝑀 − 𝐼))) |
14 | 10 | zcnd 12112 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → (𝑀 − 𝐼) ∈ ℂ) |
15 | | 1cnd 10659 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → 1 ∈
ℂ) |
16 | 14, 15 | addcomd 10865 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → ((𝑀 − 𝐼) + 1) = (1 + (𝑀 − 𝐼))) |
17 | 7 | nncnd 11675 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
18 | 3 | nncnd 11675 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ ℂ) |
19 | | 1cnd 10659 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
20 | 17, 18, 19 | npncand 11044 |
. . . . . 6
⊢ (𝜑 → ((𝑀 − 𝐼) + (𝐼 − 1)) = (𝑀 − 1)) |
21 | 20 | eqcomd 2765 |
. . . . 5
⊢ (𝜑 → (𝑀 − 1) = ((𝑀 − 𝐼) + (𝐼 − 1))) |
22 | 17, 18 | subcld 11020 |
. . . . . 6
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℂ) |
23 | 18, 19 | subcld 11020 |
. . . . . 6
⊢ (𝜑 → (𝐼 − 1) ∈ ℂ) |
24 | 22, 23 | addcomd 10865 |
. . . . 5
⊢ (𝜑 → ((𝑀 − 𝐼) + (𝐼 − 1)) = ((𝐼 − 1) + (𝑀 − 𝐼))) |
25 | 21, 24 | eqtrd 2794 |
. . . 4
⊢ (𝜑 → (𝑀 − 1) = ((𝐼 − 1) + (𝑀 − 𝐼))) |
26 | 25 | adantr 485 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → (𝑀 − 1) = ((𝐼 − 1) + (𝑀 − 𝐼))) |
27 | 2, 6, 10, 10, 11, 13, 16, 26 | fzadd2d 39530 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝐼 − 1))) → (𝑥 + (𝑀 − 𝐼)) ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) |
28 | | 1zzd 12037 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → 1 ∈
ℤ) |
29 | 4 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → 𝐼 ∈ ℤ) |
30 | 29, 28 | zsubcld 12116 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → (𝐼 − 1) ∈ ℤ) |
31 | | elfzelz 12941 |
. . . . 5
⊢ (𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)) → 𝑦 ∈ ℤ) |
32 | 31 | adantl 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → 𝑦 ∈ ℤ) |
33 | 8 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → 𝑀 ∈ ℤ) |
34 | 33, 29 | zsubcld 12116 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → (𝑀 − 𝐼) ∈ ℤ) |
35 | 32, 34 | zsubcld 12116 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → (𝑦 − (𝑀 − 𝐼)) ∈ ℤ) |
36 | | elfzle1 12944 |
. . . . 5
⊢ (𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)) → ((𝑀 − 𝐼) + 1) ≤ 𝑦) |
37 | 36 | adantl 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → ((𝑀 − 𝐼) + 1) ≤ 𝑦) |
38 | 34 | zred 12111 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → (𝑀 − 𝐼) ∈ ℝ) |
39 | | 1red 10665 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → 1 ∈
ℝ) |
40 | 32 | zred 12111 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → 𝑦 ∈ ℝ) |
41 | 38, 39, 40 | leaddsub2d 11265 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → (((𝑀 − 𝐼) + 1) ≤ 𝑦 ↔ 1 ≤ (𝑦 − (𝑀 − 𝐼)))) |
42 | 37, 41 | mpbid 235 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → 1 ≤ (𝑦 − (𝑀 − 𝐼))) |
43 | | elfzle2 12945 |
. . . . . 6
⊢ (𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)) → 𝑦 ≤ (𝑀 − 1)) |
44 | 43 | adantl 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → 𝑦 ≤ (𝑀 − 1)) |
45 | 20 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → ((𝑀 − 𝐼) + (𝐼 − 1)) = (𝑀 − 1)) |
46 | 44, 45 | breqtrrd 5053 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → 𝑦 ≤ ((𝑀 − 𝐼) + (𝐼 − 1))) |
47 | 30 | zred 12111 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → (𝐼 − 1) ∈ ℝ) |
48 | 40, 38, 47 | lesubadd2d 11262 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → ((𝑦 − (𝑀 − 𝐼)) ≤ (𝐼 − 1) ↔ 𝑦 ≤ ((𝑀 − 𝐼) + (𝐼 − 1)))) |
49 | 46, 48 | mpbird 260 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → (𝑦 − (𝑀 − 𝐼)) ≤ (𝐼 − 1)) |
50 | 28, 30, 35, 42, 49 | elfzd 12932 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) → (𝑦 − (𝑀 − 𝐼)) ∈ (1...(𝐼 − 1))) |
51 | | eqcom 2766 |
. . . . 5
⊢ ((𝑦 − (𝑀 − 𝐼)) = 𝑥 ↔ 𝑥 = (𝑦 − (𝑀 − 𝐼))) |
52 | 51 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → ((𝑦 − (𝑀 − 𝐼)) = 𝑥 ↔ 𝑥 = (𝑦 − (𝑀 − 𝐼)))) |
53 | 31 | zcnd 12112 |
. . . . . 6
⊢ (𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)) → 𝑦 ∈ ℂ) |
54 | 53 | ad2antll 729 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → 𝑦 ∈ ℂ) |
55 | 17 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → 𝑀 ∈ ℂ) |
56 | 18 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → 𝐼 ∈ ℂ) |
57 | 55, 56 | subcld 11020 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → (𝑀 − 𝐼) ∈ ℂ) |
58 | | elfznn 12970 |
. . . . . . 7
⊢ (𝑥 ∈ (1...(𝐼 − 1)) → 𝑥 ∈ ℕ) |
59 | 58 | nncnd 11675 |
. . . . . 6
⊢ (𝑥 ∈ (1...(𝐼 − 1)) → 𝑥 ∈ ℂ) |
60 | 59 | ad2antrl 728 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → 𝑥 ∈ ℂ) |
61 | 54, 57, 60 | subaddd 11038 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → ((𝑦 − (𝑀 − 𝐼)) = 𝑥 ↔ ((𝑀 − 𝐼) + 𝑥) = 𝑦)) |
62 | 52, 61 | bitr3d 284 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → (𝑥 = (𝑦 − (𝑀 − 𝐼)) ↔ ((𝑀 − 𝐼) + 𝑥) = 𝑦)) |
63 | 57, 60 | addcomd 10865 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → ((𝑀 − 𝐼) + 𝑥) = (𝑥 + (𝑀 − 𝐼))) |
64 | 63 | eqeq1d 2761 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → (((𝑀 − 𝐼) + 𝑥) = 𝑦 ↔ (𝑥 + (𝑀 − 𝐼)) = 𝑦)) |
65 | | eqcom 2766 |
. . . . 5
⊢ ((𝑥 + (𝑀 − 𝐼)) = 𝑦 ↔ 𝑦 = (𝑥 + (𝑀 − 𝐼))) |
66 | 65 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → ((𝑥 + (𝑀 − 𝐼)) = 𝑦 ↔ 𝑦 = (𝑥 + (𝑀 − 𝐼)))) |
67 | 64, 66 | bitrd 282 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → (((𝑀 − 𝐼) + 𝑥) = 𝑦 ↔ 𝑦 = (𝑥 + (𝑀 − 𝐼)))) |
68 | 62, 67 | bitrd 282 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(𝐼 − 1)) ∧ 𝑦 ∈ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) → (𝑥 = (𝑦 − (𝑀 − 𝐼)) ↔ 𝑦 = (𝑥 + (𝑀 − 𝐼)))) |
69 | 1, 27, 50, 68 | f1o2d 7388 |
1
⊢ (𝜑 → 𝐹:(1...(𝐼 − 1))–1-1-onto→(((𝑀 − 𝐼) + 1)...(𝑀 − 1))) |