Metamath Proof Explorer

Theorem lcmineqlem

Description: The least common multiple inequality lemma, a central result for future use. Theorem 3.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 16-May-2024)

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

Proof

Step Hyp Ref Expression
1 lcmineqlem.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 lcmineqlem.2 ⊢ ( 𝜑 → 7 ≤ 𝑁 )
3 7re ⊢ 7 ∈ ℝ
4 3 a1i ⊢ ( 𝜑 → 7 ∈ ℝ )
5 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
6 4 5 leloed ⊢ ( 𝜑 → ( 7 ≤ 𝑁 ↔ ( 7 < 𝑁 ∨ 7 = 𝑁 ) ) )
7 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
8 7nn ⊢ 7 ∈ ℕ
9 8 nnzi ⊢ 7 ∈ ℤ
10 zltp1le ⊢ ( ( 7 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 7 < 𝑁 ↔ ( 7 + 1 ) ≤ 𝑁 ) )
11 9 10 mpan ⊢ ( 𝑁 ∈ ℤ → ( 7 < 𝑁 ↔ ( 7 + 1 ) ≤ 𝑁 ) )
12 7 11 syl ⊢ ( 𝜑 → ( 7 < 𝑁 ↔ ( 7 + 1 ) ≤ 𝑁 ) )
13 7p1e8 ⊢ ( 7 + 1 ) = 8
14 13 breq1i ⊢ ( ( 7 + 1 ) ≤ 𝑁 ↔ 8 ≤ 𝑁 )
15 12 14 bitrdi ⊢ ( 𝜑 → ( 7 < 𝑁 ↔ 8 ≤ 𝑁 ) )
16 8re ⊢ 8 ∈ ℝ
17 16 a1i ⊢ ( 𝜑 → 8 ∈ ℝ )
18 17 5 leloed ⊢ ( 𝜑 → ( 8 ≤ 𝑁 ↔ ( 8 < 𝑁 ∨ 8 = 𝑁 ) ) )
19 1 adantr ⊢ ( ( 𝜑 ∧ 8 < 𝑁 ) → 𝑁 ∈ ℕ )
20 8p1e9 ⊢ ( 8 + 1 ) = 9
21 8nn ⊢ 8 ∈ ℕ
22 21 nnzi ⊢ 8 ∈ ℤ
23 zltp1le ⊢ ( ( 8 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 8 < 𝑁 ↔ ( 8 + 1 ) ≤ 𝑁 ) )
24 22 23 mpan ⊢ ( 𝑁 ∈ ℤ → ( 8 < 𝑁 ↔ ( 8 + 1 ) ≤ 𝑁 ) )
25 7 24 syl ⊢ ( 𝜑 → ( 8 < 𝑁 ↔ ( 8 + 1 ) ≤ 𝑁 ) )
26 25 biimpd ⊢ ( 𝜑 → ( 8 < 𝑁 → ( 8 + 1 ) ≤ 𝑁 ) )
27 26 imp ⊢ ( ( 𝜑 ∧ 8 < 𝑁 ) → ( 8 + 1 ) ≤ 𝑁 )
28 20 27 eqbrtrrid ⊢ ( ( 𝜑 ∧ 8 < 𝑁 ) → 9 ≤ 𝑁 )
29 19 28 lcmineqlem23 ⊢ ( ( 𝜑 ∧ 8 < 𝑁 ) → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )
30 29 ex ⊢ ( 𝜑 → ( 8 < 𝑁 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
31 2nn0 ⊢ 2 ∈ ℕ0
32 8nn0 ⊢ 8 ∈ ℕ0
33 5nn0 ⊢ 5 ∈ ℕ0
34 4nn0 ⊢ 4 ∈ ℕ0
35 6nn0 ⊢ 6 ∈ ℕ0
36 0nn0 ⊢ 0 ∈ ℕ0
37 2lt8 ⊢ 2 < 8
38 5lt10 ⊢ 5 < 1 0
39 6lt10 ⊢ 6 < 1 0
40 31 32 33 34 35 36 37 38 39 3decltc ⊢ 2 5 6 < 8 4 0
41 5nn ⊢ 5 ∈ ℕ
42 31 41 decnncl ⊢ 2 5 ∈ ℕ
43 42 nnnn0i ⊢ 2 5 ∈ ℕ0
44 6nn ⊢ 6 ∈ ℕ
45 43 44 decnncl ⊢ 2 5 6 ∈ ℕ
46 45 nnrei ⊢ 2 5 6 ∈ ℝ
47 4nn ⊢ 4 ∈ ℕ
48 32 47 decnncl ⊢ 8 4 ∈ ℕ
49 48 decnncl2 ⊢ 8 4 0 ∈ ℕ
50 49 nnrei ⊢ 8 4 0 ∈ ℝ
51 46 50 ltlei ⊢ ( 2 5 6 < 8 4 0 → 2 5 6 ≤ 8 4 0 )
52 40 51 ax-mp ⊢ 2 5 6 ≤ 8 4 0
53 2exp8 ⊢ ( 2 ↑ 8 ) = 2 5 6
54 oveq2 ⊢ ( 8 = 𝑁 → ( 2 ↑ 8 ) = ( 2 ↑ 𝑁 ) )
55 53 54 syl5eqr ⊢ ( 8 = 𝑁 → 2 5 6 = ( 2 ↑ 𝑁 ) )
56 lcm8un ⊢ ( lcm ‘ ( 1 ... 8 ) ) = 8 4 0
57 oveq2 ⊢ ( 8 = 𝑁 → ( 1 ... 8 ) = ( 1 ... 𝑁 ) )
58 57 fveq2d ⊢ ( 8 = 𝑁 → ( lcm ‘ ( 1 ... 8 ) ) = ( lcm ‘ ( 1 ... 𝑁 ) ) )
59 56 58 syl5eqr ⊢ ( 8 = 𝑁 → 8 4 0 = ( lcm ‘ ( 1 ... 𝑁 ) ) )
60 55 59 breq12d ⊢ ( 8 = 𝑁 → ( 2 5 6 ≤ 8 4 0 ↔ ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
61 52 60 mpbii ⊢ ( 8 = 𝑁 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )
62 61 adantl ⊢ ( ( 𝜑 ∧ 8 = 𝑁 ) → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )
63 62 ex ⊢ ( 𝜑 → ( 8 = 𝑁 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
64 30 63 jaod ⊢ ( 𝜑 → ( ( 8 < 𝑁 ∨ 8 = 𝑁 ) → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
65 18 64 sylbid ⊢ ( 𝜑 → ( 8 ≤ 𝑁 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
66 15 65 sylbid ⊢ ( 𝜑 → ( 7 < 𝑁 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
67 1nn0 ⊢ 1 ∈ ℕ0
68 1lt4 ⊢ 1 < 4
69 2lt10 ⊢ 2 < 1 0
70 8lt10 ⊢ 8 < 1 0
71 67 34 31 31 32 36 68 69 70 3decltc ⊢ 1 2 8 < 4 2 0
72 2nn ⊢ 2 ∈ ℕ
73 67 72 decnncl ⊢ 1 2 ∈ ℕ
74 73 nnnn0i ⊢ 1 2 ∈ ℕ0
75 74 21 decnncl ⊢ 1 2 8 ∈ ℕ
76 75 nnrei ⊢ 1 2 8 ∈ ℝ
77 34 72 decnncl ⊢ 4 2 ∈ ℕ
78 77 decnncl2 ⊢ 4 2 0 ∈ ℕ
79 78 nnrei ⊢ 4 2 0 ∈ ℝ
80 76 79 ltlei ⊢ ( 1 2 8 < 4 2 0 → 1 2 8 ≤ 4 2 0 )
81 71 80 ax-mp ⊢ 1 2 8 ≤ 4 2 0
82 2exp7 ⊢ ( 2 ↑ 7 ) = 1 2 8
83 oveq2 ⊢ ( 7 = 𝑁 → ( 2 ↑ 7 ) = ( 2 ↑ 𝑁 ) )
84 82 83 syl5eqr ⊢ ( 7 = 𝑁 → 1 2 8 = ( 2 ↑ 𝑁 ) )
85 lcm7un ⊢ ( lcm ‘ ( 1 ... 7 ) ) = 4 2 0
86 oveq2 ⊢ ( 7 = 𝑁 → ( 1 ... 7 ) = ( 1 ... 𝑁 ) )
87 86 fveq2d ⊢ ( 7 = 𝑁 → ( lcm ‘ ( 1 ... 7 ) ) = ( lcm ‘ ( 1 ... 𝑁 ) ) )
88 85 87 syl5eqr ⊢ ( 7 = 𝑁 → 4 2 0 = ( lcm ‘ ( 1 ... 𝑁 ) ) )
89 84 88 breq12d ⊢ ( 7 = 𝑁 → ( 1 2 8 ≤ 4 2 0 ↔ ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
90 81 89 mpbii ⊢ ( 7 = 𝑁 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )
91 90 a1i ⊢ ( 𝜑 → ( 7 = 𝑁 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
92 66 91 jaod ⊢ ( 𝜑 → ( ( 7 < 𝑁 ∨ 7 = 𝑁 ) → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
93 6 92 sylbid ⊢ ( 𝜑 → ( 7 ≤ 𝑁 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
94 2 93 mpd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )