perfectlem2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > perfectlem2		GIF version

Theorem perfectlem2 15320

Description: Lemma for perfect 15321. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by Wolf Lammen, 17-Sep-2020.)

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

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

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

Step	Hyp	Ref	Expression
1		perfectlem.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℕ)
2		1red 8058	. . . . 5 ⊢ (𝜑 → 1 ∈ ℝ)
3		perfectlem.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℕ)
4		perfectlem.3	. . . . . . . 8 ⊢ (𝜑 → ¬ 2 ∥ 𝐵)
5		perfectlem.4	. . . . . . . 8 ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))
6	3, 1, 4, 5	perfectlem1 15319	. . . . . . 7 ⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ))
7	6	simp3d 1013	. . . . . 6 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ)
8	7	nnred 9020	. . . . 5 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℝ)
9	1	nnred 9020	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ)
10	7	nnge1d 9050	. . . . 5 ⊢ (𝜑 → 1 ≤ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
11		2cn 9078	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
12		exp1 10654	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑1) = 2)
13	11, 12	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑1) = 2
14		df-2 9066	. . . . . . . . . 10 ⊢ 2 = (1 + 1)
15	13, 14	eqtri 2217	. . . . . . . . 9 ⊢ (2↑1) = (1 + 1)
16		2re 9077	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
17	16	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℝ)
18		1zzd 9370	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
19	3	peano2nnd 9022	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + 1) ∈ ℕ)
20	19	nnzd 9464	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ)
21		1lt2 9177	. . . . . . . . . . 11 ⊢ 1 < 2
22	21	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 2)
23		1re 8042	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
24	3	nnrpd 9786	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ⁺)
25		ltaddrp 9783	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝐴 ∈ ℝ⁺) → 1 < (1 + 𝐴))
26	23, 24, 25	sylancr 414	. . . . . . . . . . 11 ⊢ (𝜑 → 1 < (1 + 𝐴))
27		ax-1cn 7989	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
28	3	nncnd 9021	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
29		addcom 8180	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 + 𝐴) = (𝐴 + 1))
30	27, 28, 29	sylancr 414	. . . . . . . . . . 11 ⊢ (𝜑 → (1 + 𝐴) = (𝐴 + 1))
31	26, 30	breqtrd 4060	. . . . . . . . . 10 ⊢ (𝜑 → 1 < (𝐴 + 1))
32		ltexp2a 10700	. . . . . . . . . 10 ⊢ (((2 ∈ ℝ ∧ 1 ∈ ℤ ∧ (𝐴 + 1) ∈ ℤ) ∧ (1 < 2 ∧ 1 < (𝐴 + 1))) → (2↑1) < (2↑(𝐴 + 1)))
33	17, 18, 20, 22, 31, 32	syl32anc 1257	. . . . . . . . 9 ⊢ (𝜑 → (2↑1) < (2↑(𝐴 + 1)))
34	15, 33	eqbrtrrid 4070	. . . . . . . 8 ⊢ (𝜑 → (1 + 1) < (2↑(𝐴 + 1)))
35	6	simp1d 1011	. . . . . . . . . 10 ⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℕ)
36	35	nnred 9020	. . . . . . . . 9 ⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℝ)
37	2, 2, 36	ltaddsubd 8589	. . . . . . . 8 ⊢ (𝜑 → ((1 + 1) < (2↑(𝐴 + 1)) ↔ 1 < ((2↑(𝐴 + 1)) − 1)))
38	34, 37	mpbid 147	. . . . . . 7 ⊢ (𝜑 → 1 < ((2↑(𝐴 + 1)) − 1))
39		0lt1 8170	. . . . . . . . 9 ⊢ 0 < 1
40	39	a1i 9	. . . . . . . 8 ⊢ (𝜑 → 0 < 1)
41		peano2rem 8310	. . . . . . . . 9 ⊢ ((2↑(𝐴 + 1)) ∈ ℝ → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
42	36, 41	syl 14	. . . . . . . 8 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
43		expgt1 10686	. . . . . . . . . 10 ⊢ ((2 ∈ ℝ ∧ (𝐴 + 1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐴 + 1)))
44	16, 19, 22, 43	mp3an2i 1353	. . . . . . . . 9 ⊢ (𝜑 → 1 < (2↑(𝐴 + 1)))
45		posdif 8499	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ (2↑(𝐴 + 1)) ∈ ℝ) → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
46	23, 36, 45	sylancr 414	. . . . . . . . 9 ⊢ (𝜑 → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
47	44, 46	mpbid 147	. . . . . . . 8 ⊢ (𝜑 → 0 < ((2↑(𝐴 + 1)) − 1))
48	1	nngt0d 9051	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝐵)
49		ltdiv2 8931	. . . . . . . 8 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0 < ((2↑(𝐴 + 1)) − 1)) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)))
50	2, 40, 42, 47, 9, 48, 49	syl222anc 1265	. . . . . . 7 ⊢ (𝜑 → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)))
51	38, 50	mpbid 147	. . . . . 6 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1))
52	1	nncnd 9021	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
53	52	div1d 8824	. . . . . 6 ⊢ (𝜑 → (𝐵 / 1) = 𝐵)
54	51, 53	breqtrd 4060	. . . . 5 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < 𝐵)
55	2, 8, 9, 10, 54	lelttrd 8168	. . . 4 ⊢ (𝜑 → 1 < 𝐵)
56		eluz2b2 9694	. . . 4 ⊢ (𝐵 ∈ (ℤ_≥‘2) ↔ (𝐵 ∈ ℕ ∧ 1 < 𝐵))
57	1, 55, 56	sylanbrc 417	. . 3 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘2))
58		simprl 529	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → 𝑛 ∈ ℕ)
59	58	nnzd 9464	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → 𝑛 ∈ ℤ)
60	7	nnzd 9464	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ)
61	60	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ)
62		zdceq 9418	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℤ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ) → DECID 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
63	59, 61, 62	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → DECID 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
64	1	nnzd 9464	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℤ)
65	64	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → 𝐵 ∈ ℤ)
66		zdceq 9418	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℤ ∧ 𝐵 ∈ ℤ) → DECID 𝑛 = 𝐵)
67	59, 65, 66	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → DECID 𝑛 = 𝐵)
68		dcor 937	. . . . . . . . . 10 ⊢ (DECID 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → (DECID 𝑛 = 𝐵 → DECID (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
69	63, 67, 68	sylc 62	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → DECID (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
70		elprg 3643	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
71	58, 70	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
72	71	dcbid 839	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (DECID 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ↔ DECID (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
73	69, 72	mpbird 167	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → DECID 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
74		dvdsfi 12432	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin)
75	1, 74	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin)
76	75	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin)
77		ssrab2 3269	. . . . . . . . . . . . . 14 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ
78	77	a1i 9	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ)
79	78	sselda 3184	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ)
80	79	nnred 9020	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ)
81	79	nnnn0d 9319	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ₀)
82	81	nn0ge0d 9322	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘)
83		df-tp 3631	. . . . . . . . . . . . 13 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛})
84	7, 1	prssd 3782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
85	84	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
86		simplrl 535	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℕ)
87	86	snssd 3768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑛} ⊆ ℕ)
88	85, 87	unssd 3340	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) ⊆ ℕ)
89	83, 88	eqsstrid 3230	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ ℕ)
90	6	simp2d 1012	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℕ)
91	90	nnzd 9464	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℤ)
92		dvdsmul2 11996	. . . . . . . . . . . . . . . . . 18 ⊢ ((((2↑(𝐴 + 1)) − 1) ∈ ℤ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
93	91, 60, 92	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
94	90	nncnd 9021	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℂ)
95	42, 47	gt0ap0d 8673	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) # 0)
96	52, 94, 95	divcanap2d 8836	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = 𝐵)
97	93, 96	breqtrd 4060	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵)
98		breq1 4037	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → (𝑥 ∥ 𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵))
99	97, 98	syl5ibrcom 157	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵))
100	99	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵))
101		iddvds 11986	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ ℤ → 𝐵 ∥ 𝐵)
102	64, 101	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∥ 𝐵)
103		breq1 4037	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝐵 → (𝑥 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵))
104	102, 103	syl5ibrcom 157	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵))
105	104	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵))
106		simplrr 536	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∥ 𝐵)
107		breq1 4037	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝐵 ↔ 𝑛 ∥ 𝐵))
108	106, 107	syl5ibrcom 157	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝑛 → 𝑥 ∥ 𝐵))
109	100, 105, 108	3jaod 1315	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛) → 𝑥 ∥ 𝐵))
110		eltpi 3670	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛))
111	109, 110	impel 280	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑥 ∥ 𝐵)
112	89, 111	ssrabdv 3263	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵})
113		zdceq 9418	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ) → DECID 𝑝 = 𝑞)
114	113	rgen2 2583	. . . . . . . . . . . . . 14 ⊢ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℤ DECID 𝑝 = 𝑞
115	114	a1i 9	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℤ DECID 𝑝 = 𝑞)
116	61, 65, 59, 115	tpfidceq 7000	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin)
117	116	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin)
118	76, 80, 82, 112, 117	fsumlessfi 11642	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
119		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
120		disjsn 3685	. . . . . . . . . . . . 13 ⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
121	119, 120	sylibr 134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅)
122	83	a1i 9	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}))
123	89	sselda 3184	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℕ)
124	123	nncnd 9021	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℂ)
125	121, 122, 117, 124	fsumsplit 11589	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘))
126	7	nncnd 9021	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ)
127		id 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
128	127	sumsn 11593	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
129	7, 126, 128	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
130		id 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝐵 → 𝑘 = 𝐵)
131	130	sumsn 11593	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
132	1, 52, 131	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
133	129, 132	oveq12d 5943	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
134		incom 3356	. . . . . . . . . . . . . . . 16 ⊢ ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵})
135	8, 54	gtned 8156	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
136		disjsn2 3686	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)) → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
137	135, 136	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
138	134, 137	eqtr3id 2243	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) = ∅)
139		df-pr 3630	. . . . . . . . . . . . . . . 16 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵})
140	139	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵}))
141	114	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℤ DECID 𝑝 = 𝑞)
142	60, 64, 141	prfidceq 6998	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin)
143	84	sselda 3184	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℕ)
144	143	nncnd 9021	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℂ)
145	138, 140, 142, 144	fsumsplit 11589	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘))
146	94, 52	mulcld 8064	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) ∈ ℂ)
147	52, 146, 94, 95	divdirapd 8873	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))))
148	35	nncnd 9021	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℂ)
149		1cnd 8059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℂ)
150	148, 149, 52	subdird 8458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)))
151	52	mullidd 8061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1 · 𝐵) = 𝐵)
152	151	oveq2d 5941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
153	150, 152	eqtrd 2229	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
154	153	oveq2d 5941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)))
155	148, 52	mulcld 8064	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) ∈ ℂ)
156	52, 155	pncan3d 8357	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
157	154, 156	eqtrd 2229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
158	157	oveq1d 5940	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)))
159	148, 52, 94, 95	divassapd 8870	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
160	158, 159	eqtrd 2229	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
161	52, 94, 95	divcanap3d 8839	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = 𝐵)
162	161	oveq2d 5941	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
163	147, 160, 162	3eqtr3d 2237	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
164	133, 145, 163	3eqtr4d 2239	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
165	164	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
166	86	nncnd 9021	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℂ)
167		id 19	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛)
168	167	sumsn 11593	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑛 ∈ ℂ) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
169	166, 166, 168	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
170	165, 169	oveq12d 5943	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
171	125, 170	eqtrd 2229	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
172	3	nnnn0d 9319	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
173		expp1 10655	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ₀) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
174	11, 172, 173	sylancr 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
175		2nn 9169	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℕ
176		nnexpcl 10661	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (2↑𝐴) ∈ ℕ)
177	175, 172, 176	sylancr 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2↑𝐴) ∈ ℕ)
178	177	nncnd 9021	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2↑𝐴) ∈ ℂ)
179		mulcom 8025	. . . . . . . . . . . . . . . . . 18 ⊢ (((2↑𝐴) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
180	178, 11, 179	sylancl 413	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
181	174, 180	eqtrd 2229	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑(𝐴 + 1)) = (2 · (2↑𝐴)))
182	181	oveq1d 5940	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = ((2 · (2↑𝐴)) · 𝐵))
183		2cnd 9080	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ∈ ℂ)
184	183, 178, 52	mulassd 8067	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · (2↑𝐴)) · 𝐵) = (2 · ((2↑𝐴) · 𝐵)))
185		2prm 12320	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℙ
186		coprm 12337	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℙ ∧ 𝐵 ∈ ℤ) → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1))
187	185, 64, 186	sylancr 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1))
188	4, 187	mpbid 147	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 gcd 𝐵) = 1)
189		2z 9371	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℤ
190		rpexp1i 12347	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
191	189, 64, 172, 190	mp3an2i 1353	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
192	188, 191	mpd 13	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2↑𝐴) gcd 𝐵) = 1)
193		sgmmul 15316	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℂ ∧ ((2↑𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ((2↑𝐴) gcd 𝐵) = 1)) → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
194	149, 177, 1, 192, 193	syl13anc 1251	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
195		pncan 8249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + 1) − 1) = 𝐴)
196	28, 27, 195	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐴 + 1) − 1) = 𝐴)
197	196	oveq2d 5941	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2↑((𝐴 + 1) − 1)) = (2↑𝐴))
198	197	oveq2d 5941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = (1 σ (2↑𝐴)))
199		1sgm2ppw 15315	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 + 1) ∈ ℕ → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
200	19, 199	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
201	198, 200	eqtr3d 2231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 σ (2↑𝐴)) = ((2↑(𝐴 + 1)) − 1))
202	201	oveq1d 5940	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 σ (2↑𝐴)) · (1 σ 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
203	194, 5, 202	3eqtr3d 2237	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · ((2↑𝐴) · 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
204	182, 184, 203	3eqtrd 2233	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
205	204	oveq1d 5940	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)))
206		1nn0 9282	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
207		sgmnncl 15308	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) ∈ ℕ)
208	206, 1, 207	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 σ 𝐵) ∈ ℕ)
209	208	nncnd 9021	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 σ 𝐵) ∈ ℂ)
210	209, 94, 95	divcanap3d 8839	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (1 σ 𝐵))
211	205, 159, 210	3eqtr3d 2237	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = (1 σ 𝐵))
212		sgmval 15303	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑_𝑐1))
213	27, 1, 212	sylancr 414	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑_𝑐1))
214		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵})
215	77, 214	sselid 3182	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ)
216	215	nnrpd 9786	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ⁺)
217	216	rpcxp1d 15245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → (𝑘↑_𝑐1) = 𝑘)
218	217	sumeq2dv 11550	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑_𝑐1) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
219	211, 213, 218	3eqtrrd 2234	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
220	219	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
221	118, 171, 220	3brtr3d 4065	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
222	36, 8	remulcld 8074	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
223	222	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
224	86	nnrpd 9786	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ⁺)
225	223, 224	ltaddrpd 9822	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
226	211, 208	eqeltrd 2273	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℕ)
227	226	nnzd 9464	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℤ)
228	227	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℤ)
229	226	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℕ)
230	229, 58	nnaddcld 9055	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℕ)
231	230	nnzd 9464	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℤ)
232	231	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℤ)
233		zltnle 9389	. . . . . . . . . . 11 ⊢ ((((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℤ ∧ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℤ) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
234	228, 232, 233	syl2anc 411	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
235	225, 234	mpbid 147	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
236	221, 235	condandc 882	. . . . . . . 8 ⊢ (DECID 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} → ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}))
237	73, 236	mpcom 36	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
238		elpri 3646	. . . . . . 7 ⊢ (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
239	237, 238	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
240	239	expr 375	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
241	240	ralrimiva 2570	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
242	2, 55	gtned 8156	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≠ 1)
243	242	necomd 2453	. . . . . . . . . 10 ⊢ (𝜑 → 1 ≠ 𝐵)
244	243	neneqd 2388	. . . . . . . . 9 ⊢ (𝜑 → ¬ 1 = 𝐵)
245		1dvds 11987	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ → 1 ∥ 𝐵)
246	64, 245	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∥ 𝐵)
247		breq1 4037	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝑛 ∥ 𝐵 ↔ 1 ∥ 𝐵))
248		eqeq1 2203	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ↔ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
249		eqeq1 2203	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (𝑛 = 𝐵 ↔ 1 = 𝐵))
250	248, 249	orbi12d 794	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → ((𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵) ↔ (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))
251	247, 250	imbi12d 234	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) ↔ (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))))
252		1nn 9018	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
253	252	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℕ)
254	251, 241, 253	rspcdva 2873	. . . . . . . . . 10 ⊢ (𝜑 → (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))
255	246, 254	mpd 13	. . . . . . . . 9 ⊢ (𝜑 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))
256	244, 255	ecased 1360	. . . . . . . 8 ⊢ (𝜑 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
257	256	eqeq2d 2208	. . . . . . 7 ⊢ (𝜑 → (𝑛 = 1 ↔ 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
258	257	orbi1d 792	. . . . . 6 ⊢ (𝜑 → ((𝑛 = 1 ∨ 𝑛 = 𝐵) ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
259	258	imbi2d 230	. . . . 5 ⊢ (𝜑 → ((𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
260	259	ralbidv 2497	. . . 4 ⊢ (𝜑 → (∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
261	241, 260	mpbird 167	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)))
262		isprm2 12310	. . 3 ⊢ (𝐵 ∈ ℙ ↔ (𝐵 ∈ (ℤ_≥‘2) ∧ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵))))
263	57, 261, 262	sylanbrc 417	. 2 ⊢ (𝜑 → 𝐵 ∈ ℙ)
264		zdceq 9418	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℤ) → DECID 𝐵 = ((2↑(𝐴 + 1)) − 1))
265	64, 91, 264	syl2anc 411	. . 3 ⊢ (𝜑 → DECID 𝐵 = ((2↑(𝐴 + 1)) − 1))
266	222	ltp1d 8974	. . . 4 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
267	227	peano2zd 9468	. . . . 5 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℤ)
268		zltnle 9389	. . . . 5 ⊢ ((((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℤ ∧ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℤ) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
269	227, 267, 268	syl2anc 411	. . . 4 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
270	266, 269	mpbid 147	. . 3 ⊢ (𝜑 → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
271	215	nnred 9020	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ)
272	215	nnnn0d 9319	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ₀)
273	272	nn0ge0d 9322	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘)
274		df-tp 3631	. . . . . . . . . . 11 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1})
275		snssi 3767	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
276	252, 275	mp1i 10	. . . . . . . . . . . 12 ⊢ (𝜑 → {1} ⊆ ℕ)
277	84, 276	unssd 3340	. . . . . . . . . . 11 ⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) ⊆ ℕ)
278	274, 277	eqsstrid 3230	. . . . . . . . . 10 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
279		breq1 4037	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑥 ∥ 𝐵 ↔ 1 ∥ 𝐵))
280	246, 279	syl5ibrcom 157	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 = 1 → 𝑥 ∥ 𝐵))
281	99, 104, 280	3jaod 1315	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1) → 𝑥 ∥ 𝐵))
282		eltpi 3670	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1))
283	281, 282	impel 280	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑥 ∥ 𝐵)
284	278, 283	ssrabdv 3263	. . . . . . . . 9 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵})
285	60, 64, 18, 141	tpfidceq 7000	. . . . . . . . 9 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin)
286	75, 271, 273, 284, 285	fsumlessfi 11642	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
287	286	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
288	52, 94, 95	diveqap1ad 8843	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) = 1 ↔ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
289	288	necon3bid 2408	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1 ↔ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)))
290	289	biimpar 297	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1)
291	290	necomd 2453	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
292	243	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ 𝐵)
293	291, 292	nelprd 3649	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
294		disjsn 3685	. . . . . . . . . 10 ⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅ ↔ ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
295	293, 294	sylibr 134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅)
296	274	a1i 9	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}))
297	285	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin)
298	278	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
299	298	sselda 3184	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℕ)
300	299	nncnd 9021	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℂ)
301	295, 296, 297, 300	fsumsplit 11589	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘))
302		id 19	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → 𝑘 = 1)
303	302	sumsn 11593	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {1}𝑘 = 1)
304	2, 27, 303	sylancl 413	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ {1}𝑘 = 1)
305	164, 304	oveq12d 5943	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
306	305	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
307	301, 306	eqtrd 2229	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
308	219	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
309	287, 307, 308	3brtr3d 4065	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
310	309	ex 115	. . . . 5 ⊢ (𝜑 → (𝐵 ≠ ((2↑(𝐴 + 1)) − 1) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
311	310	a1d 22	. . . 4 ⊢ (𝜑 → (DECID 𝐵 = ((2↑(𝐴 + 1)) − 1) → (𝐵 ≠ ((2↑(𝐴 + 1)) − 1) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))))
312	311	necon1bddc 2444	. . 3 ⊢ (𝜑 → (DECID 𝐵 = ((2↑(𝐴 + 1)) − 1) → (¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) → 𝐵 = ((2↑(𝐴 + 1)) − 1))))
313	265, 270, 312	mp2d 47	. 2 ⊢ (𝜑 → 𝐵 = ((2↑(𝐴 + 1)) − 1))
314	263, 313	jca 306	1 ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 DECID wdc 835 ∨ w3o 979 = wceq 1364 ∈ wcel 2167 ≠ wne 2367 ∀wral 2475 {crab 2479 ∪ cun 3155 ∩ cin 3156 ⊆ wss 3157 ∅c0 3451 {csn 3623 {cpr 3624 {ctp 3625 class class class wbr 4034 ‘cfv 5259 (class class class)co 5925 Fincfn 6808 ℂcc 7894 ℝcr 7895 0cc0 7896 1c1 7897 + caddc 7899 · cmul 7901 < clt 8078 ≤ cle 8079 − cmin 8214 / cdiv 8716 ℕcn 9007 2c2 9058 ℕ₀cn0 9266 ℤcz 9343 ℤ_≥cuz 9618 ℝ⁺crp 9745 ↑cexp 10647 Σcsu 11535 ∥ cdvds 11969 gcd cgcd 12145 ℙcprime 12300 ↑_𝑐ccxp 15177 σ csgm 15301

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-mulrcl 7995 ax-addcom 7996 ax-mulcom 7997 ax-addass 7998 ax-mulass 7999 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-1rid 8003 ax-0id 8004 ax-rnegex 8005 ax-precex 8006 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-apti 8011 ax-pre-ltadd 8012 ax-pre-mulgt0 8013 ax-pre-mulext 8014 ax-arch 8015 ax-caucvg 8016 ax-pre-suploc 8017 ax-addf 8018 ax-mulf 8019

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-tp 3631 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-disj 4012 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-of 6139 df-1st 6207 df-2nd 6208 df-recs 6372 df-irdg 6437 df-frec 6458 df-1o 6483 df-2o 6484 df-oadd 6487 df-er 6601 df-map 6718 df-pm 6719 df-en 6809 df-dom 6810 df-fin 6811 df-sup 7059 df-inf 7060 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-reap 8619 df-ap 8626 df-div 8717 df-inn 9008 df-2 9066 df-3 9067 df-4 9068 df-n0 9267 df-xnn0 9330 df-z 9344 df-uz 9619 df-q 9711 df-rp 9746 df-xneg 9864 df-xadd 9865 df-ioo 9984 df-ico 9986 df-icc 9987 df-fz 10101 df-fzo 10235 df-fl 10377 df-mod 10432 df-seqfrec 10557 df-exp 10648 df-fac 10835 df-bc 10857 df-ihash 10885 df-shft 10997 df-cj 11024 df-re 11025 df-im 11026 df-rsqrt 11180 df-abs 11181 df-clim 11461 df-sumdc 11536 df-ef 11830 df-e 11831 df-dvds 11970 df-gcd 12146 df-prm 12301 df-pc 12479 df-rest 12943 df-topgen 12962 df-psmet 14175 df-xmet 14176 df-met 14177 df-bl 14178 df-mopn 14179 df-top 14318 df-topon 14331 df-bases 14363 df-ntr 14416 df-cn 14508 df-cnp 14509 df-tx 14573 df-cncf 14891 df-limced 14976 df-dvap 14977 df-relog 15178 df-rpcxp 15179 df-sgm 15302

This theorem is referenced by: perfect 15321

W3C validator