Proof of Theorem metakunt1
| Step | Hyp | Ref
| Expression |
| 1 | | eleq1 2829 |
. . 3
⊢ (𝑀 = if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) → (𝑀 ∈ (1...𝑀) ↔ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) ∈ (1...𝑀))) |
| 2 | | eleq1 2829 |
. . 3
⊢ (if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) → (if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) ∈ (1...𝑀) ↔ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) ∈ (1...𝑀))) |
| 3 | | 1zzd 12648 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝐼) → 1 ∈ ℤ) |
| 4 | | metakunt1.1 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 5 | 4 | nnzd 12640 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 6 | 5 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝐼) → 𝑀 ∈ ℤ) |
| 7 | 4 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝐼) → 𝑀 ∈ ℕ) |
| 8 | 7 | nnge1d 12314 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝐼) → 1 ≤ 𝑀) |
| 9 | 4 | nnred 12281 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 10 | 9 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝐼) → 𝑀 ∈ ℝ) |
| 11 | 10 | leidd 11829 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝐼) → 𝑀 ≤ 𝑀) |
| 12 | 3, 6, 6, 8, 11 | elfzd 13555 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝐼) → 𝑀 ∈ (1...𝑀)) |
| 13 | | eleq1 2829 |
. . . 4
⊢ (𝑥 = if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) → (𝑥 ∈ (1...𝑀) ↔ if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) ∈ (1...𝑀))) |
| 14 | | eleq1 2829 |
. . . 4
⊢ ((𝑥 − 1) = if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) → ((𝑥 − 1) ∈ (1...𝑀) ↔ if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) ∈ (1...𝑀))) |
| 15 | | simpllr 776 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝐼) ∧ 𝑥 < 𝐼) → 𝑥 ∈ (1...𝑀)) |
| 16 | | pm4.56 991 |
. . . . . . 7
⊢ ((¬
𝑥 = 𝐼 ∧ ¬ 𝑥 < 𝐼) ↔ ¬ (𝑥 = 𝐼 ∨ 𝑥 < 𝐼)) |
| 17 | 16 | anbi2i 623 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝐼 ∧ ¬ 𝑥 < 𝐼)) ↔ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ (𝑥 = 𝐼 ∨ 𝑥 < 𝐼))) |
| 18 | | metakunt1.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ ℕ) |
| 19 | 18 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ ℝ) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝐼 ∈ ℝ) |
| 21 | | elfznn 13593 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℕ) |
| 22 | 21 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℝ) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ℝ) |
| 24 | 20, 23 | jca 511 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → (𝐼 ∈ ℝ ∧ 𝑥 ∈ ℝ)) |
| 25 | | axlttri 11332 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐼 < 𝑥 ↔ ¬ (𝐼 = 𝑥 ∨ 𝑥 < 𝐼))) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → (𝐼 < 𝑥 ↔ ¬ (𝐼 = 𝑥 ∨ 𝑥 < 𝐼))) |
| 27 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (𝐼 = 𝑥 ↔ 𝑥 = 𝐼) |
| 28 | 27 | orbi1i 914 |
. . . . . . . . . 10
⊢ ((𝐼 = 𝑥 ∨ 𝑥 < 𝐼) ↔ (𝑥 = 𝐼 ∨ 𝑥 < 𝐼)) |
| 29 | 28 | notbii 320 |
. . . . . . . . 9
⊢ (¬
(𝐼 = 𝑥 ∨ 𝑥 < 𝐼) ↔ ¬ (𝑥 = 𝐼 ∨ 𝑥 < 𝐼)) |
| 30 | 26, 29 | bitrdi 287 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → (𝐼 < 𝑥 ↔ ¬ (𝑥 = 𝐼 ∨ 𝑥 < 𝐼))) |
| 31 | | 1zzd 12648 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 1 ∈ ℤ) |
| 32 | 5 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 𝑀 ∈ ℤ) |
| 33 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 𝑥 ∈ (1...𝑀)) |
| 34 | 33 | elfzelzd 13565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 𝑥 ∈ ℤ) |
| 35 | 34, 31 | zsubcld 12727 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → (𝑥 − 1) ∈ ℤ) |
| 36 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 1 ∈ ℝ) |
| 37 | 20 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 𝐼 ∈ ℝ) |
| 38 | 33, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 𝑥 ∈ ℝ) |
| 39 | 18 | nnge1d 12314 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ≤ 𝐼) |
| 40 | 39 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 1 ≤ 𝐼) |
| 41 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 𝐼 < 𝑥) |
| 42 | 36, 37, 38, 40, 41 | lelttrd 11419 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 1 < 𝑥) |
| 43 | 31, 34 | zltlem1d 12671 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → (1 < 𝑥 ↔ 1 ≤ (𝑥 − 1))) |
| 44 | 42, 43 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → 1 ≤ (𝑥 − 1)) |
| 45 | | 1red 11262 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 1 ∈ ℝ) |
| 46 | 23, 45 | resubcld 11691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → (𝑥 − 1) ∈ ℝ) |
| 47 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝑀 ∈ ℝ) |
| 48 | | 0le1 11786 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
| 49 | 48 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...𝑀) → 0 ≤ 1) |
| 50 | | 1red 11262 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝑀) → 1 ∈ ℝ) |
| 51 | 22, 50 | subge02d 11855 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...𝑀) → (0 ≤ 1 ↔ (𝑥 − 1) ≤ 𝑥)) |
| 52 | 49, 51 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑀) → (𝑥 − 1) ≤ 𝑥) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → (𝑥 − 1) ≤ 𝑥) |
| 54 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ≤ 𝑀) |
| 55 | 54 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ≤ 𝑀) |
| 56 | 46, 23, 47, 53, 55 | letrd 11418 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → (𝑥 − 1) ≤ 𝑀) |
| 57 | 56 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → (𝑥 − 1) ≤ 𝑀) |
| 58 | 31, 32, 35, 44, 57 | elfzd 13555 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀) ∧ 𝐼 < 𝑥) → (𝑥 − 1) ∈ (1...𝑀)) |
| 59 | 58 | 3expia 1122 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → (𝐼 < 𝑥 → (𝑥 − 1) ∈ (1...𝑀))) |
| 60 | 30, 59 | sylbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → (¬ (𝑥 = 𝐼 ∨ 𝑥 < 𝐼) → (𝑥 − 1) ∈ (1...𝑀))) |
| 61 | 60 | imp 406 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ (𝑥 = 𝐼 ∨ 𝑥 < 𝐼)) → (𝑥 − 1) ∈ (1...𝑀)) |
| 62 | 17, 61 | sylbi 217 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝐼 ∧ ¬ 𝑥 < 𝐼)) → (𝑥 − 1) ∈ (1...𝑀)) |
| 63 | 62 | anassrs 467 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝐼) ∧ ¬ 𝑥 < 𝐼) → (𝑥 − 1) ∈ (1...𝑀)) |
| 64 | 13, 14, 15, 63 | ifbothda 4564 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝐼) → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) ∈ (1...𝑀)) |
| 65 | 1, 2, 12, 64 | ifbothda 4564 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) ∈ (1...𝑀)) |
| 66 | | metakunt1.4 |
. 2
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
| 67 | 65, 66 | fmptd 7134 |
1
⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) |