Metamath Proof Explorer

Theorem lcmineqlem23

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

Ref Expression
Hypotheses lcmineqlem23.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lcmineqlem23.2 ⊢ ( 𝜑 → 9 ≤ 𝑁 )
Assertion lcmineqlem23 ( 𝜑 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )

Proof

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