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 ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdwnn.2 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑅 )
vdwnn.3 ⊢ 𝑆 = { 𝑘 ∈ ℕ ∣ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) }
Assertion vdwnnlem2 ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐴 ∈ 𝑆 → 𝐵 ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 vdwnn.1 ⊢ ( 𝜑 → 𝑅 ∈ Fin )
2 vdwnn.2 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑅 )
3 vdwnn.3 ⊢ 𝑆 = { 𝑘 ∈ ℕ ∣ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) }
4 eluzel2 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐴 ∈ ℤ )
5 peano2zm ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 − 1 ) ∈ ℤ )
6 4 5 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 − 1 ) ∈ ℤ )
7 id ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) )
8 4 zcnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐴 ∈ ℂ )
9 ax-1cn ⊢ 1 ∈ ℂ
10 npcan ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 − 1 ) + 1 ) = 𝐴 )
11 8 9 10 sylancl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐴 − 1 ) + 1 ) = 𝐴 )
12 11 fveq2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ℤ≥ ‘ ( ( 𝐴 − 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝐴 ) )
13 7 12 eleqtrrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ( ℤ≥ ‘ ( ( 𝐴 − 1 ) + 1 ) ) )
14 eluzp1m1 ⊢ ( ( ( 𝐴 − 1 ) ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( ( 𝐴 − 1 ) + 1 ) ) ) → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ ( 𝐴 − 1 ) ) )
15 6 13 14 syl2anc ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ ( 𝐴 − 1 ) ) )
16 15 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ ( 𝐴 − 1 ) ) )
17 fzss2 ⊢ ( ( 𝐵 − 1 ) ∈ ( ℤ≥ ‘ ( 𝐴 − 1 ) ) → ( 0 ... ( 𝐴 − 1 ) ) ⊆ ( 0 ... ( 𝐵 − 1 ) ) )
18 ssralv ⊢ ( ( 0 ... ( 𝐴 − 1 ) ) ⊆ ( 0 ... ( 𝐵 − 1 ) ) → ( ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) → ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
19 16 17 18 3syl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ 𝐴 ∈ ℕ ) → ( ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) → ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
20 19 reximdv ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) → ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
21 20 reximdv ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
22 21 con3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ 𝐴 ∈ ℕ ) → ( ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) → ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
23 id ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ )
24 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) )
25 eluznn ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐵 ∈ ℕ )
26 23 24 25 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ 𝐴 ∈ ℕ ) → 𝐵 ∈ ℕ )
27 22 26 jctild ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ 𝐴 ∈ ℕ ) → ( ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) → ( 𝐵 ∈ ℕ ∧ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ) )
28 27 expimpd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝐴 ∈ ℕ ∧ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) → ( 𝐵 ∈ ℕ ∧ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ) )
29 oveq1 ⊢ ( 𝑘 = 𝐴 → ( 𝑘 − 1 ) = ( 𝐴 − 1 ) )
30 29 oveq2d ⊢ ( 𝑘 = 𝐴 → ( 0 ... ( 𝑘 − 1 ) ) = ( 0 ... ( 𝐴 − 1 ) ) )
31 30 raleqdv ⊢ ( 𝑘 = 𝐴 → ( ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
32 31 2rexbidv ⊢ ( 𝑘 = 𝐴 → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
33 32 notbid ⊢ ( 𝑘 = 𝐴 → ( ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
34 33 3 elrab2 ⊢ ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ ℕ ∧ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐴 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
35 oveq1 ⊢ ( 𝑘 = 𝐵 → ( 𝑘 − 1 ) = ( 𝐵 − 1 ) )
36 35 oveq2d ⊢ ( 𝑘 = 𝐵 → ( 0 ... ( 𝑘 − 1 ) ) = ( 0 ... ( 𝐵 − 1 ) ) )
37 36 raleqdv ⊢ ( 𝑘 = 𝐵 → ( ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
38 37 2rexbidv ⊢ ( 𝑘 = 𝐵 → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
39 38 notbid ⊢ ( 𝑘 = 𝐵 → ( ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
40 39 3 elrab2 ⊢ ( 𝐵 ∈ 𝑆 ↔ ( 𝐵 ∈ ℕ ∧ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐵 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
41 28 34 40 3imtr4g ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐴 ∈ 𝑆 → 𝐵 ∈ 𝑆 ) )