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 2t4e8 ⊢ ( 2 · 4 ) = 8
45 8re ⊢ 8 ∈ ℝ
46 45 recni ⊢ 8 ∈ ℂ
47 4cn ⊢ 4 ∈ ℂ
48 46 23 47 30 divmuli ⊢ ( ( 8 / 2 ) = 4 ↔ ( 2 · 4 ) = 8 )
49 44 48 mpbir ⊢ ( 8 / 2 ) = 4
50 4nn ⊢ 4 ∈ ℕ
51 49 50 eqeltri ⊢ ( 8 / 2 ) ∈ ℕ
52 8nn ⊢ 8 ∈ ℕ
53 nndivdvds ⊢ ( ( 8 ∈ ℕ ∧ 2 ∈ ℕ ) → ( 2 ∥ 8 ↔ ( 8 / 2 ) ∈ ℕ ) )
54 52 3 53 mp2an ⊢ ( 2 ∥ 8 ↔ ( 8 / 2 ) ∈ ℕ )
55 51 54 mpbir ⊢ 2 ∥ 8
56 9m1e8 ⊢ ( 9 − 1 ) = 8
57 55 56 breqtrri ⊢ 2 ∥ ( 9 − 1 )
58 9nn ⊢ 9 ∈ ℕ
59 58 nnzi ⊢ 9 ∈ ℤ
60 oddm1even ⊢ ( 9 ∈ ℤ → ( ¬ 2 ∥ 9 ↔ 2 ∥ ( 9 − 1 ) ) )
61 59 60 ax-mp ⊢ ( ¬ 2 ∥ 9 ↔ 2 ∥ ( 9 − 1 ) )
62 57 61 mpbir ⊢ ¬ 2 ∥ 9
63 breq2 ⊢ ( 9 = 𝑁 → ( 2 ∥ 9 ↔ 2 ∥ 𝑁 ) )
64 62 63 mtbii ⊢ ( 9 = 𝑁 → ¬ 2 ∥ 𝑁 )
65 64 con2i ⊢ ( 2 ∥ 𝑁 → ¬ 9 = 𝑁 )
66 65 adantl ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ¬ 9 = 𝑁 )
67 43 66 olcnd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → 9 < 𝑁 )
68 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
69 zltp1le ⊢ ( ( 9 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 9 < 𝑁 ↔ ( 9 + 1 ) ≤ 𝑁 ) )
70 59 69 mpan ⊢ ( 𝑁 ∈ ℤ → ( 9 < 𝑁 ↔ ( 9 + 1 ) ≤ 𝑁 ) )
71 68 70 syl ⊢ ( 𝜑 → ( 9 < 𝑁 ↔ ( 9 + 1 ) ≤ 𝑁 ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( 9 < 𝑁 ↔ ( 9 + 1 ) ≤ 𝑁 ) )
73 67 72 mpbid ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( 9 + 1 ) ≤ 𝑁 )
74 38 73 eqbrtrrid ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → 1 0 ≤ 𝑁 )
75 33 35 37 74 lediv1dd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( 1 0 / 2 ) ≤ ( 𝑁 / 2 ) )
76 32 75 eqbrtrrid ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → 5 ≤ ( 𝑁 / 2 ) )
77 22 15 16 76 lesub1dd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( 5 − 1 ) ≤ ( ( 𝑁 / 2 ) − 1 ) )
78 20 77 eqbrtrrid ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → 4 ≤ ( ( 𝑁 / 2 ) − 1 ) )
79 12 14 17 19 78 ltletrd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → 0 < ( ( 𝑁 / 2 ) − 1 ) )
80 11 79 jca ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( ( ( 𝑁 / 2 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 𝑁 / 2 ) − 1 ) ) )
81 elnnz ⊢ ( ( ( 𝑁 / 2 ) − 1 ) ∈ ℕ ↔ ( ( ( 𝑁 / 2 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 𝑁 / 2 ) − 1 ) ) )
82 80 81 sylibr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( ( 𝑁 / 2 ) − 1 ) ∈ ℕ )
83 82 78 lcmineqlem22 ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( ( 2 ↑ ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 1 ) ) ) ∧ ( 2 ↑ ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) ) ) )
84 83 simprd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( 2 ↑ ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) ) )
85 4 nncnd ⊢ ( 𝜑 → 2 ∈ ℂ )
86 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
87 86 halfcld ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℂ )
88 85 87 muls1d ⊢ ( 𝜑 → ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) = ( ( 2 · ( 𝑁 / 2 ) ) − 2 ) )
89 88 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) = ( ( ( 2 · ( 𝑁 / 2 ) ) − 2 ) + 2 ) )
90 85 87 mulcld ⊢ ( 𝜑 → ( 2 · ( 𝑁 / 2 ) ) ∈ ℂ )
91 90 85 npcand ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑁 / 2 ) ) − 2 ) + 2 ) = ( 2 · ( 𝑁 / 2 ) ) )
92 89 91 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) = ( 2 · ( 𝑁 / 2 ) ) )
93 4 nnne0d ⊢ ( 𝜑 → 2 ≠ 0 )
94 86 85 93 divcan2d ⊢ ( 𝜑 → ( 2 · ( 𝑁 / 2 ) ) = 𝑁 )
95 92 94 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) = 𝑁 )
96 95 oveq2d ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) = ( 2 ↑ 𝑁 ) )
97 95 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) = ( 1 ... 𝑁 ) )
98 97 fveq2d ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) ) = ( lcm ‘ ( 1 ... 𝑁 ) ) )
99 96 98 breq12d ⊢ ( 𝜑 → ( ( 2 ↑ ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) ) ↔ ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
100 99 adantr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( ( 2 ↑ ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 / 2 ) − 1 ) ) + 2 ) ) ) ↔ ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
101 84 100 mpbid ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )
102 oddm1even ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) )
103 68 102 syl ⊢ ( 𝜑 → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 − 1 ) ) )
104 103 biimpa ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → 2 ∥ ( 𝑁 − 1 ) )
105 3 a1i ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → 2 ∈ ℕ )
106 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
107 68 106 zsubcld ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
108 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
109 45 a1i ⊢ ( 𝜑 → 8 ∈ ℝ )
110 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
111 34 110 resubcld ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
112 8pos ⊢ 0 < 8
113 112 a1i ⊢ ( 𝜑 → 0 < 8 )
114 40 34 110 2 lesub1dd ⊢ ( 𝜑 → ( 9 − 1 ) ≤ ( 𝑁 − 1 ) )
115 56 114 eqbrtrrid ⊢ ( 𝜑 → 8 ≤ ( 𝑁 − 1 ) )
116 108 109 111 113 115 ltletrd ⊢ ( 𝜑 → 0 < ( 𝑁 − 1 ) )
117 107 116 jca ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) ∈ ℤ ∧ 0 < ( 𝑁 − 1 ) ) )
118 elnnz ⊢ ( ( 𝑁 − 1 ) ∈ ℕ ↔ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 0 < ( 𝑁 − 1 ) ) )
119 117 118 sylibr ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ )
120 119 adantr ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ )
121 105 120 nndivdvdsd ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( 2 ∥ ( 𝑁 − 1 ) ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ ) )
122 104 121 mpbid ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ )
123 4 nnrpd ⊢ ( 𝜑 → 2 ∈ ℝ+ )
124 109 111 123 115 lediv1dd ⊢ ( 𝜑 → ( 8 / 2 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
125 49 124 eqbrtrrid ⊢ ( 𝜑 → 4 ≤ ( ( 𝑁 − 1 ) / 2 ) )
126 125 adantr ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → 4 ≤ ( ( 𝑁 − 1 ) / 2 ) )
127 122 126 lcmineqlem22 ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( ( 2 ↑ ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) ) ∧ ( 2 ↑ ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 2 ) ) ) ) )
128 127 simpld ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( 2 ↑ ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) ) )
129 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
130 86 129 subcld ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℂ )
131 130 85 93 divcan2d ⊢ ( 𝜑 → ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) = ( 𝑁 − 1 ) )
132 131 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) = ( ( 𝑁 − 1 ) + 1 ) )
133 86 129 npcand ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
134 132 133 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) = 𝑁 )
135 134 oveq2d ⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) = ( 2 ↑ 𝑁 ) )
136 134 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) = ( 1 ... 𝑁 ) )
137 136 fveq2d ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) ) = ( lcm ‘ ( 1 ... 𝑁 ) ) )
138 135 137 breq12d ⊢ ( 𝜑 → ( ( 2 ↑ ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) ) ↔ ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
139 138 adantr ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( ( 2 ↑ ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) ) ) ↔ ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
140 128 139 mpbid ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )
141 101 140 pm2.61dan ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )