2sqreultlem

Description: Lemma for 2sqreult . (Contributed by AV, 8-Jun-2023) (Proposed by GL, 8-Jun-2023.)

		Ref	Expression
	Assertion	2sqreultlem	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P)$

Proof

Step	Hyp	Ref	Expression
1		2sqreulem1	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P)$
2		oveq1	$⊢ b = a \to b^{2} = a^{2}$
3	2	oveq2d	$⊢ b = a \to a^{2} + b^{2} = a^{2} + a^{2}$
4	3	adantr	$⊢ (b = a \land (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0})) \to a^{2} + b^{2} = a^{2} + a^{2}$
5		nn0cn	$⊢ a \in ℕ_{0} \to a \in ℂ$
6	5	sqcld	$⊢ a \in ℕ_{0} \to a^{2} \in ℂ$
7		2times	$⊢ a^{2} \in ℂ \to 2 a^{2} = a^{2} + a^{2}$
8	7	eqcomd	$⊢ a^{2} \in ℂ \to a^{2} + a^{2} = 2 a^{2}$
9	6 8	syl	$⊢ a \in ℕ_{0} \to a^{2} + a^{2} = 2 a^{2}$
10	9	adantl	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \to a^{2} + a^{2} = 2 a^{2}$
11	10	ad2antrl	$⊢ (b = a \land (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0})) \to a^{2} + a^{2} = 2 a^{2}$
12	4 11	eqtrd	$⊢ (b = a \land (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0})) \to a^{2} + b^{2} = 2 a^{2}$
13	12	eqeq1d	$⊢ (b = a \land (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0})) \to (a^{2} + b^{2} = P \leftrightarrow 2 a^{2} = P)$
14		oveq1	$⊢ P = 2 a^{2} \to P \mod 4 = 2 a^{2} \mod 4$
15	14	eqeq1d	$⊢ P = 2 a^{2} \to (P \mod 4 = 1 \leftrightarrow 2 a^{2} \mod 4 = 1)$
16		eleq1	$⊢ P = 2 a^{2} \to (P \in ℙ \leftrightarrow 2 a^{2} \in ℙ)$
17	15 16	anbi12d	$⊢ P = 2 a^{2} \to ((P \mod 4 = 1 \land P \in ℙ) \leftrightarrow (2 a^{2} \mod 4 = 1 \land 2 a^{2} \in ℙ))$
18		nn0z	$⊢ a \in ℕ_{0} \to a \in ℤ$
19		2nn0	$⊢ 2 \in ℕ_{0}$
20		zexpcl	$⊢ (a \in ℤ \land 2 \in ℕ_{0}) \to a^{2} \in ℤ$
21	18 19 20	sylancl	$⊢ a \in ℕ_{0} \to a^{2} \in ℤ$
22		2mulprm	$⊢ a^{2} \in ℤ \to (2 a^{2} \in ℙ \leftrightarrow a^{2} = 1)$
23	21 22	syl	$⊢ a \in ℕ_{0} \to (2 a^{2} \in ℙ \leftrightarrow a^{2} = 1)$
24		oveq2	$⊢ a^{2} = 1 \to 2 a^{2} = 2 \cdot 1$
25		2t1e2	$⊢ 2 \cdot 1 = 2$
26	24 25	eqtrdi	$⊢ a^{2} = 1 \to 2 a^{2} = 2$
27	26	oveq1d	$⊢ a^{2} = 1 \to 2 a^{2} \mod 4 = 2 \mod 4$
28		2re	$⊢ 2 \in ℝ$
29		4nn	$⊢ 4 \in ℕ$
30		nnrp	$⊢ 4 \in ℕ \to 4 \in ℝ^{+}$
31	29 30	ax-mp	$⊢ 4 \in ℝ^{+}$
32		0le2	$⊢ 0 \leq 2$
33		2lt4	$⊢ 2 < 4$
34		modid	$⊢ ((2 \in ℝ \land 4 \in ℝ^{+}) \land (0 \leq 2 \land 2 < 4)) \to 2 \mod 4 = 2$
35	28 31 32 33 34	mp4an	$⊢ 2 \mod 4 = 2$
36	27 35	eqtrdi	$⊢ a^{2} = 1 \to 2 a^{2} \mod 4 = 2$
37	36	eqeq1d	$⊢ a^{2} = 1 \to (2 a^{2} \mod 4 = 1 \leftrightarrow 2 = 1)$
38		1ne2	$⊢ 1 \neq 2$
39		eqcom	$⊢ 2 = 1 \leftrightarrow 1 = 2$
40		eqneqall	$⊢ 1 = 2 \to (1 \neq 2 \to (a \leq b \to b \neq a))$
41	40	com12	$⊢ 1 \neq 2 \to (1 = 2 \to (a \leq b \to b \neq a))$
42	39 41	biimtrid	$⊢ 1 \neq 2 \to (2 = 1 \to (a \leq b \to b \neq a))$
43	38 42	ax-mp	$⊢ 2 = 1 \to (a \leq b \to b \neq a)$
44	37 43	syl6bi	$⊢ a^{2} = 1 \to (2 a^{2} \mod 4 = 1 \to (a \leq b \to b \neq a))$
45	23 44	syl6bi	$⊢ a \in ℕ_{0} \to (2 a^{2} \in ℙ \to (2 a^{2} \mod 4 = 1 \to (a \leq b \to b \neq a)))$
46	45	impcomd	$⊢ a \in ℕ_{0} \to ((2 a^{2} \mod 4 = 1 \land 2 a^{2} \in ℙ) \to (a \leq b \to b \neq a))$
47	46	com12	$⊢ (2 a^{2} \mod 4 = 1 \land 2 a^{2} \in ℙ) \to (a \in ℕ_{0} \to (a \leq b \to b \neq a))$
48	17 47	syl6bi	$⊢ P = 2 a^{2} \to ((P \mod 4 = 1 \land P \in ℙ) \to (a \in ℕ_{0} \to (a \leq b \to b \neq a)))$
49	48	expd	$⊢ P = 2 a^{2} \to (P \mod 4 = 1 \to (P \in ℙ \to (a \in ℕ_{0} \to (a \leq b \to b \neq a))))$
50	49	com34	$⊢ P = 2 a^{2} \to (P \mod 4 = 1 \to (a \in ℕ_{0} \to (P \in ℙ \to (a \leq b \to b \neq a))))$
51	50	eqcoms	$⊢ 2 a^{2} = P \to (P \mod 4 = 1 \to (a \in ℕ_{0} \to (P \in ℙ \to (a \leq b \to b \neq a))))$
52	51	com14	$⊢ P \in ℙ \to (P \mod 4 = 1 \to (a \in ℕ_{0} \to (2 a^{2} = P \to (a \leq b \to b \neq a))))$
53	52	imp31	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \to (2 a^{2} = P \to (a \leq b \to b \neq a))$
54	53	ad2antrl	$⊢ (b = a \land (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0})) \to (2 a^{2} = P \to (a \leq b \to b \neq a))$
55	13 54	sylbid	$⊢ (b = a \land (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0})) \to (a^{2} + b^{2} = P \to (a \leq b \to b \neq a))$
56	55	expimpd	$⊢ b = a \to (((((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \land a^{2} + b^{2} = P) \to (a \leq b \to b \neq a))$
57		2a1	$⊢ b \neq a \to (((((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \land a^{2} + b^{2} = P) \to (a \leq b \to b \neq a))$
58	56 57	pm2.61ine	$⊢ ((((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \land a^{2} + b^{2} = P) \to (a \leq b \to b \neq a)$
59	58	pm4.71d	$⊢ ((((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \land a^{2} + b^{2} = P) \to (a \leq b \leftrightarrow (a \leq b \land b \neq a))$
60		nn0re	$⊢ a \in ℕ_{0} \to a \in ℝ$
61	60	adantl	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \to a \in ℝ$
62		nn0re	$⊢ b \in ℕ_{0} \to b \in ℝ$
63		ltlen	$⊢ (a \in ℝ \land b \in ℝ) \to (a < b \leftrightarrow (a \leq b \land b \neq a))$
64	61 62 63	syl2an	$⊢ (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \to (a < b \leftrightarrow (a \leq b \land b \neq a))$
65	64	bibi2d	$⊢ (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \to ((a \leq b \leftrightarrow a < b) \leftrightarrow (a \leq b \leftrightarrow (a \leq b \land b \neq a)))$
66	65	adantr	$⊢ ((((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \land a^{2} + b^{2} = P) \to ((a \leq b \leftrightarrow a < b) \leftrightarrow (a \leq b \leftrightarrow (a \leq b \land b \neq a)))$
67	59 66	mpbird	$⊢ ((((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \land a^{2} + b^{2} = P) \to (a \leq b \leftrightarrow a < b)$
68	67	ex	$⊢ (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \to (a^{2} + b^{2} = P \to (a \leq b \leftrightarrow a < b))$
69	68	pm5.32rd	$⊢ (((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \land b \in ℕ_{0}) \to ((a \leq b \land a^{2} + b^{2} = P) \leftrightarrow (a < b \land a^{2} + b^{2} = P))$
70	69	reubidva	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land a \in ℕ_{0}) \to (\exists! b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \leftrightarrow \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P))$
71	70	reubidva	$⊢ (P \in ℙ \land P \mod 4 = 1) \to (\exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a \leq b \land a^{2} + b^{2} = P) \leftrightarrow \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P))$
72	1 71	mpbid	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P)$

Metamath Proof Explorer

Theorem 2sqreultlem

Proof