Proof of Theorem vdwnnlem2
| Step | Hyp | Ref
| Expression |
| 1 | | eluzel2 12883 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → 𝐴 ∈ ℤ) |
| 2 | | peano2zm 12660 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℤ) |
| 3 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → (𝐴 − 1) ∈ ℤ) |
| 4 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → 𝐵 ∈ (ℤ≥‘𝐴)) |
| 5 | 1 | zcnd 12723 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → 𝐴 ∈ ℂ) |
| 6 | | ax-1cn 11213 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
| 7 | | npcan 11517 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 −
1) + 1) = 𝐴) |
| 8 | 5, 6, 7 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → ((𝐴 − 1) + 1) = 𝐴) |
| 9 | 8 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
(ℤ≥‘𝐴) →
(ℤ≥‘((𝐴 − 1) + 1)) =
(ℤ≥‘𝐴)) |
| 10 | 4, 9 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → 𝐵 ∈
(ℤ≥‘((𝐴 − 1) + 1))) |
| 11 | | eluzp1m1 12904 |
. . . . . . . . . 10
⊢ (((𝐴 − 1) ∈ ℤ ∧
𝐵 ∈
(ℤ≥‘((𝐴 − 1) + 1))) → (𝐵 − 1) ∈
(ℤ≥‘(𝐴 − 1))) |
| 12 | 3, 10, 11 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → (𝐵 − 1) ∈
(ℤ≥‘(𝐴 − 1))) |
| 13 | 12 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) ∧ 𝐴 ∈ ℕ) → (𝐵 − 1) ∈
(ℤ≥‘(𝐴 − 1))) |
| 14 | | fzss2 13604 |
. . . . . . . 8
⊢ ((𝐵 − 1) ∈
(ℤ≥‘(𝐴 − 1)) → (0...(𝐴 − 1)) ⊆ (0...(𝐵 − 1))) |
| 15 | | ssralv 4052 |
. . . . . . . 8
⊢
((0...(𝐴 − 1))
⊆ (0...(𝐵 − 1))
→ (∀𝑚 ∈
(0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) → ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 16 | 13, 14, 15 | 3syl 18 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) ∧ 𝐴 ∈ ℕ) → (∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) → ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 17 | 16 | reximdv 3170 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) ∧ 𝐴 ∈ ℕ) → (∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) → ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 18 | 17 | reximdv 3170 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) ∧ 𝐴 ∈ ℕ) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 19 | 18 | con3d 152 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) ∧ 𝐴 ∈ ℕ) → (¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) → ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 20 | | id 22 |
. . . . 5
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ) |
| 21 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → 𝐵 ∈ (ℤ≥‘𝐴)) |
| 22 | | eluznn 12960 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → 𝐵 ∈ ℕ) |
| 23 | 20, 21, 22 | syl2anr 597 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) ∧ 𝐴 ∈ ℕ) → 𝐵 ∈ ℕ) |
| 24 | 19, 23 | jctild 525 |
. . 3
⊢ (((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) ∧ 𝐴 ∈ ℕ) → (¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) → (𝐵 ∈ ℕ ∧ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})))) |
| 25 | 24 | expimpd 453 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → ((𝐴 ∈ ℕ ∧ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) → (𝐵 ∈ ℕ ∧ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})))) |
| 26 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑘 = 𝐴 → (𝑘 − 1) = (𝐴 − 1)) |
| 27 | 26 | oveq2d 7447 |
. . . . . 6
⊢ (𝑘 = 𝐴 → (0...(𝑘 − 1)) = (0...(𝐴 − 1))) |
| 28 | 27 | raleqdv 3326 |
. . . . 5
⊢ (𝑘 = 𝐴 → (∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 29 | 28 | 2rexbidv 3222 |
. . . 4
⊢ (𝑘 = 𝐴 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 30 | 29 | notbid 318 |
. . 3
⊢ (𝑘 = 𝐴 → (¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 31 | | vdwnn.3 |
. . 3
⊢ 𝑆 = {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})} |
| 32 | 30, 31 | elrab2 3695 |
. 2
⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℕ ∧ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐴 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 33 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑘 = 𝐵 → (𝑘 − 1) = (𝐵 − 1)) |
| 34 | 33 | oveq2d 7447 |
. . . . . 6
⊢ (𝑘 = 𝐵 → (0...(𝑘 − 1)) = (0...(𝐵 − 1))) |
| 35 | 34 | raleqdv 3326 |
. . . . 5
⊢ (𝑘 = 𝐵 → (∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 36 | 35 | 2rexbidv 3222 |
. . . 4
⊢ (𝑘 = 𝐵 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 37 | 36 | notbid 318 |
. . 3
⊢ (𝑘 = 𝐵 → (¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 38 | 37, 31 | elrab2 3695 |
. 2
⊢ (𝐵 ∈ 𝑆 ↔ (𝐵 ∈ ℕ ∧ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐵 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 39 | 25, 32, 38 | 3imtr4g 296 |
1
⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐴 ∈ 𝑆 → 𝐵 ∈ 𝑆)) |