Metamath Proof Explorer


Theorem perfectlem1

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

Ref Expression
Hypotheses perfectlem.1 ( 𝜑𝐴 ∈ ℕ )
perfectlem.2 ( 𝜑𝐵 ∈ ℕ )
perfectlem.3 ( 𝜑 → ¬ 2 ∥ 𝐵 )
perfectlem.4 ( 𝜑 → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) )
Assertion perfectlem1 ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ∧ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )

Proof

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