perfectlem1

	Ref	Expression
Hypotheses	perfectlem.1	$⊢ φ \to A \in ℕ$
	perfectlem.2	$⊢ φ \to B \in ℕ$
	perfectlem.3	$⊢ φ \to \neg 2 ∥ B$
	perfectlem.4	$⊢ φ \to 1 σ 2^{A} B = 2 2^{A} B$
Assertion	perfectlem1	$⊢ φ \to (2^{A + 1} \in ℕ \land 2^{A + 1} - 1 \in ℕ \land \frac{B}{2^{A + 1} - 1} \in ℕ)$

Proof

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

Metamath Proof Explorer

Theorem perfectlem1

Proof