Metamath Proof Explorer

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 ) ∈ ℕ ) )