Proof of Theorem fzosplitprm1
Step | Hyp | Ref
| Expression |
1 | | simp1 938 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℤ) |
2 | | simp2 939 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℤ) |
3 | | zre 8355 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
4 | | zre 8355 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) |
5 | | ltle 7198 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
6 | 3, 4, 5 | syl2an 283 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
7 | 6 | 3impia 1135 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐴 ≤ 𝐵) |
8 | | eluz2 8625 |
. . . 4
⊢ (𝐵 ∈
(ℤ≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵)) |
9 | 1, 2, 7, 8 | syl3anbrc 1122 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐵 ∈ (ℤ≥‘𝐴)) |
10 | | fzosplitsn 9242 |
. . 3
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → (𝐴..^(𝐵 + 1)) = ((𝐴..^𝐵) ∪ {𝐵})) |
11 | 9, 10 | syl 14 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^(𝐵 + 1)) = ((𝐴..^𝐵) ∪ {𝐵})) |
12 | | zcn 8356 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) |
13 | | ax-1cn 7069 |
. . . . . . 7
⊢ 1 ∈
ℂ |
14 | | npcan 7317 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐵 −
1) + 1) = 𝐵) |
15 | 14 | eqcomd 2086 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 1 ∈
ℂ) → 𝐵 = ((𝐵 − 1) +
1)) |
16 | 12, 13, 15 | sylancl 404 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → 𝐵 = ((𝐵 − 1) + 1)) |
17 | 16 | 3ad2ant2 960 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐵 = ((𝐵 − 1) + 1)) |
18 | 17 | oveq2d 5548 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^𝐵) = (𝐴..^((𝐵 − 1) + 1))) |
19 | | peano2zm 8389 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → (𝐵 − 1) ∈
ℤ) |
20 | 19 | 3ad2ant2 960 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐵 − 1) ∈ ℤ) |
21 | | zltlem1 8408 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ 𝐴 ≤ (𝐵 − 1))) |
22 | 21 | biimp3a 1276 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐴 ≤ (𝐵 − 1)) |
23 | | eluz2 8625 |
. . . . . 6
⊢ ((𝐵 − 1) ∈
(ℤ≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ (𝐵 − 1) ∈ ℤ ∧ 𝐴 ≤ (𝐵 − 1))) |
24 | 1, 20, 22, 23 | syl3anbrc 1122 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐵 − 1) ∈
(ℤ≥‘𝐴)) |
25 | | fzosplitsn 9242 |
. . . . 5
⊢ ((𝐵 − 1) ∈
(ℤ≥‘𝐴) → (𝐴..^((𝐵 − 1) + 1)) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)})) |
26 | 24, 25 | syl 14 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^((𝐵 − 1) + 1)) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)})) |
27 | 18, 26 | eqtrd 2113 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^𝐵) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)})) |
28 | 27 | uneq1d 3125 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → ((𝐴..^𝐵) ∪ {𝐵}) = (((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)}) ∪ {𝐵})) |
29 | | unass 3129 |
. . 3
⊢ (((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)}) ∪ {𝐵}) = ((𝐴..^(𝐵 − 1)) ∪ ({(𝐵 − 1)} ∪ {𝐵})) |
30 | | df-pr 3405 |
. . . . . 6
⊢ {(𝐵 − 1), 𝐵} = ({(𝐵 − 1)} ∪ {𝐵}) |
31 | 30 | eqcomi 2085 |
. . . . 5
⊢ ({(𝐵 − 1)} ∪ {𝐵}) = {(𝐵 − 1), 𝐵} |
32 | 31 | a1i 9 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → ({(𝐵 − 1)} ∪ {𝐵}) = {(𝐵 − 1), 𝐵}) |
33 | 32 | uneq2d 3126 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → ((𝐴..^(𝐵 − 1)) ∪ ({(𝐵 − 1)} ∪ {𝐵})) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1), 𝐵})) |
34 | 29, 33 | syl5eq 2125 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)}) ∪ {𝐵}) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1), 𝐵})) |
35 | 11, 28, 34 | 3eqtrd 2117 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^(𝐵 + 1)) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1), 𝐵})) |