Metamath Proof Explorer

Theorem vdwnnlem3

Description: Lemma for vdwnn . (Contributed by Mario Carneiro, 13-Sep-2014) (Proof shortened by AV, 27-Sep-2020)

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
vdwnn.4 ⊢φ→∀c∈RS≠∅
Assertion vdwnnlem3 ⊢¬φ

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 vdwnn.4 ⊢φ→∀c∈RS≠∅
5 3 ssrab3 ⊢S⊆ℕ
6 nnuz ⊢ℕ=ℤ≥1
7 5 6 sseqtri ⊢S⊆ℤ≥1
8 4 r19.21bi ⊢φ∧c∈R→S≠∅
9 infssuzcl ⊢S⊆ℤ≥1∧S≠∅→supSℝ<∈S
10 7 8 9 sylancr ⊢φ∧c∈R→supSℝ<∈S
11 5 10 sselid ⊢φ∧c∈R→supSℝ<∈ℕ
12 11 nnred ⊢φ∧c∈R→supSℝ<∈ℝ
13 12 ralrimiva ⊢φ→∀c∈RsupSℝ<∈ℝ
14 fimaxre3 ⊢R∈Fin∧∀c∈RsupSℝ<∈ℝ→∃x∈ℝ∀c∈RsupSℝ<≤x
15 1 13 14 syl2anc ⊢φ→∃x∈ℝ∀c∈RsupSℝ<≤x
16 1nn ⊢1∈ℕ
17 ffvelcdm ⊢F:ℕ⟶R∧1∈ℕ→F⁡1∈R
18 2 16 17 sylancl ⊢φ→F⁡1∈R
19 18 ne0d ⊢φ→R≠∅
20 19 adantr ⊢φ∧x∈ℝ→R≠∅
21 r19.2z ⊢R≠∅∧∀c∈RsupSℝ<≤x→∃c∈RsupSℝ<≤x
22 21 ex ⊢R≠∅→∀c∈RsupSℝ<≤x→∃c∈RsupSℝ<≤x
23 20 22 syl ⊢φ∧x∈ℝ→∀c∈RsupSℝ<≤x→∃c∈RsupSℝ<≤x
24 simplr ⊢φ∧x∈ℝ∧c∈R→x∈ℝ
25 fllep1 ⊢x∈ℝ→x≤x+1
26 24 25 syl ⊢φ∧x∈ℝ∧c∈R→x≤x+1
27 12 adantlr ⊢φ∧x∈ℝ∧c∈R→supSℝ<∈ℝ
28 24 flcld ⊢φ∧x∈ℝ∧c∈R→x∈ℤ
29 28 peano2zd ⊢φ∧x∈ℝ∧c∈R→x+1∈ℤ
30 29 zred ⊢φ∧x∈ℝ∧c∈R→x+1∈ℝ
31 letr ⊢supSℝ<∈ℝ∧x∈ℝ∧x+1∈ℝ→supSℝ<≤x∧x≤x+1→supSℝ<≤x+1
32 27 24 30 31 syl3anc ⊢φ∧x∈ℝ∧c∈R→supSℝ<≤x∧x≤x+1→supSℝ<≤x+1
33 26 32 mpan2d ⊢φ∧x∈ℝ∧c∈R→supSℝ<≤x→supSℝ<≤x+1
34 11 adantlr ⊢φ∧x∈ℝ∧c∈R→supSℝ<∈ℕ
35 34 nnzd ⊢φ∧x∈ℝ∧c∈R→supSℝ<∈ℤ
36 eluz ⊢supSℝ<∈ℤ∧x+1∈ℤ→x+1∈ℤ≥supSℝ<↔supSℝ<≤x+1
37 35 29 36 syl2anc ⊢φ∧x∈ℝ∧c∈R→x+1∈ℤ≥supSℝ<↔supSℝ<≤x+1
38 simpll ⊢φ∧x∈ℝ∧c∈R→φ
39 10 adantlr ⊢φ∧x∈ℝ∧c∈R→supSℝ<∈S
40 1 2 3 vdwnnlem2 ⊢φ∧x+1∈ℤ≥supSℝ<→supSℝ<∈S→x+1∈S
41 40 impancom ⊢φ∧supSℝ<∈S→x+1∈ℤ≥supSℝ<→x+1∈S
42 38 39 41 syl2anc ⊢φ∧x∈ℝ∧c∈R→x+1∈ℤ≥supSℝ<→x+1∈S
43 37 42 sylbird ⊢φ∧x∈ℝ∧c∈R→supSℝ<≤x+1→x+1∈S
44 33 43 syld ⊢φ∧x∈ℝ∧c∈R→supSℝ<≤x→x+1∈S
45 5 sseli ⊢x+1∈S→x+1∈ℕ
46 45 nnnn0d ⊢x+1∈S→x+1∈ℕ0
47 44 46 syl6 ⊢φ∧x∈ℝ∧c∈R→supSℝ<≤x→x+1∈ℕ0
48 47 rexlimdva ⊢φ∧x∈ℝ→∃c∈RsupSℝ<≤x→x+1∈ℕ0
49 1 adantr ⊢φ∧x+1∈ℕ0→R∈Fin
50 2 adantr ⊢φ∧x+1∈ℕ0→F:ℕ⟶R
51 simpr ⊢φ∧x+1∈ℕ0→x+1∈ℕ0
52 vdwnnlem1 ⊢R∈Fin∧F:ℕ⟶R∧x+1∈ℕ0→∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
53 49 50 51 52 syl3anc ⊢φ∧x+1∈ℕ0→∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
54 53 ex ⊢φ→x+1∈ℕ0→∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
55 54 adantr ⊢φ∧x∈ℝ→x+1∈ℕ0→∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
56 23 48 55 3syld ⊢φ∧x∈ℝ→∀c∈RsupSℝ<≤x→∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
57 oveq1 ⊢k=x+1→k−1=x+1-1
58 57 oveq2d ⊢k=x+1→0…k−1=0…x+1-1
59 58 raleqdv ⊢k=x+1→∀m∈0…k−1a+m⁢d∈F-1c↔∀m∈0…x+1-1a+m⁢d∈F-1c
60 59 2rexbidv ⊢k=x+1→∃a∈ℕ∃d∈ℕ∀m∈0…k−1a+m⁢d∈F-1c↔∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
61 60 notbid ⊢k=x+1→¬∃a∈ℕ∃d∈ℕ∀m∈0…k−1a+m⁢d∈F-1c↔¬∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
62 61 3 elrab2 ⊢x+1∈S↔x+1∈ℕ∧¬∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
63 62 simprbi ⊢x+1∈S→¬∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
64 44 63 syl6 ⊢φ∧x∈ℝ∧c∈R→supSℝ<≤x→¬∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
65 64 ralimdva ⊢φ∧x∈ℝ→∀c∈RsupSℝ<≤x→∀c∈R¬∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
66 ralnex ⊢∀c∈R¬∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c↔¬∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
67 65 66 imbitrdi ⊢φ∧x∈ℝ→∀c∈RsupSℝ<≤x→¬∃c∈R∃a∈ℕ∃d∈ℕ∀m∈0…x+1-1a+m⁢d∈F-1c
68 56 67 pm2.65d ⊢φ∧x∈ℝ→¬∀c∈RsupSℝ<≤x
69 68 nrexdv ⊢φ→¬∃x∈ℝ∀c∈RsupSℝ<≤x
70 15 69 pm2.65i ⊢¬φ