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 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 = N → 2 ∥ 9 ↔ 2 ∥ N
64 62 63 mtbii ⊢ 9 = N → ¬ 2 ∥ N
65 64 con2i ⊢ 2 ∥ N → ¬ 9 = N
66 65 adantl ⊢ φ ∧ 2 ∥ N → ¬ 9 = N
67 43 66 olcnd ⊢ φ ∧ 2 ∥ N → 9 < N
68 1 nnzd ⊢ φ → N ∈ ℤ
69 zltp1le ⊢ 9 ∈ ℤ ∧ N ∈ ℤ → 9 < N ↔ 9 + 1 ≤ N
70 59 69 mpan ⊢ N ∈ ℤ → 9 < N ↔ 9 + 1 ≤ N
71 68 70 syl ⊢ φ → 9 < N ↔ 9 + 1 ≤ N
72 71 adantr ⊢ φ ∧ 2 ∥ N → 9 < N ↔ 9 + 1 ≤ N
73 67 72 mpbid ⊢ φ ∧ 2 ∥ N → 9 + 1 ≤ N
74 38 73 eqbrtrrid ⊢ φ ∧ 2 ∥ N → 10 ≤ N
75 33 35 37 74 lediv1dd ⊢ φ ∧ 2 ∥ N → 10 2 ≤ N 2
76 32 75 eqbrtrrid ⊢ φ ∧ 2 ∥ N → 5 ≤ N 2
77 22 15 16 76 lesub1dd ⊢ φ ∧ 2 ∥ N → 5 − 1 ≤ N 2 − 1
78 20 77 eqbrtrrid ⊢ φ ∧ 2 ∥ N → 4 ≤ N 2 − 1
79 12 14 17 19 78 ltletrd ⊢ φ ∧ 2 ∥ N → 0 < N 2 − 1
80 11 79 jca ⊢ φ ∧ 2 ∥ N → N 2 − 1 ∈ ℤ ∧ 0 < N 2 − 1
81 elnnz ⊢ N 2 − 1 ∈ ℕ ↔ N 2 − 1 ∈ ℤ ∧ 0 < N 2 − 1
82 80 81 sylibr ⊢ φ ∧ 2 ∥ N → N 2 − 1 ∈ ℕ
83 82 78 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
84 83 simprd ⊢ φ ∧ 2 ∥ N → 2 2 ⁢ N 2 − 1 + 2 ≤ lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 2
85 4 nncnd ⊢ φ → 2 ∈ ℂ
86 1 nncnd ⊢ φ → N ∈ ℂ
87 86 halfcld ⊢ φ → N 2 ∈ ℂ
88 85 87 muls1d ⊢ φ → 2 ⁢ N 2 − 1 = 2 ⁢ N 2 − 2
89 88 oveq1d ⊢ φ → 2 ⁢ N 2 − 1 + 2 = 2 ⁢ N 2 - 2 + 2
90 85 87 mulcld ⊢ φ → 2 ⁢ N 2 ∈ ℂ
91 90 85 npcand ⊢ φ → 2 ⁢ N 2 - 2 + 2 = 2 ⁢ N 2
92 89 91 eqtrd ⊢ φ → 2 ⁢ N 2 − 1 + 2 = 2 ⁢ N 2
93 4 nnne0d ⊢ φ → 2 ≠ 0
94 86 85 93 divcan2d ⊢ φ → 2 ⁢ N 2 = N
95 92 94 eqtrd ⊢ φ → 2 ⁢ N 2 − 1 + 2 = N
96 95 oveq2d ⊢ φ → 2 2 ⁢ N 2 − 1 + 2 = 2 N
97 95 oveq2d ⊢ φ → 1 … 2 ⁢ N 2 − 1 + 2 = 1 … N
98 97 fveq2d ⊢ φ → lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 2 = lcm _ ⁡ 1 … N
99 96 98 breq12d ⊢ φ → 2 2 ⁢ N 2 − 1 + 2 ≤ lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 2 ↔ 2 N ≤ lcm _ ⁡ 1 … N
100 99 adantr ⊢ φ ∧ 2 ∥ N → 2 2 ⁢ N 2 − 1 + 2 ≤ lcm _ ⁡ 1 … 2 ⁢ N 2 − 1 + 2 ↔ 2 N ≤ lcm _ ⁡ 1 … N
101 84 100 mpbid ⊢ φ ∧ 2 ∥ N → 2 N ≤ lcm _ ⁡ 1 … N
102 oddm1even ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ 2 ∥ N − 1
103 68 102 syl ⊢ φ → ¬ 2 ∥ N ↔ 2 ∥ N − 1
104 103 biimpa ⊢ φ ∧ ¬ 2 ∥ N → 2 ∥ N − 1
105 3 a1i ⊢ φ ∧ ¬ 2 ∥ N → 2 ∈ ℕ
106 1zzd ⊢ φ → 1 ∈ ℤ
107 68 106 zsubcld ⊢ φ → N − 1 ∈ ℤ
108 0red ⊢ φ → 0 ∈ ℝ
109 45 a1i ⊢ φ → 8 ∈ ℝ
110 1red ⊢ φ → 1 ∈ ℝ
111 34 110 resubcld ⊢ φ → N − 1 ∈ ℝ
112 8pos ⊢ 0 < 8
113 112 a1i ⊢ φ → 0 < 8
114 40 34 110 2 lesub1dd ⊢ φ → 9 − 1 ≤ N − 1
115 56 114 eqbrtrrid ⊢ φ → 8 ≤ N − 1
116 108 109 111 113 115 ltletrd ⊢ φ → 0 < N − 1
117 107 116 jca ⊢ φ → N − 1 ∈ ℤ ∧ 0 < N − 1
118 elnnz ⊢ N − 1 ∈ ℕ ↔ N − 1 ∈ ℤ ∧ 0 < N − 1
119 117 118 sylibr ⊢ φ → N − 1 ∈ ℕ
120 119 adantr ⊢ φ ∧ ¬ 2 ∥ N → N − 1 ∈ ℕ
121 105 120 nndivdvdsd ⊢ φ ∧ ¬ 2 ∥ N → 2 ∥ N − 1 ↔ N − 1 2 ∈ ℕ
122 104 121 mpbid ⊢ φ ∧ ¬ 2 ∥ N → N − 1 2 ∈ ℕ
123 4 nnrpd ⊢ φ → 2 ∈ ℝ +
124 109 111 123 115 lediv1dd ⊢ φ → 8 2 ≤ N − 1 2
125 49 124 eqbrtrrid ⊢ φ → 4 ≤ N − 1 2
126 125 adantr ⊢ φ ∧ ¬ 2 ∥ N → 4 ≤ N − 1 2
127 122 126 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
128 127 simpld ⊢ φ ∧ ¬ 2 ∥ N → 2 2 ⁢ N − 1 2 + 1 ≤ lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 1
129 1cnd ⊢ φ → 1 ∈ ℂ
130 86 129 subcld ⊢ φ → N − 1 ∈ ℂ
131 130 85 93 divcan2d ⊢ φ → 2 ⁢ N − 1 2 = N − 1
132 131 oveq1d ⊢ φ → 2 ⁢ N − 1 2 + 1 = N - 1 + 1
133 86 129 npcand ⊢ φ → N - 1 + 1 = N
134 132 133 eqtrd ⊢ φ → 2 ⁢ N − 1 2 + 1 = N
135 134 oveq2d ⊢ φ → 2 2 ⁢ N − 1 2 + 1 = 2 N
136 134 oveq2d ⊢ φ → 1 … 2 ⁢ N − 1 2 + 1 = 1 … N
137 136 fveq2d ⊢ φ → lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 1 = lcm _ ⁡ 1 … N
138 135 137 breq12d ⊢ φ → 2 2 ⁢ N − 1 2 + 1 ≤ lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 1 ↔ 2 N ≤ lcm _ ⁡ 1 … N
139 138 adantr ⊢ φ ∧ ¬ 2 ∥ N → 2 2 ⁢ N − 1 2 + 1 ≤ lcm _ ⁡ 1 … 2 ⁢ N − 1 2 + 1 ↔ 2 N ≤ lcm _ ⁡ 1 … N
140 128 139 mpbid ⊢ φ ∧ ¬ 2 ∥ N → 2 N ≤ lcm _ ⁡ 1 … N
141 101 140 pm2.61dan ⊢ φ → 2 N ≤ lcm _ ⁡ 1 … N