Metamath Proof Explorer

Theorem fmtnoprmfac1lem

Description: Lemma for fmtnoprmfac1 : The order of 2 modulo a prime that divides the n-th Fermat number is 2^(n+1). (Contributed by AV, 25-Jul-2021) (Proof shortened by AV, 18-Mar-2022)

Ref Expression
Assertion fmtnoprmfac1lem ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) )

Proof

Step Hyp Ref Expression
1 eldifi โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ โ„™ )
2 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
3 1 2 syl โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ โ„• )
4 3 ad2antlr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
5 nnnn0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•0 )
6 fmtno โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( FermatNo โ€˜ ๐‘ ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) )
7 5 6 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( FermatNo โ€˜ ๐‘ ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) )
8 7 breq2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†” ๐‘ƒ โˆฅ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) ) )
9 8 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†” ๐‘ƒ โˆฅ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) ) )
10 9 biimpa โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ๐‘ƒ โˆฅ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) )
11 dvdsmod0 โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘ƒ โˆฅ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 )
12 4 10 11 syl2anc โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 )
13 12 ex โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 ) )
14 2nn โŠข 2 โˆˆ โ„•
15 14 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„• )
16 2nn0 โŠข 2 โˆˆ โ„•0
17 16 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„•0 )
18 17 5 nn0expcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 )
19 15 18 nnexpcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„• )
20 19 nnzd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค )
21 20 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค )
22 1zzd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ 1 โˆˆ โ„ค )
23 3 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
24 summodnegmod โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„• ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†” ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
25 21 22 23 24 syl3anc โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†” ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
26 neg1z โŠข - 1 โˆˆ โ„ค
27 21 26 jctir โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค โˆง - 1 โˆˆ โ„ค ) )
28 27 adantr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค โˆง - 1 โˆˆ โ„ค ) )
29 2 nnrpd โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„+ )
30 1 29 syl โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ โ„+ )
31 17 30 anim12i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( 2 โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„+ ) )
32 31 adantr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†’ ( 2 โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„+ ) )
33 simpr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
34 modexp โŠข ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค โˆง - 1 โˆˆ โ„ค ) โˆง ( 2 โˆˆ โ„•0 โˆง ๐‘ƒ โˆˆ โ„+ ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) mod ๐‘ƒ ) = ( ( - 1 โ†‘ 2 ) mod ๐‘ƒ ) )
35 28 32 33 34 syl3anc โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) mod ๐‘ƒ ) = ( ( - 1 โ†‘ 2 ) mod ๐‘ƒ ) )
36 35 ex โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) mod ๐‘ƒ ) = ( ( - 1 โ†‘ 2 ) mod ๐‘ƒ ) ) )
37 2cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„‚ )
38 37 18 17 3jca โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โˆˆ โ„‚ โˆง ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 โˆง 2 โˆˆ โ„•0 ) )
39 38 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( 2 โˆˆ โ„‚ โˆง ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 โˆง 2 โˆˆ โ„•0 ) )
40 expmul โŠข ( ( 2 โˆˆ โ„‚ โˆง ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 โˆง 2 โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) ยท 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) )
41 39 40 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) ยท 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) )
42 2cnd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ 2 โˆˆ โ„‚ )
43 5 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ๐‘ โˆˆ โ„•0 )
44 42 43 expp1d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( 2 โ†‘ ( ๐‘ + 1 ) ) = ( ( 2 โ†‘ ๐‘ ) ยท 2 ) )
45 44 eqcomd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( 2 โ†‘ ๐‘ ) ยท 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) )
46 45 oveq2d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ๐‘ ) ยท 2 ) ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) )
47 41 46 eqtr3d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) )
48 47 oveq1d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) mod ๐‘ƒ ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) )
49 neg1sqe1 โŠข ( - 1 โ†‘ 2 ) = 1
50 49 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( - 1 โ†‘ 2 ) = 1 )
51 50 oveq1d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( - 1 โ†‘ 2 ) mod ๐‘ƒ ) = ( 1 mod ๐‘ƒ ) )
52 3 nnred โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ โ„ )
53 prmgt1 โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ 1 < ๐‘ƒ )
54 1 53 syl โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ 1 < ๐‘ƒ )
55 1mod โŠข ( ( ๐‘ƒ โˆˆ โ„ โˆง 1 < ๐‘ƒ ) โ†’ ( 1 mod ๐‘ƒ ) = 1 )
56 52 54 55 syl2anc โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ( 1 mod ๐‘ƒ ) = 1 )
57 56 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( 1 mod ๐‘ƒ ) = 1 )
58 51 57 eqtrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( - 1 โ†‘ 2 ) mod ๐‘ƒ ) = 1 )
59 48 58 eqeq12d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) mod ๐‘ƒ ) = ( ( - 1 โ†‘ 2 ) mod ๐‘ƒ ) โ†” ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) )
60 simpll โŠข ( ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โˆง ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 ) โ†’ ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) )
61 20 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค )
62 1zzd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ 1 โˆˆ โ„ค )
63 2 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ๐‘ƒ โˆˆ โ„• )
64 61 62 63 3jca โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„• ) )
65 1 64 sylan2 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„• ) )
66 65 adantr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„• ) )
67 66 24 syl โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†” ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
68 m1modnnsub1 โŠข ( ๐‘ƒ โˆˆ โ„• โ†’ ( - 1 mod ๐‘ƒ ) = ( ๐‘ƒ โˆ’ 1 ) )
69 23 68 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( - 1 mod ๐‘ƒ ) = ( ๐‘ƒ โˆ’ 1 ) )
70 eldifsni โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โ‰  2 )
71 70 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ๐‘ƒ โ‰  2 )
72 71 necomd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ 2 โ‰  ๐‘ƒ )
73 3 nncnd โŠข ( ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
74 73 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
75 1cnd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ 1 โˆˆ โ„‚ )
76 74 75 75 subadd2d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) = 1 โ†” ( 1 + 1 ) = ๐‘ƒ ) )
77 1p1e2 โŠข ( 1 + 1 ) = 2
78 77 eqeq1i โŠข ( ( 1 + 1 ) = ๐‘ƒ โ†” 2 = ๐‘ƒ )
79 76 78 bitrdi โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) = 1 โ†” 2 = ๐‘ƒ ) )
80 79 necon3bid โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) โ‰  1 โ†” 2 โ‰  ๐‘ƒ ) )
81 72 80 mpbird โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โ‰  1 )
82 69 81 eqnetrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( - 1 mod ๐‘ƒ ) โ‰  1 )
83 82 adantr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โ†’ ( - 1 mod ๐‘ƒ ) โ‰  1 )
84 83 adantr โŠข ( ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†’ ( - 1 mod ๐‘ƒ ) โ‰  1 )
85 eqeq1 โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = 1 โ†” ( - 1 mod ๐‘ƒ ) = 1 ) )
86 85 adantl โŠข ( ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = 1 โ†” ( - 1 mod ๐‘ƒ ) = 1 ) )
87 86 necon3bid โŠข ( ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) โ‰  1 โ†” ( - 1 mod ๐‘ƒ ) โ‰  1 ) )
88 84 87 mpbird โŠข ( ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) โ‰  1 )
89 88 ex โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) โ‰  1 ) )
90 67 89 sylbid โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) โ‰  1 ) )
91 90 imp โŠข ( ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โˆง ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) โ‰  1 )
92 simplr โŠข ( ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โˆง ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 )
93 odz2prm2pw โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) โ‰  1 โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) ) โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) )
94 60 91 92 93 syl12anc โŠข ( ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โˆง ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 ) โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) )
95 94 ex โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โˆง ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) )
96 95 ex โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ + 1 ) ) ) mod ๐‘ƒ ) = 1 โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) ) )
97 59 96 sylbid โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ†‘ 2 ) mod ๐‘ƒ ) = ( ( - 1 โ†‘ 2 ) mod ๐‘ƒ ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) ) )
98 36 97 syld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) ) )
99 25 98 sylbid โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) ) )
100 99 pm2.43d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + 1 ) mod ๐‘ƒ ) = 0 โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) )
101 13 100 syld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) ) โ†’ ( ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) ) )
102 101 3impia โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ ( โ„™ โˆ– { 2 } ) โˆง ๐‘ƒ โˆฅ ( FermatNo โ€˜ ๐‘ ) ) โ†’ ( ( odโ„ค โ€˜ ๐‘ƒ ) โ€˜ 2 ) = ( 2 โ†‘ ( ๐‘ + 1 ) ) )