Metamath Proof Explorer

Theorem fmtnoprmfac1

Description: Divisor of Fermat number (special form of Euler's result, see fmtnofac1 ): Let F_n be a Fermat number. Let p be a prime divisor of F_n. Then p is in the form: k*2^(n+1)+1 where k is a positive integer. (Contributed by AV, 25-Jul-2021)

Ref Expression
Assertion fmtnoprmfac1 ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 breq1 โŠข ( ๐‘ƒ = 2 โ†’ ( ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†” 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) ) )
2 1 adantr โŠข ( ( ๐‘ƒ = 2 โˆง ๐‘ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†” 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) ) )
3 nnnn0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•0 )
4 fmtnoodd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ยฌ 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) )
5 3 4 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ยฌ 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) )
6 5 adantl โŠข ( ( ๐‘ƒ = 2 โˆง ๐‘ โˆˆ โ„• ) โ†’ ยฌ 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) )
7 6 pm2.21d โŠข ( ( ๐‘ƒ = 2 โˆง ๐‘ โˆˆ โ„• ) โ†’ ( 2 โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
8 2 7 sylbid โŠข ( ( ๐‘ƒ = 2 โˆง ๐‘ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
9 8 a1d โŠข ( ( ๐‘ƒ = 2 โˆง ๐‘ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) ) )
10 9 ex โŠข ( ๐‘ƒ = 2 โ†’ ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) ) ) )
11 10 3impd โŠข ( ๐‘ƒ = 2 โ†’ ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
12 simpr1 โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ ๐‘ โˆˆ โ„• )
13 neqne โŠข ( ยฌ ๐‘ƒ = 2 โ†’ ๐‘ƒ โ‰  2 )
14 13 anim2i โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ ๐‘ƒ = 2 ) โ†’ ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โ‰  2 ) )
15 eldifsn โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†” ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โ‰  2 ) )
16 14 15 sylibr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ยฌ ๐‘ƒ = 2 ) โ†’ ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) )
17 16 ex โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ยฌ ๐‘ƒ = 2 โ†’ ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) )
18 17 3ad2ant2 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ( ยฌ ๐‘ƒ = 2 โ†’ ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) )
19 18 impcom โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) )
20 simpr3 โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) )
21 fmtnoprmfac1lem โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) )
22 12 19 20 21 syl3anc โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) )
23 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
24 23 ad2antll โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
25 2z โŠข 2 โˆˆ โ„ค
26 25 a1i โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ 2 โˆˆ โ„ค )
27 13 necomd โŠข ( ยฌ ๐‘ƒ = 2 โ†’ 2 โ‰  ๐‘ƒ )
28 27 adantr โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ 2 โ‰  ๐‘ƒ )
29 2prm โŠข 2 โˆˆ โ„™
30 29 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„™ )
31 30 anim1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( 2 โˆˆ โ„™ โˆง ๐‘ƒ โˆˆ โ„™ ) )
32 31 adantl โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( 2 โˆˆ โ„™ โˆง ๐‘ƒ โˆˆ โ„™ ) )
33 prmrp โŠข ( ( 2 โˆˆ โ„™ โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( ( 2 gcd ๐‘ƒ ) = 1 โ†” 2 โ‰  ๐‘ƒ ) )
34 32 33 syl โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( 2 gcd ๐‘ƒ ) = 1 โ†” 2 โ‰  ๐‘ƒ ) )
35 28 34 mpbird โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( 2 gcd ๐‘ƒ ) = 1 )
36 odzphi โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง 2 โˆˆ โ„ค โˆง ( 2 gcd ๐‘ƒ ) = 1 ) โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ฯ• โ€˜ ๐‘ƒ ) )
37 24 26 35 36 syl3anc โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ฯ• โ€˜ ๐‘ƒ ) )
38 phiprm โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ฯ• โ€˜ ๐‘ƒ ) = ( ๐‘ƒ โˆ’ 1 ) )
39 38 ad2antll โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ฯ• โ€˜ ๐‘ƒ ) = ( ๐‘ƒ โˆ’ 1 ) )
40 39 breq2d โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ฯ• โ€˜ ๐‘ƒ ) โ†” ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) )
41 breq1 โŠข ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†” ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) )
42 41 adantl โŠข ( ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โˆง ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†” ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) )
43 2nn โŠข 2 โˆˆ โ„•
44 43 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„• )
45 peano2nn โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ + 1 ) โˆˆ โ„• )
46 45 nnnn0d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ + 1 ) โˆˆ โ„•0 )
47 44 46 nnexpcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆˆ โ„• )
48 23 nnnn0d โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•0 )
49 prmuz2 โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
50 eluzle โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 2 โ‰ค ๐‘ƒ )
51 49 50 syl โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ 2 โ‰ค ๐‘ƒ )
52 nn0ge2m1nn โŠข ( ( ๐‘ƒ โˆˆ โ„•0 โˆง 2 โ‰ค ๐‘ƒ ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„• )
53 48 51 52 syl2anc โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„• )
54 47 53 anim12i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆˆ โ„• โˆง ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„• ) )
55 54 adantl โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆˆ โ„• โˆง ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„• ) )
56 nndivides โŠข ( ( ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆˆ โ„• โˆง ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„• ) โ†’ ( ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†” โˆƒ ๐‘˜ โˆˆ โ„• ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) = ( ๐‘ƒ โˆ’ 1 ) ) )
57 55 56 syl โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†” โˆƒ ๐‘˜ โˆˆ โ„• ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) = ( ๐‘ƒ โˆ’ 1 ) ) )
58 eqcom โŠข ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) = ( ๐‘ƒ โˆ’ 1 ) โ†” ( ๐‘ƒ โˆ’ 1 ) = ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) )
59 58 a1i โŠข ( ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) = ( ๐‘ƒ โˆ’ 1 ) โ†” ( ๐‘ƒ โˆ’ 1 ) = ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) ) )
60 23 nncnd โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„‚ )
61 60 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
62 61 adantr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
63 1cnd โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ 1 โˆˆ โ„‚ )
64 nncn โŠข ( ๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„‚ )
65 64 adantl โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ๐‘˜ โˆˆ โ„‚ )
66 peano2nn0 โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ๐‘ + 1 ) โˆˆ โ„•0 )
67 3 66 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ + 1 ) โˆˆ โ„•0 )
68 44 67 nnexpcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆˆ โ„• )
69 68 nncnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆˆ โ„‚ )
70 69 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆˆ โ„‚ )
71 70 adantr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆˆ โ„‚ )
72 65 71 mulcld โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) โˆˆ โ„‚ )
73 62 63 72 subadd2d โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) = ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) โ†” ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) = ๐‘ƒ ) )
74 73 adantll โŠข ( ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) = ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) โ†” ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) = ๐‘ƒ ) )
75 eqcom โŠข ( ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) = ๐‘ƒ โ†” ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) )
76 75 a1i โŠข ( ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) = ๐‘ƒ โ†” ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
77 59 74 76 3bitrd โŠข ( ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) = ( ๐‘ƒ โˆ’ 1 ) โ†” ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
78 77 rexbidva โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) = ( ๐‘ƒ โˆ’ 1 ) โ†” โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
79 78 biimpd โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) = ( ๐‘ƒ โˆ’ 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
80 57 79 sylbid โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
81 80 adantr โŠข ( ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โˆง ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) โ†’ ( ( 2 โ†‘ ( ๐‘ + 1 ) ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
82 42 81 sylbid โŠข ( ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โˆง ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
83 82 ex โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) ) )
84 83 com23 โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ๐‘ƒ โˆ’ 1 ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) ) )
85 40 84 sylbid โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) โˆฅ ( ฯ• โ€˜ ๐‘ƒ ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) ) )
86 37 85 mpd โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
87 86 3adantr3 โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ ( ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
88 22 87 mpd โŠข ( ( ยฌ ๐‘ƒ = 2 โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) )
89 88 ex โŠข ( ยฌ ๐‘ƒ = 2 โ†’ ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) ) )
90 11 89 pm2.61i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ โˆƒ ๐‘˜ โˆˆ โ„• ๐‘ƒ = ( ( ๐‘˜ ยท ( 2 โ†‘ ( ๐‘ + 1 ) ) ) + 1 ) )