Proof of Theorem metakunt29
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | metakunt29.1 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 2 |  | metakunt29.2 | . . . 4
⊢ (𝜑 → 𝐼 ∈ ℕ) | 
| 3 |  | metakunt29.3 | . . . 4
⊢ (𝜑 → 𝐼 ≤ 𝑀) | 
| 4 |  | metakunt29.4 | . . . 4
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) | 
| 5 |  | metakunt29.5 | . . . 4
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) | 
| 6 |  | metakunt29.6 | . . . 4
⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) | 
| 7 |  | metakunt29.7 | . . . 4
⊢ (𝜑 → ¬ 𝑋 = 𝐼) | 
| 8 |  | metakunt29.8 | . . . 4
⊢ (𝜑 → 𝑋 < 𝐼) | 
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | metakunt27 42233 | . . 3
⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼))) | 
| 10 | 9 | fveq2d 6909 | . 2
⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = (𝐶‘(𝑋 + (𝑀 − 𝐼)))) | 
| 11 |  | metakunt29.9 | . . . 4
⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) | 
| 12 | 11 | a1i 11 | . . 3
⊢ (𝜑 → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))) | 
| 13 |  | elfznn 13594 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) | 
| 14 | 4, 13 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℕ) | 
| 15 |  | nnre 12274 | . . . . . . . . . . 11
⊢ (𝑋 ∈ ℕ → 𝑋 ∈
ℝ) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 17 | 1 | nnred 12282 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 18 | 2 | nnred 12282 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ ℝ) | 
| 19 | 17, 18 | resubcld 11692 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ) | 
| 20 | 16, 19 | readdcld 11291 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ) | 
| 21 | 16 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 22 | 17 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 23 | 18 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ ℂ) | 
| 24 | 21, 22, 23 | addsub12d 11644 | . . . . . . . . . 10
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) = (𝑀 + (𝑋 − 𝐼))) | 
| 25 | 22, 23, 21 | subsub2d 11650 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) = (𝑀 + (𝑋 − 𝐼))) | 
| 26 | 18, 16 | resubcld 11692 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ) | 
| 27 | 16, 18 | posdifd 11851 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 < 𝐼 ↔ 0 < (𝐼 − 𝑋))) | 
| 28 | 8, 27 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (𝐼 − 𝑋)) | 
| 29 | 26, 28 | elrpd 13075 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 − 𝑋) ∈
ℝ+) | 
| 30 | 17, 29 | ltsubrpd 13110 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) < 𝑀) | 
| 31 | 25, 30 | eqbrtrrd 5166 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀 + (𝑋 − 𝐼)) < 𝑀) | 
| 32 | 24, 31 | eqbrtrd 5164 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) < 𝑀) | 
| 33 | 20, 32 | ltned 11398 | . . . . . . . 8
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀) | 
| 34 | 33 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀) | 
| 35 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼))) | 
| 36 | 35 | neeq1d 2999 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑦 ≠ 𝑀 ↔ (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)) | 
| 37 | 34, 36 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 ≠ 𝑀) | 
| 38 | 37 | neneqd 2944 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 = 𝑀) | 
| 39 | 38 | iffalsed 4535 | . . . 4
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) | 
| 40 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) | 
| 41 | 18 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ∈ ℝ) | 
| 42 | 16 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑋 ∈ ℝ) | 
| 43 | 17 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑀 ∈ ℝ) | 
| 44 | 43, 41 | resubcld 11692 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑀 − 𝐼) ∈ ℝ) | 
| 45 | 42, 44 | readdcld 11291 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ) | 
| 46 | 41, 45 | lenltd 11408 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)) | 
| 47 | 40, 46 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼) | 
| 48 | 47 | 3adant2 1131 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼) | 
| 49 |  | simp2 1137 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼))) | 
| 50 | 49 | breq1d 5152 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼)) | 
| 51 | 50 | notbid 318 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (¬ 𝑦 < 𝐼 ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)) | 
| 52 | 48, 51 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 < 𝐼) | 
| 53 | 52 | iffalsed 4535 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = (𝑦 + 1)) | 
| 54 | 49 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 + 1) = ((𝑋 + (𝑀 − 𝐼)) + 1)) | 
| 55 | 53, 54 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 1)) | 
| 56 |  | simp3 1138 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) | 
| 57 | 56 | iftrued 4532 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 1) | 
| 58 | 57 | eqcomd 2742 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) | 
| 59 |  | metakunt29.10 | . . . . . . . . 9
⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) | 
| 60 | 58, 59 | eqtr4di 2794 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = 𝐻) | 
| 61 | 60 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ((𝑋 + (𝑀 − 𝐼)) + 1) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 62 | 55, 61 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 63 | 62 | 3expa 1118 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 64 | 20, 18 | ltnled 11409 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 ↔ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))) | 
| 65 | 64 | biimprd 248 | . . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)) | 
| 66 | 65 | imp 406 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼) | 
| 67 | 66 | 3adant2 1131 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼) | 
| 68 |  | simp2 1137 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼))) | 
| 69 | 68 | breq1d 5152 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼)) | 
| 70 | 67, 69 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 < 𝐼) | 
| 71 | 70 | iftrued 4532 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = 𝑦) | 
| 72 | 21 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑋 ∈ ℂ) | 
| 73 | 22 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑀 ∈ ℂ) | 
| 74 | 23 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐼 ∈ ℂ) | 
| 75 | 73, 74 | subcld 11621 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑀 − 𝐼) ∈ ℂ) | 
| 76 | 72, 75 | addcld 11281 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) ∈ ℂ) | 
| 77 | 76 | addridd 11462 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = (𝑋 + (𝑀 − 𝐼))) | 
| 78 | 77 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 0)) | 
| 79 | 64 | biimpa 476 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) | 
| 80 | 79 | iffalsed 4535 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 0) | 
| 81 | 80 | eqcomd 2742 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) | 
| 82 | 59 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) | 
| 83 | 82 | eqcomd 2742 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 𝐻) | 
| 84 | 81, 83 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = 𝐻) | 
| 85 | 84 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 86 | 78, 85 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 87 | 86 | ex 412 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))) | 
| 88 | 65, 87 | syld 47 | . . . . . . . . . 10
⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))) | 
| 89 | 88 | imp 406 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 90 | 89 | 3adant2 1131 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 91 | 68, 90 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 92 | 71, 91 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 93 | 92 | 3expa 1118 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 94 | 63, 93 | pm2.61dan 812 | . . . 4
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 95 | 39, 94 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 96 |  | 1zzd 12650 | . . . 4
⊢ (𝜑 → 1 ∈
ℤ) | 
| 97 | 1 | nnzd 12642 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 98 | 14 | nnzd 12642 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ ℤ) | 
| 99 | 2 | nnzd 12642 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 100 | 97, 99 | zsubcld 12729 | . . . . 5
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ) | 
| 101 | 98, 100 | zaddcld 12728 | . . . 4
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ) | 
| 102 |  | 1p0e1 12391 | . . . . 5
⊢ (1 + 0) =
1 | 
| 103 |  | 1red 11263 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) | 
| 104 |  | 0red 11265 | . . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) | 
| 105 | 14 | nnge1d 12315 | . . . . . 6
⊢ (𝜑 → 1 ≤ 𝑋) | 
| 106 | 17, 18 | subge0d 11854 | . . . . . . 7
⊢ (𝜑 → (0 ≤ (𝑀 − 𝐼) ↔ 𝐼 ≤ 𝑀)) | 
| 107 | 3, 106 | mpbird 257 | . . . . . 6
⊢ (𝜑 → 0 ≤ (𝑀 − 𝐼)) | 
| 108 | 103, 104,
16, 19, 105, 107 | le2addd 11883 | . . . . 5
⊢ (𝜑 → (1 + 0) ≤ (𝑋 + (𝑀 − 𝐼))) | 
| 109 | 102, 108 | eqbrtrrid 5178 | . . . 4
⊢ (𝜑 → 1 ≤ (𝑋 + (𝑀 − 𝐼))) | 
| 110 | 20, 17, 32 | ltled 11410 | . . . 4
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≤ 𝑀) | 
| 111 | 96, 97, 101, 109, 110 | elfzd 13556 | . . 3
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ (1...𝑀)) | 
| 112 | 111 | elfzelzd 13566 | . . . 4
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ) | 
| 113 |  | 0zd 12627 | . . . . . 6
⊢ (𝜑 → 0 ∈
ℤ) | 
| 114 | 96, 113 | ifcld 4571 | . . . . 5
⊢ (𝜑 → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ) | 
| 115 | 59 | a1i 11 | . . . . . 6
⊢ (𝜑 → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) | 
| 116 | 115 | eleq1d 2825 | . . . . 5
⊢ (𝜑 → (𝐻 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ)) | 
| 117 | 114, 116 | mpbird 257 | . . . 4
⊢ (𝜑 → 𝐻 ∈ ℤ) | 
| 118 | 112, 117 | zaddcld 12728 | . . 3
⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) + 𝐻) ∈ ℤ) | 
| 119 | 12, 95, 111, 118 | fvmptd 7022 | . 2
⊢ (𝜑 → (𝐶‘(𝑋 + (𝑀 − 𝐼))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) | 
| 120 | 10, 119 | eqtrd 2776 | 1
⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |