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−1a+m⁢d∈F-1c
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−1a+m⁢d∈F-1c
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−1a+m⁢d∈F-1c→∀m∈0…A−1a+m⁢d∈F-1c
19 16 17 18 3syl ⊢φ∧B∈ℤ≥A∧A∈ℕ→∀m∈0…B−1a+m⁢d∈F-1c→∀m∈0…A−1a+m⁢d∈F-1c
20 19 reximdv ⊢φ∧B∈ℤ≥A∧A∈ℕ→∃d∈ℕ∀m∈0…B−1a+m⁢d∈F-1c→∃d∈ℕ∀m∈0…A−1a+m⁢d∈F-1c
21 20 reximdv ⊢φ∧B∈ℤ≥A∧A∈ℕ→∃a∈ℕ∃d∈ℕ∀m∈0…B−1a+m⁢d∈F-1c→∃a∈ℕ∃d∈ℕ∀m∈0…A−1a+m⁢d∈F-1c
22 21 con3d ⊢φ∧B∈ℤ≥A∧A∈ℕ→¬∃a∈ℕ∃d∈ℕ∀m∈0…A−1a+m⁢d∈F-1c→¬∃a∈ℕ∃d∈ℕ∀m∈0…B−1a+m⁢d∈F-1c
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−1a+m⁢d∈F-1c→B∈ℕ∧¬∃a∈ℕ∃d∈ℕ∀m∈0…B−1a+m⁢d∈F-1c
28 27 expimpd ⊢φ∧B∈ℤ≥A→A∈ℕ∧¬∃a∈ℕ∃d∈ℕ∀m∈0…A−1a+m⁢d∈F-1c→B∈ℕ∧¬∃a∈ℕ∃d∈ℕ∀m∈0…B−1a+m⁢d∈F-1c
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−1a+m⁢d∈F-1c↔∀m∈0…A−1a+m⁢d∈F-1c
32 31 2rexbidv ⊢k=A→∃a∈ℕ∃d∈ℕ∀m∈0…k−1a+m⁢d∈F-1c↔∃a∈ℕ∃d∈ℕ∀m∈0…A−1a+m⁢d∈F-1c
33 32 notbid ⊢k=A→¬∃a∈ℕ∃d∈ℕ∀m∈0…k−1a+m⁢d∈F-1c↔¬∃a∈ℕ∃d∈ℕ∀m∈0…A−1a+m⁢d∈F-1c
34 33 3 elrab2 ⊢A∈S↔A∈ℕ∧¬∃a∈ℕ∃d∈ℕ∀m∈0…A−1a+m⁢d∈F-1c
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−1a+m⁢d∈F-1c↔∀m∈0…B−1a+m⁢d∈F-1c
38 37 2rexbidv ⊢k=B→∃a∈ℕ∃d∈ℕ∀m∈0…k−1a+m⁢d∈F-1c↔∃a∈ℕ∃d∈ℕ∀m∈0…B−1a+m⁢d∈F-1c
39 38 notbid ⊢k=B→¬∃a∈ℕ∃d∈ℕ∀m∈0…k−1a+m⁢d∈F-1c↔¬∃a∈ℕ∃d∈ℕ∀m∈0…B−1a+m⁢d∈F-1c
40 39 3 elrab2 ⊢B∈S↔B∈ℕ∧¬∃a∈ℕ∃d∈ℕ∀m∈0…B−1a+m⁢d∈F-1c
41 28 34 40 3imtr4g ⊢φ∧B∈ℤ≥A→A∈S→B∈S