Proof of Theorem zsupcllemstep
Step | Hyp | Ref
| Expression |
1 | | eluzelz 9483 |
. . . . 5
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝐾 ∈ ℤ) |
2 | 1 | ad3antrrr 489 |
. . . 4
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) → 𝐾 ∈ ℤ) |
3 | | nfv 1521 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝐾 ∈
(ℤ≥‘𝑀) |
4 | | nfv 1521 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) |
5 | | nfcv 2312 |
. . . . . . . . . 10
⊢
Ⅎ𝑦ℤ |
6 | | nfra1 2501 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 |
7 | | nfra1 2501 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧) |
8 | 6, 7 | nfan 1558 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)) |
9 | 5, 8 | nfrexya 2511 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)) |
10 | 4, 9 | nfim 1565 |
. . . . . . . 8
⊢
Ⅎ𝑦((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
11 | 3, 10 | nfan 1558 |
. . . . . . 7
⊢
Ⅎ𝑦(𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) |
12 | | nfv 1521 |
. . . . . . 7
⊢
Ⅎ𝑦(𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) |
13 | 11, 12 | nfan 1558 |
. . . . . 6
⊢
Ⅎ𝑦((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) |
14 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑦[𝐾 / 𝑛]𝜓 |
15 | 13, 14 | nfan 1558 |
. . . . 5
⊢
Ⅎ𝑦(((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) |
16 | | nfcv 2312 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛ℤ |
17 | 16 | elrabsf 2993 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ↔ (𝑦 ∈ ℤ ∧ [𝑦 / 𝑛]𝜓)) |
18 | 17 | simprbi 273 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} → [𝑦 / 𝑛]𝜓) |
19 | | sbsbc 2959 |
. . . . . . . . 9
⊢ ([𝑦 / 𝑛]𝜓 ↔ [𝑦 / 𝑛]𝜓) |
20 | 18, 19 | sylibr 133 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} → [𝑦 / 𝑛]𝜓) |
21 | 20 | ad2antlr 486 |
. . . . . . 7
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) ∧ 𝐾 < 𝑦) → [𝑦 / 𝑛]𝜓) |
22 | | elrabi 2883 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} → 𝑦 ∈ ℤ) |
23 | | zltp1le 9253 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝐾 < 𝑦 ↔ (𝐾 + 1) ≤ 𝑦)) |
24 | 2, 22, 23 | syl2an 287 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) → (𝐾 < 𝑦 ↔ (𝐾 + 1) ≤ 𝑦)) |
25 | 24 | biimpa 294 |
. . . . . . . . 9
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) ∧ 𝐾 < 𝑦) → (𝐾 + 1) ≤ 𝑦) |
26 | 2 | peano2zd 9324 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) → (𝐾 + 1) ∈ ℤ) |
27 | | eluz 9487 |
. . . . . . . . . . 11
⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑦 ∈
(ℤ≥‘(𝐾 + 1)) ↔ (𝐾 + 1) ≤ 𝑦)) |
28 | 26, 22, 27 | syl2an 287 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) → (𝑦 ∈ (ℤ≥‘(𝐾 + 1)) ↔ (𝐾 + 1) ≤ 𝑦)) |
29 | 28 | adantr 274 |
. . . . . . . . 9
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) ∧ 𝐾 < 𝑦) → (𝑦 ∈ (ℤ≥‘(𝐾 + 1)) ↔ (𝐾 + 1) ≤ 𝑦)) |
30 | 25, 29 | mpbird 166 |
. . . . . . . 8
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) ∧ 𝐾 < 𝑦) → 𝑦 ∈ (ℤ≥‘(𝐾 + 1))) |
31 | | simprr 527 |
. . . . . . . . 9
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) |
32 | 31 | ad3antrrr 489 |
. . . . . . . 8
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) ∧ 𝐾 < 𝑦) → ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) |
33 | | nfs1v 1932 |
. . . . . . . . . 10
⊢
Ⅎ𝑛[𝑦 / 𝑛]𝜓 |
34 | 33 | nfn 1651 |
. . . . . . . . 9
⊢
Ⅎ𝑛 ¬
[𝑦 / 𝑛]𝜓 |
35 | | sbequ12 1764 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑦 → (𝜓 ↔ [𝑦 / 𝑛]𝜓)) |
36 | 35 | notbid 662 |
. . . . . . . . 9
⊢ (𝑛 = 𝑦 → (¬ 𝜓 ↔ ¬ [𝑦 / 𝑛]𝜓)) |
37 | 34, 36 | rspc 2828 |
. . . . . . . 8
⊢ (𝑦 ∈
(ℤ≥‘(𝐾 + 1)) → (∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓 → ¬ [𝑦 / 𝑛]𝜓)) |
38 | 30, 32, 37 | sylc 62 |
. . . . . . 7
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) ∧ 𝐾 < 𝑦) → ¬ [𝑦 / 𝑛]𝜓) |
39 | 21, 38 | pm2.65da 656 |
. . . . . 6
⊢
(((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) → ¬ 𝐾 < 𝑦) |
40 | 39 | ex 114 |
. . . . 5
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) → (𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} → ¬ 𝐾 < 𝑦)) |
41 | 15, 40 | ralrimi 2541 |
. . . 4
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) → ∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝐾 < 𝑦) |
42 | 2 | ad2antrr 485 |
. . . . . . . 8
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 𝐾) → 𝐾 ∈ ℤ) |
43 | | simpllr 529 |
. . . . . . . 8
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 𝐾) → [𝐾 / 𝑛]𝜓) |
44 | 16 | elrabsf 2993 |
. . . . . . . 8
⊢ (𝐾 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ↔ (𝐾 ∈ ℤ ∧ [𝐾 / 𝑛]𝜓)) |
45 | 42, 43, 44 | sylanbrc 415 |
. . . . . . 7
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 𝐾) → 𝐾 ∈ {𝑛 ∈ ℤ ∣ 𝜓}) |
46 | | breq2 3991 |
. . . . . . . 8
⊢ (𝑧 = 𝐾 → (𝑦 < 𝑧 ↔ 𝑦 < 𝐾)) |
47 | 46 | rspcev 2834 |
. . . . . . 7
⊢ ((𝐾 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ∧ 𝑦 < 𝐾) → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧) |
48 | 45, 47 | sylancom 418 |
. . . . . 6
⊢
((((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < 𝐾) → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧) |
49 | 48 | exp31 362 |
. . . . 5
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) → (𝑦 ∈ ℝ → (𝑦 < 𝐾 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
50 | 15, 49 | ralrimi 2541 |
. . . 4
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) → ∀𝑦 ∈ ℝ (𝑦 < 𝐾 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)) |
51 | | breq1 3990 |
. . . . . . . 8
⊢ (𝑥 = 𝐾 → (𝑥 < 𝑦 ↔ 𝐾 < 𝑦)) |
52 | 51 | notbid 662 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝐾 < 𝑦)) |
53 | 52 | ralbidv 2470 |
. . . . . 6
⊢ (𝑥 = 𝐾 → (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝐾 < 𝑦)) |
54 | | breq2 3991 |
. . . . . . . 8
⊢ (𝑥 = 𝐾 → (𝑦 < 𝑥 ↔ 𝑦 < 𝐾)) |
55 | 54 | imbi1d 230 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → ((𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧) ↔ (𝑦 < 𝐾 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
56 | 55 | ralbidv 2470 |
. . . . . 6
⊢ (𝑥 = 𝐾 → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝐾 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
57 | 53, 56 | anbi12d 470 |
. . . . 5
⊢ (𝑥 = 𝐾 → ((∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝐾 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝐾 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) |
58 | 57 | rspcev 2834 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧
(∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝐾 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝐾 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
59 | 2, 41, 50, 58 | syl12anc 1231 |
. . 3
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ [𝐾 / 𝑛]𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
60 | | sbcng 2995 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → ([𝐾 / 𝑛] ¬ 𝜓 ↔ ¬ [𝐾 / 𝑛]𝜓)) |
61 | 60 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → ([𝐾 / 𝑛] ¬ 𝜓 ↔ ¬ [𝐾 / 𝑛]𝜓)) |
62 | 61 | biimpar 295 |
. . . . . 6
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ ¬ [𝐾 / 𝑛]𝜓) → [𝐾 / 𝑛] ¬ 𝜓) |
63 | | sbcsng 3640 |
. . . . . . 7
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → ([𝐾 / 𝑛] ¬ 𝜓 ↔ ∀𝑛 ∈ {𝐾} ¬ 𝜓)) |
64 | 63 | ad3antrrr 489 |
. . . . . 6
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ ¬ [𝐾 / 𝑛]𝜓) → ([𝐾 / 𝑛] ¬ 𝜓 ↔ ∀𝑛 ∈ {𝐾} ¬ 𝜓)) |
65 | 62, 64 | mpbid 146 |
. . . . 5
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ ¬ [𝐾 / 𝑛]𝜓) → ∀𝑛 ∈ {𝐾} ¬ 𝜓) |
66 | | simplrr 531 |
. . . . 5
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ ¬ [𝐾 / 𝑛]𝜓) → ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) |
67 | | uzid 9488 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
(ℤ≥‘𝐾)) |
68 | | peano2uz 9529 |
. . . . . . . . . . 11
⊢ (𝐾 ∈
(ℤ≥‘𝐾) → (𝐾 + 1) ∈
(ℤ≥‘𝐾)) |
69 | 67, 68 | syl 14 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (𝐾 + 1) ∈
(ℤ≥‘𝐾)) |
70 | | fzouzsplit 10122 |
. . . . . . . . . 10
⊢ ((𝐾 + 1) ∈
(ℤ≥‘𝐾) → (ℤ≥‘𝐾) = ((𝐾..^(𝐾 + 1)) ∪
(ℤ≥‘(𝐾 + 1)))) |
71 | 1, 69, 70 | 3syl 17 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝐾) = ((𝐾..^(𝐾 + 1)) ∪
(ℤ≥‘(𝐾 + 1)))) |
72 | | fzosn 10148 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → (𝐾..^(𝐾 + 1)) = {𝐾}) |
73 | 1, 72 | syl 14 |
. . . . . . . . . 10
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾..^(𝐾 + 1)) = {𝐾}) |
74 | 73 | uneq1d 3280 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → ((𝐾..^(𝐾 + 1)) ∪
(ℤ≥‘(𝐾 + 1))) = ({𝐾} ∪ (ℤ≥‘(𝐾 + 1)))) |
75 | 71, 74 | eqtrd 2203 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝐾) = ({𝐾} ∪ (ℤ≥‘(𝐾 + 1)))) |
76 | 75 | raleqdv 2671 |
. . . . . . 7
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓 ↔ ∀𝑛 ∈ ({𝐾} ∪ (ℤ≥‘(𝐾 + 1))) ¬ 𝜓)) |
77 | | ralunb 3308 |
. . . . . . 7
⊢
(∀𝑛 ∈
({𝐾} ∪
(ℤ≥‘(𝐾 + 1))) ¬ 𝜓 ↔ (∀𝑛 ∈ {𝐾} ¬ 𝜓 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) |
78 | 76, 77 | bitrdi 195 |
. . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓 ↔ (∀𝑛 ∈ {𝐾} ¬ 𝜓 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓))) |
79 | 78 | ad3antrrr 489 |
. . . . 5
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ ¬ [𝐾 / 𝑛]𝜓) → (∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓 ↔ (∀𝑛 ∈ {𝐾} ¬ 𝜓 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓))) |
80 | 65, 66, 79 | mpbir2and 939 |
. . . 4
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ ¬ [𝐾 / 𝑛]𝜓) → ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) |
81 | | simprl 526 |
. . . . . 6
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → 𝜑) |
82 | | simplr 525 |
. . . . . 6
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) |
83 | 81, 82 | mpand 427 |
. . . . 5
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → (∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓 → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) |
84 | 83 | adantr 274 |
. . . 4
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ ¬ [𝐾 / 𝑛]𝜓) → (∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓 → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) |
85 | 80, 84 | mpd 13 |
. . 3
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) ∧ ¬ [𝐾 / 𝑛]𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
86 | | zsupcllemstep.dc |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID
𝜓) |
87 | 86 | ralrimiva 2543 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ (ℤ≥‘𝑀)DECID 𝜓) |
88 | 81, 87 | syl 14 |
. . . . 5
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → ∀𝑛 ∈ (ℤ≥‘𝑀)DECID 𝜓) |
89 | | nfsbc1v 2973 |
. . . . . . . 8
⊢
Ⅎ𝑛[𝐾 / 𝑛]𝜓 |
90 | 89 | nfdc 1652 |
. . . . . . 7
⊢
Ⅎ𝑛DECID [𝐾 / 𝑛]𝜓 |
91 | | sbceq1a 2964 |
. . . . . . . 8
⊢ (𝑛 = 𝐾 → (𝜓 ↔ [𝐾 / 𝑛]𝜓)) |
92 | 91 | dcbid 833 |
. . . . . . 7
⊢ (𝑛 = 𝐾 → (DECID 𝜓 ↔ DECID
[𝐾 / 𝑛]𝜓)) |
93 | 90, 92 | rspc 2828 |
. . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (∀𝑛 ∈ (ℤ≥‘𝑀)DECID 𝜓 → DECID
[𝐾 / 𝑛]𝜓)) |
94 | 93 | ad2antrr 485 |
. . . . 5
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → (∀𝑛 ∈ (ℤ≥‘𝑀)DECID 𝜓 → DECID
[𝐾 / 𝑛]𝜓)) |
95 | 88, 94 | mpd 13 |
. . . 4
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → DECID [𝐾 / 𝑛]𝜓) |
96 | | exmiddc 831 |
. . . 4
⊢
(DECID [𝐾 / 𝑛]𝜓 → ([𝐾 / 𝑛]𝜓 ∨ ¬ [𝐾 / 𝑛]𝜓)) |
97 | 95, 96 | syl 14 |
. . 3
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → ([𝐾 / 𝑛]𝜓 ∨ ¬ [𝐾 / 𝑛]𝜓)) |
98 | 59, 85, 97 | mpjaodan 793 |
. 2
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))) ∧ (𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓)) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
99 | 98 | exp31 362 |
1
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) → ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))))) |