41prothprm

		Ref	Expression
	Hypothesis	41prothprm.p	$⊢ P = 41$
	Assertion	41prothprm	$⊢ (P = 5 2^{3} + 1 \land P \in ℙ)$

Proof

Step	Hyp	Ref	Expression
1		41prothprm.p	$⊢ P = 41$
2	1	41prothprmlem2	$⊢ 3^{\frac{P - 1}{2}} \mod P = -1 \mod P$
3		dfdec10	$⊢ 41 = 10 \cdot 4 + 1$
4		4t2e8	$⊢ 4 \cdot 2 = 8$
5		4cn	$⊢ 4 \in ℂ$
6		2cn	$⊢ 2 \in ℂ$
7	5 6	mulcomi	$⊢ 4 \cdot 2 = 2 \cdot 4$
8	4 7	eqtr3i	$⊢ 8 = 2 \cdot 4$
9	8	oveq2i	$⊢ 5 \cdot 8 = 5 2 \cdot 4$
10		5cn	$⊢ 5 \in ℂ$
11	10 6 5	mulassi	$⊢ 5 \cdot 2 \cdot 4 = 5 2 \cdot 4$
12		5t2e10	$⊢ 5 \cdot 2 = 10$
13	12	oveq1i	$⊢ 5 \cdot 2 \cdot 4 = 10 \cdot 4$
14	9 11 13	3eqtr2i	$⊢ 5 \cdot 8 = 10 \cdot 4$
15		cu2	$⊢ 2^{3} = 8$
16	15	eqcomi	$⊢ 8 = 2^{3}$
17	16	oveq2i	$⊢ 5 \cdot 8 = 5 2^{3}$
18	14 17	eqtr3i	$⊢ 10 \cdot 4 = 5 2^{3}$
19	18	oveq1i	$⊢ 10 \cdot 4 + 1 = 5 2^{3} + 1$
20	1 3 19	3eqtri	$⊢ P = 5 2^{3} + 1$
21		simpr	$⊢ (3^{\frac{P - 1}{2}} \mod P = -1 \mod P \land P = 5 2^{3} + 1) \to P = 5 2^{3} + 1$
22		3nn	$⊢ 3 \in ℕ$
23	22	a1i	$⊢ (3^{\frac{P - 1}{2}} \mod P = -1 \mod P \land P = 5 2^{3} + 1) \to 3 \in ℕ$
24		5nn	$⊢ 5 \in ℕ$
25	24	a1i	$⊢ (3^{\frac{P - 1}{2}} \mod P = -1 \mod P \land P = 5 2^{3} + 1) \to 5 \in ℕ$
26		5lt8	$⊢ 5 < 8$
27	26 15	breqtrri	$⊢ 5 < 2^{3}$
28	27	a1i	$⊢ (3^{\frac{P - 1}{2}} \mod P = -1 \mod P \land P = 5 2^{3} + 1) \to 5 < 2^{3}$
29		3z	$⊢ 3 \in ℤ$
30	29	a1i	$⊢ 3^{\frac{P - 1}{2}} \mod P = -1 \mod P \to 3 \in ℤ$
31		oveq1	$⊢ x = 3 \to x^{\frac{P - 1}{2}} = 3^{\frac{P - 1}{2}}$
32	31	oveq1d	$⊢ x = 3 \to x^{\frac{P - 1}{2}} \mod P = 3^{\frac{P - 1}{2}} \mod P$
33	32	eqeq1d	$⊢ x = 3 \to (x^{\frac{P - 1}{2}} \mod P = -1 \mod P \leftrightarrow 3^{\frac{P - 1}{2}} \mod P = -1 \mod P)$
34	33	adantl	$⊢ (3^{\frac{P - 1}{2}} \mod P = -1 \mod P \land x = 3) \to (x^{\frac{P - 1}{2}} \mod P = -1 \mod P \leftrightarrow 3^{\frac{P - 1}{2}} \mod P = -1 \mod P)$
35		id	$⊢ 3^{\frac{P - 1}{2}} \mod P = -1 \mod P \to 3^{\frac{P - 1}{2}} \mod P = -1 \mod P$
36	30 34 35	rspcedvd	$⊢ 3^{\frac{P - 1}{2}} \mod P = -1 \mod P \to \exists x \in ℤ x^{\frac{P - 1}{2}} \mod P = -1 \mod P$
37	36	adantr	$⊢ (3^{\frac{P - 1}{2}} \mod P = -1 \mod P \land P = 5 2^{3} + 1) \to \exists x \in ℤ x^{\frac{P - 1}{2}} \mod P = -1 \mod P$
38	23 25 21 28 37	proththd	$⊢ (3^{\frac{P - 1}{2}} \mod P = -1 \mod P \land P = 5 2^{3} + 1) \to P \in ℙ$
39	21 38	jca	$⊢ (3^{\frac{P - 1}{2}} \mod P = -1 \mod P \land P = 5 2^{3} + 1) \to (P = 5 2^{3} + 1 \land P \in ℙ)$
40	2 20 39	mp2an	$⊢ (P = 5 2^{3} + 1 \land P \in ℙ)$

Metamath Proof Explorer

Theorem 41prothprm

Proof