Metamath Proof Explorer

Theorem stoweidlem14

Description: There exists a k as in the proof of Lemma 1 in BrosowskiDeutsh p. 90: k is an integer and 1 < k * δ < 2. D is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem14.1 ⊢ 𝐴 = { 𝑗 ∈ ℕ ∣ ( 1 / 𝐷 ) < 𝑗 }
stoweidlem14.2 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
stoweidlem14.3 ⊢ ( 𝜑 → 𝐷 < 1 )
Assertion stoweidlem14 ( 𝜑 → ∃ 𝑘 ∈ ℕ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem14.1 ⊢ 𝐴 = { 𝑗 ∈ ℕ ∣ ( 1 / 𝐷 ) < 𝑗 }
2 stoweidlem14.2 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
3 stoweidlem14.3 ⊢ ( 𝜑 → 𝐷 < 1 )
4 ssrab2 ⊢ { 𝑗 ∈ ℕ ∣ ( 1 / 𝐷 ) < 𝑗 } ⊆ ℕ
5 4 a1i ⊢ ( 𝜑 → { 𝑗 ∈ ℕ ∣ ( 1 / 𝐷 ) < 𝑗 } ⊆ ℕ )
6 1 5 eqsstrid ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
7 2 rprecred ⊢ ( 𝜑 → ( 1 / 𝐷 ) ∈ ℝ )
8 arch ⊢ ( ( 1 / 𝐷 ) ∈ ℝ → ∃ 𝑘 ∈ ℕ ( 1 / 𝐷 ) < 𝑘 )
9 breq2 ⊢ ( 𝑗 = 𝑘 → ( ( 1 / 𝐷 ) < 𝑗 ↔ ( 1 / 𝐷 ) < 𝑘 ) )
10 9 elrab ⊢ ( 𝑘 ∈ { 𝑗 ∈ ℕ ∣ ( 1 / 𝐷 ) < 𝑗 } ↔ ( 𝑘 ∈ ℕ ∧ ( 1 / 𝐷 ) < 𝑘 ) )
11 10 biimpri ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 1 / 𝐷 ) < 𝑘 ) → 𝑘 ∈ { 𝑗 ∈ ℕ ∣ ( 1 / 𝐷 ) < 𝑗 } )
12 11 1 eleqtrrdi ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 1 / 𝐷 ) < 𝑘 ) → 𝑘 ∈ 𝐴 )
13 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 1 / 𝐷 ) < 𝑘 ) → ( 1 / 𝐷 ) < 𝑘 )
14 12 13 jca ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 1 / 𝐷 ) < 𝑘 ) → ( 𝑘 ∈ 𝐴 ∧ ( 1 / 𝐷 ) < 𝑘 ) )
15 14 reximi2 ⊢ ( ∃ 𝑘 ∈ ℕ ( 1 / 𝐷 ) < 𝑘 → ∃ 𝑘 ∈ 𝐴 ( 1 / 𝐷 ) < 𝑘 )
16 rexn0 ⊢ ( ∃ 𝑘 ∈ 𝐴 ( 1 / 𝐷 ) < 𝑘 → 𝐴 ≠ ∅ )
17 7 8 15 16 4syl ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
18 nnwo ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅ ) → ∃ 𝑘 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 )
19 6 17 18 syl2anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 )
20 df-rex ⊢ ( ∃ 𝑘 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ↔ ∃ 𝑘 ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) )
21 19 20 sylib ⊢ ( 𝜑 → ∃ 𝑘 ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) )
22 9 1 elrab2 ⊢ ( 𝑘 ∈ 𝐴 ↔ ( 𝑘 ∈ ℕ ∧ ( 1 / 𝐷 ) < 𝑘 ) )
23 22 simplbi ⊢ ( 𝑘 ∈ 𝐴 → 𝑘 ∈ ℕ )
24 23 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) → 𝑘 ∈ ℕ )
25 simpl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) → 𝜑 )
26 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) → 𝑘 ∈ 𝐴 )
27 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) → ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 )
28 nfcv ⊢ Ⅎ 𝑧 𝐴
29 nfrab1 ⊢ Ⅎ 𝑗 { 𝑗 ∈ ℕ ∣ ( 1 / 𝐷 ) < 𝑗 }
30 1 29 nfcxfr ⊢ Ⅎ 𝑗 𝐴
31 nfv ⊢ Ⅎ 𝑗 𝑘 ≤ 𝑧
32 nfv ⊢ Ⅎ 𝑧 𝑘 ≤ 𝑗
33 breq2 ⊢ ( 𝑧 = 𝑗 → ( 𝑘 ≤ 𝑧 ↔ 𝑘 ≤ 𝑗 ) )
34 28 30 31 32 33 cbvralfw ⊢ ( ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ↔ ∀ 𝑗 ∈ 𝐴 𝑘 ≤ 𝑗 )
35 27 34 sylib ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) → ∀ 𝑗 ∈ 𝐴 𝑘 ≤ 𝑗 )
36 22 simprbi ⊢ ( 𝑘 ∈ 𝐴 → ( 1 / 𝐷 ) < 𝑘 )
37 36 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑗 ∈ 𝐴 𝑘 ≤ 𝑗 ) ) → ( 1 / 𝐷 ) < 𝑘 )
38 23 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑗 ∈ 𝐴 𝑘 ≤ 𝑗 ) ) → 𝑘 ∈ ℕ )
39 1red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℝ )
40 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ )
42 2 rpregt0d ⊢ ( 𝜑 → ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) )
44 ltdivmul2 ⊢ ( ( 1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( ( 1 / 𝐷 ) < 𝑘 ↔ 1 < ( 𝑘 · 𝐷 ) ) )
45 39 41 43 44 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝐷 ) < 𝑘 ↔ 1 < ( 𝑘 · 𝐷 ) ) )
46 38 45 syldan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑗 ∈ 𝐴 𝑘 ≤ 𝑗 ) ) → ( ( 1 / 𝐷 ) < 𝑘 ↔ 1 < ( 𝑘 · 𝐷 ) ) )
47 37 46 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑗 ∈ 𝐴 𝑘 ≤ 𝑗 ) ) → 1 < ( 𝑘 · 𝐷 ) )
48 25 26 35 47 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) → 1 < ( 𝑘 · 𝐷 ) )
49 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 · 𝐷 ) = ( 1 · 𝐷 ) )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 1 ) → ( 𝑘 · 𝐷 ) = ( 1 · 𝐷 ) )
51 2 rpcnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 1 ) → 𝐷 ∈ ℂ )
53 52 mullidd ⊢ ( ( 𝜑 ∧ 𝑘 = 1 ) → ( 1 · 𝐷 ) = 𝐷 )
54 50 53 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 = 1 ) → ( 𝑘 · 𝐷 ) = 𝐷 )
55 54 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 = 1 ) → ( ( 𝑘 · 𝐷 ) / 2 ) = ( 𝐷 / 2 ) )
56 2 rpred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
57 56 rehalfcld ⊢ ( 𝜑 → ( 𝐷 / 2 ) ∈ ℝ )
58 halfre ⊢ ( 1 / 2 ) ∈ ℝ
59 58 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
60 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
61 2re ⊢ 2 ∈ ℝ
62 61 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
63 2pos ⊢ 0 < 2
64 63 a1i ⊢ ( 𝜑 → 0 < 2 )
65 ltdiv1 ⊢ ( ( 𝐷 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝐷 < 1 ↔ ( 𝐷 / 2 ) < ( 1 / 2 ) ) )
66 56 60 62 64 65 syl112anc ⊢ ( 𝜑 → ( 𝐷 < 1 ↔ ( 𝐷 / 2 ) < ( 1 / 2 ) ) )
67 3 66 mpbid ⊢ ( 𝜑 → ( 𝐷 / 2 ) < ( 1 / 2 ) )
68 halflt1 ⊢ ( 1 / 2 ) < 1
69 68 a1i ⊢ ( 𝜑 → ( 1 / 2 ) < 1 )
70 57 59 60 67 69 lttrd ⊢ ( 𝜑 → ( 𝐷 / 2 ) < 1 )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 1 ) → ( 𝐷 / 2 ) < 1 )
72 55 71 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 = 1 ) → ( ( 𝑘 · 𝐷 ) / 2 ) < 1 )
73 72 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ 𝑘 = 1 ) → ( ( 𝑘 · 𝐷 ) / 2 ) < 1 )
74 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → 𝜑 )
75 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → 𝑘 ∈ 𝐴 )
76 75 23 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → 𝑘 ∈ ℕ )
77 neqne ⊢ ( ¬ 𝑘 = 1 → 𝑘 ≠ 1 )
78 77 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → 𝑘 ≠ 1 )
79 eluz2b3 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≠ 1 ) )
80 76 78 79 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
81 peano2rem ⊢ ( 𝑘 ∈ ℝ → ( 𝑘 − 1 ) ∈ ℝ )
82 75 23 40 81 4syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑘 − 1 ) ∈ ℝ )
83 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → 𝐷 ∈ ℝ )
84 2 rpne0d ⊢ ( 𝜑 → 𝐷 ≠ 0 )
85 84 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → 𝐷 ≠ 0 )
86 83 85 rereccld ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ( 1 / 𝐷 ) ∈ ℝ )
87 1zzd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → 1 ∈ ℤ )
88 df-2 ⊢ 2 = ( 1 + 1 )
89 88 fveq2i ⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( 1 + 1 ) )
90 89 eleq2i ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑘 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
91 eluzsub ⊢ ( ( 1 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
92 90 91 syl3an3b ⊢ ( ( 1 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑘 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
93 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
94 92 93 eleqtrrdi ⊢ ( ( 1 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑘 − 1 ) ∈ ℕ )
95 87 87 80 94 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑘 − 1 ) ∈ ℕ )
96 23 40 syl ⊢ ( 𝑘 ∈ 𝐴 → 𝑘 ∈ ℝ )
97 96 adantl ⊢ ( ( ( 𝑘 − 1 ) ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ℝ )
98 97 81 syl ⊢ ( ( ( 𝑘 − 1 ) ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑘 − 1 ) ∈ ℝ )
99 simpr ⊢ ( ( ( 𝑘 − 1 ) ∈ ℝ ∧ 𝑘 ∈ ℝ ) → 𝑘 ∈ ℝ )
100 99 ltm1d ⊢ ( ( ( 𝑘 − 1 ) ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑘 − 1 ) < 𝑘 )
101 ltnle ⊢ ( ( ( 𝑘 − 1 ) ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝑘 − 1 ) < 𝑘 ↔ ¬ 𝑘 ≤ ( 𝑘 − 1 ) ) )
102 100 101 mpbid ⊢ ( ( ( 𝑘 − 1 ) ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ¬ 𝑘 ≤ ( 𝑘 − 1 ) )
103 98 97 102 syl2anc ⊢ ( ( ( 𝑘 − 1 ) ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ¬ 𝑘 ≤ ( 𝑘 − 1 ) )
104 breq2 ⊢ ( 𝑧 = ( 𝑘 − 1 ) → ( 𝑘 ≤ 𝑧 ↔ 𝑘 ≤ ( 𝑘 − 1 ) ) )
105 104 notbid ⊢ ( 𝑧 = ( 𝑘 − 1 ) → ( ¬ 𝑘 ≤ 𝑧 ↔ ¬ 𝑘 ≤ ( 𝑘 − 1 ) ) )
106 105 rspcev ⊢ ( ( ( 𝑘 − 1 ) ∈ 𝐴 ∧ ¬ 𝑘 ≤ ( 𝑘 − 1 ) ) → ∃ 𝑧 ∈ 𝐴 ¬ 𝑘 ≤ 𝑧 )
107 103 106 syldan ⊢ ( ( ( 𝑘 − 1 ) ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ∃ 𝑧 ∈ 𝐴 ¬ 𝑘 ≤ 𝑧 )
108 rexnal ⊢ ( ∃ 𝑧 ∈ 𝐴 ¬ 𝑘 ≤ 𝑧 ↔ ¬ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 )
109 107 108 sylib ⊢ ( ( ( 𝑘 − 1 ) ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ¬ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 )
110 109 ex ⊢ ( ( 𝑘 − 1 ) ∈ 𝐴 → ( 𝑘 ∈ 𝐴 → ¬ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) )
111 imnan ⊢ ( ( 𝑘 ∈ 𝐴 → ¬ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ↔ ¬ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) )
112 110 111 sylib ⊢ ( ( 𝑘 − 1 ) ∈ 𝐴 → ¬ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) )
113 112 con2i ⊢ ( ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) → ¬ ( 𝑘 − 1 ) ∈ 𝐴 )
114 113 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ¬ ( 𝑘 − 1 ) ∈ 𝐴 )
115 breq2 ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( 1 / 𝐷 ) < 𝑗 ↔ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) ) )
116 115 1 elrab2 ⊢ ( ( 𝑘 − 1 ) ∈ 𝐴 ↔ ( ( 𝑘 − 1 ) ∈ ℕ ∧ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) ) )
117 114 116 sylnib ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ¬ ( ( 𝑘 − 1 ) ∈ ℕ ∧ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) ) )
118 ianor ⊢ ( ¬ ( ( 𝑘 − 1 ) ∈ ℕ ∧ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) ) ↔ ( ¬ ( 𝑘 − 1 ) ∈ ℕ ∨ ¬ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) ) )
119 117 118 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ( ¬ ( 𝑘 − 1 ) ∈ ℕ ∨ ¬ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) ) )
120 imor ⊢ ( ( ( 𝑘 − 1 ) ∈ ℕ → ¬ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) ) ↔ ( ¬ ( 𝑘 − 1 ) ∈ ℕ ∨ ¬ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) ) )
121 119 120 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( 𝑘 − 1 ) ∈ ℕ → ¬ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) ) )
122 95 121 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ¬ ( 1 / 𝐷 ) < ( 𝑘 − 1 ) )
123 82 86 122 nltled ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) )
124 eluzelre ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → 𝑘 ∈ ℝ )
125 124 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑘 ∈ ℝ )
126 56 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐷 ∈ ℝ )
127 125 126 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑘 · 𝐷 ) ∈ ℝ )
128 127 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑘 · 𝐷 ) / 2 ) ∈ ℝ )
129 128 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 𝑘 · 𝐷 ) / 2 ) ∈ ℝ )
130 60 56 readdcld ⊢ ( 𝜑 → ( 1 + 𝐷 ) ∈ ℝ )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 1 + 𝐷 ) ∈ ℝ )
132 131 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 1 + 𝐷 ) / 2 ) ∈ ℝ )
133 132 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 1 + 𝐷 ) / 2 ) ∈ ℝ )
134 1red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → 1 ∈ ℝ )
135 eluzelcn ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → 𝑘 ∈ ℂ )
136 135 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑘 ∈ ℂ )
137 51 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐷 ∈ ℂ )
138 136 137 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑘 · 𝐷 ) ∈ ℂ )
139 138 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 𝑘 · 𝐷 ) ∈ ℂ )
140 51 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → 𝐷 ∈ ℂ )
141 139 140 npcand ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( ( 𝑘 · 𝐷 ) − 𝐷 ) + 𝐷 ) = ( 𝑘 · 𝐷 ) )
142 127 126 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑘 · 𝐷 ) − 𝐷 ) ∈ ℝ )
143 142 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 𝑘 · 𝐷 ) − 𝐷 ) ∈ ℝ )
144 56 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → 𝐷 ∈ ℝ )
145 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) )
146 1red ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ )
147 124 146 resubcld ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑘 − 1 ) ∈ ℝ )
148 147 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 𝑘 − 1 ) ∈ ℝ )
149 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 1 / 𝐷 ) ∈ ℝ )
150 42 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) )
151 lemul1 ⊢ ( ( ( 𝑘 − 1 ) ∈ ℝ ∧ ( 1 / 𝐷 ) ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ↔ ( ( 𝑘 − 1 ) · 𝐷 ) ≤ ( ( 1 / 𝐷 ) · 𝐷 ) ) )
152 148 149 150 151 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ↔ ( ( 𝑘 − 1 ) · 𝐷 ) ≤ ( ( 1 / 𝐷 ) · 𝐷 ) ) )
153 145 152 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 𝑘 − 1 ) · 𝐷 ) ≤ ( ( 1 / 𝐷 ) · 𝐷 ) )
154 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 1 ∈ ℂ )
155 136 154 137 subdird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑘 − 1 ) · 𝐷 ) = ( ( 𝑘 · 𝐷 ) − ( 1 · 𝐷 ) ) )
156 137 mullidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 1 · 𝐷 ) = 𝐷 )
157 156 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑘 · 𝐷 ) − ( 1 · 𝐷 ) ) = ( ( 𝑘 · 𝐷 ) − 𝐷 ) )
158 155 157 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑘 − 1 ) · 𝐷 ) = ( ( 𝑘 · 𝐷 ) − 𝐷 ) )
159 158 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 𝑘 − 1 ) · 𝐷 ) = ( ( 𝑘 · 𝐷 ) − 𝐷 ) )
160 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
161 160 51 84 3jca ⊢ ( 𝜑 → ( 1 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) )
162 161 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 1 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) )
163 divcan1 ⊢ ( ( 1 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) → ( ( 1 / 𝐷 ) · 𝐷 ) = 1 )
164 162 163 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 1 / 𝐷 ) · 𝐷 ) = 1 )
165 153 159 164 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 𝑘 · 𝐷 ) − 𝐷 ) ≤ 1 )
166 143 134 144 165 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( ( 𝑘 · 𝐷 ) − 𝐷 ) + 𝐷 ) ≤ ( 1 + 𝐷 ) )
167 141 166 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 𝑘 · 𝐷 ) ≤ ( 1 + 𝐷 ) )
168 127 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 𝑘 · 𝐷 ) ∈ ℝ )
169 130 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 1 + 𝐷 ) ∈ ℝ )
170 61 63 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
171 170 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
172 lediv1 ⊢ ( ( ( 𝑘 · 𝐷 ) ∈ ℝ ∧ ( 1 + 𝐷 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑘 · 𝐷 ) ≤ ( 1 + 𝐷 ) ↔ ( ( 𝑘 · 𝐷 ) / 2 ) ≤ ( ( 1 + 𝐷 ) / 2 ) ) )
173 168 169 171 172 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 𝑘 · 𝐷 ) ≤ ( 1 + 𝐷 ) ↔ ( ( 𝑘 · 𝐷 ) / 2 ) ≤ ( ( 1 + 𝐷 ) / 2 ) ) )
174 167 173 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 𝑘 · 𝐷 ) / 2 ) ≤ ( ( 1 + 𝐷 ) / 2 ) )
175 56 60 60 3 ltadd2dd ⊢ ( 𝜑 → ( 1 + 𝐷 ) < ( 1 + 1 ) )
176 1p1e2 ⊢ ( 1 + 1 ) = 2
177 175 176 breqtrdi ⊢ ( 𝜑 → ( 1 + 𝐷 ) < 2 )
178 ltdiv1 ⊢ ( ( ( 1 + 𝐷 ) ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 1 + 𝐷 ) < 2 ↔ ( ( 1 + 𝐷 ) / 2 ) < ( 2 / 2 ) ) )
179 130 62 62 64 178 syl112anc ⊢ ( 𝜑 → ( ( 1 + 𝐷 ) < 2 ↔ ( ( 1 + 𝐷 ) / 2 ) < ( 2 / 2 ) ) )
180 177 179 mpbid ⊢ ( 𝜑 → ( ( 1 + 𝐷 ) / 2 ) < ( 2 / 2 ) )
181 2div2e1 ⊢ ( 2 / 2 ) = 1
182 180 181 breqtrdi ⊢ ( 𝜑 → ( ( 1 + 𝐷 ) / 2 ) < 1 )
183 182 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 1 + 𝐷 ) / 2 ) < 1 )
184 129 133 134 174 183 lelttrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑘 − 1 ) ≤ ( 1 / 𝐷 ) ) → ( ( 𝑘 · 𝐷 ) / 2 ) < 1 )
185 74 80 123 184 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( 𝑘 · 𝐷 ) / 2 ) < 1 )
186 73 185 pm2.61dan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) → ( ( 𝑘 · 𝐷 ) / 2 ) < 1 )
187 24 48 186 jca32 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) ) → ( 𝑘 ∈ ℕ ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) )
188 187 ex ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) → ( 𝑘 ∈ ℕ ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) ) )
189 188 eximdv ⊢ ( 𝜑 → ( ∃ 𝑘 ( 𝑘 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝑘 ≤ 𝑧 ) → ∃ 𝑘 ( 𝑘 ∈ ℕ ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) ) )
190 21 189 mpd ⊢ ( 𝜑 → ∃ 𝑘 ( 𝑘 ∈ ℕ ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) )
191 df-rex ⊢ ( ∃ 𝑘 ∈ ℕ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ↔ ∃ 𝑘 ( 𝑘 ∈ ℕ ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) )
192 190 191 sylibr ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℕ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) )