This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → A ∈ ℤ
sqrt2irrlem.2 ⊢ φ → B ∈ ℕ
sqrt2irrlem.3 ⊢ φ → 2 = A B
Assertion sqrt2irrlem ⊢ φ → A 2 ∈ ℤ ∧ B 2 ∈ ℕ

Proof

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