Metamath Proof Explorer

Theorem lcmineqlem23

Description: Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem23.1 ⊢ φ → N ∈ ℕ
lcmineqlem23.2 ⊢ φ → 9 ≤ N
Assertion lcmineqlem23 ⊢ φ → 2 N ≤ lcm _ ⁡ 1 … N

Proof

Step Hyp Ref Expression
1 lcmineqlem23.1 ⊢ φ → N ∈ ℕ
2 lcmineqlem23.2 ⊢ φ → 9 ≤ N
3 2nn ⊢ 2 ∈ ℕ
4 3 a1i ⊢ φ → 2 ∈ ℕ
5 1 4 jca ⊢ φ → N ∈ ℕ ∧ 2 ∈ ℕ
6 nndivdvds ⊢ N ∈ ℕ ∧ 2 ∈ ℕ → 2 ∥ N ↔ N 2 ∈ ℕ
7 5 6 syl ⊢ φ → 2 ∥ N ↔ N 2 ∈ ℕ
8 7 biimpa ⊢ φ ∧ 2 ∥ N → N 2 ∈ ℕ
9 8 nnzd ⊢ φ ∧ 2 ∥ N → N 2 ∈ ℤ
10 1zzd ⊢ φ ∧ 2 ∥ N → 1 ∈ ℤ
11 9 10 zsubcld ⊢ φ ∧ 2 ∥ N → N 2 − 1 ∈ ℤ
12 0red ⊢ φ ∧ 2 ∥ N → 0 ∈ ℝ
13 4re ⊢ 4 ∈ ℝ
14 13 a1i ⊢ φ ∧ 2 ∥ N → 4 ∈ ℝ
15 8 nnred ⊢ φ ∧ 2 ∥ N → N 2 ∈ ℝ
16 1red ⊢ φ ∧ 2 ∥ N → 1 ∈ ℝ
17 15 16 resubcld ⊢ φ ∧ 2 ∥ N → N 2 − 1 ∈ ℝ
18 4pos ⊢ 0 < 4
19 18 a1i ⊢ φ ∧ 2 ∥ N → 0 < 4
20 5m1e4 ⊢ 5 − 1 = 4
21 5re ⊢ 5 ∈ ℝ
22 21 a1i ⊢ φ ∧ 2 ∥ N → 5 ∈ ℝ
23 3 nncni ⊢ 2 ∈ ℂ
24 5cn ⊢ 5 ∈ ℂ
25 23 24 mulcomi ⊢ 2 ⋅ 5 = 5 ⋅ 2
26 5t2e10 ⊢ 5 ⋅ 2 = 10
27 25 26 eqtri ⊢ 2 ⋅ 5 = 10
28 10re ⊢ 10 ∈ ℝ
29 28 recni ⊢ 10 ∈ ℂ
30 3 nnne0i ⊢ 2 ≠ 0
31 29 23 24 30 divmuli ⊢ 10 2 = 5 ↔ 2 ⋅ 5 = 10
32 27 31 mpbir ⊢ 10 2 = 5
33 28 a1i ⊢ φ ∧ 2 ∥ N → 10 ∈ ℝ
34 1 nnred ⊢ φ → N ∈ ℝ
35 34 adantr ⊢ φ ∧ 2 ∥ N → N ∈ ℝ
36 2rp ⊢ 2 ∈ ℝ +
37 36 a1i ⊢ φ ∧ 2 ∥ N → 2 ∈ ℝ +
38 9p1e10 ⊢ 9 + 1 = 10
39 9re ⊢ 9 ∈ ℝ
40 39 a1i ⊢ φ → 9 ∈ ℝ
41 40 34 leloed ⊢ φ → 9 ≤ N ↔ 9 < N ∨ 9 = N
42 2 41 mpbid ⊢ φ → 9 < N ∨ 9 = N
43 42 adantr ⊢ φ ∧ 2 ∥ N → 9 < N ∨ 9 = N
44 4cn ⊢ 4 ∈ ℂ
45 23 44 mulcomi ⊢ 2 ⋅ 4 = 4 ⋅ 2
46 4t2e8 ⊢ 4 ⋅ 2 = 8
47 45 46 eqtri ⊢ 2 ⋅ 4 = 8
48 8re ⊢ 8 ∈ ℝ
49 48 recni ⊢ 8 ∈ ℂ
50 49 23 44 30 divmuli ⊢ 8 2 = 4 ↔ 2 ⋅ 4 = 8
51 47 50 mpbir ⊢ 8 2 = 4
52 4nn ⊢ 4 ∈ ℕ
53 51 52 eqeltri ⊢ 8 2 ∈ ℕ
54 8nn ⊢ 8 ∈ ℕ
55 nndivdvds ⊢ 8 ∈ ℕ ∧ 2 ∈ ℕ → 2 ∥ 8 ↔ 8 2 ∈ ℕ
56 54 3 55 mp2an ⊢ 2 ∥ 8 ↔ 8 2 ∈ ℕ
57 53 56 mpbir ⊢ 2 ∥ 8
58 9m1e8 ⊢ 9 − 1 = 8
59 57 58 breqtrri ⊢ 2 ∥ 9 − 1
60 9nn ⊢ 9 ∈ ℕ
61 60 nnzi ⊢ 9 ∈ ℤ
62 oddm1even ⊢ 9 ∈ ℤ → ¬ 2 ∥ 9 ↔ 2 ∥ 9 − 1
63 61 62 ax-mp ⊢ ¬ 2 ∥ 9 ↔ 2 ∥ 9 − 1
64 59 63 mpbir ⊢ ¬ 2 ∥ 9
65 breq2 ⊢ 9 = N → 2 ∥ 9 ↔ 2 ∥ N
66 64 65 mtbii ⊢ 9 = N → ¬ 2 ∥ N
67 66 con2i ⊢ 2 ∥ N → ¬ 9 = N
68 67 adantl ⊢ φ ∧ 2 ∥ N → ¬ 9 = N
69 43 68 olcnd ⊢ φ ∧ 2 ∥ N → 9 < N
70 1 nnzd ⊢ φ → N ∈ ℤ
71 zltp1le ⊢ 9 ∈ ℤ ∧ N ∈ ℤ → 9 < N ↔ 9 + 1 ≤ N
72 61 71 mpan ⊢ N ∈ ℤ → 9 < N ↔ 9 + 1 ≤ N
73 70 72 syl ⊢ φ → 9 < N ↔ 9 + 1 ≤ N
74 73 adantr ⊢ φ ∧ 2 ∥ N → 9 < N ↔ 9 + 1 ≤ N
75 69 74 mpbid ⊢ φ ∧ 2 ∥ N → 9 + 1 ≤ N
76 38 75 eqbrtrrid ⊢ φ ∧ 2 ∥ N → 10 ≤ N
77 33 35 37 76 lediv1dd ⊢ φ ∧ 2 ∥ N → 10 2 ≤ N 2
78 32 77 eqbrtrrid ⊢ φ ∧ 2 ∥ N → 5 ≤ N 2
79 22 15 16 78 lesub1dd ⊢ φ ∧ 2 ∥ N → 5 − 1 ≤ N 2 − 1
80 20 79 eqbrtrrid ⊢ φ ∧ 2 ∥ N → 4 ≤ N 2 − 1
81 12 14 17 19 80 ltletrd ⊢ φ ∧ 2 ∥ N → 0 < N 2 − 1
82 11 81 jca ⊢ φ ∧ 2 ∥ N → N 2 − 1 ∈ ℤ ∧ 0 < N 2 − 1
83 elnnz ⊢ N 2 − 1 ∈ ℕ ↔ N 2 − 1 ∈ ℤ ∧ 0 < N 2 − 1
84 82 83 sylibr ⊢ φ ∧ 2 ∥ N → N 2 − 1 ∈ ℕ
85 84 80 lcmineqlem22 ⊢ φ ∧ 2 ∥ N → 2 2 ⁢ N 2 − 1 + 1 ≤ lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 1 ∧ 2 2 ⁢ N 2 − 1 + 2 ≤ lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 2
86 85 simprd ⊢ φ ∧ 2 ∥ N → 2 2 ⁢ N 2 − 1 + 2 ≤ lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 2
87 4 nncnd ⊢ φ → 2 ∈ ℂ
88 1 nncnd ⊢ φ → N ∈ ℂ
89 88 halfcld ⊢ φ → N 2 ∈ ℂ
90 87 89 muls1d ⊢ φ → 2 ⁢ N 2 − 1 = 2 ⁢ N 2 − 2
91 90 oveq1d ⊢ φ → 2 ⁢ N 2 − 1 + 2 = 2 ⁢ N 2 - 2 + 2
92 87 89 mulcld ⊢ φ → 2 ⁢ N 2 ∈ ℂ
93 92 87 npcand ⊢ φ → 2 ⁢ N 2 - 2 + 2 = 2 ⁢ N 2
94 91 93 eqtrd ⊢ φ → 2 ⁢ N 2 − 1 + 2 = 2 ⁢ N 2
95 4 nnne0d ⊢ φ → 2 ≠ 0
96 88 87 95 divcan2d ⊢ φ → 2 ⁢ N 2 = N
97 94 96 eqtrd ⊢ φ → 2 ⁢ N 2 − 1 + 2 = N
98 97 oveq2d ⊢ φ → 2 2 ⁢ N 2 − 1 + 2 = 2 N
99 97 oveq2d ⊢ φ → 1 … 2 ⁢ N 2 − 1 + 2 = 1 … N
100 99 fveq2d ⊢ φ → lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 2 = lcm _ ⁡ 1 … N
101 98 100 breq12d ⊢ φ → 2 2 ⁢ N 2 − 1 + 2 ≤ lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 2 ↔ 2 N ≤ lcm _ ⁡ 1 … N
102 101 adantr ⊢ φ ∧ 2 ∥ N → 2 2 ⁢ N 2 − 1 + 2 ≤ lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 2 ↔ 2 N ≤ lcm _ ⁡ 1 … N
103 86 102 mpbid ⊢ φ ∧ 2 ∥ N → 2 N ≤ lcm _ ⁡ 1 … N
104 oddm1even ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ 2 ∥ N − 1
105 70 104 syl ⊢ φ → ¬ 2 ∥ N ↔ 2 ∥ N − 1
106 105 biimpa ⊢ φ ∧ ¬ 2 ∥ N → 2 ∥ N − 1
107 3 a1i ⊢ φ ∧ ¬ 2 ∥ N → 2 ∈ ℕ
108 1zzd ⊢ φ → 1 ∈ ℤ
109 70 108 zsubcld ⊢ φ → N − 1 ∈ ℤ
110 0red ⊢ φ → 0 ∈ ℝ
111 48 a1i ⊢ φ → 8 ∈ ℝ
112 1red ⊢ φ → 1 ∈ ℝ
113 34 112 resubcld ⊢ φ → N − 1 ∈ ℝ
114 8pos ⊢ 0 < 8
115 114 a1i ⊢ φ → 0 < 8
116 40 34 112 2 lesub1dd ⊢ φ → 9 − 1 ≤ N − 1
117 58 116 eqbrtrrid ⊢ φ → 8 ≤ N − 1
118 110 111 113 115 117 ltletrd ⊢ φ → 0 < N − 1
119 109 118 jca ⊢ φ → N − 1 ∈ ℤ ∧ 0 < N − 1
120 elnnz ⊢ N − 1 ∈ ℕ ↔ N − 1 ∈ ℤ ∧ 0 < N − 1
121 119 120 sylibr ⊢ φ → N − 1 ∈ ℕ
122 121 adantr ⊢ φ ∧ ¬ 2 ∥ N → N − 1 ∈ ℕ
123 107 122 nndivdvdsd ⊢ φ ∧ ¬ 2 ∥ N → 2 ∥ N − 1 ↔ N − 1 2 ∈ ℕ
124 106 123 mpbid ⊢ φ ∧ ¬ 2 ∥ N → N − 1 2 ∈ ℕ
125 44 23 mulcomi ⊢ 4 ⋅ 2 = 2 ⋅ 4
126 125 46 eqtr3i ⊢ 2 ⋅ 4 = 8
127 126 50 mpbir ⊢ 8 2 = 4
128 4 nnrpd ⊢ φ → 2 ∈ ℝ +
129 111 113 128 117 lediv1dd ⊢ φ → 8 2 ≤ N − 1 2
130 127 129 eqbrtrrid ⊢ φ → 4 ≤ N − 1 2
131 130 adantr ⊢ φ ∧ ¬ 2 ∥ N → 4 ≤ N − 1 2
132 124 131 lcmineqlem22 ⊢ φ ∧ ¬ 2 ∥ N → 2 2 ⁢ N − 1 2 + 1 ≤ lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 1 ∧ 2 2 ⁢ N − 1 2 + 2 ≤ lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 2
133 132 simpld ⊢ φ ∧ ¬ 2 ∥ N → 2 2 ⁢ N − 1 2 + 1 ≤ lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 1
134 1cnd ⊢ φ → 1 ∈ ℂ
135 88 134 subcld ⊢ φ → N − 1 ∈ ℂ
136 135 87 95 divcan2d ⊢ φ → 2 ⁢ N − 1 2 = N − 1
137 136 oveq1d ⊢ φ → 2 ⁢ N − 1 2 + 1 = N - 1 + 1
138 88 134 npcand ⊢ φ → N - 1 + 1 = N
139 137 138 eqtrd ⊢ φ → 2 ⁢ N − 1 2 + 1 = N
140 139 oveq2d ⊢ φ → 2 2 ⁢ N − 1 2 + 1 = 2 N
141 139 oveq2d ⊢ φ → 1 … 2 ⁢ N − 1 2 + 1 = 1 … N
142 141 fveq2d ⊢ φ → lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 1 = lcm _ ⁡ 1 … N
143 140 142 breq12d ⊢ φ → 2 2 ⁢ N − 1 2 + 1 ≤ lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 1 ↔ 2 N ≤ lcm _ ⁡ 1 … N
144 143 adantr ⊢ φ ∧ ¬ 2 ∥ N → 2 2 ⁢ N − 1 2 + 1 ≤ lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 1 ↔ 2 N ≤ lcm _ ⁡ 1 … N
145 133 144 mpbid ⊢ φ ∧ ¬ 2 ∥ N → 2 N ≤ lcm _ ⁡ 1 … N
146 103 145 pm2.61dan ⊢ φ → 2 N ≤ lcm _ ⁡ 1 … N