Metamath Proof Explorer


Theorem prmlem1

Description: A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses prmlem1.n โŠข ๐‘ โˆˆ โ„•
prmlem1.gt โŠข 1 < ๐‘
prmlem1.2 โŠข ยฌ 2 โˆฅ ๐‘
prmlem1.3 โŠข ยฌ 3 โˆฅ ๐‘
prmlem1.lt โŠข ๐‘ < 2 5
Assertion prmlem1 ๐‘ โˆˆ โ„™

Proof

Step Hyp Ref Expression
1 prmlem1.n โŠข ๐‘ โˆˆ โ„•
2 prmlem1.gt โŠข 1 < ๐‘
3 prmlem1.2 โŠข ยฌ 2 โˆฅ ๐‘
4 prmlem1.3 โŠข ยฌ 3 โˆฅ ๐‘
5 prmlem1.lt โŠข ๐‘ < 2 5
6 eluzelre โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ ๐‘ฅ โˆˆ โ„ )
7 6 resqcld โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ ( ๐‘ฅ โ†‘ 2 ) โˆˆ โ„ )
8 eluzle โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ 5 โ‰ค ๐‘ฅ )
9 5re โŠข 5 โˆˆ โ„
10 5nn0 โŠข 5 โˆˆ โ„•0
11 10 nn0ge0i โŠข 0 โ‰ค 5
12 le2sq2 โŠข ( ( ( 5 โˆˆ โ„ โˆง 0 โ‰ค 5 ) โˆง ( ๐‘ฅ โˆˆ โ„ โˆง 5 โ‰ค ๐‘ฅ ) ) โ†’ ( 5 โ†‘ 2 ) โ‰ค ( ๐‘ฅ โ†‘ 2 ) )
13 9 11 12 mpanl12 โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง 5 โ‰ค ๐‘ฅ ) โ†’ ( 5 โ†‘ 2 ) โ‰ค ( ๐‘ฅ โ†‘ 2 ) )
14 6 8 13 syl2anc โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ ( 5 โ†‘ 2 ) โ‰ค ( ๐‘ฅ โ†‘ 2 ) )
15 1 nnrei โŠข ๐‘ โˆˆ โ„
16 9 resqcli โŠข ( 5 โ†‘ 2 ) โˆˆ โ„
17 5cn โŠข 5 โˆˆ โ„‚
18 17 sqvali โŠข ( 5 โ†‘ 2 ) = ( 5 ยท 5 )
19 5t5e25 โŠข ( 5 ยท 5 ) = 2 5
20 18 19 eqtri โŠข ( 5 โ†‘ 2 ) = 2 5
21 5 20 breqtrri โŠข ๐‘ < ( 5 โ†‘ 2 )
22 ltletr โŠข ( ( ๐‘ โˆˆ โ„ โˆง ( 5 โ†‘ 2 ) โˆˆ โ„ โˆง ( ๐‘ฅ โ†‘ 2 ) โˆˆ โ„ ) โ†’ ( ( ๐‘ < ( 5 โ†‘ 2 ) โˆง ( 5 โ†‘ 2 ) โ‰ค ( ๐‘ฅ โ†‘ 2 ) ) โ†’ ๐‘ < ( ๐‘ฅ โ†‘ 2 ) ) )
23 21 22 mpani โŠข ( ( ๐‘ โˆˆ โ„ โˆง ( 5 โ†‘ 2 ) โˆˆ โ„ โˆง ( ๐‘ฅ โ†‘ 2 ) โˆˆ โ„ ) โ†’ ( ( 5 โ†‘ 2 ) โ‰ค ( ๐‘ฅ โ†‘ 2 ) โ†’ ๐‘ < ( ๐‘ฅ โ†‘ 2 ) ) )
24 15 16 23 mp3an12 โŠข ( ( ๐‘ฅ โ†‘ 2 ) โˆˆ โ„ โ†’ ( ( 5 โ†‘ 2 ) โ‰ค ( ๐‘ฅ โ†‘ 2 ) โ†’ ๐‘ < ( ๐‘ฅ โ†‘ 2 ) ) )
25 7 14 24 sylc โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ ๐‘ < ( ๐‘ฅ โ†‘ 2 ) )
26 ltnle โŠข ( ( ๐‘ โˆˆ โ„ โˆง ( ๐‘ฅ โ†‘ 2 ) โˆˆ โ„ ) โ†’ ( ๐‘ < ( ๐‘ฅ โ†‘ 2 ) โ†” ยฌ ( ๐‘ฅ โ†‘ 2 ) โ‰ค ๐‘ ) )
27 15 7 26 sylancr โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ ( ๐‘ < ( ๐‘ฅ โ†‘ 2 ) โ†” ยฌ ( ๐‘ฅ โ†‘ 2 ) โ‰ค ๐‘ ) )
28 25 27 mpbid โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ ยฌ ( ๐‘ฅ โ†‘ 2 ) โ‰ค ๐‘ )
29 28 pm2.21d โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ ( ( ๐‘ฅ โ†‘ 2 ) โ‰ค ๐‘ โ†’ ยฌ ๐‘ฅ โˆฅ ๐‘ ) )
30 29 adantld โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ ( ( ๐‘ฅ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ( ๐‘ฅ โ†‘ 2 ) โ‰ค ๐‘ ) โ†’ ยฌ ๐‘ฅ โˆฅ ๐‘ ) )
31 30 adantl โŠข ( ( ยฌ 2 โˆฅ 5 โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) ) โ†’ ( ( ๐‘ฅ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ( ๐‘ฅ โ†‘ 2 ) โ‰ค ๐‘ ) โ†’ ยฌ ๐‘ฅ โˆฅ ๐‘ ) )
32 1 2 3 4 31 prmlem1a โŠข ๐‘ โˆˆ โ„™