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

Proof

Step Hyp Ref Expression
1 vdwnn.1 ⊢ ( 𝜑 → 𝑅 ∈ Fin )
2 vdwnn.2 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑅 )
3 vdwnn.3 ⊢ 𝑆 = { 𝑘 ∈ ℕ ∣ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) }
4 vdwnn.4 ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝑅 𝑆 ≠ ∅ )
5 3 ssrab3 ⊢ 𝑆 ⊆ ℕ
6 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
7 5 6 sseqtri ⊢ 𝑆 ⊆ ( ℤ≥ ‘ 1 )
8 4 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑅 ) → 𝑆 ≠ ∅ )
9 infssuzcl ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑆 ≠ ∅ ) → inf ( 𝑆 , ℝ , < ) ∈ 𝑆 )
10 7 8 9 sylancr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑅 ) → inf ( 𝑆 , ℝ , < ) ∈ 𝑆 )
11 5 10 sselid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑅 ) → inf ( 𝑆 , ℝ , < ) ∈ ℕ )
12 11 nnred ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑅 ) → inf ( 𝑆 , ℝ , < ) ∈ ℝ )
13 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ∈ ℝ )
14 fimaxre3 ⊢ ( ( 𝑅 ∈ Fin ∧ ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 )
15 1 13 14 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 )
16 1nn ⊢ 1 ∈ ℕ
17 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ 𝑅 ∧ 1 ∈ ℕ ) → ( 𝐹 ‘ 1 ) ∈ 𝑅 )
18 2 16 17 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ 𝑅 )
19 18 ne0d ⊢ ( 𝜑 → 𝑅 ≠ ∅ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑅 ≠ ∅ )
21 r19.2z ⊢ ( ( 𝑅 ≠ ∅ ∧ ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 ) → ∃ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 )
22 21 ex ⊢ ( 𝑅 ≠ ∅ → ( ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → ∃ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 ) )
23 20 22 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → ∃ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 ) )
24 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → 𝑥 ∈ ℝ )
25 fllep1 ⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
26 24 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
27 12 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → inf ( 𝑆 , ℝ , < ) ∈ ℝ )
28 24 flcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
29 28 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℤ )
30 29 zred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ )
31 letr ⊢ ( ( inf ( 𝑆 , ℝ , < ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ) → ( ( inf ( 𝑆 , ℝ , < ) ≤ 𝑥 ∧ 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → inf ( 𝑆 , ℝ , < ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
32 27 24 30 31 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( ( inf ( 𝑆 , ℝ , < ) ≤ 𝑥 ∧ 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → inf ( 𝑆 , ℝ , < ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
33 26 32 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → inf ( 𝑆 , ℝ , < ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
34 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → inf ( 𝑆 , ℝ , < ) ∈ ℕ )
35 34 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → inf ( 𝑆 , ℝ , < ) ∈ ℤ )
36 eluz ⊢ ( ( inf ( 𝑆 , ℝ , < ) ∈ ℤ ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℤ ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ inf ( 𝑆 , ℝ , < ) ) ↔ inf ( 𝑆 , ℝ , < ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
37 35 29 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ inf ( 𝑆 , ℝ , < ) ) ↔ inf ( 𝑆 , ℝ , < ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
38 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → 𝜑 )
39 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → inf ( 𝑆 , ℝ , < ) ∈ 𝑆 )
40 1 2 3 vdwnnlem2 ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ inf ( 𝑆 , ℝ , < ) ) ) → ( inf ( 𝑆 , ℝ , < ) ∈ 𝑆 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ 𝑆 ) )
41 40 impancom ⊢ ( ( 𝜑 ∧ inf ( 𝑆 , ℝ , < ) ∈ 𝑆 ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ inf ( 𝑆 , ℝ , < ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ 𝑆 ) )
42 38 39 41 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ inf ( 𝑆 , ℝ , < ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ 𝑆 ) )
43 37 42 sylbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( inf ( 𝑆 , ℝ , < ) ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ 𝑆 ) )
44 33 43 syld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ 𝑆 ) )
45 5 sseli ⊢ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ 𝑆 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
46 45 nnnn0d ⊢ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ 𝑆 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 )
47 44 46 syl6 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 ) )
48 47 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 ) )
49 1 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 ) → 𝑅 ∈ Fin )
50 2 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 ) → 𝐹 : ℕ ⟶ 𝑅 )
51 simpr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 )
52 vdwnnlem1 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
53 49 50 51 52 syl3anc ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
54 53 ex ⊢ ( 𝜑 → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ0 → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
56 23 48 55 3syld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
57 oveq1 ⊢ ( 𝑘 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 𝑘 − 1 ) = ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) )
58 57 oveq2d ⊢ ( 𝑘 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 0 ... ( 𝑘 − 1 ) ) = ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) )
59 58 raleqdv ⊢ ( 𝑘 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
60 59 2rexbidv ⊢ ( 𝑘 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
61 60 notbid ⊢ ( 𝑘 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
62 61 3 elrab2 ⊢ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ 𝑆 ↔ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ ∧ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
63 62 simprbi ⊢ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ 𝑆 → ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
64 44 63 syl6 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑐 ∈ 𝑅 ) → ( inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
65 64 ralimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → ∀ 𝑐 ∈ 𝑅 ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
66 ralnex ⊢ ( ∀ 𝑐 ∈ 𝑅 ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ¬ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
67 65 66 imbitrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 → ¬ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
68 56 67 pm2.65d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ¬ ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 )
69 68 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑐 ∈ 𝑅 inf ( 𝑆 , ℝ , < ) ≤ 𝑥 )
70 15 69 pm2.65i ⊢ ¬ 𝜑