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 − 1 a + m ⁢ d ∈ F -1 c
vdwnn.4 ⊢ φ → ∀ c ∈ R S ≠ ∅
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 − 1 a + m ⁢ d ∈ F -1 c
4 vdwnn.4 ⊢ φ → ∀ c ∈ R S ≠ ∅
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 ≠ ∅ → inf S ℝ < ∈ S
10 7 8 9 sylancr ⊢ φ ∧ c ∈ R → inf S ℝ < ∈ S
11 5 10 sselid ⊢ φ ∧ c ∈ R → inf S ℝ < ∈ ℕ
12 11 nnred ⊢ φ ∧ c ∈ R → inf S ℝ < ∈ ℝ
13 12 ralrimiva ⊢ φ → ∀ c ∈ R inf S ℝ < ∈ ℝ
14 fimaxre3 ⊢ R ∈ Fin ∧ ∀ c ∈ R inf S ℝ < ∈ ℝ → ∃ x ∈ ℝ ∀ c ∈ R inf S ℝ < ≤ x
15 1 13 14 syl2anc ⊢ φ → ∃ x ∈ ℝ ∀ c ∈ R inf S ℝ < ≤ 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 ∈ R inf S ℝ < ≤ x → ∃ c ∈ R inf S ℝ < ≤ x
22 21 ex ⊢ R ≠ ∅ → ∀ c ∈ R inf S ℝ < ≤ x → ∃ c ∈ R inf S ℝ < ≤ x
23 20 22 syl ⊢ φ ∧ x ∈ ℝ → ∀ c ∈ R inf S ℝ < ≤ x → ∃ c ∈ R inf S ℝ < ≤ 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 → inf S ℝ < ∈ ℝ
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 ⊢ inf S ℝ < ∈ ℝ ∧ x ∈ ℝ ∧ x + 1 ∈ ℝ → inf S ℝ < ≤ x ∧ x ≤ x + 1 → inf S ℝ < ≤ x + 1
32 27 24 30 31 syl3anc ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → inf S ℝ < ≤ x ∧ x ≤ x + 1 → inf S ℝ < ≤ x + 1
33 26 32 mpan2d ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → inf S ℝ < ≤ x → inf S ℝ < ≤ x + 1
34 11 adantlr ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → inf S ℝ < ∈ ℕ
35 34 nnzd ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → inf S ℝ < ∈ ℤ
36 eluz ⊢ inf S ℝ < ∈ ℤ ∧ x + 1 ∈ ℤ → x + 1 ∈ ℤ ≥ inf S ℝ < ↔ inf S ℝ < ≤ x + 1
37 35 29 36 syl2anc ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → x + 1 ∈ ℤ ≥ inf S ℝ < ↔ inf S ℝ < ≤ x + 1
38 simpll ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → φ
39 10 adantlr ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → inf S ℝ < ∈ S
40 1 2 3 vdwnnlem2 ⊢ φ ∧ x + 1 ∈ ℤ ≥ inf S ℝ < → inf S ℝ < ∈ S → x + 1 ∈ S
41 40 impancom ⊢ φ ∧ inf S ℝ < ∈ S → x + 1 ∈ ℤ ≥ inf S ℝ < → x + 1 ∈ S
42 38 39 41 syl2anc ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → x + 1 ∈ ℤ ≥ inf S ℝ < → x + 1 ∈ S
43 37 42 sylbird ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → inf S ℝ < ≤ x + 1 → x + 1 ∈ S
44 33 43 syld ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → inf S ℝ < ≤ 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 → inf S ℝ < ≤ x → x + 1 ∈ ℕ 0
48 47 rexlimdva ⊢ φ ∧ x ∈ ℝ → ∃ c ∈ R inf S ℝ < ≤ 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 - 1 a + m ⁢ d ∈ F -1 c
53 49 50 51 52 syl3anc ⊢ φ ∧ x + 1 ∈ ℕ 0 → ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
54 53 ex ⊢ φ → x + 1 ∈ ℕ 0 → ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
55 54 adantr ⊢ φ ∧ x ∈ ℝ → x + 1 ∈ ℕ 0 → ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
56 23 48 55 3syld ⊢ φ ∧ x ∈ ℝ → ∀ c ∈ R inf S ℝ < ≤ x → ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
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 − 1 a + m ⁢ d ∈ F -1 c ↔ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
60 59 2rexbidv ⊢ k = x + 1 → ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
61 60 notbid ⊢ k = x + 1 → ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
62 61 3 elrab2 ⊢ x + 1 ∈ S ↔ x + 1 ∈ ℕ ∧ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
63 62 simprbi ⊢ x + 1 ∈ S → ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
64 44 63 syl6 ⊢ φ ∧ x ∈ ℝ ∧ c ∈ R → inf S ℝ < ≤ x → ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
65 64 ralimdva ⊢ φ ∧ x ∈ ℝ → ∀ c ∈ R inf S ℝ < ≤ x → ∀ c ∈ R ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
66 ralnex ⊢ ∀ c ∈ R ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c ↔ ¬ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
67 65 66 imbitrdi ⊢ φ ∧ x ∈ ℝ → ∀ c ∈ R inf S ℝ < ≤ x → ¬ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … x + 1 - 1 a + m ⁢ d ∈ F -1 c
68 56 67 pm2.65d ⊢ φ ∧ x ∈ ℝ → ¬ ∀ c ∈ R inf S ℝ < ≤ x
69 68 nrexdv ⊢ φ → ¬ ∃ x ∈ ℝ ∀ c ∈ R inf S ℝ < ≤ x
70 15 69 pm2.65i ⊢ ¬ φ