perfectALTVlem2 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > perfectALTVlem2		Structured version Visualization version GIF version

Theorem perfectALTVlem2 43907

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

**Hypotheses**
Ref	Expression
perfectALTVlem.1	⊢ (𝜑 → 𝐴 ∈ ℕ)
perfectALTVlem.2	⊢ (𝜑 → 𝐵 ∈ ℕ)
perfectALTVlem.3	⊢ (𝜑 → 𝐵 ∈ Odd )
perfectALTVlem.4	⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))

**Assertion**
Ref	Expression
perfectALTVlem2	⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))

Proof of Theorem perfectALTVlem2 Dummy variables 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		perfectALTVlem.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℕ)
2		1re 10641	. . . . . 6 ⊢ 1 ∈ ℝ
3	2	a1i 11	. . . . 5 ⊢ (𝜑 → 1 ∈ ℝ)
4		perfectALTVlem.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℕ)
5		perfectALTVlem.3	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ Odd )
6		perfectALTVlem.4	. . . . . . . 8 ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))
7	4, 1, 5, 6	perfectALTVlem1 43906	. . . . . . 7 ⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ))
8	7	simp3d 1140	. . . . . 6 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ)
9	8	nnred 11653	. . . . 5 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℝ)
10	1	nnred 11653	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ)
11	8	nnge1d 11686	. . . . 5 ⊢ (𝜑 → 1 ≤ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
12		2cn 11713	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
13		exp1 13436	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑1) = 2)
14	12, 13	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑1) = 2
15		df-2 11701	. . . . . . . . . 10 ⊢ 2 = (1 + 1)
16	14, 15	eqtri 2844	. . . . . . . . 9 ⊢ (2↑1) = (1 + 1)
17		2re 11712	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
18	17	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℝ)
19		1zzd 12014	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
20	4	peano2nnd 11655	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + 1) ∈ ℕ)
21	20	nnzd 12087	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ)
22		1lt2 11809	. . . . . . . . . . 11 ⊢ 1 < 2
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 2)
24	4	nnrpd 12430	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ⁺)
25		ltaddrp 12427	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝐴 ∈ ℝ⁺) → 1 < (1 + 𝐴))
26	2, 24, 25	sylancr 589	. . . . . . . . . . 11 ⊢ (𝜑 → 1 < (1 + 𝐴))
27		ax-1cn 10595	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
28	4	nncnd 11654	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
29		addcom 10826	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 + 𝐴) = (𝐴 + 1))
30	27, 28, 29	sylancr 589	. . . . . . . . . . 11 ⊢ (𝜑 → (1 + 𝐴) = (𝐴 + 1))
31	26, 30	breqtrd 5092	. . . . . . . . . 10 ⊢ (𝜑 → 1 < (𝐴 + 1))
32		ltexp2a 13531	. . . . . . . . . 10 ⊢ (((2 ∈ ℝ ∧ 1 ∈ ℤ ∧ (𝐴 + 1) ∈ ℤ) ∧ (1 < 2 ∧ 1 < (𝐴 + 1))) → (2↑1) < (2↑(𝐴 + 1)))
33	18, 19, 21, 23, 31, 32	syl32anc 1374	. . . . . . . . 9 ⊢ (𝜑 → (2↑1) < (2↑(𝐴 + 1)))
34	16, 33	eqbrtrrid 5102	. . . . . . . 8 ⊢ (𝜑 → (1 + 1) < (2↑(𝐴 + 1)))
35	7	simp1d 1138	. . . . . . . . . 10 ⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℕ)
36	35	nnred 11653	. . . . . . . . 9 ⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℝ)
37	3, 3, 36	ltaddsubd 11240	. . . . . . . 8 ⊢ (𝜑 → ((1 + 1) < (2↑(𝐴 + 1)) ↔ 1 < ((2↑(𝐴 + 1)) − 1)))
38	34, 37	mpbid 234	. . . . . . 7 ⊢ (𝜑 → 1 < ((2↑(𝐴 + 1)) − 1))
39		1rp 12394	. . . . . . . . 9 ⊢ 1 ∈ ℝ⁺
40	39	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ⁺)
41		peano2rem 10953	. . . . . . . . . . 11 ⊢ ((2↑(𝐴 + 1)) ∈ ℝ → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
42	36, 41	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
43		expgt1 13468	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ (𝐴 + 1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐴 + 1)))
44	18, 20, 23, 43	syl3anc 1367	. . . . . . . . . . 11 ⊢ (𝜑 → 1 < (2↑(𝐴 + 1)))
45		posdif 11133	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ (2↑(𝐴 + 1)) ∈ ℝ) → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
46	2, 36, 45	sylancr 589	. . . . . . . . . . 11 ⊢ (𝜑 → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
47	44, 46	mpbid 234	. . . . . . . . . 10 ⊢ (𝜑 → 0 < ((2↑(𝐴 + 1)) − 1))
48	42, 47	jca 514	. . . . . . . . 9 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0 < ((2↑(𝐴 + 1)) − 1)))
49		elrp 12392	. . . . . . . . 9 ⊢ (((2↑(𝐴 + 1)) − 1) ∈ ℝ⁺ ↔ (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0 < ((2↑(𝐴 + 1)) − 1)))
50	48, 49	sylibr 236	. . . . . . . 8 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℝ⁺)
51		nnrp 12401	. . . . . . . . 9 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℝ⁺)
52	1, 51	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℝ⁺)
53	40, 50, 52	ltdiv2d 12455	. . . . . . 7 ⊢ (𝜑 → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)))
54	38, 53	mpbid 234	. . . . . 6 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1))
55	1	nncnd 11654	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
56	55	div1d 11408	. . . . . 6 ⊢ (𝜑 → (𝐵 / 1) = 𝐵)
57	54, 56	breqtrd 5092	. . . . 5 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < 𝐵)
58	3, 9, 10, 11, 57	lelttrd 10798	. . . 4 ⊢ (𝜑 → 1 < 𝐵)
59		eluz2b2 12322	. . . 4 ⊢ (𝐵 ∈ (ℤ_≥‘2) ↔ (𝐵 ∈ ℕ ∧ 1 < 𝐵))
60	1, 58, 59	sylanbrc 585	. . 3 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘2))
61		fzfid 13342	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝐵) ∈ Fin)
62		dvdsssfz1 15668	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵))
63	1, 62	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵))
64		ssfi 8738	. . . . . . . . . . . 12 ⊢ (((1...𝐵) ∈ Fin ∧ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin)
65	61, 63, 64	syl2anc 586	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin)
66	65	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin)
67		ssrab2 4056	. . . . . . . . . . . . 13 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ
68	67	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ)
69	68	sselda 3967	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ)
70	69	nnred 11653	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ)
71	69	nnnn0d 11956	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ₀)
72	71	nn0ge0d 11959	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘)
73		df-tp 4572	. . . . . . . . . . . 12 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛})
74		prssi 4754	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧ 𝐵 ∈ ℕ) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
75	8, 1, 74	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
76	75	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
77		simplrl 775	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℕ)
78	77	snssd 4742	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑛} ⊆ ℕ)
79	76, 78	unssd 4162	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) ⊆ ℕ)
80	73, 79	eqsstrid 4015	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ ℕ)
81		eltpi 4625	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛))
82	7	simp2d 1139	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℕ)
83	82	nnzd 12087	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℤ)
84	8	nnzd 12087	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ)
85		dvdsmul2 15632	. . . . . . . . . . . . . . . . . 18 ⊢ ((((2↑(𝐴 + 1)) − 1) ∈ ℤ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
86	83, 84, 85	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
87	82	nncnd 11654	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℂ)
88	82	nnne0d 11688	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ≠ 0)
89	55, 87, 88	divcan2d 11418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = 𝐵)
90	86, 89	breqtrd 5092	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵)
91		breq1 5069	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → (𝑥 ∥ 𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵))
92	90, 91	syl5ibrcom 249	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵))
93	92	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵))
94	1	nnzd 12087	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℤ)
95		iddvds 15623	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ ℤ → 𝐵 ∥ 𝐵)
96	94, 95	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∥ 𝐵)
97		breq1 5069	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝐵 → (𝑥 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵))
98	96, 97	syl5ibrcom 249	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵))
99	98	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵))
100		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∥ 𝐵)
101		breq1 5069	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝐵 ↔ 𝑛 ∥ 𝐵))
102	100, 101	syl5ibrcom 249	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝑛 → 𝑥 ∥ 𝐵))
103	93, 99, 102	3jaod 1424	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛) → 𝑥 ∥ 𝐵))
104	81, 103	syl5 34	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → 𝑥 ∥ 𝐵))
105	104	imp 409	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑥 ∥ 𝐵)
106	80, 105	ssrabdv 4050	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵})
107	66, 70, 72, 106	fsumless 15151	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
108		simpr 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
109		disjsn 4647	. . . . . . . . . . . 12 ⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
110	108, 109	sylibr 236	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅)
111	73	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}))
112		tpfi 8794	. . . . . . . . . . . 12 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin
113	112	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin)
114	80	sselda 3967	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℕ)
115	114	nncnd 11654	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℂ)
116	110, 111, 113, 115	fsumsplit 15097	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘))
117	8	nncnd 11654	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ)
118		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
119	118	sumsn 15101	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
120	8, 117, 119	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
121		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝐵 → 𝑘 = 𝐵)
122	121	sumsn 15101	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
123	1, 55, 122	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
124	120, 123	oveq12d 7174	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
125		incom 4178	. . . . . . . . . . . . . . 15 ⊢ ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵})
126	9, 57	gtned 10775	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
127		disjsn2 4648	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)) → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
128	126, 127	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
129	125, 128	syl5eqr 2870	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) = ∅)
130		df-pr 4570	. . . . . . . . . . . . . . 15 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵})
131	130	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵}))
132		prfi 8793	. . . . . . . . . . . . . . 15 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin
133	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin)
134	75	sselda 3967	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℕ)
135	134	nncnd 11654	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℂ)
136	129, 131, 133, 135	fsumsplit 15097	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘))
137	87, 55	mulcld 10661	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) ∈ ℂ)
138	55, 137, 87, 88	divdird 11454	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))))
139	35	nncnd 11654	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℂ)
140	27	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℂ)
141	139, 140, 55	subdird 11097	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)))
142	55	mulid2d 10659	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 · 𝐵) = 𝐵)
143	142	oveq2d 7172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
144	141, 143	eqtrd 2856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
145	144	oveq2d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)))
146	139, 55	mulcld 10661	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) ∈ ℂ)
147	55, 146	pncan3d 11000	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
148	145, 147	eqtrd 2856	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
149	148	oveq1d 7171	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)))
150	139, 55, 87, 88	divassd 11451	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
151	149, 150	eqtrd 2856	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
152	55, 87, 88	divcan3d 11421	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = 𝐵)
153	152	oveq2d 7172	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
154	138, 151, 153	3eqtr3d 2864	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
155	124, 136, 154	3eqtr4d 2866	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
156	155	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
157	77	nncnd 11654	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℂ)
158		id 22	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛)
159	158	sumsn 15101	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℂ ∧ 𝑛 ∈ ℂ) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
160	157, 157, 159	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
161	156, 160	oveq12d 7174	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
162	116, 161	eqtrd 2856	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
163	4	nnnn0d 11956	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
164		expp1 13437	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ₀) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
165	12, 163, 164	sylancr 589	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
166		2nn 11711	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ
167		nnexpcl 13443	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (2↑𝐴) ∈ ℕ)
168	166, 163, 167	sylancr 589	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2↑𝐴) ∈ ℕ)
169	168	nncnd 11654	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑𝐴) ∈ ℂ)
170		mulcom 10623	. . . . . . . . . . . . . . . . 17 ⊢ (((2↑𝐴) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
171	169, 12, 170	sylancl 588	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
172	165, 171	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2↑(𝐴 + 1)) = (2 · (2↑𝐴)))
173	172	oveq1d 7171	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = ((2 · (2↑𝐴)) · 𝐵))
174	12	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
175	174, 169, 55	mulassd 10664	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (2↑𝐴)) · 𝐵) = (2 · ((2↑𝐴) · 𝐵)))
176		isodd7 43850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Odd ↔ (𝐵 ∈ ℤ ∧ (2 gcd 𝐵) = 1))
177		simpr 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℤ ∧ (2 gcd 𝐵) = 1) → (2 gcd 𝐵) = 1)
178	176, 177	sylbi 219	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ Odd → (2 gcd 𝐵) = 1)
179	5, 178	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 gcd 𝐵) = 1)
180		2z 12015	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℤ
181	180	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2 ∈ ℤ)
182		rpexp1i 16065	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
183	181, 94, 163, 182	syl3anc 1367	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
184	179, 183	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2↑𝐴) gcd 𝐵) = 1)
185		sgmmul 25777	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ ((2↑𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ((2↑𝐴) gcd 𝐵) = 1)) → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
186	140, 168, 1, 184, 185	syl13anc 1368	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
187		pncan 10892	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + 1) − 1) = 𝐴)
188	28, 27, 187	sylancl 588	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐴 + 1) − 1) = 𝐴)
189	188	oveq2d 7172	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2↑((𝐴 + 1) − 1)) = (2↑𝐴))
190	189	oveq2d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = (1 σ (2↑𝐴)))
191		1sgm2ppw 25776	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 + 1) ∈ ℕ → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
192	20, 191	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
193	190, 192	eqtr3d 2858	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 σ (2↑𝐴)) = ((2↑(𝐴 + 1)) − 1))
194	193	oveq1d 7171	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1 σ (2↑𝐴)) · (1 σ 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
195	186, 6, 194	3eqtr3d 2864	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · ((2↑𝐴) · 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
196	173, 175, 195	3eqtrd 2860	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
197	196	oveq1d 7171	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)))
198		1nn0 11914	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ₀
199		sgmnncl 25724	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) ∈ ℕ)
200	198, 1, 199	sylancr 589	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 σ 𝐵) ∈ ℕ)
201	200	nncnd 11654	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 σ 𝐵) ∈ ℂ)
202	201, 87, 88	divcan3d 11421	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (1 σ 𝐵))
203	197, 150, 202	3eqtr3d 2864	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = (1 σ 𝐵))
204		sgmval 25719	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑_𝑐1))
205	27, 1, 204	sylancr 589	. . . . . . . . . . 11 ⊢ (𝜑 → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑_𝑐1))
206		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵})
207	67, 206	sseldi 3965	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ)
208	207	nncnd 11654	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℂ)
209	208	cxp1d 25289	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → (𝑘↑_𝑐1) = 𝑘)
210	209	sumeq2dv 15060	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑_𝑐1) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
211	203, 205, 210	3eqtrrd 2861	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
212	211	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
213	107, 162, 212	3brtr3d 5097	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
214	36, 9	remulcld 10671	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
215	214	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
216	77	nnrpd 12430	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ⁺)
217	215, 216	ltaddrpd 12465	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
218	77	nnred 11653	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ)
219	215, 218	readdcld 10670	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℝ)
220	215, 219	ltnled 10787	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((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 234	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
222	213, 221	condan 816	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
223		elpri 4589	. . . . . . 7 ⊢ (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
224	222, 223	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
225	224	expr 459	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
226	225	ralrimiva 3182	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
227	3, 58	gtned 10775	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ≠ 1)
228	227	necomd 3071	. . . . . . . . 9 ⊢ (𝜑 → 1 ≠ 𝐵)
229		1nn 11649	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
230	229	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℕ)
231		1dvds 15624	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℤ → 1 ∥ 𝐵)
232	94, 231	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∥ 𝐵)
233		breq1 5069	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (𝑛 ∥ 𝐵 ↔ 1 ∥ 𝐵))
234		eqeq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ↔ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
235		eqeq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → (𝑛 = 𝐵 ↔ 1 = 𝐵))
236	234, 235	orbi12d 915	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → ((𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵) ↔ (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))
237	233, 236	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → ((𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) ↔ (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))))
238	237	rspcv 3618	. . . . . . . . . . . 12 ⊢ (1 ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) → (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))))
239	230, 226, 232, 238	syl3c 66	. . . . . . . . . . 11 ⊢ (𝜑 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))
240	239	ord 860	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 1 = 𝐵))
241	240	necon1ad 3033	. . . . . . . . 9 ⊢ (𝜑 → (1 ≠ 𝐵 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
242	228, 241	mpd 15	. . . . . . . 8 ⊢ (𝜑 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
243	242	eqeq2d 2832	. . . . . . 7 ⊢ (𝜑 → (𝑛 = 1 ↔ 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
244	243	orbi1d 913	. . . . . 6 ⊢ (𝜑 → ((𝑛 = 1 ∨ 𝑛 = 𝐵) ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
245	244	imbi2d 343	. . . . 5 ⊢ (𝜑 → ((𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
246	245	ralbidv 3197	. . . 4 ⊢ (𝜑 → (∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
247	226, 246	mpbird 259	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)))
248		isprm2 16026	. . 3 ⊢ (𝐵 ∈ ℙ ↔ (𝐵 ∈ (ℤ_≥‘2) ∧ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵))))
249	60, 247, 248	sylanbrc 585	. 2 ⊢ (𝜑 → 𝐵 ∈ ℙ)
250	214	ltp1d 11570	. . . 4 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
251		peano2re 10813	. . . . . 6 ⊢ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
252	214, 251	syl 17	. . . . 5 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
253	214, 252	ltnled 10787	. . . 4 ⊢ (𝜑 → (((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 234	. . 3 ⊢ (𝜑 → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
255	207	nnred 11653	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ)
256	207	nnnn0d 11956	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ₀)
257	256	nn0ge0d 11959	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘)
258		df-tp 4572	. . . . . . . . . 10 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1})
259		snssi 4741	. . . . . . . . . . . 12 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
260	229, 259	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → {1} ⊆ ℕ)
261	75, 260	unssd 4162	. . . . . . . . . 10 ⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) ⊆ ℕ)
262	258, 261	eqsstrid 4015	. . . . . . . . 9 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
263		eltpi 4625	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1))
264		breq1 5069	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑥 ∥ 𝐵 ↔ 1 ∥ 𝐵))
265	232, 264	syl5ibrcom 249	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 = 1 → 𝑥 ∥ 𝐵))
266	92, 98, 265	3jaod 1424	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1) → 𝑥 ∥ 𝐵))
267	263, 266	syl5 34	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → 𝑥 ∥ 𝐵))
268	267	imp 409	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑥 ∥ 𝐵)
269	262, 268	ssrabdv 4050	. . . . . . . 8 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵})
270	65, 255, 257, 269	fsumless 15151	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
271	270	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
272	55, 87, 88	diveq1ad 11425	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) = 1 ↔ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
273	272	necon3bid 3060	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1 ↔ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)))
274	273	biimpar 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1)
275	274	necomd 3071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
276	228	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ 𝐵)
277	275, 276	nelprd 4596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
278		disjsn 4647	. . . . . . . . 9 ⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅ ↔ ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
279	277, 278	sylibr 236	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅)
280	258	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}))
281		tpfi 8794	. . . . . . . . 9 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin
282	281	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin)
283	262	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
284	283	sselda 3967	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℕ)
285	284	nncnd 11654	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℂ)
286	279, 280, 282, 285	fsumsplit 15097	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘))
287		id 22	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → 𝑘 = 1)
288	287	sumsn 15101	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {1}𝑘 = 1)
289	140, 27, 288	sylancl 588	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ {1}𝑘 = 1)
290	155, 289	oveq12d 7174	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
291	290	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
292	286, 291	eqtrd 2856	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
293	211	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
294	271, 292, 293	3brtr3d 5097	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
295	294	ex 415	. . . 4 ⊢ (𝜑 → (𝐵 ≠ ((2↑(𝐴 + 1)) − 1) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
296	295	necon1bd 3034	. . 3 ⊢ (𝜑 → (¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) → 𝐵 = ((2↑(𝐴 + 1)) − 1)))
297	254, 296	mpd 15	. 2 ⊢ (𝜑 → 𝐵 = ((2↑(𝐴 + 1)) − 1))
298	249, 297	jca 514	1 ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∨ w3o 1082 = wceq 1537 ∈ wcel 2114 ≠ wne 3016 ∀wral 3138 {crab 3142 ∪ cun 3934 ∩ cin 3935 ⊆ wss 3936 ∅c0 4291 {csn 4567 {cpr 4569 {ctp 4571 class class class wbr 5066 ‘cfv 6355 (class class class)co 7156 Fincfn 8509 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 < clt 10675 ≤ cle 10676 − cmin 10870 / cdiv 11297 ℕcn 11638 2c2 11693 ℕ₀cn0 11898 ℤcz 11982 ℤ_≥cuz 12244 ℝ⁺crp 12390 ...cfz 12893 ↑cexp 13430 Σcsu 15042 ∥ cdvds 15607 gcd cgcd 15843 ℙcprime 16015 ↑_𝑐ccxp 25139 σ csgm 25673 Odd codd 43810

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-inf2 9104 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615 ax-addf 10616 ax-mulf 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-om 7581 df-1st 7689 df-2nd 7690 df-supp 7831 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-2o 8103 df-oadd 8106 df-er 8289 df-map 8408 df-pm 8409 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fsupp 8834 df-fi 8875 df-sup 8906 df-inf 8907 df-oi 8974 df-card 9368 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-z 11983 df-dec 12100 df-uz 12245 df-q 12350 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ioo 12743 df-ioc 12744 df-ico 12745 df-icc 12746 df-fz 12894 df-fzo 13035 df-fl 13163 df-mod 13239 df-seq 13371 df-exp 13431 df-fac 13635 df-bc 13664 df-hash 13692 df-shft 14426 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-limsup 14828 df-clim 14845 df-rlim 14846 df-sum 15043 df-ef 15421 df-sin 15423 df-cos 15424 df-pi 15426 df-dvds 15608 df-gcd 15844 df-prm 16016 df-pc 16174 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-mulr 16579 df-starv 16580 df-sca 16581 df-vsca 16582 df-ip 16583 df-tset 16584 df-ple 16585 df-ds 16587 df-unif 16588 df-hom 16589 df-cco 16590 df-rest 16696 df-topn 16697 df-0g 16715 df-gsum 16716 df-topgen 16717 df-pt 16718 df-prds 16721 df-xrs 16775 df-qtop 16780 df-imas 16781 df-xps 16783 df-mre 16857 df-mrc 16858 df-acs 16860 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-submnd 17957 df-mulg 18225 df-cntz 18447 df-cmn 18908 df-psmet 20537 df-xmet 20538 df-met 20539 df-bl 20540 df-mopn 20541 df-fbas 20542 df-fg 20543 df-cnfld 20546 df-top 21502 df-topon 21519 df-topsp 21541 df-bases 21554 df-cld 21627 df-ntr 21628 df-cls 21629 df-nei 21706 df-lp 21744 df-perf 21745 df-cn 21835 df-cnp 21836 df-haus 21923 df-tx 22170 df-hmeo 22363 df-fil 22454 df-fm 22546 df-flim 22547 df-flf 22548 df-xms 22930 df-ms 22931 df-tms 22932 df-cncf 23486 df-limc 24464 df-dv 24465 df-log 25140 df-cxp 25141 df-sgm 25679 df-even 43811 df-odd 43812

This theorem is referenced by: perfectALTV 43908

W3C validator