Proof of Theorem ssfzoulel
Step | Hyp | Ref
| Expression |
1 | | simpl2 1194 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → 𝐴 ∈ ℤ) |
2 | | simpl3 1195 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → 𝐵 ∈ ℤ) |
3 | | zre 12180 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
4 | | zre 12180 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) |
5 | | ltnle 10912 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
6 | 3, 4, 5 | syl2an 599 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
7 | 6 | 3adant1 1132 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
8 | 7 | biimpar 481 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → 𝐴 < 𝐵) |
9 | | ssfzo12 13335 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → (0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁))) |
10 | 1, 2, 8, 9 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → (0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁))) |
11 | 4 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈
ℝ) |
12 | | 0red 10836 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 0 ∈
ℝ) |
13 | 3 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈
ℝ) |
14 | | letr 10926 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ ∧ 𝐴 ∈
ℝ) → ((𝐵 ≤ 0
∧ 0 ≤ 𝐴) →
𝐵 ≤ 𝐴)) |
15 | 11, 12, 13, 14 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 0 ∧ 0 ≤ 𝐴) → 𝐵 ≤ 𝐴)) |
16 | 15 | expcomd 420 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ≤
𝐴 → (𝐵 ≤ 0 → 𝐵 ≤ 𝐴))) |
17 | 16 | imp 410 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 0 ≤
𝐴) → (𝐵 ≤ 0 → 𝐵 ≤ 𝐴)) |
18 | 17 | con3d 155 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 0 ≤
𝐴) → (¬ 𝐵 ≤ 𝐴 → ¬ 𝐵 ≤ 0)) |
19 | 18 | ex 416 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ≤
𝐴 → (¬ 𝐵 ≤ 𝐴 → ¬ 𝐵 ≤ 0))) |
20 | 19 | 3adant1 1132 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (0 ≤ 𝐴 →
(¬ 𝐵 ≤ 𝐴 → ¬ 𝐵 ≤ 0))) |
21 | 20 | com23 86 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (¬ 𝐵 ≤ 𝐴 → (0 ≤ 𝐴 → ¬ 𝐵 ≤ 0))) |
22 | 21 | imp 410 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → (0 ≤ 𝐴 → ¬ 𝐵 ≤ 0)) |
23 | | nn0re 12099 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
24 | 4, 23, 3 | 3anim123i 1153 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝐵 ∈ ℝ
∧ 𝑁 ∈ ℝ
∧ 𝐴 ∈
ℝ)) |
25 | 24 | 3coml 1129 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐵 ∈ ℝ
∧ 𝑁 ∈ ℝ
∧ 𝐴 ∈
ℝ)) |
26 | | letr 10926 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐵 ≤ 𝑁 ∧ 𝑁 ≤ 𝐴) → 𝐵 ≤ 𝐴)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐵 ≤ 𝑁 ∧ 𝑁 ≤ 𝐴) → 𝐵 ≤ 𝐴)) |
28 | 27 | expdimp 456 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ 𝐵 ≤ 𝑁) → (𝑁 ≤ 𝐴 → 𝐵 ≤ 𝐴)) |
29 | 28 | con3d 155 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ 𝐵 ≤ 𝑁) → (¬ 𝐵 ≤ 𝐴 → ¬ 𝑁 ≤ 𝐴)) |
30 | 29 | impancom 455 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → (𝐵 ≤ 𝑁 → ¬ 𝑁 ≤ 𝐴)) |
31 | 22, 30 | anim12d 612 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁) → (¬ 𝐵 ≤ 0 ∧ ¬ 𝑁 ≤ 𝐴))) |
32 | | ioran 984 |
. . . . . . . 8
⊢ (¬
(𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0) ↔ (¬ 𝑁 ≤ 𝐴 ∧ ¬ 𝐵 ≤ 0)) |
33 | 32 | biancomi 466 |
. . . . . . 7
⊢ (¬
(𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0) ↔ (¬ 𝐵 ≤ 0 ∧ ¬ 𝑁 ≤ 𝐴)) |
34 | 31, 33 | syl6ibr 255 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((0 ≤ 𝐴 ∧ 𝐵 ≤ 𝑁) → ¬ (𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0))) |
35 | 10, 34 | syld 47 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → ¬ (𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0))) |
36 | 35 | con2d 136 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ ¬ 𝐵 ≤ 𝐴) → ((𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0) → ¬ (𝐴..^𝐵) ⊆ (0..^𝑁))) |
37 | 36 | impancom 455 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ (𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ (0..^𝑁))) |
38 | 37 | con4d 115 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
∧ (𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → 𝐵 ≤ 𝐴)) |
39 | 38 | ex 416 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → 𝐵 ≤ 𝐴))) |