Proof of Theorem ssfzoulel
Step | Hyp | Ref
| Expression |
1 | | simpl2 1058 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → 𝐴 ∈ ℤ) |
2 | | simpl3 1059 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → 𝐵 ∈ ℤ) |
3 | | zre 11258 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
4 | | zre 11258 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) |
5 | | ltnle 9996 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
6 | 3, 4, 5 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
7 | 6 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
8 | 7 | biimpar 501 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → 𝐴 < 𝐵) |
9 | | ssfzo12 12427 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → (0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁))) |
10 | 1, 2, 8, 9 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → (0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁))) |
11 | 4 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈
ℝ) |
12 | | 0red 9920 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 0 ∈
ℝ) |
13 | 3 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈
ℝ) |
14 | | letr 10010 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ ∧ 𝐴 ∈
ℝ) → ((𝐵 ≤ 0
∧ 0 ≤ 𝐴) →
𝐵 ≤ 𝐴)) |
15 | 11, 12, 13, 14 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 0 ∧ 0 ≤ 𝐴) → 𝐵 ≤ 𝐴)) |
16 | 15 | expcomd 453 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ≤
𝐴 → (𝐵 ≤ 0 → 𝐵 ≤ 𝐴))) |
17 | 16 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 0 ≤
𝐴) → (𝐵 ≤ 0 → 𝐵 ≤ 𝐴)) |
18 | 17 | con3d 147 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 0 ≤
𝐴) → (¬ 𝐵 ≤ 𝐴 → ¬ 𝐵 ≤ 0)) |
19 | 18 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ≤
𝐴 → (¬ 𝐵 ≤ 𝐴 → ¬ 𝐵 ≤ 0))) |
20 | 19 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (0 ≤ 𝐴 →
(¬ 𝐵 ≤ 𝐴 → ¬ 𝐵 ≤ 0))) |
21 | 20 | com23 84 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (¬ 𝐵 ≤ 𝐴 → (0 ≤ 𝐴 → ¬ 𝐵 ≤ 0))) |
22 | 21 | imp 444 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → (0 ≤ 𝐴 → ¬ 𝐵 ≤ 0)) |
23 | | nn0re 11178 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
24 | 4, 23, 3 | 3anim123i 1240 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝐵 ∈ ℝ
∧ 𝑁 ∈ ℝ
∧ 𝐴 ∈
ℝ)) |
25 | 24 | 3coml 1264 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐵 ∈ ℝ
∧ 𝑁 ∈ ℝ
∧ 𝐴 ∈
ℝ)) |
26 | | letr 10010 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐵 ≤ 𝑁 ∧ 𝑁 ≤ 𝐴) → 𝐵 ≤ 𝐴)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐵 ≤ 𝑁 ∧ 𝑁 ≤ 𝐴) → 𝐵 ≤ 𝐴)) |
28 | 27 | expdimp 452 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ 𝐵 ≤ 𝑁) → (𝑁 ≤ 𝐴 → 𝐵 ≤ 𝐴)) |
29 | 28 | con3d 147 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ 𝐵 ≤ 𝑁) → (¬ 𝐵 ≤ 𝐴 → ¬ 𝑁 ≤ 𝐴)) |
30 | 29 | impancom 455 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → (𝐵 ≤ 𝑁 → ¬ 𝑁 ≤ 𝐴)) |
31 | 22, 30 | anim12d 584 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁) → (¬ 𝐵 ≤ 0 ∧ ¬ 𝑁 ≤ 𝐴))) |
32 | | ioran 510 |
. . . . . . . 8
⊢ (¬
(𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0) ↔ (¬ 𝑁 ≤ 𝐴 ∧ ¬ 𝐵 ≤ 0)) |
33 | | ancom 465 |
. . . . . . . 8
⊢ ((¬
𝑁 ≤ 𝐴 ∧ ¬ 𝐵 ≤ 0) ↔ (¬ 𝐵 ≤ 0 ∧ ¬ 𝑁 ≤ 𝐴)) |
34 | 32, 33 | bitri 263 |
. . . . . . 7
⊢ (¬
(𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0) ↔ (¬ 𝐵 ≤ 0 ∧ ¬ 𝑁 ≤ 𝐴)) |
35 | 31, 34 | syl6ibr 241 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁) → ¬ (𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0))) |
36 | 10, 35 | syld 46 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → ¬ (𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0))) |
37 | 36 | con2d 128 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0) → ¬ (𝐴..^𝐵) ⊆ (0..^𝑁))) |
38 | 37 | impancom 455 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ (𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ (0..^𝑁))) |
39 | 38 | con4d 113 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ (𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → 𝐵 ≤ 𝐴)) |
40 | 39 | ex 449 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → 𝐵 ≤ 𝐴))) |