Proof of Theorem fzosplitprm1
Step | Hyp | Ref
| Expression |
1 | | simp1 992 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℤ) |
2 | | simp2 993 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℤ) |
3 | | zre 9216 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
4 | | zre 9216 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) |
5 | | ltle 8007 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
6 | 3, 4, 5 | syl2an 287 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
7 | 6 | 3impia 1195 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐴 ≤ 𝐵) |
8 | | eluz2 9493 |
. . . 4
⊢ (𝐵 ∈
(ℤ≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵)) |
9 | 1, 2, 7, 8 | syl3anbrc 1176 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐵 ∈ (ℤ≥‘𝐴)) |
10 | | fzosplitsn 10189 |
. . 3
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → (𝐴..^(𝐵 + 1)) = ((𝐴..^𝐵) ∪ {𝐵})) |
11 | 9, 10 | syl 14 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^(𝐵 + 1)) = ((𝐴..^𝐵) ∪ {𝐵})) |
12 | | zcn 9217 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) |
13 | | ax-1cn 7867 |
. . . . . . 7
⊢ 1 ∈
ℂ |
14 | | npcan 8128 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐵 −
1) + 1) = 𝐵) |
15 | 14 | eqcomd 2176 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 1 ∈
ℂ) → 𝐵 = ((𝐵 − 1) +
1)) |
16 | 12, 13, 15 | sylancl 411 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → 𝐵 = ((𝐵 − 1) + 1)) |
17 | 16 | 3ad2ant2 1014 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐵 = ((𝐵 − 1) + 1)) |
18 | 17 | oveq2d 5869 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^𝐵) = (𝐴..^((𝐵 − 1) + 1))) |
19 | | peano2zm 9250 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → (𝐵 − 1) ∈
ℤ) |
20 | 19 | 3ad2ant2 1014 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐵 − 1) ∈ ℤ) |
21 | | zltlem1 9269 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ 𝐴 ≤ (𝐵 − 1))) |
22 | 21 | biimp3a 1340 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → 𝐴 ≤ (𝐵 − 1)) |
23 | | eluz2 9493 |
. . . . . 6
⊢ ((𝐵 − 1) ∈
(ℤ≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ (𝐵 − 1) ∈ ℤ ∧ 𝐴 ≤ (𝐵 − 1))) |
24 | 1, 20, 22, 23 | syl3anbrc 1176 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐵 − 1) ∈
(ℤ≥‘𝐴)) |
25 | | fzosplitsn 10189 |
. . . . 5
⊢ ((𝐵 − 1) ∈
(ℤ≥‘𝐴) → (𝐴..^((𝐵 − 1) + 1)) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)})) |
26 | 24, 25 | syl 14 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^((𝐵 − 1) + 1)) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)})) |
27 | 18, 26 | eqtrd 2203 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^𝐵) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)})) |
28 | 27 | uneq1d 3280 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → ((𝐴..^𝐵) ∪ {𝐵}) = (((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)}) ∪ {𝐵})) |
29 | | unass 3284 |
. . 3
⊢ (((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)}) ∪ {𝐵}) = ((𝐴..^(𝐵 − 1)) ∪ ({(𝐵 − 1)} ∪ {𝐵})) |
30 | | df-pr 3590 |
. . . . . 6
⊢ {(𝐵 − 1), 𝐵} = ({(𝐵 − 1)} ∪ {𝐵}) |
31 | 30 | eqcomi 2174 |
. . . . 5
⊢ ({(𝐵 − 1)} ∪ {𝐵}) = {(𝐵 − 1), 𝐵} |
32 | 31 | a1i 9 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → ({(𝐵 − 1)} ∪ {𝐵}) = {(𝐵 − 1), 𝐵}) |
33 | 32 | uneq2d 3281 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → ((𝐴..^(𝐵 − 1)) ∪ ({(𝐵 − 1)} ∪ {𝐵})) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1), 𝐵})) |
34 | 29, 33 | eqtrid 2215 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)}) ∪ {𝐵}) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1), 𝐵})) |
35 | 11, 28, 34 | 3eqtrd 2207 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → (𝐴..^(𝐵 + 1)) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1), 𝐵})) |