Metamath Proof Explorer

Theorem vdwnnlem2

Description: Lemma for vdwnn . The set of all "bad" k for the theorem is upwards-closed, because a long AP implies a short AP. (Contributed by Mario Carneiro, 13-Sep-2014)

Ref Expression
Hypotheses vdwnn.1 ⊢ φ → R ∈ Fin
vdwnn.2 ⊢ φ → F : ℕ ⟶ R
vdwnn.3 ⊢ S = k ∈ ℕ | ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c
Assertion vdwnnlem2 ⊢ φ ∧ B ∈ ℤ ≥ A → A ∈ S → B ∈ S

Proof

Step Hyp Ref Expression
1 vdwnn.1 ⊢ φ → R ∈ Fin
2 vdwnn.2 ⊢ φ → F : ℕ ⟶ R
3 vdwnn.3 ⊢ S = k ∈ ℕ | ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c
4 eluzel2 ⊢ B ∈ ℤ ≥ A → A ∈ ℤ
5 peano2zm ⊢ A ∈ ℤ → A − 1 ∈ ℤ
6 4 5 syl ⊢ B ∈ ℤ ≥ A → A − 1 ∈ ℤ
7 id ⊢ B ∈ ℤ ≥ A → B ∈ ℤ ≥ A
8 4 zcnd ⊢ B ∈ ℤ ≥ A → A ∈ ℂ
9 ax-1cn ⊢ 1 ∈ ℂ
10 npcan ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → A - 1 + 1 = A
11 8 9 10 sylancl ⊢ B ∈ ℤ ≥ A → A - 1 + 1 = A
12 11 fveq2d ⊢ B ∈ ℤ ≥ A → ℤ ≥ A - 1 + 1 = ℤ ≥ A
13 7 12 eleqtrrd ⊢ B ∈ ℤ ≥ A → B ∈ ℤ ≥ A - 1 + 1
14 eluzp1m1 ⊢ A − 1 ∈ ℤ ∧ B ∈ ℤ ≥ A - 1 + 1 → B − 1 ∈ ℤ ≥ A − 1
15 6 13 14 syl2anc ⊢ B ∈ ℤ ≥ A → B − 1 ∈ ℤ ≥ A − 1
16 15 ad2antlr ⊢ φ ∧ B ∈ ℤ ≥ A ∧ A ∈ ℕ → B − 1 ∈ ℤ ≥ A − 1
17 fzss2 ⊢ B − 1 ∈ ℤ ≥ A − 1 → 0 … A − 1 ⊆ 0 … B − 1
18 ssralv ⊢ 0 … A − 1 ⊆ 0 … B − 1 → ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c → ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c
19 16 17 18 3syl ⊢ φ ∧ B ∈ ℤ ≥ A ∧ A ∈ ℕ → ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c → ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c
20 19 reximdv ⊢ φ ∧ B ∈ ℤ ≥ A ∧ A ∈ ℕ → ∃ d ∈ ℕ ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c → ∃ d ∈ ℕ ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c
21 20 reximdv ⊢ φ ∧ B ∈ ℤ ≥ A ∧ A ∈ ℕ → ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c → ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c
22 21 con3d ⊢ φ ∧ B ∈ ℤ ≥ A ∧ A ∈ ℕ → ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c → ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c
23 id ⊢ A ∈ ℕ → A ∈ ℕ
24 simpr ⊢ φ ∧ B ∈ ℤ ≥ A → B ∈ ℤ ≥ A
25 eluznn ⊢ A ∈ ℕ ∧ B ∈ ℤ ≥ A → B ∈ ℕ
26 23 24 25 syl2anr ⊢ φ ∧ B ∈ ℤ ≥ A ∧ A ∈ ℕ → B ∈ ℕ
27 22 26 jctild ⊢ φ ∧ B ∈ ℤ ≥ A ∧ A ∈ ℕ → ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c → B ∈ ℕ ∧ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c
28 27 expimpd ⊢ φ ∧ B ∈ ℤ ≥ A → A ∈ ℕ ∧ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c → B ∈ ℕ ∧ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c
29 oveq1 ⊢ k = A → k − 1 = A − 1
30 29 oveq2d ⊢ k = A → 0 … k − 1 = 0 … A − 1
31 30 raleqdv ⊢ k = A → ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c
32 31 2rexbidv ⊢ k = A → ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c
33 32 notbid ⊢ k = A → ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c
34 33 3 elrab2 ⊢ A ∈ S ↔ A ∈ ℕ ∧ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … A − 1 a + m ⁢ d ∈ F -1 c
35 oveq1 ⊢ k = B → k − 1 = B − 1
36 35 oveq2d ⊢ k = B → 0 … k − 1 = 0 … B − 1
37 36 raleqdv ⊢ k = B → ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c
38 37 2rexbidv ⊢ k = B → ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c
39 38 notbid ⊢ k = B → ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c
40 39 3 elrab2 ⊢ B ∈ S ↔ B ∈ ℕ ∧ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … B − 1 a + m ⁢ d ∈ F -1 c
41 28 34 40 3imtr4g ⊢ φ ∧ B ∈ ℤ ≥ A → A ∈ S → B ∈ S