Metamath Proof Explorer


Theorem perfectlem1

Description: Lemma for perfect . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses perfectlem.1
|- ( ph -> A e. NN )
perfectlem.2
|- ( ph -> B e. NN )
perfectlem.3
|- ( ph -> -. 2 || B )
perfectlem.4
|- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )
Assertion perfectlem1
|- ( ph -> ( ( 2 ^ ( A + 1 ) ) e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )

Proof

Step Hyp Ref Expression
1 perfectlem.1
 |-  ( ph -> A e. NN )
2 perfectlem.2
 |-  ( ph -> B e. NN )
3 perfectlem.3
 |-  ( ph -> -. 2 || B )
4 perfectlem.4
 |-  ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )
5 2nn
 |-  2 e. NN
6 1 nnnn0d
 |-  ( ph -> A e. NN0 )
7 peano2nn0
 |-  ( A e. NN0 -> ( A + 1 ) e. NN0 )
8 6 7 syl
 |-  ( ph -> ( A + 1 ) e. NN0 )
9 nnexpcl
 |-  ( ( 2 e. NN /\ ( A + 1 ) e. NN0 ) -> ( 2 ^ ( A + 1 ) ) e. NN )
10 5 8 9 sylancr
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) e. NN )
11 2re
 |-  2 e. RR
12 1 peano2nnd
 |-  ( ph -> ( A + 1 ) e. NN )
13 1lt2
 |-  1 < 2
14 13 a1i
 |-  ( ph -> 1 < 2 )
15 expgt1
 |-  ( ( 2 e. RR /\ ( A + 1 ) e. NN /\ 1 < 2 ) -> 1 < ( 2 ^ ( A + 1 ) ) )
16 11 12 14 15 mp3an2i
 |-  ( ph -> 1 < ( 2 ^ ( A + 1 ) ) )
17 1nn
 |-  1 e. NN
18 nnsub
 |-  ( ( 1 e. NN /\ ( 2 ^ ( A + 1 ) ) e. NN ) -> ( 1 < ( 2 ^ ( A + 1 ) ) <-> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN ) )
19 17 10 18 sylancr
 |-  ( ph -> ( 1 < ( 2 ^ ( A + 1 ) ) <-> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN ) )
20 16 19 mpbid
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN )
21 10 nnzd
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) e. ZZ )
22 peano2zm
 |-  ( ( 2 ^ ( A + 1 ) ) e. ZZ -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ )
23 21 22 syl
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ )
24 1nn0
 |-  1 e. NN0
25 sgmnncl
 |-  ( ( 1 e. NN0 /\ B e. NN ) -> ( 1 sigma B ) e. NN )
26 24 2 25 sylancr
 |-  ( ph -> ( 1 sigma B ) e. NN )
27 26 nnzd
 |-  ( ph -> ( 1 sigma B ) e. ZZ )
28 dvdsmul1
 |-  ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ /\ ( 1 sigma B ) e. ZZ ) -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
29 23 27 28 syl2anc
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
30 2cn
 |-  2 e. CC
31 expp1
 |-  ( ( 2 e. CC /\ A e. NN0 ) -> ( 2 ^ ( A + 1 ) ) = ( ( 2 ^ A ) x. 2 ) )
32 30 6 31 sylancr
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) = ( ( 2 ^ A ) x. 2 ) )
33 nnexpcl
 |-  ( ( 2 e. NN /\ A e. NN0 ) -> ( 2 ^ A ) e. NN )
34 5 6 33 sylancr
 |-  ( ph -> ( 2 ^ A ) e. NN )
35 34 nncnd
 |-  ( ph -> ( 2 ^ A ) e. CC )
36 mulcom
 |-  ( ( ( 2 ^ A ) e. CC /\ 2 e. CC ) -> ( ( 2 ^ A ) x. 2 ) = ( 2 x. ( 2 ^ A ) ) )
37 35 30 36 sylancl
 |-  ( ph -> ( ( 2 ^ A ) x. 2 ) = ( 2 x. ( 2 ^ A ) ) )
38 32 37 eqtrd
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) = ( 2 x. ( 2 ^ A ) ) )
39 38 oveq1d
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. B ) = ( ( 2 x. ( 2 ^ A ) ) x. B ) )
40 30 a1i
 |-  ( ph -> 2 e. CC )
41 2 nncnd
 |-  ( ph -> B e. CC )
42 40 35 41 mulassd
 |-  ( ph -> ( ( 2 x. ( 2 ^ A ) ) x. B ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )
43 ax-1cn
 |-  1 e. CC
44 43 a1i
 |-  ( ph -> 1 e. CC )
45 2prm
 |-  2 e. Prime
46 2 nnzd
 |-  ( ph -> B e. ZZ )
47 coprm
 |-  ( ( 2 e. Prime /\ B e. ZZ ) -> ( -. 2 || B <-> ( 2 gcd B ) = 1 ) )
48 45 46 47 sylancr
 |-  ( ph -> ( -. 2 || B <-> ( 2 gcd B ) = 1 ) )
49 3 48 mpbid
 |-  ( ph -> ( 2 gcd B ) = 1 )
50 2z
 |-  2 e. ZZ
51 rpexp1i
 |-  ( ( 2 e. ZZ /\ B e. ZZ /\ A e. NN0 ) -> ( ( 2 gcd B ) = 1 -> ( ( 2 ^ A ) gcd B ) = 1 ) )
52 50 46 6 51 mp3an2i
 |-  ( ph -> ( ( 2 gcd B ) = 1 -> ( ( 2 ^ A ) gcd B ) = 1 ) )
53 49 52 mpd
 |-  ( ph -> ( ( 2 ^ A ) gcd B ) = 1 )
54 sgmmul
 |-  ( ( 1 e. CC /\ ( ( 2 ^ A ) e. NN /\ B e. NN /\ ( ( 2 ^ A ) gcd B ) = 1 ) ) -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( ( 1 sigma ( 2 ^ A ) ) x. ( 1 sigma B ) ) )
55 44 34 2 53 54 syl13anc
 |-  ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( ( 1 sigma ( 2 ^ A ) ) x. ( 1 sigma B ) ) )
56 1 nncnd
 |-  ( ph -> A e. CC )
57 pncan
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - 1 ) = A )
58 56 43 57 sylancl
 |-  ( ph -> ( ( A + 1 ) - 1 ) = A )
59 58 oveq2d
 |-  ( ph -> ( 2 ^ ( ( A + 1 ) - 1 ) ) = ( 2 ^ A ) )
60 59 oveq2d
 |-  ( ph -> ( 1 sigma ( 2 ^ ( ( A + 1 ) - 1 ) ) ) = ( 1 sigma ( 2 ^ A ) ) )
61 1sgm2ppw
 |-  ( ( A + 1 ) e. NN -> ( 1 sigma ( 2 ^ ( ( A + 1 ) - 1 ) ) ) = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
62 12 61 syl
 |-  ( ph -> ( 1 sigma ( 2 ^ ( ( A + 1 ) - 1 ) ) ) = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
63 60 62 eqtr3d
 |-  ( ph -> ( 1 sigma ( 2 ^ A ) ) = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
64 63 oveq1d
 |-  ( ph -> ( ( 1 sigma ( 2 ^ A ) ) x. ( 1 sigma B ) ) = ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
65 55 4 64 3eqtr3d
 |-  ( ph -> ( 2 x. ( ( 2 ^ A ) x. B ) ) = ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
66 39 42 65 3eqtrd
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. B ) = ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
67 29 66 breqtrrd
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( 2 ^ ( A + 1 ) ) x. B ) )
68 23 21 gcdcomd
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) gcd ( 2 ^ ( A + 1 ) ) ) = ( ( 2 ^ ( A + 1 ) ) gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
69 iddvdsexp
 |-  ( ( 2 e. ZZ /\ ( A + 1 ) e. NN ) -> 2 || ( 2 ^ ( A + 1 ) ) )
70 50 12 69 sylancr
 |-  ( ph -> 2 || ( 2 ^ ( A + 1 ) ) )
71 n2dvds1
 |-  -. 2 || 1
72 50 a1i
 |-  ( ph -> 2 e. ZZ )
73 1zzd
 |-  ( ph -> 1 e. ZZ )
74 72 21 73 3jca
 |-  ( ph -> ( 2 e. ZZ /\ ( 2 ^ ( A + 1 ) ) e. ZZ /\ 1 e. ZZ ) )
75 dvdssub2
 |-  ( ( ( 2 e. ZZ /\ ( 2 ^ ( A + 1 ) ) e. ZZ /\ 1 e. ZZ ) /\ 2 || ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> ( 2 || ( 2 ^ ( A + 1 ) ) <-> 2 || 1 ) )
76 74 75 sylan
 |-  ( ( ph /\ 2 || ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> ( 2 || ( 2 ^ ( A + 1 ) ) <-> 2 || 1 ) )
77 71 76 mtbiri
 |-  ( ( ph /\ 2 || ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> -. 2 || ( 2 ^ ( A + 1 ) ) )
78 77 ex
 |-  ( ph -> ( 2 || ( ( 2 ^ ( A + 1 ) ) - 1 ) -> -. 2 || ( 2 ^ ( A + 1 ) ) ) )
79 70 78 mt2d
 |-  ( ph -> -. 2 || ( ( 2 ^ ( A + 1 ) ) - 1 ) )
80 coprm
 |-  ( ( 2 e. Prime /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ ) -> ( -. 2 || ( ( 2 ^ ( A + 1 ) ) - 1 ) <-> ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 ) )
81 45 23 80 sylancr
 |-  ( ph -> ( -. 2 || ( ( 2 ^ ( A + 1 ) ) - 1 ) <-> ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 ) )
82 79 81 mpbid
 |-  ( ph -> ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 )
83 rpexp1i
 |-  ( ( 2 e. ZZ /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ /\ ( A + 1 ) e. NN0 ) -> ( ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 -> ( ( 2 ^ ( A + 1 ) ) gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 ) )
84 50 23 8 83 mp3an2i
 |-  ( ph -> ( ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 -> ( ( 2 ^ ( A + 1 ) ) gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 ) )
85 82 84 mpd
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 )
86 68 85 eqtrd
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) gcd ( 2 ^ ( A + 1 ) ) ) = 1 )
87 coprmdvds
 |-  ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ /\ ( 2 ^ ( A + 1 ) ) e. ZZ /\ B e. ZZ ) -> ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( 2 ^ ( A + 1 ) ) x. B ) /\ ( ( ( 2 ^ ( A + 1 ) ) - 1 ) gcd ( 2 ^ ( A + 1 ) ) ) = 1 ) -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || B ) )
88 23 21 46 87 syl3anc
 |-  ( ph -> ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( 2 ^ ( A + 1 ) ) x. B ) /\ ( ( ( 2 ^ ( A + 1 ) ) - 1 ) gcd ( 2 ^ ( A + 1 ) ) ) = 1 ) -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || B ) )
89 67 86 88 mp2and
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || B )
90 nndivdvds
 |-  ( ( B e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN ) -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) || B <-> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )
91 2 20 90 syl2anc
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) || B <-> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )
92 89 91 mpbid
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN )
93 10 20 92 3jca
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )