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	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
	sqrt2irrlem.2	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	sqrt2irrlem.3	⊢ ( 𝜑 → ( √ ‘ 2 ) = ( 𝐴 / 𝐵 ) )
Assertion	sqrt2irrlem	⊢ ( 𝜑 → ( ( 𝐴 / 2 ) ∈ ℤ ∧ ( 𝐵 / 2 ) ∈ ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		sqrt2irrlem.1	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2		sqrt2irrlem.2	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		sqrt2irrlem.3	⊢ ( 𝜑 → ( √ ‘ 2 ) = ( 𝐴 / 𝐵 ) )
4		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
5	4	sqsqrtd	⊢ ( 𝜑 → ( ( √ ‘ 2 ) ↑ 2 ) = 2 )
6	3	oveq1d	⊢ ( 𝜑 → ( ( √ ‘ 2 ) ↑ 2 ) = ( ( 𝐴 / 𝐵 ) ↑ 2 ) )
7	5 6	eqtr3d	⊢ ( 𝜑 → 2 = ( ( 𝐴 / 𝐵 ) ↑ 2 ) )
8	1	zcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
9	2	nncnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10	2	nnne0d	⊢ ( 𝜑 → 𝐵 ≠ 0 )
11	8 9 10	sqdivd	⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) )
12	7 11	eqtrd	⊢ ( 𝜑 → 2 = ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) )
13	12	oveq1d	⊢ ( 𝜑 → ( 2 · ( 𝐵 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) )
14	8	sqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
15	2	nnsqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℕ )
16	15	nncnd	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
17	15	nnne0d	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ≠ 0 )
18	14 16 17	divcan1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) / ( 𝐵 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) = ( 𝐴 ↑ 2 ) )
19	13 18	eqtrd	⊢ ( 𝜑 → ( 2 · ( 𝐵 ↑ 2 ) ) = ( 𝐴 ↑ 2 ) )
20	19	oveq1d	⊢ ( 𝜑 → ( ( 2 · ( 𝐵 ↑ 2 ) ) / 2 ) = ( ( 𝐴 ↑ 2 ) / 2 ) )
21		2ne0	⊢ 2 ≠ 0
22	21	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
23	16 4 22	divcan3d	⊢ ( 𝜑 → ( ( 2 · ( 𝐵 ↑ 2 ) ) / 2 ) = ( 𝐵 ↑ 2 ) )
24	20 23	eqtr3d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) / 2 ) = ( 𝐵 ↑ 2 ) )
25	24 15	eqeltrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℕ )
26	25	nnzd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℤ )
27		zesq	⊢ ( 𝐴 ∈ ℤ → ( ( 𝐴 / 2 ) ∈ ℤ ↔ ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℤ ) )
28	1 27	syl	⊢ ( 𝜑 → ( ( 𝐴 / 2 ) ∈ ℤ ↔ ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℤ ) )
29	26 28	mpbird	⊢ ( 𝜑 → ( 𝐴 / 2 ) ∈ ℤ )
30	4	sqvald	⊢ ( 𝜑 → ( 2 ↑ 2 ) = ( 2 · 2 ) )
31	30	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) / ( 2 · 2 ) ) )
32	8 4 22	sqdivd	⊢ ( 𝜑 → ( ( 𝐴 / 2 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) / ( 2 ↑ 2 ) ) )
33	14 4 4 22 22	divdiv1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) / 2 ) / 2 ) = ( ( 𝐴 ↑ 2 ) / ( 2 · 2 ) ) )
34	31 32 33	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 / 2 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) / 2 ) / 2 ) )
35	24	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) / 2 ) / 2 ) = ( ( 𝐵 ↑ 2 ) / 2 ) )
36	34 35	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 / 2 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) / 2 ) )
37		zsqcl	⊢ ( ( 𝐴 / 2 ) ∈ ℤ → ( ( 𝐴 / 2 ) ↑ 2 ) ∈ ℤ )
38	29 37	syl	⊢ ( 𝜑 → ( ( 𝐴 / 2 ) ↑ 2 ) ∈ ℤ )
39	36 38	eqeltrrd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) / 2 ) ∈ ℤ )
40	15	nnrpd	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ+ )
41	40	rphalfcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) / 2 ) ∈ ℝ+ )
42	41	rpgt0d	⊢ ( 𝜑 → 0 < ( ( 𝐵 ↑ 2 ) / 2 ) )
43		elnnz	⊢ ( ( ( 𝐵 ↑ 2 ) / 2 ) ∈ ℕ ↔ ( ( ( 𝐵 ↑ 2 ) / 2 ) ∈ ℤ ∧ 0 < ( ( 𝐵 ↑ 2 ) / 2 ) ) )
44	39 42 43	sylanbrc	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) / 2 ) ∈ ℕ )
45		nnesq	⊢ ( 𝐵 ∈ ℕ → ( ( 𝐵 / 2 ) ∈ ℕ ↔ ( ( 𝐵 ↑ 2 ) / 2 ) ∈ ℕ ) )
46	2 45	syl	⊢ ( 𝜑 → ( ( 𝐵 / 2 ) ∈ ℕ ↔ ( ( 𝐵 ↑ 2 ) / 2 ) ∈ ℕ ) )
47	44 46	mpbird	⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℕ )
48	29 47	jca	⊢ ( 𝜑 → ( ( 𝐴 / 2 ) ∈ ℤ ∧ ( 𝐵 / 2 ) ∈ ℕ ) )