Proof of Theorem metakunt2
Step | Hyp | Ref
| Expression |
1 | | eleq1 2838 |
. . 3
⊢ (𝐼 = if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))) → (𝐼 ∈ (1...𝑀) ↔ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))) ∈ (1...𝑀))) |
2 | | eleq1 2838 |
. . 3
⊢ (if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)) = if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))) → (if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)) ∈ (1...𝑀) ↔ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))) ∈ (1...𝑀))) |
3 | | 1zzd 12037 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝑀) → 1 ∈ ℤ) |
4 | | metakunt2.1 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
5 | 4 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | 5 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝑀) → 𝑀 ∈ ℤ) |
7 | | metakunt2.2 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℕ) |
8 | 7 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ ℤ) |
9 | 8 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝑀) → 𝐼 ∈ ℤ) |
10 | 7 | nnge1d 11707 |
. . . . 5
⊢ (𝜑 → 1 ≤ 𝐼) |
11 | 10 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝑀) → 1 ≤ 𝐼) |
12 | | metakunt2.3 |
. . . . 5
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
13 | 12 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝑀) → 𝐼 ≤ 𝑀) |
14 | 3, 6, 9, 11, 13 | elfzd 12932 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝑀) → 𝐼 ∈ (1...𝑀)) |
15 | | eleq1 2838 |
. . . 4
⊢ (𝑥 = if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)) → (𝑥 ∈ (1...𝑀) ↔ if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)) ∈ (1...𝑀))) |
16 | | eleq1 2838 |
. . . 4
⊢ ((𝑥 + 1) = if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)) → ((𝑥 + 1) ∈ (1...𝑀) ↔ if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)) ∈ (1...𝑀))) |
17 | | simpllr 776 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → 𝑥 ∈ (1...𝑀)) |
18 | | 1zzd 12037 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼)) → 1 ∈ ℤ) |
19 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼)) → 𝑀 ∈ ℤ) |
20 | | elfznn 12970 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℕ) |
21 | 20 | nnzd 12110 |
. . . . . . . 8
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℤ) |
22 | 21 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼)) → 𝑥 ∈ ℤ) |
23 | 22 | peano2zd 12114 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼)) → (𝑥 + 1) ∈ ℤ) |
24 | | 0p1e1 11781 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
25 | | 0red 10667 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...𝑀) → 0 ∈ ℝ) |
26 | 20 | nnred 11674 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℝ) |
27 | | 1red 10665 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...𝑀) → 1 ∈ ℝ) |
28 | 20 | nnnn0d 11979 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℕ0) |
29 | 28 | nn0ge0d 11982 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...𝑀) → 0 ≤ 𝑥) |
30 | 25, 26, 27, 29 | leadd1dd 11277 |
. . . . . . . 8
⊢ (𝑥 ∈ (1...𝑀) → (0 + 1) ≤ (𝑥 + 1)) |
31 | 24, 30 | eqbrtrrid 5061 |
. . . . . . 7
⊢ (𝑥 ∈ (1...𝑀) → 1 ≤ (𝑥 + 1)) |
32 | 31 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼)) → 1 ≤ (𝑥 + 1)) |
33 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → 𝑥 ∈ (1...𝑀)) |
34 | | neqne 2957 |
. . . . . . . . . 10
⊢ (¬
𝑥 = 𝑀 → 𝑥 ≠ 𝑀) |
35 | 34 | adantl 486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → 𝑥 ≠ 𝑀) |
36 | 33, 35 | fzne2d 39533 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → 𝑥 < 𝑀) |
37 | 36 | adantrr 717 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼)) → 𝑥 < 𝑀) |
38 | 21 | adantl 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ℤ) |
39 | 5 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝑀 ∈ ℤ) |
40 | 38, 39 | zltp1led 39532 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀)) |
41 | 40 | adantr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼)) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀)) |
42 | 37, 41 | mpbid 235 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼)) → (𝑥 + 1) ≤ 𝑀) |
43 | 18, 19, 23, 32, 42 | elfzd 12932 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ (¬ 𝑥 = 𝑀 ∧ ¬ 𝑥 < 𝐼)) → (𝑥 + 1) ∈ (1...𝑀)) |
44 | 43 | anassrs 472 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → (𝑥 + 1) ∈ (1...𝑀)) |
45 | 15, 16, 17, 44 | ifbothda 4451 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)) ∈ (1...𝑀)) |
46 | 1, 2, 14, 45 | ifbothda 4451 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))) ∈ (1...𝑀)) |
47 | | metakunt2.4 |
. 2
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1)))) |
48 | 46, 47 | fmptd 6862 |
1
⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) |