Metamath Proof Explorer

Theorem perfectALTVlem2

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

Ref Expression
Hypotheses perfectALTVlem.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
perfectALTVlem.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
perfectALTVlem.3 ⊢ ( 𝜑 → 𝐵 ∈ Odd )
perfectALTVlem.4 ⊢ ( 𝜑 → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) )
Assertion perfectALTVlem2 ( 𝜑 → ( 𝐵 ∈ ℙ ∧ 𝐵 = ( ( 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 1re ⊢ 1 ∈ ℝ
6 5 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
7 1 2 3 4 perfectALTVlem1 ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ∧ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )
8 7 simp3d ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ )
9 8 nnred ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℝ )
10 2 nnred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
11 8 nnge1d ⊢ ( 𝜑 → 1 ≤ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
12 2cn ⊢ 2 ∈ ℂ
13 exp1 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 1 ) = 2 )
14 12 13 ax-mp ⊢ ( 2 ↑ 1 ) = 2
15 df-2 ⊢ 2 = ( 1 + 1 )
16 14 15 eqtri ⊢ ( 2 ↑ 1 ) = ( 1 + 1 )
17 2re ⊢ 2 ∈ ℝ
18 17 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
19 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
20 1 peano2nnd ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℕ )
21 20 nnzd ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℤ )
22 1lt2 ⊢ 1 < 2
23 22 a1i ⊢ ( 𝜑 → 1 < 2 )
24 1 nnrpd ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
25 ltaddrp ⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 1 < ( 1 + 𝐴 ) )
26 5 24 25 sylancr ⊢ ( 𝜑 → 1 < ( 1 + 𝐴 ) )
27 ax-1cn ⊢ 1 ∈ ℂ
28 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
29 addcom ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 + 𝐴 ) = ( 𝐴 + 1 ) )
30 27 28 29 sylancr ⊢ ( 𝜑 → ( 1 + 𝐴 ) = ( 𝐴 + 1 ) )
31 26 30 breqtrd ⊢ ( 𝜑 → 1 < ( 𝐴 + 1 ) )
32 ltexp2a ⊢ ( ( ( 2 ∈ ℝ ∧ 1 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℤ ) ∧ ( 1 < 2 ∧ 1 < ( 𝐴 + 1 ) ) ) → ( 2 ↑ 1 ) < ( 2 ↑ ( 𝐴 + 1 ) ) )
33 18 19 21 23 31 32 syl32anc ⊢ ( 𝜑 → ( 2 ↑ 1 ) < ( 2 ↑ ( 𝐴 + 1 ) ) )
34 16 33 eqbrtrrid ⊢ ( 𝜑 → ( 1 + 1 ) < ( 2 ↑ ( 𝐴 + 1 ) ) )
35 7 simp1d ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ )
36 35 nnred ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℝ )
37 6 6 36 ltaddsubd ⊢ ( 𝜑 → ( ( 1 + 1 ) < ( 2 ↑ ( 𝐴 + 1 ) ) ↔ 1 < ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
38 34 37 mpbid ⊢ ( 𝜑 → 1 < ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
39 1rp ⊢ 1 ∈ ℝ+
40 39 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
41 peano2rem ⊢ ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℝ → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℝ )
42 36 41 syl ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℝ )
43 expgt1 ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℕ ∧ 1 < 2 ) → 1 < ( 2 ↑ ( 𝐴 + 1 ) ) )
44 18 20 23 43 syl3anc ⊢ ( 𝜑 → 1 < ( 2 ↑ ( 𝐴 + 1 ) ) )
45 posdif ⊢ ( ( 1 ∈ ℝ ∧ ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℝ ) → ( 1 < ( 2 ↑ ( 𝐴 + 1 ) ) ↔ 0 < ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
46 5 36 45 sylancr ⊢ ( 𝜑 → ( 1 < ( 2 ↑ ( 𝐴 + 1 ) ) ↔ 0 < ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
47 44 46 mpbid ⊢ ( 𝜑 → 0 < ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
48 42 47 jca ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℝ ∧ 0 < ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
49 elrp ⊢ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℝ+ ↔ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℝ ∧ 0 < ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
50 48 49 sylibr ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℝ+ )
51 nnrp ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
52 2 51 syl ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
53 40 50 52 ltdiv2d ⊢ ( 𝜑 → ( 1 < ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ↔ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) < ( 𝐵 / 1 ) ) )
54 38 53 mpbid ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) < ( 𝐵 / 1 ) )
55 2 nncnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
56 55 div1d ⊢ ( 𝜑 → ( 𝐵 / 1 ) = 𝐵 )
57 54 56 breqtrd ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) < 𝐵 )
58 6 9 10 11 57 lelttrd ⊢ ( 𝜑 → 1 < 𝐵 )
59 eluz2b2 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐵 ∈ ℕ ∧ 1 < 𝐵 ) )
60 2 58 59 sylanbrc ⊢ ( 𝜑 → 𝐵 ∈ ( ℤ≥ ‘ 2 ) )
61 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ∈ Fin )
62 dvdsssfz1 ⊢ ( 𝐵 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ⊆ ( 1 ... 𝐵 ) )
63 2 62 syl ⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ⊆ ( 1 ... 𝐵 ) )
64 ssfi ⊢ ( ( ( 1 ... 𝐵 ) ∈ Fin ∧ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ⊆ ( 1 ... 𝐵 ) ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ∈ Fin )
65 61 63 64 syl2anc ⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ∈ Fin )
66 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ∈ Fin )
67 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ⊆ ℕ
68 67 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ⊆ ℕ )
69 68 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 𝑘 ∈ ℕ )
70 69 nnred ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 𝑘 ∈ ℝ )
71 69 nnnn0d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 𝑘 ∈ ℕ0 )
72 71 nn0ge0d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 0 ≤ 𝑘 )
73 df-tp ⊢ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } = ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∪ { 𝑛 } )
74 prssi ⊢ ( ( ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ∧ 𝐵 ∈ ℕ ) → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ⊆ ℕ )
75 8 2 74 syl2anc ⊢ ( 𝜑 → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ⊆ ℕ )
76 75 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ⊆ ℕ )
77 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → 𝑛 ∈ ℕ )
78 77 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → { 𝑛 } ⊆ ℕ )
79 76 78 unssd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∪ { 𝑛 } ) ⊆ ℕ )
80 73 79 eqsstrid ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } ⊆ ℕ )
81 eltpi ⊢ ( 𝑥 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } → ( 𝑥 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛 ) )
82 7 simp2d ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ )
83 82 nnzd ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ )
84 8 nnzd ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℤ )
85 dvdsmul2 ⊢ ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℤ ) → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∥ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
86 83 84 85 syl2anc ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∥ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
87 82 nncnd ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℂ )
88 82 nnne0d ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ≠ 0 )
89 55 87 88 divcan2d ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) = 𝐵 )
90 86 89 breqtrd ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∥ 𝐵 )
91 breq1 ⊢ ( 𝑥 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ( 𝑥 ∥ 𝐵 ↔ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∥ 𝐵 ) )
92 90 91 syl5ibrcom ⊢ ( 𝜑 → ( 𝑥 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → 𝑥 ∥ 𝐵 ) )
93 92 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( 𝑥 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → 𝑥 ∥ 𝐵 ) )
94 2 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
95 iddvds ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∥ 𝐵 )
96 94 95 syl ⊢ ( 𝜑 → 𝐵 ∥ 𝐵 )
97 breq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵 ) )
98 96 97 syl5ibrcom ⊢ ( 𝜑 → ( 𝑥 = 𝐵 → 𝑥 ∥ 𝐵 ) )
99 98 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( 𝑥 = 𝐵 → 𝑥 ∥ 𝐵 ) )
100 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → 𝑛 ∥ 𝐵 )
101 breq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∥ 𝐵 ↔ 𝑛 ∥ 𝐵 ) )
102 100 101 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( 𝑥 = 𝑛 → 𝑥 ∥ 𝐵 ) )
103 93 99 102 3jaod ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( ( 𝑥 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛 ) → 𝑥 ∥ 𝐵 ) )
104 81 103 syl5 ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( 𝑥 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } → 𝑥 ∥ 𝐵 ) )
105 104 imp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) ∧ 𝑥 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } ) → 𝑥 ∥ 𝐵 )
106 80 105 ssrabdv ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } ⊆ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } )
107 66 70 72 106 fsumless ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } 𝑘 ≤ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } 𝑘 )
108 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } )
109 disjsn ⊢ ( ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∩ { 𝑛 } ) = ∅ ↔ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } )
110 108 109 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∩ { 𝑛 } ) = ∅ )
111 73 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } = ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∪ { 𝑛 } ) )
112 tpfi ⊢ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } ∈ Fin
113 112 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } ∈ Fin )
114 80 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) ∧ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } ) → 𝑘 ∈ ℕ )
115 114 nncnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) ∧ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } ) → 𝑘 ∈ ℂ )
116 110 111 113 115 fsumsplit ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } 𝑘 = ( Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } 𝑘 + Σ 𝑘 ∈ { 𝑛 } 𝑘 ) )
117 8 nncnd ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℂ )
118 id ⊢ ( 𝑘 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → 𝑘 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
119 118 sumsn ⊢ ( ( ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ∧ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℂ ) → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } 𝑘 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
120 8 117 119 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } 𝑘 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
121 id ⊢ ( 𝑘 = 𝐵 → 𝑘 = 𝐵 )
122 121 sumsn ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝐵 } 𝑘 = 𝐵 )
123 2 55 122 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐵 } 𝑘 = 𝐵 )
124 120 123 oveq12d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } 𝑘 + Σ 𝑘 ∈ { 𝐵 } 𝑘 ) = ( ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) + 𝐵 ) )
125 incom ⊢ ( { 𝐵 } ∩ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } ) = ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } ∩ { 𝐵 } )
126 9 57 gtned ⊢ ( 𝜑 → 𝐵 ≠ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
127 disjsn2 ⊢ ( 𝐵 ≠ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ( { 𝐵 } ∩ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } ) = ∅ )
128 126 127 syl ⊢ ( 𝜑 → ( { 𝐵 } ∩ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } ) = ∅ )
129 125 128 eqtr3id ⊢ ( 𝜑 → ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } ∩ { 𝐵 } ) = ∅ )
130 df-pr ⊢ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } = ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } ∪ { 𝐵 } )
131 130 a1i ⊢ ( 𝜑 → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } = ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } ∪ { 𝐵 } ) )
132 prfi ⊢ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∈ Fin
133 132 a1i ⊢ ( 𝜑 → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∈ Fin )
134 75 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → 𝑘 ∈ ℕ )
135 134 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → 𝑘 ∈ ℂ )
136 129 131 133 135 fsumsplit ⊢ ( 𝜑 → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } 𝑘 = ( Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) } 𝑘 + Σ 𝑘 ∈ { 𝐵 } 𝑘 ) )
137 87 55 mulcld ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) ∈ ℂ )
138 55 137 87 88 divdird ⊢ ( 𝜑 → ( ( 𝐵 + ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = ( ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) + ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
139 35 nncnd ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℂ )
140 27 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
141 139 140 55 subdird ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) − ( 1 · 𝐵 ) ) )
142 55 mullidd ⊢ ( 𝜑 → ( 1 · 𝐵 ) = 𝐵 )
143 142 oveq2d ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) − ( 1 · 𝐵 ) ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) − 𝐵 ) )
144 141 143 eqtrd ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) − 𝐵 ) )
145 144 oveq2d ⊢ ( 𝜑 → ( 𝐵 + ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) ) = ( 𝐵 + ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) − 𝐵 ) ) )
146 139 55 mulcld ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) ∈ ℂ )
147 55 146 pncan3d ⊢ ( 𝜑 → ( 𝐵 + ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) − 𝐵 ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) )
148 145 147 eqtrd ⊢ ( 𝜑 → ( 𝐵 + ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) )
149 148 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 + ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
150 139 55 87 88 divassd ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
151 149 150 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 + ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
152 55 87 88 divcan3d ⊢ ( 𝜑 → ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 𝐵 )
153 152 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) + ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · 𝐵 ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) = ( ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) + 𝐵 ) )
154 138 151 153 3eqtr3d ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) = ( ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) + 𝐵 ) )
155 124 136 154 3eqtr4d ⊢ ( 𝜑 → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } 𝑘 = ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
156 155 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } 𝑘 = ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
157 77 nncnd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → 𝑛 ∈ ℂ )
158 id ⊢ ( 𝑘 = 𝑛 → 𝑘 = 𝑛 )
159 158 sumsn ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑛 } 𝑘 = 𝑛 )
160 157 157 159 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → Σ 𝑘 ∈ { 𝑛 } 𝑘 = 𝑛 )
161 156 160 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } 𝑘 + Σ 𝑘 ∈ { 𝑛 } 𝑘 ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 𝑛 ) )
162 116 161 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 𝑛 } 𝑘 = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 𝑛 ) )
163 1 nnnn0d ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
164 expp1 ⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℕ0 ) → ( 2 ↑ ( 𝐴 + 1 ) ) = ( ( 2 ↑ 𝐴 ) · 2 ) )
165 12 163 164 sylancr ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) = ( ( 2 ↑ 𝐴 ) · 2 ) )
166 2nn ⊢ 2 ∈ ℕ
167 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐴 ∈ ℕ0 ) → ( 2 ↑ 𝐴 ) ∈ ℕ )
168 166 163 167 sylancr ⊢ ( 𝜑 → ( 2 ↑ 𝐴 ) ∈ ℕ )
169 168 nncnd ⊢ ( 𝜑 → ( 2 ↑ 𝐴 ) ∈ ℂ )
170 mulcom ⊢ ( ( ( 2 ↑ 𝐴 ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 2 ↑ 𝐴 ) · 2 ) = ( 2 · ( 2 ↑ 𝐴 ) ) )
171 169 12 170 sylancl ⊢ ( 𝜑 → ( ( 2 ↑ 𝐴 ) · 2 ) = ( 2 · ( 2 ↑ 𝐴 ) ) )
172 165 171 eqtrd ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) = ( 2 · ( 2 ↑ 𝐴 ) ) )
173 172 oveq1d ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) = ( ( 2 · ( 2 ↑ 𝐴 ) ) · 𝐵 ) )
174 12 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
175 174 169 55 mulassd ⊢ ( 𝜑 → ( ( 2 · ( 2 ↑ 𝐴 ) ) · 𝐵 ) = ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) )
176 isodd7 ⊢ ( 𝐵 ∈ Odd ↔ ( 𝐵 ∈ ℤ ∧ ( 2 gcd 𝐵 ) = 1 ) )
177 simpr ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 2 gcd 𝐵 ) = 1 ) → ( 2 gcd 𝐵 ) = 1 )
178 176 177 sylbi ⊢ ( 𝐵 ∈ Odd → ( 2 gcd 𝐵 ) = 1 )
179 3 178 syl ⊢ ( 𝜑 → ( 2 gcd 𝐵 ) = 1 )
180 2z ⊢ 2 ∈ ℤ
181 180 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
182 rpexp1i ⊢ ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( ( 2 gcd 𝐵 ) = 1 → ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 ) )
183 181 94 163 182 syl3anc ⊢ ( 𝜑 → ( ( 2 gcd 𝐵 ) = 1 → ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 ) )
184 179 183 mpd ⊢ ( 𝜑 → ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 )
185 sgmmul ⊢ ( ( 1 ∈ ℂ ∧ ( ( 2 ↑ 𝐴 ) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 ) ) → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( ( 1 σ ( 2 ↑ 𝐴 ) ) · ( 1 σ 𝐵 ) ) )
186 140 168 2 184 185 syl13anc ⊢ ( 𝜑 → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( ( 1 σ ( 2 ↑ 𝐴 ) ) · ( 1 σ 𝐵 ) ) )
187 pncan ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
188 28 27 187 sylancl ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
189 188 oveq2d ⊢ ( 𝜑 → ( 2 ↑ ( ( 𝐴 + 1 ) − 1 ) ) = ( 2 ↑ 𝐴 ) )
190 189 oveq2d ⊢ ( 𝜑 → ( 1 σ ( 2 ↑ ( ( 𝐴 + 1 ) − 1 ) ) ) = ( 1 σ ( 2 ↑ 𝐴 ) ) )
191 1sgm2ppw ⊢ ( ( 𝐴 + 1 ) ∈ ℕ → ( 1 σ ( 2 ↑ ( ( 𝐴 + 1 ) − 1 ) ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
192 20 191 syl ⊢ ( 𝜑 → ( 1 σ ( 2 ↑ ( ( 𝐴 + 1 ) − 1 ) ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
193 190 192 eqtr3d ⊢ ( 𝜑 → ( 1 σ ( 2 ↑ 𝐴 ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
194 193 oveq1d ⊢ ( 𝜑 → ( ( 1 σ ( 2 ↑ 𝐴 ) ) · ( 1 σ 𝐵 ) ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
195 186 4 194 3eqtr3d ⊢ ( 𝜑 → ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
196 173 175 195 3eqtrd ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
197 196 oveq1d ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
198 1nn0 ⊢ 1 ∈ ℕ0
199 sgmnncl ⊢ ( ( 1 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 σ 𝐵 ) ∈ ℕ )
200 198 2 199 sylancr ⊢ ( 𝜑 → ( 1 σ 𝐵 ) ∈ ℕ )
201 200 nncnd ⊢ ( 𝜑 → ( 1 σ 𝐵 ) ∈ ℂ )
202 201 87 88 divcan3d ⊢ ( 𝜑 → ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = ( 1 σ 𝐵 ) )
203 197 150 202 3eqtr3d ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) = ( 1 σ 𝐵 ) )
204 sgmval ⊢ ( ( 1 ∈ ℂ ∧ 𝐵 ∈ ℕ ) → ( 1 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ( 𝑘 ↑𝑐 1 ) )
205 27 2 204 sylancr ⊢ ( 𝜑 → ( 1 σ 𝐵 ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ( 𝑘 ↑𝑐 1 ) )
206 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } )
207 67 206 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 𝑘 ∈ ℕ )
208 207 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 𝑘 ∈ ℂ )
209 208 cxp1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → ( 𝑘 ↑𝑐 1 ) = 𝑘 )
210 209 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ( 𝑘 ↑𝑐 1 ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } 𝑘 )
211 203 205 210 3eqtrrd ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } 𝑘 = ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
212 211 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } 𝑘 = ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
213 107 162 212 3brtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 𝑛 ) ≤ ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
214 36 9 remulcld ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) ∈ ℝ )
215 214 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) ∈ ℝ )
216 77 nnrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → 𝑛 ∈ ℝ+ )
217 215 216 ltaddrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) < ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 𝑛 ) )
218 77 nnred ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → 𝑛 ∈ ℝ )
219 215 218 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 𝑛 ) ∈ ℝ )
220 215 219 ltnled ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) < ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 𝑛 ) ↔ ¬ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 𝑛 ) ≤ ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) ) )
221 217 220 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) ∧ ¬ 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ) → ¬ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 𝑛 ) ≤ ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
222 213 221 condan ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) → 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } )
223 elpri ⊢ ( 𝑛 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } → ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) )
224 222 223 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵 ) ) → ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) )
225 224 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 ∥ 𝐵 → ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) ) )
226 225 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑛 ∥ 𝐵 → ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) ) )
227 6 58 gtned ⊢ ( 𝜑 → 𝐵 ≠ 1 )
228 227 necomd ⊢ ( 𝜑 → 1 ≠ 𝐵 )
229 1nn ⊢ 1 ∈ ℕ
230 229 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
231 1dvds ⊢ ( 𝐵 ∈ ℤ → 1 ∥ 𝐵 )
232 94 231 syl ⊢ ( 𝜑 → 1 ∥ 𝐵 )
233 breq1 ⊢ ( 𝑛 = 1 → ( 𝑛 ∥ 𝐵 ↔ 1 ∥ 𝐵 ) )
234 eqeq1 ⊢ ( 𝑛 = 1 → ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ↔ 1 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
235 eqeq1 ⊢ ( 𝑛 = 1 → ( 𝑛 = 𝐵 ↔ 1 = 𝐵 ) )
236 234 235 orbi12d ⊢ ( 𝑛 = 1 → ( ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) ↔ ( 1 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 1 = 𝐵 ) ) )
237 233 236 imbi12d ⊢ ( 𝑛 = 1 → ( ( 𝑛 ∥ 𝐵 → ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) ) ↔ ( 1 ∥ 𝐵 → ( 1 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 1 = 𝐵 ) ) ) )
238 237 rspcv ⊢ ( 1 ∈ ℕ → ( ∀ 𝑛 ∈ ℕ ( 𝑛 ∥ 𝐵 → ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) ) → ( 1 ∥ 𝐵 → ( 1 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 1 = 𝐵 ) ) ) )
239 230 226 232 238 syl3c ⊢ ( 𝜑 → ( 1 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 1 = 𝐵 ) )
240 239 ord ⊢ ( 𝜑 → ( ¬ 1 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → 1 = 𝐵 ) )
241 240 necon1ad ⊢ ( 𝜑 → ( 1 ≠ 𝐵 → 1 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
242 228 241 mpd ⊢ ( 𝜑 → 1 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
243 242 eqeq2d ⊢ ( 𝜑 → ( 𝑛 = 1 ↔ 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
244 243 orbi1d ⊢ ( 𝜑 → ( ( 𝑛 = 1 ∨ 𝑛 = 𝐵 ) ↔ ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) ) )
245 244 imbi2d ⊢ ( 𝜑 → ( ( 𝑛 ∥ 𝐵 → ( 𝑛 = 1 ∨ 𝑛 = 𝐵 ) ) ↔ ( 𝑛 ∥ 𝐵 → ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) ) ) )
246 245 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℕ ( 𝑛 ∥ 𝐵 → ( 𝑛 = 1 ∨ 𝑛 = 𝐵 ) ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑛 ∥ 𝐵 → ( 𝑛 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑛 = 𝐵 ) ) ) )
247 226 246 mpbird ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑛 ∥ 𝐵 → ( 𝑛 = 1 ∨ 𝑛 = 𝐵 ) ) )
248 isprm2 ⊢ ( 𝐵 ∈ ℙ ↔ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ∥ 𝐵 → ( 𝑛 = 1 ∨ 𝑛 = 𝐵 ) ) ) )
249 60 247 248 sylanbrc ⊢ ( 𝜑 → 𝐵 ∈ ℙ )
250 214 ltp1d ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) < ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) )
251 peano2re ⊢ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) ∈ ℝ → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) ∈ ℝ )
252 214 251 syl ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) ∈ ℝ )
253 214 252 ltnled ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) < ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) ↔ ¬ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) ≤ ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) ) )
254 250 253 mpbid ⊢ ( 𝜑 → ¬ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) ≤ ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
255 207 nnred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 𝑘 ∈ ℝ )
256 207 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 𝑘 ∈ ℕ0 )
257 256 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } ) → 0 ≤ 𝑘 )
258 df-tp ⊢ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } = ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∪ { 1 } )
259 snssi ⊢ ( 1 ∈ ℕ → { 1 } ⊆ ℕ )
260 229 259 mp1i ⊢ ( 𝜑 → { 1 } ⊆ ℕ )
261 75 260 unssd ⊢ ( 𝜑 → ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∪ { 1 } ) ⊆ ℕ )
262 258 261 eqsstrid ⊢ ( 𝜑 → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } ⊆ ℕ )
263 eltpi ⊢ ( 𝑥 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } → ( 𝑥 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1 ) )
264 breq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ∥ 𝐵 ↔ 1 ∥ 𝐵 ) )
265 232 264 syl5ibrcom ⊢ ( 𝜑 → ( 𝑥 = 1 → 𝑥 ∥ 𝐵 ) )
266 92 98 265 3jaod ⊢ ( 𝜑 → ( ( 𝑥 = ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1 ) → 𝑥 ∥ 𝐵 ) )
267 263 266 syl5 ⊢ ( 𝜑 → ( 𝑥 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } → 𝑥 ∥ 𝐵 ) )
268 267 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } ) → 𝑥 ∥ 𝐵 )
269 262 268 ssrabdv ⊢ ( 𝜑 → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } ⊆ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } )
270 65 255 257 269 fsumless ⊢ ( 𝜑 → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } 𝑘 ≤ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } 𝑘 )
271 270 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } 𝑘 ≤ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } 𝑘 )
272 55 87 88 diveq1ad ⊢ ( 𝜑 → ( ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 ↔ 𝐵 = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
273 272 necon3bid ⊢ ( 𝜑 → ( ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ≠ 1 ↔ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
274 273 biimpar ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ≠ 1 )
275 274 necomd ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → 1 ≠ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
276 228 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → 1 ≠ 𝐵 )
277 275 276 nelprd ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ¬ 1 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } )
278 disjsn ⊢ ( ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∩ { 1 } ) = ∅ ↔ ¬ 1 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } )
279 277 278 sylibr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∩ { 1 } ) = ∅ )
280 258 a1i ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } = ( { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } ∪ { 1 } ) )
281 tpfi ⊢ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } ∈ Fin
282 281 a1i ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } ∈ Fin )
283 262 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } ⊆ ℕ )
284 283 sselda ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∧ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } ) → 𝑘 ∈ ℕ )
285 284 nncnd ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∧ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } ) → 𝑘 ∈ ℂ )
286 279 280 282 285 fsumsplit ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } 𝑘 = ( Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } 𝑘 + Σ 𝑘 ∈ { 1 } 𝑘 ) )
287 id ⊢ ( 𝑘 = 1 → 𝑘 = 1 )
288 287 sumsn ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ { 1 } 𝑘 = 1 )
289 140 27 288 sylancl ⊢ ( 𝜑 → Σ 𝑘 ∈ { 1 } 𝑘 = 1 )
290 155 289 oveq12d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } 𝑘 + Σ 𝑘 ∈ { 1 } 𝑘 ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) )
291 290 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ( Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 } 𝑘 + Σ 𝑘 ∈ { 1 } 𝑘 ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) )
292 286 291 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → Σ 𝑘 ∈ { ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) , 𝐵 , 1 } 𝑘 = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) )
293 211 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵 } 𝑘 = ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
294 271 292 293 3brtr3d ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) ≤ ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) )
295 294 ex ⊢ ( 𝜑 → ( 𝐵 ≠ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) ≤ ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) ) )
296 295 necon1bd ⊢ ( 𝜑 → ( ¬ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) + 1 ) ≤ ( ( 2 ↑ ( 𝐴 + 1 ) ) · ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ) → 𝐵 = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
297 254 296 mpd ⊢ ( 𝜑 → 𝐵 = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
298 249 297 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℙ ∧ 𝐵 = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )