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 ) )