2sq2

Description: 2 is the sum of squares of two nonnegative integers iff the two integers are 1 . (Contributed by AV, 19-Jun-2023)

		Ref	Expression
	Assertion	2sq2	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} + B^{2} = 2 \leftrightarrow (A = 1 \land B = 1))$

Proof

Step	Hyp	Ref	Expression
1		nn0sqcl	$⊢ A \in ℕ_{0} \to A^{2} \in ℕ_{0}$
2		nn0sqcl	$⊢ B \in ℕ_{0} \to B^{2} \in ℕ_{0}$
3	2	nn0red	$⊢ B \in ℕ_{0} \to B^{2} \in ℝ$
4	1 3	anim12ci	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (B^{2} \in ℝ \land A^{2} \in ℕ_{0})$
5	4	adantr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to (B^{2} \in ℝ \land A^{2} \in ℕ_{0})$
6		nn0addge2	$⊢ (B^{2} \in ℝ \land A^{2} \in ℕ_{0}) \to B^{2} \leq A^{2} + B^{2}$
7	5 6	syl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to B^{2} \leq A^{2} + B^{2}$
8		breq2	$⊢ A^{2} + B^{2} = 2 \to (B^{2} \leq A^{2} + B^{2} \leftrightarrow B^{2} \leq 2)$
9	8	adantl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to (B^{2} \leq A^{2} + B^{2} \leftrightarrow B^{2} \leq 2)$
10	2	ad2antlr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to B^{2} \in ℕ_{0}$
11		nn0le2is012	$⊢ (B^{2} \in ℕ_{0} \land B^{2} \leq 2) \to (B^{2} = 0 \lor B^{2} = 1 \lor B^{2} = 2)$
12	11	ex	$⊢ B^{2} \in ℕ_{0} \to (B^{2} \leq 2 \to (B^{2} = 0 \lor B^{2} = 1 \lor B^{2} = 2))$
13	10 12	syl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to (B^{2} \leq 2 \to (B^{2} = 0 \lor B^{2} = 1 \lor B^{2} = 2))$
14		oveq2	$⊢ B^{2} = 0 \to A^{2} + B^{2} = A^{2} + 0$
15	14	eqeq1d	$⊢ B^{2} = 0 \to (A^{2} + B^{2} = 2 \leftrightarrow A^{2} + 0 = 2)$
16	15	adantl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land B^{2} = 0) \to (A^{2} + B^{2} = 2 \leftrightarrow A^{2} + 0 = 2)$
17	1	nn0cnd	$⊢ A \in ℕ_{0} \to A^{2} \in ℂ$
18	17	addridd	$⊢ A \in ℕ_{0} \to A^{2} + 0 = A^{2}$
19	18	adantr	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A^{2} + 0 = A^{2}$
20	19	eqeq1d	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} + 0 = 2 \leftrightarrow A^{2} = 2)$
21	1	nn0red	$⊢ A \in ℕ_{0} \to A^{2} \in ℝ$
22		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
23	22	sqge0d	$⊢ A \in ℕ_{0} \to 0 \leq A^{2}$
24		2nn0	$⊢ 2 \in ℕ_{0}$
25	24	a1i	$⊢ A \in ℕ_{0} \to 2 \in ℕ_{0}$
26	25	nn0red	$⊢ A \in ℕ_{0} \to 2 \in ℝ$
27		0le2	$⊢ 0 \leq 2$
28	27	a1i	$⊢ A \in ℕ_{0} \to 0 \leq 2$
29		sqrt11	$⊢ ((A^{2} \in ℝ \land 0 \leq A^{2}) \land (2 \in ℝ \land 0 \leq 2)) \to (\sqrt{A^{2}} = \sqrt{2} \leftrightarrow A^{2} = 2)$
30	21 23 26 28 29	syl22anc	$⊢ A \in ℕ_{0} \to (\sqrt{A^{2}} = \sqrt{2} \leftrightarrow A^{2} = 2)$
31		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
32	22 31	sqrtsqd	$⊢ A \in ℕ_{0} \to \sqrt{A^{2}} = A$
33	32	eqeq1d	$⊢ A \in ℕ_{0} \to (\sqrt{A^{2}} = \sqrt{2} \leftrightarrow A = \sqrt{2})$
34		sqrt2irr	$⊢ \sqrt{2} \notin ℚ$
35		df-nel	$⊢ \sqrt{2} \notin ℚ \leftrightarrow \neg \sqrt{2} \in ℚ$
36		id	$⊢ \sqrt{2} = A \to \sqrt{2} = A$
37	36	eqcoms	$⊢ A = \sqrt{2} \to \sqrt{2} = A$
38	37	eleq1d	$⊢ A = \sqrt{2} \to (\sqrt{2} \in ℚ \leftrightarrow A \in ℚ)$
39	38	notbid	$⊢ A = \sqrt{2} \to (\neg \sqrt{2} \in ℚ \leftrightarrow \neg A \in ℚ)$
40	39	adantl	$⊢ (A \in ℕ_{0} \land A = \sqrt{2}) \to (\neg \sqrt{2} \in ℚ \leftrightarrow \neg A \in ℚ)$
41		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
42		zq	$⊢ A \in ℤ \to A \in ℚ$
43	41 42	syl	$⊢ A \in ℕ_{0} \to A \in ℚ$
44	43	pm2.24d	$⊢ A \in ℕ_{0} \to (\neg A \in ℚ \to (A = 1 \land B = 1))$
45	44	adantr	$⊢ (A \in ℕ_{0} \land A = \sqrt{2}) \to (\neg A \in ℚ \to (A = 1 \land B = 1))$
46	40 45	sylbid	$⊢ (A \in ℕ_{0} \land A = \sqrt{2}) \to (\neg \sqrt{2} \in ℚ \to (A = 1 \land B = 1))$
47	46	com12	$⊢ \neg \sqrt{2} \in ℚ \to ((A \in ℕ_{0} \land A = \sqrt{2}) \to (A = 1 \land B = 1))$
48	47	expd	$⊢ \neg \sqrt{2} \in ℚ \to (A \in ℕ_{0} \to (A = \sqrt{2} \to (A = 1 \land B = 1)))$
49	35 48	sylbi	$⊢ \sqrt{2} \notin ℚ \to (A \in ℕ_{0} \to (A = \sqrt{2} \to (A = 1 \land B = 1)))$
50	34 49	ax-mp	$⊢ A \in ℕ_{0} \to (A = \sqrt{2} \to (A = 1 \land B = 1))$
51	33 50	sylbid	$⊢ A \in ℕ_{0} \to (\sqrt{A^{2}} = \sqrt{2} \to (A = 1 \land B = 1))$
52	30 51	sylbird	$⊢ A \in ℕ_{0} \to (A^{2} = 2 \to (A = 1 \land B = 1))$
53	52	adantr	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} = 2 \to (A = 1 \land B = 1))$
54	20 53	sylbid	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} + 0 = 2 \to (A = 1 \land B = 1))$
55	54	adantr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land B^{2} = 0) \to (A^{2} + 0 = 2 \to (A = 1 \land B = 1))$
56	16 55	sylbid	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land B^{2} = 0) \to (A^{2} + B^{2} = 2 \to (A = 1 \land B = 1))$
57	56	impancom	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to (B^{2} = 0 \to (A = 1 \land B = 1))$
58		oveq2	$⊢ B^{2} = 1 \to A^{2} + B^{2} = A^{2} + 1$
59	58	eqeq1d	$⊢ B^{2} = 1 \to (A^{2} + B^{2} = 2 \leftrightarrow A^{2} + 1 = 2)$
60		2cnd	$⊢ A \in ℕ_{0} \to 2 \in ℂ$
61		1cnd	$⊢ A \in ℕ_{0} \to 1 \in ℂ$
62	60 61 17	3jca	$⊢ A \in ℕ_{0} \to (2 \in ℂ \land 1 \in ℂ \land A^{2} \in ℂ)$
63	62	adantr	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (2 \in ℂ \land 1 \in ℂ \land A^{2} \in ℂ)$
64		subadd2	$⊢ (2 \in ℂ \land 1 \in ℂ \land A^{2} \in ℂ) \to (2 - 1 = A^{2} \leftrightarrow A^{2} + 1 = 2)$
65	63 64	syl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (2 - 1 = A^{2} \leftrightarrow A^{2} + 1 = 2)$
66	65	bicomd	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} + 1 = 2 \leftrightarrow 2 - 1 = A^{2})$
67	59 66	sylan9bbr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land B^{2} = 1) \to (A^{2} + B^{2} = 2 \leftrightarrow 2 - 1 = A^{2})$
68		nn0sqeq1	$⊢ (B \in ℕ_{0} \land B^{2} = 1) \to B = 1$
69	68	ex	$⊢ B \in ℕ_{0} \to (B^{2} = 1 \to B = 1)$
70	69	adantl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (B^{2} = 1 \to B = 1)$
71		2m1e1	$⊢ 2 - 1 = 1$
72	71	a1i	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to 2 - 1 = 1$
73	72	eqeq1d	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (2 - 1 = A^{2} \leftrightarrow 1 = A^{2})$
74		eqcom	$⊢ 1 = A^{2} \leftrightarrow A^{2} = 1$
75	73 74	bitrdi	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (2 - 1 = A^{2} \leftrightarrow A^{2} = 1)$
76		nn0sqeq1	$⊢ (A \in ℕ_{0} \land A^{2} = 1) \to A = 1$
77	76	ex	$⊢ A \in ℕ_{0} \to (A^{2} = 1 \to A = 1)$
78	77	adantr	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} = 1 \to A = 1)$
79		id	$⊢ (A = 1 \land B = 1) \to (A = 1 \land B = 1)$
80	79	ex	$⊢ A = 1 \to (B = 1 \to (A = 1 \land B = 1))$
81	78 80	syl6	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} = 1 \to (B = 1 \to (A = 1 \land B = 1)))$
82	75 81	sylbid	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (2 - 1 = A^{2} \to (B = 1 \to (A = 1 \land B = 1)))$
83	82	com23	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (B = 1 \to (2 - 1 = A^{2} \to (A = 1 \land B = 1)))$
84	70 83	syld	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (B^{2} = 1 \to (2 - 1 = A^{2} \to (A = 1 \land B = 1)))$
85	84	imp	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land B^{2} = 1) \to (2 - 1 = A^{2} \to (A = 1 \land B = 1))$
86	67 85	sylbid	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land B^{2} = 1) \to (A^{2} + B^{2} = 2 \to (A = 1 \land B = 1))$
87	86	impancom	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to (B^{2} = 1 \to (A = 1 \land B = 1))$
88		nn0re	$⊢ B \in ℕ_{0} \to B \in ℝ$
89		nn0ge0	$⊢ B \in ℕ_{0} \to 0 \leq B$
90	88 89	sqrtsqd	$⊢ B \in ℕ_{0} \to \sqrt{B^{2}} = B$
91	90	eqcomd	$⊢ B \in ℕ_{0} \to B = \sqrt{B^{2}}$
92	91	eqeq1d	$⊢ B \in ℕ_{0} \to (B = \sqrt{2} \leftrightarrow \sqrt{B^{2}} = \sqrt{2})$
93	88	sqge0d	$⊢ B \in ℕ_{0} \to 0 \leq B^{2}$
94		2re	$⊢ 2 \in ℝ$
95	94	a1i	$⊢ B \in ℕ_{0} \to 2 \in ℝ$
96	27	a1i	$⊢ B \in ℕ_{0} \to 0 \leq 2$
97		sqrt11	$⊢ ((B^{2} \in ℝ \land 0 \leq B^{2}) \land (2 \in ℝ \land 0 \leq 2)) \to (\sqrt{B^{2}} = \sqrt{2} \leftrightarrow B^{2} = 2)$
98	3 93 95 96 97	syl22anc	$⊢ B \in ℕ_{0} \to (\sqrt{B^{2}} = \sqrt{2} \leftrightarrow B^{2} = 2)$
99	92 98	bitrd	$⊢ B \in ℕ_{0} \to (B = \sqrt{2} \leftrightarrow B^{2} = 2)$
100		id	$⊢ \sqrt{2} = B \to \sqrt{2} = B$
101	100	eqcoms	$⊢ B = \sqrt{2} \to \sqrt{2} = B$
102	101	eleq1d	$⊢ B = \sqrt{2} \to (\sqrt{2} \in ℚ \leftrightarrow B \in ℚ)$
103	102	adantl	$⊢ (B \in ℕ_{0} \land B = \sqrt{2}) \to (\sqrt{2} \in ℚ \leftrightarrow B \in ℚ)$
104	103	notbid	$⊢ (B \in ℕ_{0} \land B = \sqrt{2}) \to (\neg \sqrt{2} \in ℚ \leftrightarrow \neg B \in ℚ)$
105		nn0z	$⊢ B \in ℕ_{0} \to B \in ℤ$
106		zq	$⊢ B \in ℤ \to B \in ℚ$
107	105 106	syl	$⊢ B \in ℕ_{0} \to B \in ℚ$
108	107	pm2.24d	$⊢ B \in ℕ_{0} \to (\neg B \in ℚ \to (A = 1 \land B = 1))$
109	108	adantr	$⊢ (B \in ℕ_{0} \land B = \sqrt{2}) \to (\neg B \in ℚ \to (A = 1 \land B = 1))$
110	104 109	sylbid	$⊢ (B \in ℕ_{0} \land B = \sqrt{2}) \to (\neg \sqrt{2} \in ℚ \to (A = 1 \land B = 1))$
111	110	com12	$⊢ \neg \sqrt{2} \in ℚ \to ((B \in ℕ_{0} \land B = \sqrt{2}) \to (A = 1 \land B = 1))$
112	111	expd	$⊢ \neg \sqrt{2} \in ℚ \to (B \in ℕ_{0} \to (B = \sqrt{2} \to (A = 1 \land B = 1)))$
113	35 112	sylbi	$⊢ \sqrt{2} \notin ℚ \to (B \in ℕ_{0} \to (B = \sqrt{2} \to (A = 1 \land B = 1)))$
114	34 113	ax-mp	$⊢ B \in ℕ_{0} \to (B = \sqrt{2} \to (A = 1 \land B = 1))$
115	99 114	sylbird	$⊢ B \in ℕ_{0} \to (B^{2} = 2 \to (A = 1 \land B = 1))$
116	115	ad2antlr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to (B^{2} = 2 \to (A = 1 \land B = 1))$
117	57 87 116	3jaod	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to ((B^{2} = 0 \lor B^{2} = 1 \lor B^{2} = 2) \to (A = 1 \land B = 1))$
118	13 117	syld	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to (B^{2} \leq 2 \to (A = 1 \land B = 1))$
119	9 118	sylbid	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to (B^{2} \leq A^{2} + B^{2} \to (A = 1 \land B = 1))$
120	7 119	mpd	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land A^{2} + B^{2} = 2) \to (A = 1 \land B = 1)$
121	120	ex	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} + B^{2} = 2 \to (A = 1 \land B = 1))$
122		oveq1	$⊢ A = 1 \to A^{2} = 1^{2}$
123		sq1	$⊢ 1^{2} = 1$
124	122 123	eqtrdi	$⊢ A = 1 \to A^{2} = 1$
125		oveq1	$⊢ B = 1 \to B^{2} = 1^{2}$
126	125 123	eqtrdi	$⊢ B = 1 \to B^{2} = 1$
127	124 126	oveqan12d	$⊢ (A = 1 \land B = 1) \to A^{2} + B^{2} = 1 + 1$
128		1p1e2	$⊢ 1 + 1 = 2$
129	127 128	eqtrdi	$⊢ (A = 1 \land B = 1) \to A^{2} + B^{2} = 2$
130	121 129	impbid1	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} + B^{2} = 2 \leftrightarrow (A = 1 \land B = 1))$

Metamath Proof Explorer

Theorem 2sq2

Proof