Proof of Theorem metakunt30
Step | Hyp | Ref
| Expression |
1 | | metakunt30.1 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | | metakunt30.2 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ ℕ) |
3 | | metakunt30.3 |
. . . 4
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
4 | | metakunt30.4 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
5 | | metakunt30.5 |
. . . 4
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
6 | | metakunt30.6 |
. . . 4
⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) |
7 | | metakunt30.7 |
. . . 4
⊢ (𝜑 → ¬ 𝑋 = 𝐼) |
8 | | metakunt30.8 |
. . . 4
⊢ (𝜑 → ¬ 𝑋 < 𝐼) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | metakunt28 39659 |
. . 3
⊢ (𝜑 → (𝐵‘(𝐴‘𝑋)) = (𝑋 − 𝐼)) |
10 | 9 | fveq2d 6655 |
. 2
⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = (𝐶‘(𝑋 − 𝐼))) |
11 | | metakunt30.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 | 2 | nnred 11674 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ ℝ) |
18 | 16, 17 | resubcld 11091 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 − 𝐼) ∈ ℝ) |
19 | 1 | nnred 11674 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
20 | 19, 17 | resubcld 11091 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ) |
21 | | elfzle2 12945 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ≤ 𝑀) |
22 | 4, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ 𝑀) |
23 | 16, 19, 17, 22 | lesub1dd 11279 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 − 𝐼) ≤ (𝑀 − 𝐼)) |
24 | 2 | nnrpd 12455 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈
ℝ+) |
25 | 19, 24 | ltsubrpd 12489 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 𝐼) < 𝑀) |
26 | 18, 20, 19, 23, 25 | lelttrd 10821 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 − 𝐼) < 𝑀) |
27 | 18, 26 | ltned 10799 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 − 𝐼) ≠ 𝑀) |
28 | 27 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼)) → (𝑋 − 𝐼) ≠ 𝑀) |
29 | | neeq1 3011 |
. . . . . . . 8
⊢ (𝑦 = (𝑋 − 𝐼) → (𝑦 ≠ 𝑀 ↔ (𝑋 − 𝐼) ≠ 𝑀)) |
30 | 29 | adantl 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼)) → (𝑦 ≠ 𝑀 ↔ (𝑋 − 𝐼) ≠ 𝑀)) |
31 | 28, 30 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼)) → 𝑦 ≠ 𝑀) |
32 | 31 | neneqd 2954 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼)) → ¬ 𝑦 = 𝑀) |
33 | 32 | iffalsed 4424 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼)) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) |
34 | 17, 18 | lenltd 10809 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐼 ≤ (𝑋 − 𝐼) ↔ ¬ (𝑋 − 𝐼) < 𝐼)) |
35 | 34 | biimpa 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐼 ≤ (𝑋 − 𝐼)) → ¬ (𝑋 − 𝐼) < 𝐼) |
36 | 35 | 3adant2 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → ¬ (𝑋 − 𝐼) < 𝐼) |
37 | | breq1 5028 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋 − 𝐼) → (𝑦 < 𝐼 ↔ (𝑋 − 𝐼) < 𝐼)) |
38 | 37 | 3ad2ant2 1132 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑦 < 𝐼 ↔ (𝑋 − 𝐼) < 𝐼)) |
39 | 36, 38 | mtbird 329 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → ¬ 𝑦 < 𝐼) |
40 | 39 | iffalsed 4424 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = (𝑦 + 1)) |
41 | | simp2 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → 𝑦 = (𝑋 − 𝐼)) |
42 | 41 | oveq1d 7158 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑦 + 1) = ((𝑋 − 𝐼) + 1)) |
43 | | simp3 1136 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → 𝐼 ≤ (𝑋 − 𝐼)) |
44 | 43 | iftrued 4421 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) = 1) |
45 | 44 | eqcomd 2765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → 1 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)) |
46 | | metakunt30.10 |
. . . . . . . . . . . 12
⊢ 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) |
47 | 46 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)) |
48 | 47 | eqcomd 2765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) = 𝐻) |
49 | 45, 48 | eqtrd 2794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → 1 = 𝐻) |
50 | 49 | oveq2d 7159 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → ((𝑋 − 𝐼) + 1) = ((𝑋 − 𝐼) + 𝐻)) |
51 | 42, 50 | eqtrd 2794 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑦 + 1) = ((𝑋 − 𝐼) + 𝐻)) |
52 | 40, 51 | eqtrd 2794 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 − 𝐼) + 𝐻)) |
53 | 52 | 3expa 1116 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 = (𝑋 − 𝐼)) ∧ 𝐼 ≤ (𝑋 − 𝐼)) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 − 𝐼) + 𝐻)) |
54 | | simpr 489 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → ¬ 𝐼 ≤ (𝑋 − 𝐼)) |
55 | 18 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑋 − 𝐼) ∈ ℝ) |
56 | 17 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → 𝐼 ∈ ℝ) |
57 | 55, 56 | ltnled 10810 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → ((𝑋 − 𝐼) < 𝐼 ↔ ¬ 𝐼 ≤ (𝑋 − 𝐼))) |
58 | 54, 57 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑋 − 𝐼) < 𝐼) |
59 | 58 | 3adant2 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑋 − 𝐼) < 𝐼) |
60 | 37 | 3ad2ant2 1132 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑦 < 𝐼 ↔ (𝑋 − 𝐼) < 𝐼)) |
61 | 59, 60 | mpbird 260 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → 𝑦 < 𝐼) |
62 | 61 | iftrued 4421 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = 𝑦) |
63 | | simp2 1135 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → 𝑦 = (𝑋 − 𝐼)) |
64 | | nncn 11667 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℕ → 𝑋 ∈
ℂ) |
65 | 14, 64 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ ℂ) |
66 | 65 | 3ad2ant1 1131 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → 𝑋 ∈ ℂ) |
67 | 2 | nncnd 11675 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ ℂ) |
68 | 67 | 3ad2ant1 1131 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → 𝐼 ∈ ℂ) |
69 | 66, 68 | subcld 11020 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑋 − 𝐼) ∈ ℂ) |
70 | 69 | addid1d 10863 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → ((𝑋 − 𝐼) + 0) = (𝑋 − 𝐼)) |
71 | 70 | eqcomd 2765 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑋 − 𝐼) = ((𝑋 − 𝐼) + 0)) |
72 | 46 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)) |
73 | | simp3 1136 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → ¬ 𝐼 ≤ (𝑋 − 𝐼)) |
74 | 73 | iffalsed 4424 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) = 0) |
75 | 72, 74 | eqtrd 2794 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → 𝐻 = 0) |
76 | 75 | eqcomd 2765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → 0 = 𝐻) |
77 | 76 | oveq2d 7159 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → ((𝑋 − 𝐼) + 0) = ((𝑋 − 𝐼) + 𝐻)) |
78 | 71, 77 | eqtrd 2794 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → (𝑋 − 𝐼) = ((𝑋 − 𝐼) + 𝐻)) |
79 | 63, 78 | eqtrd 2794 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → 𝑦 = ((𝑋 − 𝐼) + 𝐻)) |
80 | 62, 79 | eqtrd 2794 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 − 𝐼) + 𝐻)) |
81 | 80 | 3expa 1116 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 = (𝑋 − 𝐼)) ∧ ¬ 𝐼 ≤ (𝑋 − 𝐼)) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 − 𝐼) + 𝐻)) |
82 | 53, 81 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼)) → if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)) = ((𝑋 − 𝐼) + 𝐻)) |
83 | 33, 82 | eqtrd 2794 |
. . 3
⊢ ((𝜑 ∧ 𝑦 = (𝑋 − 𝐼)) → if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))) = ((𝑋 − 𝐼) + 𝐻)) |
84 | | 1zzd 12037 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
85 | 1 | nnzd 12110 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
86 | 14 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℤ) |
87 | 2 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ ℤ) |
88 | 86, 87 | zsubcld 12116 |
. . . 4
⊢ (𝜑 → (𝑋 − 𝐼) ∈ ℤ) |
89 | | 1m1e0 11731 |
. . . . . 6
⊢ (1
− 1) = 0 |
90 | 17, 16, 8 | nltled 10813 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ≤ 𝑋) |
91 | 7 | neqned 2956 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≠ 𝐼) |
92 | 90, 91 | jca 516 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 ≤ 𝑋 ∧ 𝑋 ≠ 𝐼)) |
93 | 17, 16 | ltlend 10808 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 < 𝑋 ↔ (𝐼 ≤ 𝑋 ∧ 𝑋 ≠ 𝐼))) |
94 | 92, 93 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 → 𝐼 < 𝑋) |
95 | 17, 16 | posdifd 11250 |
. . . . . . 7
⊢ (𝜑 → (𝐼 < 𝑋 ↔ 0 < (𝑋 − 𝐼))) |
96 | 94, 95 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → 0 < (𝑋 − 𝐼)) |
97 | 89, 96 | eqbrtrid 5060 |
. . . . 5
⊢ (𝜑 → (1 − 1) < (𝑋 − 𝐼)) |
98 | | zlem1lt 12058 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ (𝑋
− 𝐼) ∈ ℤ)
→ (1 ≤ (𝑋 −
𝐼) ↔ (1 − 1)
< (𝑋 − 𝐼))) |
99 | 84, 88, 98 | syl2anc 588 |
. . . . 5
⊢ (𝜑 → (1 ≤ (𝑋 − 𝐼) ↔ (1 − 1) < (𝑋 − 𝐼))) |
100 | 97, 99 | mpbird 260 |
. . . 4
⊢ (𝜑 → 1 ≤ (𝑋 − 𝐼)) |
101 | 18, 19, 26 | ltled 10811 |
. . . 4
⊢ (𝜑 → (𝑋 − 𝐼) ≤ 𝑀) |
102 | 84, 85, 88, 100, 101 | elfzd 12932 |
. . 3
⊢ (𝜑 → (𝑋 − 𝐼) ∈ (1...𝑀)) |
103 | | 0zd 12017 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℤ) |
104 | 84, 103 | ifcld 4459 |
. . . . 5
⊢ (𝜑 → if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) ∈ ℤ) |
105 | 46 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)) |
106 | 105 | eleq1d 2835 |
. . . . 5
⊢ (𝜑 → (𝐻 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) ∈ ℤ)) |
107 | 104, 106 | mpbird 260 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ ℤ) |
108 | 88, 107 | zaddcld 12115 |
. . 3
⊢ (𝜑 → ((𝑋 − 𝐼) + 𝐻) ∈ ℤ) |
109 | 12, 83, 102, 108 | fvmptd 6759 |
. 2
⊢ (𝜑 → (𝐶‘(𝑋 − 𝐼)) = ((𝑋 − 𝐼) + 𝐻)) |
110 | 10, 109 | eqtrd 2794 |
1
⊢ (𝜑 → (𝐶‘(𝐵‘(𝐴‘𝑋))) = ((𝑋 − 𝐼) + 𝐻)) |