Metamath Proof Explorer

Theorem perfectALTVlem1

Description: Lemma for perfectALTV . (Contributed by Mario Carneiro, 7-Jun-2016) (Revised by AV, 1-Jul-2020)

Ref Expression
Hypotheses perfectALTVlem.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
perfectALTVlem.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
perfectALTVlem.3 ⊢ ( 𝜑 → 𝐵 ∈ Odd )
perfectALTVlem.4 ⊢ ( 𝜑 → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) )
Assertion perfectALTVlem1 ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ∧ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )

Proof

Step Hyp Ref Expression
1 perfectALTVlem.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 perfectALTVlem.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 perfectALTVlem.3 ⊢ ( 𝜑 → 𝐵 ∈ Odd )
4 perfectALTVlem.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 11 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
13 1 peano2nnd ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℕ )
14 1lt2 ⊢ 1 < 2
15 14 a1i ⊢ ( 𝜑 → 1 < 2 )
16 expgt1 ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℕ ∧ 1 < 2 ) → 1 < ( 2 ↑ ( 𝐴 + 1 ) ) )
17 12 13 15 16 syl3anc ⊢ ( 𝜑 → 1 < ( 2 ↑ ( 𝐴 + 1 ) ) )
18 1nn ⊢ 1 ∈ ℕ
19 nnsub ⊢ ( ( 1 ∈ ℕ ∧ ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ ) → ( 1 < ( 2 ↑ ( 𝐴 + 1 ) ) ↔ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ) )
20 18 10 19 sylancr ⊢ ( 𝜑 → ( 1 < ( 2 ↑ ( 𝐴 + 1 ) ) ↔ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ) )
21 17 20 mpbid ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ )
22 10 nnzd ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℤ )
23 peano2zm ⊢ ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℤ → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ )
24 22 23 syl ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ )
25 1nn0 ⊢ 1 ∈ ℕ0
26 sgmnncl ⊢ ( ( 1 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 σ 𝐵 ) ∈ ℕ )
27 25 2 26 sylancr ⊢ ( 𝜑 → ( 1 σ 𝐵 ) ∈ ℕ )
28 27 nnzd ⊢ ( 𝜑 → ( 1 σ 𝐵 ) ∈ ℤ )
29 dvdsmul1 ⊢ ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 1 σ 𝐵 ) ∈ ℤ ) → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
30 24 28 29 syl2anc ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
31 2cn ⊢ 2 ∈ ℂ
32 expp1 ⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℕ0 ) → ( 2 ↑ ( 𝐴 + 1 ) ) = ( ( 2 ↑ 𝐴 ) · 2 ) )
33 31 6 32 sylancr ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) = ( ( 2 ↑ 𝐴 ) · 2 ) )
34 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐴 ∈ ℕ0 ) → ( 2 ↑ 𝐴 ) ∈ ℕ )
35 5 6 34 sylancr ⊢ ( 𝜑 → ( 2 ↑ 𝐴 ) ∈ ℕ )
36 35 nncnd ⊢ ( 𝜑 → ( 2 ↑ 𝐴 ) ∈ ℂ )
37 mulcom ⊢ ( ( ( 2 ↑ 𝐴 ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 2 ↑ 𝐴 ) · 2 ) = ( 2 · ( 2 ↑ 𝐴 ) ) )
38 36 31 37 sylancl ⊢ ( 𝜑 → ( ( 2 ↑ 𝐴 ) · 2 ) = ( 2 · ( 2 ↑ 𝐴 ) ) )
39 33 38 eqtrd ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) = ( 2 · ( 2 ↑ 𝐴 ) ) )
40 39 oveq1d ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) = ( ( 2 · ( 2 ↑ 𝐴 ) ) · 𝐵 ) )
41 31 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
42 2 nncnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
43 41 36 42 mulassd ⊢ ( 𝜑 → ( ( 2 · ( 2 ↑ 𝐴 ) ) · 𝐵 ) = ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) )
44 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
45 isodd7 ⊢ ( 𝐵 ∈ Odd ↔ ( 𝐵 ∈ ℤ ∧ ( 2 gcd 𝐵 ) = 1 ) )
46 45 simprbi ⊢ ( 𝐵 ∈ Odd → ( 2 gcd 𝐵 ) = 1 )
47 3 46 syl ⊢ ( 𝜑 → ( 2 gcd 𝐵 ) = 1 )
48 2z ⊢ 2 ∈ ℤ
49 48 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
50 2 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
51 rpexp1i ⊢ ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( ( 2 gcd 𝐵 ) = 1 → ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 ) )
52 49 50 6 51 syl3anc ⊢ ( 𝜑 → ( ( 2 gcd 𝐵 ) = 1 → ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 ) )
53 47 52 mpd ⊢ ( 𝜑 → ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 )
54 sgmmul ⊢ ( ( 1 ∈ ℂ ∧ ( ( 2 ↑ 𝐴 ) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 ) ) → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( ( 1 σ ( 2 ↑ 𝐴 ) ) · ( 1 σ 𝐵 ) ) )
55 44 35 2 53 54 syl13anc ⊢ ( 𝜑 → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( ( 1 σ ( 2 ↑ 𝐴 ) ) · ( 1 σ 𝐵 ) ) )
56 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
57 pncan1 ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
58 56 57 syl ⊢ ( 𝜑 → ( ( 𝐴 + 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 13 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 40 43 65 3eqtrd ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
67 30 66 breqtrrd ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) )
68 24 22 gcdcomd ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) gcd ( 2 ↑ ( 𝐴 + 1 ) ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
69 nnpw2evenALTV ⊢ ( ( 𝐴 + 1 ) ∈ ℕ → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ Even )
70 evenm1odd ⊢ ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ Even → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ Odd )
71 isodd7 ⊢ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ Odd ↔ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 ) )
72 71 simprbi ⊢ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ Odd → ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 )
73 13 69 70 72 4syl ⊢ ( 𝜑 → ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 )
74 rpexp1i ⊢ ( ( 2 ∈ ℤ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℕ0 ) → ( ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 → ( ( 2 ↑ ( 𝐴 + 1 ) ) gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 ) )
75 49 24 8 74 syl3anc ⊢ ( 𝜑 → ( ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 → ( ( 2 ↑ ( 𝐴 + 1 ) ) gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 ) )
76 73 75 mpd ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 )
77 68 76 eqtrd ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) gcd ( 2 ↑ ( 𝐴 + 1 ) ) ) = 1 )
78 coprmdvds ⊢ ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) ∧ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) gcd ( 2 ↑ ( 𝐴 + 1 ) ) ) = 1 ) → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 ) )
79 24 22 50 78 syl3anc ⊢ ( 𝜑 → ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) ∧ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) gcd ( 2 ↑ ( 𝐴 + 1 ) ) ) = 1 ) → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 ) )
80 67 77 79 mp2and ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 )
81 nndivdvds ⊢ ( ( 𝐵 ∈ ℕ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ) → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 ↔ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )
82 2 21 81 syl2anc ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 ↔ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )
83 80 82 mpbid ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ )
84 10 21 83 3jca ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ∧ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )