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 
|- ( ph -> N e. NN )
lcmineqlem.2 
|- ( ph -> 7 <_ N )
Assertion lcmineqlem 
|- ( ph -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem.1 
 |-  ( ph -> N e. NN )
2 lcmineqlem.2 
 |-  ( ph -> 7 <_ N )
3 7re 
 |-  7 e. RR
4 3 a1i 
 |-  ( ph -> 7 e. RR )
5 1 nnred 
 |-  ( ph -> N e. RR )
6 4 5 leloed 
 |-  ( ph -> ( 7 <_ N <-> ( 7 < N \/ 7 = N ) ) )
7 1 nnzd 
 |-  ( ph -> N e. ZZ )
8 7nn 
 |-  7 e. NN
9 8 nnzi 
 |-  7 e. ZZ
10 zltp1le 
 |-  ( ( 7 e. ZZ /\ N e. ZZ ) -> ( 7 < N <-> ( 7 + 1 ) <_ N ) )
11 9 10 mpan 
 |-  ( N e. ZZ -> ( 7 < N <-> ( 7 + 1 ) <_ N ) )
12 7 11 syl 
 |-  ( ph -> ( 7 < N <-> ( 7 + 1 ) <_ N ) )
13 7p1e8 
 |-  ( 7 + 1 ) = 8
14 13 breq1i 
 |-  ( ( 7 + 1 ) <_ N <-> 8 <_ N )
15 12 14 bitrdi 
 |-  ( ph -> ( 7 < N <-> 8 <_ N ) )
16 8re 
 |-  8 e. RR
17 16 a1i 
 |-  ( ph -> 8 e. RR )
18 17 5 leloed 
 |-  ( ph -> ( 8 <_ N <-> ( 8 < N \/ 8 = N ) ) )
19 1 adantr 
 |-  ( ( ph /\ 8 < N ) -> N e. NN )
20 8p1e9 
 |-  ( 8 + 1 ) = 9
21 8nn 
 |-  8 e. NN
22 21 nnzi 
 |-  8 e. ZZ
23 zltp1le 
 |-  ( ( 8 e. ZZ /\ N e. ZZ ) -> ( 8 < N <-> ( 8 + 1 ) <_ N ) )
24 22 23 mpan 
 |-  ( N e. ZZ -> ( 8 < N <-> ( 8 + 1 ) <_ N ) )
25 7 24 syl 
 |-  ( ph -> ( 8 < N <-> ( 8 + 1 ) <_ N ) )
26 25 biimpd 
 |-  ( ph -> ( 8 < N -> ( 8 + 1 ) <_ N ) )
27 26 imp 
 |-  ( ( ph /\ 8 < N ) -> ( 8 + 1 ) <_ N )
28 20 27 eqbrtrrid 
 |-  ( ( ph /\ 8 < N ) -> 9 <_ N )
29 19 28 lcmineqlem23 
 |-  ( ( ph /\ 8 < N ) -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )
30 29 ex 
 |-  ( ph -> ( 8 < N -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
31 2nn0 
 |-  2 e. NN0
32 8nn0 
 |-  8 e. NN0
33 5nn0 
 |-  5 e. NN0
34 4nn0 
 |-  4 e. NN0
35 6nn0 
 |-  6 e. NN0
36 0nn0 
 |-  0 e. NN0
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 e. NN
42 31 41 decnncl 
 |-  ; 2 5 e. NN
43 42 nnnn0i 
 |-  ; 2 5 e. NN0
44 6nn 
 |-  6 e. NN
45 43 44 decnncl 
 |-  ; ; 2 5 6 e. NN
46 45 nnrei 
 |-  ; ; 2 5 6 e. RR
47 4nn 
 |-  4 e. NN
48 32 47 decnncl 
 |-  ; 8 4 e. NN
49 48 decnncl2 
 |-  ; ; 8 4 0 e. NN
50 49 nnrei 
 |-  ; ; 8 4 0 e. RR
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 = N -> ( 2 ^ 8 ) = ( 2 ^ N ) )
55 53 54 eqtr3id 
 |-  ( 8 = N -> ; ; 2 5 6 = ( 2 ^ N ) )
56 lcm8un 
 |-  ( _lcm ` ( 1 ... 8 ) ) = ; ; 8 4 0
57 oveq2 
 |-  ( 8 = N -> ( 1 ... 8 ) = ( 1 ... N ) )
58 57 fveq2d 
 |-  ( 8 = N -> ( _lcm ` ( 1 ... 8 ) ) = ( _lcm ` ( 1 ... N ) ) )
59 56 58 eqtr3id 
 |-  ( 8 = N -> ; ; 8 4 0 = ( _lcm ` ( 1 ... N ) ) )
60 55 59 breq12d 
 |-  ( 8 = N -> ( ; ; 2 5 6 <_ ; ; 8 4 0 <-> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
61 52 60 mpbii 
 |-  ( 8 = N -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )
62 61 adantl 
 |-  ( ( ph /\ 8 = N ) -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )
63 62 ex 
 |-  ( ph -> ( 8 = N -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
64 30 63 jaod 
 |-  ( ph -> ( ( 8 < N \/ 8 = N ) -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
65 18 64 sylbid 
 |-  ( ph -> ( 8 <_ N -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
66 15 65 sylbid 
 |-  ( ph -> ( 7 < N -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
67 1nn0 
 |-  1 e. NN0
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 e. NN
73 67 72 decnncl 
 |-  ; 1 2 e. NN
74 73 nnnn0i 
 |-  ; 1 2 e. NN0
75 74 21 decnncl 
 |-  ; ; 1 2 8 e. NN
76 75 nnrei 
 |-  ; ; 1 2 8 e. RR
77 34 72 decnncl 
 |-  ; 4 2 e. NN
78 77 decnncl2 
 |-  ; ; 4 2 0 e. NN
79 78 nnrei 
 |-  ; ; 4 2 0 e. RR
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 = N -> ( 2 ^ 7 ) = ( 2 ^ N ) )
84 82 83 eqtr3id 
 |-  ( 7 = N -> ; ; 1 2 8 = ( 2 ^ N ) )
85 lcm7un 
 |-  ( _lcm ` ( 1 ... 7 ) ) = ; ; 4 2 0
86 oveq2 
 |-  ( 7 = N -> ( 1 ... 7 ) = ( 1 ... N ) )
87 86 fveq2d 
 |-  ( 7 = N -> ( _lcm ` ( 1 ... 7 ) ) = ( _lcm ` ( 1 ... N ) ) )
88 85 87 eqtr3id 
 |-  ( 7 = N -> ; ; 4 2 0 = ( _lcm ` ( 1 ... N ) ) )
89 84 88 breq12d 
 |-  ( 7 = N -> ( ; ; 1 2 8 <_ ; ; 4 2 0 <-> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
90 81 89 mpbii 
 |-  ( 7 = N -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )
91 90 a1i 
 |-  ( ph -> ( 7 = N -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
92 66 91 jaod 
 |-  ( ph -> ( ( 7 < N \/ 7 = N ) -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
93 6 92 sylbid 
 |-  ( ph -> ( 7 <_ N -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
94 2 93 mpd 
 |-  ( ph -> ( 2 ^ N ) <_ ( _lcm ` ( 1 ... N ) ) )