perfectALTVlem1

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

	Ref	Expression
Hypotheses	perfectALTVlem.1	$⊢ φ \to A \in ℕ$
	perfectALTVlem.2	$⊢ φ \to B \in ℕ$
	perfectALTVlem.3	$⊢ φ \to B \in Odd$
	perfectALTVlem.4	$⊢ φ \to 1 σ 2^{A} B = 2 2^{A} B$
Assertion	perfectALTVlem1	$⊢ φ \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		perfectALTVlem.1	$⊢ φ \to A \in ℕ$
2		perfectALTVlem.2	$⊢ φ \to B \in ℕ$
3		perfectALTVlem.3	$⊢ φ \to B \in Odd$
4		perfectALTVlem.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	11	a1i	$⊢ φ \to 2 \in ℝ$
13	1	peano2nnd	$⊢ φ \to A + 1 \in ℕ$
14		1lt2	$⊢ 1 < 2$
15	14	a1i	$⊢ φ \to 1 < 2$
16		expgt1	$⊢ (2 \in ℝ \land A + 1 \in ℕ \land 1 < 2) \to 1 < 2^{A + 1}$
17	12 13 15 16	syl3anc	$⊢ φ \to 1 < 2^{A + 1}$
18		1nn	$⊢ 1 \in ℕ$
19		nnsub	$⊢ (1 \in ℕ \land 2^{A + 1} \in ℕ) \to (1 < 2^{A + 1} \leftrightarrow 2^{A + 1} - 1 \in ℕ)$
20	18 10 19	sylancr	$⊢ φ \to (1 < 2^{A + 1} \leftrightarrow 2^{A + 1} - 1 \in ℕ)$
21	17 20	mpbid	$⊢ φ \to 2^{A + 1} - 1 \in ℕ$
22	10	nnzd	$⊢ φ \to 2^{A + 1} \in ℤ$
23		peano2zm	$⊢ 2^{A + 1} \in ℤ \to 2^{A + 1} - 1 \in ℤ$
24	22 23	syl	$⊢ φ \to 2^{A + 1} - 1 \in ℤ$
25		1nn0	$⊢ 1 \in ℕ_{0}$
26		sgmnncl	$⊢ (1 \in ℕ_{0} \land B \in ℕ) \to 1 σ B \in ℕ$
27	25 2 26	sylancr	$⊢ φ \to 1 σ B \in ℕ$
28	27	nnzd	$⊢ φ \to 1 σ B \in ℤ$
29		dvdsmul1	$⊢ (2^{A + 1} - 1 \in ℤ \land 1 σ B \in ℤ) \to (2^{A + 1} - 1) ∥ (2^{A + 1} - 1) (1 σ B)$
30	24 28 29	syl2anc	$⊢ φ \to (2^{A + 1} - 1) ∥ (2^{A + 1} - 1) (1 σ B)$
31		2cn	$⊢ 2 \in ℂ$
32		expp1	$⊢ (2 \in ℂ \land A \in ℕ_{0}) \to 2^{A + 1} = 2^{A} \cdot 2$
33	31 6 32	sylancr	$⊢ φ \to 2^{A + 1} = 2^{A} \cdot 2$
34		nnexpcl	$⊢ (2 \in ℕ \land A \in ℕ_{0}) \to 2^{A} \in ℕ$
35	5 6 34	sylancr	$⊢ φ \to 2^{A} \in ℕ$
36	35	nncnd	$⊢ φ \to 2^{A} \in ℂ$
37		mulcom	$⊢ (2^{A} \in ℂ \land 2 \in ℂ) \to 2^{A} \cdot 2 = 2 2^{A}$
38	36 31 37	sylancl	$⊢ φ \to 2^{A} \cdot 2 = 2 2^{A}$
39	33 38	eqtrd	$⊢ φ \to 2^{A + 1} = 2 2^{A}$
40	39	oveq1d	$⊢ φ \to 2^{A + 1} B = 2 2^{A} B$
41	31	a1i	$⊢ φ \to 2 \in ℂ$
42	2	nncnd	$⊢ φ \to B \in ℂ$
43	41 36 42	mulassd	$⊢ φ \to 2 2^{A} B = 2 2^{A} B$
44		1cnd	$⊢ φ \to 1 \in ℂ$
45		isodd7	$⊢ B \in Odd \leftrightarrow (B \in ℤ \land 2 \gcd B = 1)$
46	45	simprbi	$⊢ B \in Odd \to 2 \gcd B = 1$
47	3 46	syl	$⊢ φ \to 2 \gcd B = 1$
48		2z	$⊢ 2 \in ℤ$
49	48	a1i	$⊢ φ \to 2 \in ℤ$
50	2	nnzd	$⊢ φ \to B \in ℤ$
51		rpexp1i	$⊢ (2 \in ℤ \land B \in ℤ \land A \in ℕ_{0}) \to (2 \gcd B = 1 \to 2^{A} \gcd B = 1)$
52	49 50 6 51	syl3anc	$⊢ φ \to (2 \gcd B = 1 \to 2^{A} \gcd B = 1)$
53	47 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 35 2 53 54	syl13anc	$⊢ φ \to 1 σ 2^{A} B = (1 σ 2^{A}) (1 σ B)$
56	1	nncnd	$⊢ φ \to A \in ℂ$
57		pncan1	$⊢ A \in ℂ \to A + 1 - 1 = A$
58	56 57	syl	$⊢ φ \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	13 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	40 43 65	3eqtrd	$⊢ φ \to 2^{A + 1} B = (2^{A + 1} - 1) (1 σ B)$
67	30 66	breqtrrd	$⊢ φ \to (2^{A + 1} - 1) ∥ 2^{A + 1} B$
68	24 22	gcdcomd	$⊢ φ \to (2^{A + 1} - 1) \gcd 2^{A + 1} = 2^{A + 1} \gcd (2^{A + 1} - 1)$
69		nnpw2evenALTV	$⊢ A + 1 \in ℕ \to 2^{A + 1} \in Even$
70	13 69	syl	$⊢ φ \to 2^{A + 1} \in Even$
71		evenm1odd	$⊢ 2^{A + 1} \in Even \to 2^{A + 1} - 1 \in Odd$
72	70 71	syl	$⊢ φ \to 2^{A + 1} - 1 \in Odd$
73		isodd7	$⊢ 2^{A + 1} - 1 \in Odd \leftrightarrow (2^{A + 1} - 1 \in ℤ \land 2 \gcd (2^{A + 1} - 1) = 1)$
74	73	simprbi	$⊢ 2^{A + 1} - 1 \in Odd \to 2 \gcd (2^{A + 1} - 1) = 1$
75	72 74	syl	$⊢ φ \to 2 \gcd (2^{A + 1} - 1) = 1$
76		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)$
77	49 24 8 76	syl3anc	$⊢ φ \to (2 \gcd (2^{A + 1} - 1) = 1 \to 2^{A + 1} \gcd (2^{A + 1} - 1) = 1)$
78	75 77	mpd	$⊢ φ \to 2^{A + 1} \gcd (2^{A + 1} - 1) = 1$
79	68 78	eqtrd	$⊢ φ \to (2^{A + 1} - 1) \gcd 2^{A + 1} = 1$
80		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)$
81	24 22 50 80	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)$
82	67 79 81	mp2and	$⊢ φ \to (2^{A + 1} - 1) ∥ B$
83		nndivdvds	$⊢ (B \in ℕ \land 2^{A + 1} - 1 \in ℕ) \to ((2^{A + 1} - 1) ∥ B \leftrightarrow \frac{B}{2^{A + 1} - 1} \in ℕ)$
84	2 21 83	syl2anc	$⊢ φ \to ((2^{A + 1} - 1) ∥ B \leftrightarrow \frac{B}{2^{A + 1} - 1} \in ℕ)$
85	82 84	mpbid	$⊢ φ \to \frac{B}{2^{A + 1} - 1} \in ℕ$
86	10 21 85	3jca	$⊢ φ \to (2^{A + 1} \in ℕ \land 2^{A + 1} - 1 \in ℕ \land \frac{B}{2^{A + 1} - 1} \in ℕ)$

Metamath Proof Explorer

Theorem perfectALTVlem1

Proof