MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sqr2irrlem Structured version   GIF version

Theorem sqr2irrlem 12967
Description: Lemma for irrationality of square root of 2. The core of the proof - if 𝐴 / 𝐵 = √(2), then 𝐴 and 𝐵 are even, so 𝐴 / 2 and 𝐵 / 2 are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
Hypotheses
Ref Expression
sqr2irrlem.1 (𝜑𝐴 ∈ ℤ)
sqr2irrlem.2 (𝜑𝐵 ∈ ℕ)
sqr2irrlem.3 (𝜑 → (√‘2) = (𝐴 / 𝐵))
Assertion
Ref Expression
sqr2irrlem (𝜑 → ((𝐴 / 2) ∈ ℤ ∧ (𝐵 / 2) ∈ ℕ))

Proof of Theorem sqr2irrlem
StepHypRef Expression
1 2cn 10168 . . . . . . . . . . . 12 2 ∈ ℂ
2 sqrth 12288 . . . . . . . . . . . 12 (2 ∈ ℂ → ((√‘2)↑2) = 2)
31, 2ax-mp 5 . . . . . . . . . . 11 ((√‘2)↑2) = 2
4 sqr2irrlem.3 . . . . . . . . . . . 12 (𝜑 → (√‘2) = (𝐴 / 𝐵))
54oveq1d 6196 . . . . . . . . . . 11 (𝜑 → ((√‘2)↑2) = ((𝐴 / 𝐵)↑2))
63, 5syl5eqr 2525 . . . . . . . . . 10 (𝜑 → 2 = ((𝐴 / 𝐵)↑2))
7 sqr2irrlem.1 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℤ)
87zcnd 10474 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
9 sqr2irrlem.2 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℕ)
109nncnd 10114 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
119nnne0d 10142 . . . . . . . . . . 11 (𝜑𝐵 ≠ 0)
128, 10, 11sqdivd 11640 . . . . . . . . . 10 (𝜑 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
136, 12eqtrd 2511 . . . . . . . . 9 (𝜑 → 2 = ((𝐴↑2) / (𝐵↑2)))
1413oveq1d 6196 . . . . . . . 8 (𝜑 → (2 · (𝐵↑2)) = (((𝐴↑2) / (𝐵↑2)) · (𝐵↑2)))
158sqcld 11625 . . . . . . . . 9 (𝜑 → (𝐴↑2) ∈ ℂ)
169nnsqcld 11647 . . . . . . . . . 10 (𝜑 → (𝐵↑2) ∈ ℕ)
1716nncnd 10114 . . . . . . . . 9 (𝜑 → (𝐵↑2) ∈ ℂ)
1816nnne0d 10142 . . . . . . . . 9 (𝜑 → (𝐵↑2) ≠ 0)
1915, 17, 18divcan1d 9889 . . . . . . . 8 (𝜑 → (((𝐴↑2) / (𝐵↑2)) · (𝐵↑2)) = (𝐴↑2))
2014, 19eqtrd 2511 . . . . . . 7 (𝜑 → (2 · (𝐵↑2)) = (𝐴↑2))
2120oveq1d 6196 . . . . . 6 (𝜑 → ((2 · (𝐵↑2)) / 2) = ((𝐴↑2) / 2))
221a1i 11 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
23 2ne0 10181 . . . . . . . 8 2 ≠ 0
2423a1i 11 . . . . . . 7 (𝜑 → 2 ≠ 0)
2517, 22, 24divcan3d 9893 . . . . . 6 (𝜑 → ((2 · (𝐵↑2)) / 2) = (𝐵↑2))
2621, 25eqtr3d 2513 . . . . 5 (𝜑 → ((𝐴↑2) / 2) = (𝐵↑2))
2726, 16eqeltrd 2553 . . . 4 (𝜑 → ((𝐴↑2) / 2) ∈ ℕ)
2827nnzd 10472 . . 3 (𝜑 → ((𝐴↑2) / 2) ∈ ℤ)
29 zesq 11606 . . . 4 (𝐴 ∈ ℤ → ((𝐴 / 2) ∈ ℤ ↔ ((𝐴↑2) / 2) ∈ ℤ))
307, 29syl 16 . . 3 (𝜑 → ((𝐴 / 2) ∈ ℤ ↔ ((𝐴↑2) / 2) ∈ ℤ))
3128, 30mpbird 225 . 2 (𝜑 → (𝐴 / 2) ∈ ℤ)
321sqvali 11565 . . . . . . . 8 (2↑2) = (2 · 2)
3332oveq2i 6192 . . . . . . 7 ((𝐴↑2) / (2↑2)) = ((𝐴↑2) / (2 · 2))
348, 22, 24sqdivd 11640 . . . . . . 7 (𝜑 → ((𝐴 / 2)↑2) = ((𝐴↑2) / (2↑2)))
3515, 22, 22, 24, 24divdiv1d 9919 . . . . . . 7 (𝜑 → (((𝐴↑2) / 2) / 2) = ((𝐴↑2) / (2 · 2)))
3633, 34, 353eqtr4a 2537 . . . . . 6 (𝜑 → ((𝐴 / 2)↑2) = (((𝐴↑2) / 2) / 2))
3726oveq1d 6196 . . . . . 6 (𝜑 → (((𝐴↑2) / 2) / 2) = ((𝐵↑2) / 2))
3836, 37eqtrd 2511 . . . . 5 (𝜑 → ((𝐴 / 2)↑2) = ((𝐵↑2) / 2))
39 zsqcl 11556 . . . . . 6 ((𝐴 / 2) ∈ ℤ → ((𝐴 / 2)↑2) ∈ ℤ)
4031, 39syl 16 . . . . 5 (𝜑 → ((𝐴 / 2)↑2) ∈ ℤ)
4138, 40eqeltrrd 2554 . . . 4 (𝜑 → ((𝐵↑2) / 2) ∈ ℤ)
4216nnrpd 10747 . . . . . 6 (𝜑 → (𝐵↑2) ∈ ℝ+)
4342rphalfcld 10760 . . . . 5 (𝜑 → ((𝐵↑2) / 2) ∈ ℝ+)
4443rpgt0d 10751 . . . 4 (𝜑 → 0 < ((𝐵↑2) / 2))
45 elnnz 10390 . . . 4 (((𝐵↑2) / 2) ∈ ℕ ↔ (((𝐵↑2) / 2) ∈ ℤ ∧ 0 < ((𝐵↑2) / 2)))
4641, 44, 45sylanbrc 647 . . 3 (𝜑 → ((𝐵↑2) / 2) ∈ ℕ)
47 nnesq 11607 . . . 4 (𝐵 ∈ ℕ → ((𝐵 / 2) ∈ ℕ ↔ ((𝐵↑2) / 2) ∈ ℕ))
489, 47syl 16 . . 3 (𝜑 → ((𝐵 / 2) ∈ ℕ ↔ ((𝐵↑2) / 2) ∈ ℕ))
4946, 48mpbird 225 . 2 (𝜑 → (𝐵 / 2) ∈ ℕ)
5031, 49jca 520 1 (𝜑 → ((𝐴 / 2) ∈ ℤ ∧ (𝐵 / 2) ∈ ℕ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 178  wa 360   = wceq 1662  wcel 1734  wne 2642   class class class wbr 4293  cfv 5553  (class class class)co 6181  cc 9085  0cc0 9087   · cmul 9092   < clt 9217   / cdiv 9775  cn 10098  2c2 10147  cz 10380  cexp 11486  csqr 12158
This theorem is referenced by:  sqr2irr  12968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-5 1573  ax-17 1636  ax-9 1677  ax-8 1698  ax-13 1736  ax-14 1738  ax-6 1753  ax-7 1758  ax-11 1770  ax-12 1963  ax-ext 2460  ax-sep 4414  ax-nul 4422  ax-pow 4467  ax-pr 4493  ax-un 4793  ax-cnex 9143  ax-resscn 9144  ax-1cn 9145  ax-icn 9146  ax-addcl 9147  ax-addrcl 9148  ax-mulcl 9149  ax-mulrcl 9150  ax-mulcom 9151  ax-addass 9152  ax-mulass 9153  ax-distr 9154  ax-i2m1 9155  ax-1ne0 9156  ax-1rid 9157  ax-rnegex 9158  ax-rrecex 9159  ax-cnre 9160  ax-pre-lttri 9161  ax-pre-lttrn 9162  ax-pre-ltadd 9163  ax-pre-mulgt0 9164  ax-pre-sup 9165
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 939  df-3an 940  df-tru 1334  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2325  df-mo 2326  df-clab 2466  df-cleq 2472  df-clel 2475  df-nfc 2604  df-ne 2644  df-nel 2645  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3005  df-sbc 3210  df-csb 3311  df-dif 3353  df-un 3355  df-in 3357  df-ss 3364  df-pss 3366  df-nul 3658  df-if 3810  df-pw 3875  df-sn 3894  df-pr 3895  df-tp 3896  df-op 3897  df-uni 4094  df-iun 4174  df-br 4294  df-opab 4352  df-mpt 4353  df-tr 4387  df-eprel 4586  df-id 4590  df-po 4595  df-so 4596  df-fr 4633  df-we 4635  df-ord 4676  df-on 4677  df-lim 4678  df-suc 4679  df-om 4938  df-xp 4976  df-rel 4977  df-cnv 4978  df-co 4979  df-dm 4980  df-rn 4981  df-res 4982  df-ima 4983  df-iota 5516  df-fun 5555  df-fn 5556  df-f 5557  df-f1 5558  df-fo 5559  df-f1o 5560  df-fv 5561  df-ov 6184  df-oprab 6185  df-mpt2 6186  df-2nd 6452  df-riota 6654  df-recs 6728  df-rdg 6763  df-er 7000  df-en 7205  df-dom 7206  df-sdom 7207  df-sup 7541  df-pnf 9219  df-mnf 9220  df-xr 9221  df-ltxr 9222  df-le 9223  df-sub 9391  df-neg 9392  df-div 9776  df-nn 10099  df-2 10156  df-3 10157  df-n0 10320  df-z 10381  df-uz 10587  df-rp 10713  df-seq 11428  df-exp 11487  df-cj 12024  df-re 12025  df-im 12026  df-sqr 12160  df-abs 12161
  Copyright terms: Public domain W3C validator