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 39658 |
. . 3
⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 + (𝑀 − 𝐼))) |
10 | 9 | fveq2d 6655 |
. 2
⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = (𝐶‘(𝑋 + (𝑀 − 𝐼)))) |
11 | | metakunt29.9 |
. . . 4
⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) |
12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))) |
13 | | elfznn 12970 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
14 | 4, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℕ) |
15 | | nnre 11666 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℕ → 𝑋 ∈
ℝ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) |
17 | 1 | nnred 11674 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
18 | 2 | nnred 11674 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ ℝ) |
19 | 17, 18 | resubcld 11091 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ) |
20 | 16, 19 | readdcld 10693 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ) |
21 | 16 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℂ) |
22 | 17 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℂ) |
23 | 18 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ ℂ) |
24 | 21, 22, 23 | addsub12d 11043 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) = (𝑀 + (𝑋 − 𝐼))) |
25 | 22, 23, 21 | subsub2d 11049 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) = (𝑀 + (𝑋 − 𝐼))) |
26 | 18, 16 | resubcld 11091 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼 − 𝑋) ∈ ℝ) |
27 | 16, 18 | posdifd 11250 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 < 𝐼 ↔ 0 < (𝐼 − 𝑋))) |
28 | 8, 27 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (𝐼 − 𝑋)) |
29 | 26, 28 | elrpd 12454 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 − 𝑋) ∈
ℝ+) |
30 | 17, 29 | ltsubrpd 12489 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − (𝐼 − 𝑋)) < 𝑀) |
31 | 25, 30 | eqbrtrrd 5049 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 + (𝑋 − 𝐼)) < 𝑀) |
32 | 24, 31 | eqbrtrd 5047 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) < 𝑀) |
33 | 20, 32 | ltned 10799 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀) |
34 | 33 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀) |
35 | | simpr 489 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼))) |
36 | 35 | neeq1d 3008 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → (𝑦 ≠ 𝑀 ↔ (𝑋 + (𝑀 − 𝐼)) ≠ 𝑀)) |
37 | 34, 36 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → 𝑦 ≠ 𝑀) |
38 | 37 | neneqd 2954 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 = 𝑀) |
39 | 38 | iffalsed 4424 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) |
40 | | simpr 489 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) |
41 | 18 | adantr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ∈ ℝ) |
42 | 16 | adantr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑋 ∈ ℝ) |
43 | 17 | adantr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑀 ∈ ℝ) |
44 | 43, 41 | resubcld 11091 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑀 − 𝐼) ∈ ℝ) |
45 | 42, 44 | readdcld 10693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) ∈ ℝ) |
46 | 41, 45 | lenltd 10809 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)) |
47 | 40, 46 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼) |
48 | 47 | 3adant2 1129 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼) |
49 | | simp2 1135 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼))) |
50 | 49 | breq1d 5035 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼)) |
51 | 50 | notbid 322 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (¬ 𝑦 < 𝐼 ↔ ¬ (𝑋 + (𝑀 − 𝐼)) < 𝐼)) |
52 | 48, 51 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ¬ 𝑦 < 𝐼) |
53 | 52 | iffalsed 4424 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = (𝑦 + 1)) |
54 | 49 | oveq1d 7158 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 + 1) = ((𝑋 + (𝑀 − 𝐼)) + 1)) |
55 | 53, 54 | eqtrd 2794 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 1)) |
56 | | simp3 1136 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) |
57 | 56 | iftrued 4421 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 1) |
58 | 57 | eqcomd 2765 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) |
59 | | metakunt29.10 |
. . . . . . . . 9
⊢ 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) |
60 | 58, 59 | eqtr4di 2812 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 1 = 𝐻) |
61 | 60 | oveq2d 7159 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → ((𝑋 + (𝑀 − 𝐼)) + 1) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
62 | 55, 61 | eqtrd 2794 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
63 | 62 | 3expa 1116 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
64 | 20, 18 | ltnled 10810 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 ↔ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))) |
65 | 64 | biimprd 251 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) < 𝐼)) |
66 | 65 | imp 411 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼) |
67 | 66 | 3adant2 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) < 𝐼) |
68 | | simp2 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = (𝑋 + (𝑀 − 𝐼))) |
69 | 68 | breq1d 5035 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑦 < 𝐼 ↔ (𝑋 + (𝑀 − 𝐼)) < 𝐼)) |
70 | 67, 69 | mpbird 260 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 < 𝐼) |
71 | 70 | iftrued 4421 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = 𝑦) |
72 | 21 | adantr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑋 ∈ ℂ) |
73 | 22 | adantr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝑀 ∈ ℂ) |
74 | 23 | adantr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐼 ∈ ℂ) |
75 | 73, 74 | subcld 11020 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑀 − 𝐼) ∈ ℂ) |
76 | 72, 75 | addcld 10683 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) ∈ ℂ) |
77 | 76 | addid1d 10863 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = (𝑋 + (𝑀 − 𝐼))) |
78 | 77 | eqcomd 2765 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 0)) |
79 | 64 | biimpa 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) |
80 | 79 | iffalsed 4424 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 0) |
81 | 80 | eqcomd 2765 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) |
82 | 59 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) |
83 | 82 | eqcomd 2765 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 𝐻) |
84 | 81, 83 | eqtrd 2794 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → 0 = 𝐻) |
85 | 84 | oveq2d 7159 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → ((𝑋 + (𝑀 − 𝐼)) + 0) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
86 | 78, 85 | eqtrd 2794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 + (𝑀 − 𝐼)) < 𝐼) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
87 | 86 | ex 417 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) < 𝐼 → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))) |
88 | 65, 87 | syld 47 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻))) |
89 | 88 | imp 411 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
90 | 89 | 3adant2 1129 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → (𝑋 + (𝑀 − 𝐼)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
91 | 68, 90 | eqtrd 2794 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → 𝑦 = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
92 | 71, 91 | eqtrd 2794 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
93 | 92 | 3expa 1116 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) ∧ ¬ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
94 | 63, 93 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
95 | 39, 94 | eqtrd 2794 |
. . 3
⊢ ((𝜑 ∧ 𝑦 = (𝑋 + (𝑀 − 𝐼))) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
96 | | 1zzd 12037 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
97 | 1 | nnzd 12110 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
98 | 14 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℤ) |
99 | 2 | nnzd 12110 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℤ) |
100 | 97, 99 | zsubcld 12116 |
. . . . 5
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ) |
101 | 98, 100 | zaddcld 12115 |
. . . 4
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ) |
102 | | 1p0e1 11783 |
. . . . 5
⊢ (1 + 0) =
1 |
103 | | 1red 10665 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
104 | | 0red 10667 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
105 | 14 | nnge1d 11707 |
. . . . . 6
⊢ (𝜑 → 1 ≤ 𝑋) |
106 | 17, 18 | subge0d 11253 |
. . . . . . 7
⊢ (𝜑 → (0 ≤ (𝑀 − 𝐼) ↔ 𝐼 ≤ 𝑀)) |
107 | 3, 106 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝑀 − 𝐼)) |
108 | 103, 104,
16, 19, 105, 107 | le2addd 11282 |
. . . . 5
⊢ (𝜑 → (1 + 0) ≤ (𝑋 + (𝑀 − 𝐼))) |
109 | 102, 108 | eqbrtrrid 5061 |
. . . 4
⊢ (𝜑 → 1 ≤ (𝑋 + (𝑀 − 𝐼))) |
110 | 20, 17, 32 | ltled 10811 |
. . . 4
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ≤ 𝑀) |
111 | 96, 97, 101, 109, 110 | elfzd 12932 |
. . 3
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ (1...𝑀)) |
112 | 111 | elfzelzd 12942 |
. . . 4
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ) |
113 | | 0zd 12017 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℤ) |
114 | 96, 113 | ifcld 4459 |
. . . . 5
⊢ (𝜑 → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ) |
115 | 59 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐻 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) |
116 | 115 | eleq1d 2835 |
. . . . 5
⊢ (𝜑 → (𝐻 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ)) |
117 | 114, 116 | mpbird 260 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ ℤ) |
118 | 112, 117 | zaddcld 12115 |
. . 3
⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) + 𝐻) ∈ ℤ) |
119 | 12, 95, 111, 118 | fvmptd 6759 |
. 2
⊢ (𝜑 → (𝐶‘(𝑋 + (𝑀 − 𝐼))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |
120 | 10, 119 | eqtrd 2794 |
1
⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 + (𝑀 − 𝐼)) + 𝐻)) |