Theorem sqrt2irrlem

Description: Lemma for sqrt2irr . This is the core of the proof: if A / B = sqrt ( 2 ) , then A and B are even, so A / 2 and B / 2 are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). This is Metamath 100 proof #1. (Contributed by NM, 20-Aug-2001) (Revised by Mario Carneiro, 12-Sep-2015) (Proof shortened by JV, 4-Jan-2022)

	Ref	Expression
Hypotheses	sqrt2irrlem.1	$$⊢\phi \to A\in \mathbb{Z}$$
	sqrt2irrlem.2	$$⊢\phi \to B\in \mathbb{N}$$
	sqrt2irrlem.3	$$⊢\phi \to \sqrt{2}=\frac{A}{B}$$
Assertion	sqrt2irrlem	$$⊢\phi \to \left(\frac{A}{2}\in \mathbb{Z}\wedge \frac{B}{2}\in \mathbb{N}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sqrt2irrlem.1	$$⊢\phi \to A\in \mathbb{Z}$$
2		sqrt2irrlem.2	$$⊢\phi \to B\in \mathbb{N}$$
3		sqrt2irrlem.3	$$⊢\phi \to \sqrt{2}=\frac{A}{B}$$
4		2cnd	$$⊢\phi \to 2\in ℂ$$
5	4	sqsqrtd	$$⊢\phi \to {\sqrt{2}}^2=2$$
6	3	oveq1d	$$⊢\phi \to {\sqrt{2}}^2={\left(\frac{A}{B}\right)}^2$$
7	5 6	eqtr3d	$$⊢\phi \to 2={\left(\frac{A}{B}\right)}^2$$
8	1	zcnd	$$⊢\phi \to A\in ℂ$$
9	2	nncnd	$$⊢\phi \to B\in ℂ$$
10	2	nnne0d	$$⊢\phi \to B\ne 0$$
11	8 9 10	sqdivd	$$⊢\phi \to {\left(\frac{A}{B}\right)}^2=\frac{A^2}{B^2}$$
12	7 11	eqtrd	$$⊢\phi \to 2=\frac{A^2}{B^2}$$
13	12	oveq1d	$$⊢\phi \to 2B^2=\left(\frac{A^2}{B^2}\right)B^2$$
14	8	sqcld	$$⊢\phi \to A^2\in ℂ$$
15	2	nnsqcld	$$⊢\phi \to B^2\in \mathbb{N}$$
16	15	nncnd	$$⊢\phi \to B^2\in ℂ$$
17	15	nnne0d	$$⊢\phi \to B^2\ne 0$$
18	14 16 17	divcan1d	$$⊢\phi \to \left(\frac{A^2}{B^2}\right)B^2=A^2$$
19	13 18	eqtrd	$$⊢\phi \to 2B^2=A^2$$
20	19	oveq1d	$$⊢\phi \to \frac{2B^2}{2}=\frac{A^2}{2}$$
21		2ne0	$$⊢2\ne 0$$
22	21	a1i	$$⊢\phi \to 2\ne 0$$
23	16 4 22	divcan3d	$$⊢\phi \to \frac{2B^2}{2}=B^2$$
24	20 23	eqtr3d	$$⊢\phi \to \frac{A^2}{2}=B^2$$
25	24 15	eqeltrd	$$⊢\phi \to \frac{A^2}{2}\in \mathbb{N}$$
26	25	nnzd	$$⊢\phi \to \frac{A^2}{2}\in \mathbb{Z}$$
27		zesq	$$⊢A\in \mathbb{Z}\to \left(\frac{A}{2}\in \mathbb{Z}\leftrightarrow \frac{A^2}{2}\in \mathbb{Z}\right)$$
28	1 27	syl	$$⊢\phi \to \left(\frac{A}{2}\in \mathbb{Z}\leftrightarrow \frac{A^2}{2}\in \mathbb{Z}\right)$$
29	26 28	mpbird	$$⊢\phi \to \frac{A}{2}\in \mathbb{Z}$$
30	4	sqvald	$$⊢\phi \to 2^2=2\cdot 2$$
31	30	oveq2d	$$⊢\phi \to \frac{A^2}{2^2}=\frac{A^2}{2\cdot 2}$$
32	8 4 22	sqdivd	$$⊢\phi \to {\left(\frac{A}{2}\right)}^2=\frac{A^2}{2^2}$$
33	14 4 4 22 22	divdiv1d	$$⊢\phi \to \frac{\frac{A^2}{2}}{2}=\frac{A^2}{2\cdot 2}$$
34	31 32 33	3eqtr4d	$$⊢\phi \to {\left(\frac{A}{2}\right)}^2=\frac{\frac{A^2}{2}}{2}$$
35	24	oveq1d	$$⊢\phi \to \frac{\frac{A^2}{2}}{2}=\frac{B^2}{2}$$
36	34 35	eqtrd	$$⊢\phi \to {\left(\frac{A}{2}\right)}^2=\frac{B^2}{2}$$
37		zsqcl	$$⊢\frac{A}{2}\in \mathbb{Z}\to {\left(\frac{A}{2}\right)}^2\in \mathbb{Z}$$
38	29 37	syl	$$⊢\phi \to {\left(\frac{A}{2}\right)}^2\in \mathbb{Z}$$
39	36 38	eqeltrrd	$$⊢\phi \to \frac{B^2}{2}\in \mathbb{Z}$$
40	15	nnrpd	$$⊢\phi \to B^2\in {ℝ}^{+}$$
41	40	rphalfcld	$$⊢\phi \to \frac{B^2}{2}\in {ℝ}^{+}$$
42	41	rpgt0d	$$⊢\phi \to 0<\frac{B^2}{2}$$
43		elnnz	$$⊢\frac{B^2}{2}\in \mathbb{N}\leftrightarrow \left(\frac{B^2}{2}\in \mathbb{Z}\wedge 0<\frac{B^2}{2}\right)$$
44	39 42 43	sylanbrc	$$⊢\phi \to \frac{B^2}{2}\in \mathbb{N}$$
45		nnesq	$$⊢B\in \mathbb{N}\to \left(\frac{B}{2}\in \mathbb{N}\leftrightarrow \frac{B^2}{2}\in \mathbb{N}\right)$$
46	2 45	syl	$$⊢\phi \to \left(\frac{B}{2}\in \mathbb{N}\leftrightarrow \frac{B^2}{2}\in \mathbb{N}\right)$$
47	44 46	mpbird	$$⊢\phi \to \frac{B}{2}\in \mathbb{N}$$
48	29 47	jca	$$⊢\phi \to \left(\frac{A}{2}\in \mathbb{Z}\wedge \frac{B}{2}\in \mathbb{N}\right)$$