Metamath Proof Explorer

Theorem fmtnofac1

Description: Divisor of Fermat number (Euler's Result), see ProofWiki "Divisor of Fermat Number/Euler's Result", 24-Jul-2021, https://proofwiki.org/wiki/Divisor_of_Fermat_Number/Euler's_Result ): "Let F_n be a Fermat number. Let m be divisor of F_n. Then m is in the form: k*2^(n+1)+1 where k is a positive integer." Here, however, k must be a nonnegative integer, because k must be 0 to represent 1 (which is a divisor of F_n ).

Historical Note: In 1747, Leonhard Paul Euler proved that a divisor of a Fermat number F_n is always in the form kx2^(n+1)+1. This was later refined to k*2^(n+2)+1 by François Édouard Anatole Lucas, see fmtnofac2 . (Contributed by AV, 30-Jul-2021)

Ref Expression
Assertion fmtnofac1 ( ( 𝑁 ∈ β„• ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 elnn1uz2 ⊒ ( 𝑁 ∈ β„• ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ) )
2 5prm ⊒ 5 ∈ β„™
3 dvdsprime ⊒ ( ( 5 ∈ β„™ ∧ 𝑀 ∈ β„• ) β†’ ( 𝑀 βˆ₯ 5 ↔ ( 𝑀 = 5 ∨ 𝑀 = 1 ) ) )
4 2 3 mpan ⊒ ( 𝑀 ∈ β„• β†’ ( 𝑀 βˆ₯ 5 ↔ ( 𝑀 = 5 ∨ 𝑀 = 1 ) ) )
5 1nn0 ⊒ 1 ∈ β„•0
6 5 a1i ⊒ ( 𝑀 = 5 β†’ 1 ∈ β„•0 )
7 simpl ⊒ ( ( 𝑀 = 5 ∧ π‘˜ = 1 ) β†’ 𝑀 = 5 )
8 oveq1 ⊒ ( π‘˜ = 1 β†’ ( π‘˜ Β· 4 ) = ( 1 Β· 4 ) )
9 8 oveq1d ⊒ ( π‘˜ = 1 β†’ ( ( π‘˜ Β· 4 ) + 1 ) = ( ( 1 Β· 4 ) + 1 ) )
10 9 adantl ⊒ ( ( 𝑀 = 5 ∧ π‘˜ = 1 ) β†’ ( ( π‘˜ Β· 4 ) + 1 ) = ( ( 1 Β· 4 ) + 1 ) )
11 7 10 eqeq12d ⊒ ( ( 𝑀 = 5 ∧ π‘˜ = 1 ) β†’ ( 𝑀 = ( ( π‘˜ Β· 4 ) + 1 ) ↔ 5 = ( ( 1 Β· 4 ) + 1 ) ) )
12 df-5 ⊒ 5 = ( 4 + 1 )
13 4cn ⊒ 4 ∈ β„‚
14 13 mullidi ⊒ ( 1 · 4 ) = 4
15 14 eqcomi ⊒ 4 = ( 1 · 4 )
16 15 oveq1i ⊒ ( 4 + 1 ) = ( ( 1 · 4 ) + 1 )
17 12 16 eqtri ⊒ 5 = ( ( 1 · 4 ) + 1 )
18 17 a1i ⊒ ( 𝑀 = 5 β†’ 5 = ( ( 1 Β· 4 ) + 1 ) )
19 6 11 18 rspcedvd ⊒ ( 𝑀 = 5 β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· 4 ) + 1 ) )
20 0nn0 ⊒ 0 ∈ β„•0
21 20 a1i ⊒ ( 𝑀 = 1 β†’ 0 ∈ β„•0 )
22 simpl ⊒ ( ( 𝑀 = 1 ∧ π‘˜ = 0 ) β†’ 𝑀 = 1 )
23 oveq1 ⊒ ( π‘˜ = 0 β†’ ( π‘˜ Β· 4 ) = ( 0 Β· 4 ) )
24 23 oveq1d ⊒ ( π‘˜ = 0 β†’ ( ( π‘˜ Β· 4 ) + 1 ) = ( ( 0 Β· 4 ) + 1 ) )
25 24 adantl ⊒ ( ( 𝑀 = 1 ∧ π‘˜ = 0 ) β†’ ( ( π‘˜ Β· 4 ) + 1 ) = ( ( 0 Β· 4 ) + 1 ) )
26 22 25 eqeq12d ⊒ ( ( 𝑀 = 1 ∧ π‘˜ = 0 ) β†’ ( 𝑀 = ( ( π‘˜ Β· 4 ) + 1 ) ↔ 1 = ( ( 0 Β· 4 ) + 1 ) ) )
27 13 mul02i ⊒ ( 0 · 4 ) = 0
28 27 oveq1i ⊒ ( ( 0 · 4 ) + 1 ) = ( 0 + 1 )
29 0p1e1 ⊒ ( 0 + 1 ) = 1
30 28 29 eqtri ⊒ ( ( 0 · 4 ) + 1 ) = 1
31 30 eqcomi ⊒ 1 = ( ( 0 · 4 ) + 1 )
32 31 a1i ⊒ ( 𝑀 = 1 β†’ 1 = ( ( 0 Β· 4 ) + 1 ) )
33 21 26 32 rspcedvd ⊒ ( 𝑀 = 1 β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· 4 ) + 1 ) )
34 19 33 jaoi ⊒ ( ( 𝑀 = 5 ∨ 𝑀 = 1 ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· 4 ) + 1 ) )
35 4 34 syl6bi ⊒ ( 𝑀 ∈ β„• β†’ ( 𝑀 βˆ₯ 5 β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· 4 ) + 1 ) ) )
36 fveq2 ⊒ ( 𝑁 = 1 β†’ ( FermatNo β€˜ 𝑁 ) = ( FermatNo β€˜ 1 ) )
37 fmtno1 ⊒ ( FermatNo β€˜ 1 ) = 5
38 36 37 eqtrdi ⊒ ( 𝑁 = 1 β†’ ( FermatNo β€˜ 𝑁 ) = 5 )
39 38 breq2d ⊒ ( 𝑁 = 1 β†’ ( 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ↔ 𝑀 βˆ₯ 5 ) )
40 oveq1 ⊒ ( 𝑁 = 1 β†’ ( 𝑁 + 1 ) = ( 1 + 1 ) )
41 1p1e2 ⊒ ( 1 + 1 ) = 2
42 40 41 eqtrdi ⊒ ( 𝑁 = 1 β†’ ( 𝑁 + 1 ) = 2 )
43 42 oveq2d ⊒ ( 𝑁 = 1 β†’ ( 2 ↑ ( 𝑁 + 1 ) ) = ( 2 ↑ 2 ) )
44 sq2 ⊒ ( 2 ↑ 2 ) = 4
45 43 44 eqtrdi ⊒ ( 𝑁 = 1 β†’ ( 2 ↑ ( 𝑁 + 1 ) ) = 4 )
46 45 oveq2d ⊒ ( 𝑁 = 1 β†’ ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( π‘˜ Β· 4 ) )
47 46 oveq1d ⊒ ( 𝑁 = 1 β†’ ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) = ( ( π‘˜ Β· 4 ) + 1 ) )
48 47 eqeq2d ⊒ ( 𝑁 = 1 β†’ ( 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ↔ 𝑀 = ( ( π‘˜ Β· 4 ) + 1 ) ) )
49 48 rexbidv ⊒ ( 𝑁 = 1 β†’ ( βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ↔ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· 4 ) + 1 ) ) )
50 39 49 imbi12d ⊒ ( 𝑁 = 1 β†’ ( ( 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ↔ ( 𝑀 βˆ₯ 5 β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· 4 ) + 1 ) ) ) )
51 35 50 imbitrrid ⊒ ( 𝑁 = 1 β†’ ( 𝑀 ∈ β„• β†’ ( 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) )
52 fmtnofac2 ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ 𝑛 ∈ β„•0 𝑀 = ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
53 id ⊒ ( 𝑛 ∈ β„•0 β†’ 𝑛 ∈ β„•0 )
54 2nn0 ⊒ 2 ∈ β„•0
55 54 a1i ⊒ ( 𝑛 ∈ β„•0 β†’ 2 ∈ β„•0 )
56 53 55 nn0mulcld ⊒ ( 𝑛 ∈ β„•0 β†’ ( 𝑛 Β· 2 ) ∈ β„•0 )
57 56 adantl ⊒ ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝑛 Β· 2 ) ∈ β„•0 )
58 57 adantr ⊒ ( ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑀 = ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) β†’ ( 𝑛 Β· 2 ) ∈ β„•0 )
59 simpr ⊒ ( ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑀 = ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) β†’ 𝑀 = ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
60 oveq1 ⊒ ( π‘˜ = ( 𝑛 Β· 2 ) β†’ ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑛 Β· 2 ) Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) )
61 60 oveq1d ⊒ ( π‘˜ = ( 𝑛 Β· 2 ) β†’ ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) = ( ( ( 𝑛 Β· 2 ) Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) )
62 59 61 eqeqan12d ⊒ ( ( ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑀 = ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ π‘˜ = ( 𝑛 Β· 2 ) ) β†’ ( 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ↔ ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( ( 𝑛 Β· 2 ) Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) )
63 eluzge2nn0 ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ 𝑁 ∈ β„•0 )
64 63 nn0cnd ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ 𝑁 ∈ β„‚ )
65 add1p1 ⊒ ( 𝑁 ∈ β„‚ β†’ ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
66 64 65 syl ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
67 66 eqcomd ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 𝑁 + 2 ) = ( ( 𝑁 + 1 ) + 1 ) )
68 67 oveq2d ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 2 ↑ ( 𝑁 + 2 ) ) = ( 2 ↑ ( ( 𝑁 + 1 ) + 1 ) ) )
69 2cnd ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ 2 ∈ β„‚ )
70 peano2nn0 ⊒ ( 𝑁 ∈ β„•0 β†’ ( 𝑁 + 1 ) ∈ β„•0 )
71 63 70 syl ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 𝑁 + 1 ) ∈ β„•0 )
72 69 71 expp1d ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 2 ↑ ( ( 𝑁 + 1 ) + 1 ) ) = ( ( 2 ↑ ( 𝑁 + 1 ) ) Β· 2 ) )
73 54 a1i ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ 2 ∈ β„•0 )
74 73 71 nn0expcld ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 2 ↑ ( 𝑁 + 1 ) ) ∈ β„•0 )
75 74 nn0cnd ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 2 ↑ ( 𝑁 + 1 ) ) ∈ β„‚ )
76 75 69 mulcomd ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( ( 2 ↑ ( 𝑁 + 1 ) ) Β· 2 ) = ( 2 Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) )
77 68 72 76 3eqtrd ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 2 ↑ ( 𝑁 + 2 ) ) = ( 2 Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) )
78 77 adantr ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( 2 ↑ ( 𝑁 + 2 ) ) = ( 2 Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) )
79 78 oveq2d ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( 𝑛 Β· ( 2 Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
80 nn0cn ⊒ ( 𝑛 ∈ β„•0 β†’ 𝑛 ∈ β„‚ )
81 80 adantl ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑛 ∈ β„•0 ) β†’ 𝑛 ∈ β„‚ )
82 2cnd ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑛 ∈ β„•0 ) β†’ 2 ∈ β„‚ )
83 75 adantr ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( 2 ↑ ( 𝑁 + 1 ) ) ∈ β„‚ )
84 81 82 83 mulassd ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( ( 𝑛 Β· 2 ) Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( 𝑛 Β· ( 2 Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
85 79 84 eqtr4d ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( 𝑛 Β· 2 ) Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) )
86 85 3ad2antl1 ⊒ ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( 𝑛 Β· 2 ) Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) )
87 86 adantr ⊒ ( ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑀 = ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) β†’ ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( 𝑛 Β· 2 ) Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) )
88 87 oveq1d ⊒ ( ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑀 = ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) β†’ ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( ( 𝑛 Β· 2 ) Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) )
89 58 62 88 rspcedvd ⊒ ( ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑀 = ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) )
90 89 rexlimdva2 ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ ( βˆƒ 𝑛 ∈ β„•0 𝑀 = ( ( 𝑛 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) )
91 52 90 mpd ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) )
92 91 3exp ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 𝑀 ∈ β„• β†’ ( 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) )
93 51 92 jaoi ⊒ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ) β†’ ( 𝑀 ∈ β„• β†’ ( 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) )
94 1 93 sylbi ⊒ ( 𝑁 ∈ β„• β†’ ( 𝑀 ∈ β„• β†’ ( 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) )
95 94 3imp ⊒ ( ( 𝑁 ∈ β„• ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) )