Proof of Theorem metakunt7
| Step | Hyp | Ref
| Expression |
| 1 | | metakunt7.4 |
. . . 4
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
| 2 | 1 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))) |
| 3 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 = 𝐼 ↔ 𝑋 = 𝐼)) |
| 4 | | breq1 5146 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) |
| 5 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
| 6 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 − 1) = (𝑋 − 1)) |
| 7 | 4, 5, 6 | ifbieq12d 4554 |
. . . . . 6
⊢ (𝑥 = 𝑋 → if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
| 8 | 3, 7 | ifbieq2d 4552 |
. . . . 5
⊢ (𝑥 = 𝑋 → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) |
| 9 | 8 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝐼 < 𝑋) ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)))) |
| 10 | | metakunt7.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ ℕ) |
| 11 | 10 | nnred 12281 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ ℝ) |
| 12 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ∈ ℝ) |
| 13 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 < 𝑋) |
| 14 | 12, 13 | ltned 11397 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ≠ 𝑋) |
| 15 | 14 | necomd 2996 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝑋 ≠ 𝐼) |
| 16 | | df-ne 2941 |
. . . . . . . 8
⊢ (𝑋 ≠ 𝐼 ↔ ¬ 𝑋 = 𝐼) |
| 17 | 15, 16 | sylib 218 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ 𝑋 = 𝐼) |
| 18 | | iffalse 4534 |
. . . . . . 7
⊢ (¬
𝑋 = 𝐼 → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
| 19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) |
| 20 | | metakunt7.6 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
| 21 | | elfznn 13593 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℕ) |
| 23 | 22 | nnred 12281 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 24 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝑋 ∈ ℝ) |
| 25 | 12, 24, 13 | ltled 11409 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ≤ 𝑋) |
| 26 | 12, 24 | lenltd 11407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼)) |
| 27 | 25, 26 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ 𝑋 < 𝐼) |
| 28 | | iffalse 4534 |
. . . . . . 7
⊢ (¬
𝑋 < 𝐼 → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = (𝑋 − 1)) |
| 29 | 27, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if(𝑋 < 𝐼, 𝑋, (𝑋 − 1)) = (𝑋 − 1)) |
| 30 | 19, 29 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = (𝑋 − 1)) |
| 31 | 30 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝐼 < 𝑋) ∧ 𝑥 = 𝑋) → if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))) = (𝑋 − 1)) |
| 32 | 9, 31 | eqtrd 2777 |
. . 3
⊢ (((𝜑 ∧ 𝐼 < 𝑋) ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))) = (𝑋 − 1)) |
| 33 | 20 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝑋 ∈ (1...𝑀)) |
| 34 | 33 | elfzelzd 13565 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝑋 ∈ ℤ) |
| 35 | | 1zzd 12648 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 1 ∈ ℤ) |
| 36 | 34, 35 | zsubcld 12727 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝑋 − 1) ∈ ℤ) |
| 37 | 2, 32, 33, 36 | fvmptd 7023 |
. 2
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐴‘𝑋) = (𝑋 − 1)) |
| 38 | | 1red 11262 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
| 39 | 23, 38 | resubcld 11691 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 1) ∈ ℝ) |
| 40 | | elfzle2 13568 |
. . . . . . . 8
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ≤ 𝑀) |
| 41 | 20, 40 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≤ 𝑀) |
| 42 | 20 | elfzelzd 13565 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℤ) |
| 43 | | metakunt7.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 44 | 43 | nnzd 12640 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 45 | | zlem1lt 12669 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑋 ≤ 𝑀 ↔ (𝑋 − 1) < 𝑀)) |
| 46 | 42, 44, 45 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ≤ 𝑀 ↔ (𝑋 − 1) < 𝑀)) |
| 47 | 41, 46 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 1) < 𝑀) |
| 48 | 39, 47 | ltned 11397 |
. . . . 5
⊢ (𝜑 → (𝑋 − 1) ≠ 𝑀) |
| 49 | 48 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝑋 − 1) ≠ 𝑀) |
| 50 | 37, 49 | eqnetrd 3008 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐴‘𝑋) ≠ 𝑀) |
| 51 | 50 | neneqd 2945 |
. 2
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ (𝐴‘𝑋) = 𝑀) |
| 52 | 10 | nnzd 12640 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℤ) |
| 53 | | zltlem1 12670 |
. . . . . . 7
⊢ ((𝐼 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝐼 < 𝑋 ↔ 𝐼 ≤ (𝑋 − 1))) |
| 54 | 53 | biimpd 229 |
. . . . . 6
⊢ ((𝐼 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝐼 < 𝑋 → 𝐼 ≤ (𝑋 − 1))) |
| 55 | 52, 42, 54 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐼 < 𝑋 → 𝐼 ≤ (𝑋 − 1))) |
| 56 | 55 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ≤ (𝑋 − 1)) |
| 57 | 56, 37 | breqtrrd 5171 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → 𝐼 ≤ (𝐴‘𝑋)) |
| 58 | 36 | zred 12722 |
. . . . 5
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝑋 − 1) ∈ ℝ) |
| 59 | 37, 58 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐴‘𝑋) ∈ ℝ) |
| 60 | 12, 59 | lenltd 11407 |
. . 3
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → (𝐼 ≤ (𝐴‘𝑋) ↔ ¬ (𝐴‘𝑋) < 𝐼)) |
| 61 | 57, 60 | mpbid 232 |
. 2
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ¬ (𝐴‘𝑋) < 𝐼) |
| 62 | 37, 51, 61 | 3jca 1129 |
1
⊢ ((𝜑 ∧ 𝐼 < 𝑋) → ((𝐴‘𝑋) = (𝑋 − 1) ∧ ¬ (𝐴‘𝑋) = 𝑀 ∧ ¬ (𝐴‘𝑋) < 𝐼)) |