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 
|- ( ph -> A e. ZZ )
sqrt2irrlem.2 
|- ( ph -> B e. NN )
sqrt2irrlem.3 
|- ( ph -> ( sqrt ` 2 ) = ( A / B ) )
Assertion sqrt2irrlem 
|- ( ph -> ( ( A / 2 ) e. ZZ /\ ( B / 2 ) e. NN ) )

Proof

Step Hyp Ref Expression
1 sqrt2irrlem.1 
 |-  ( ph -> A e. ZZ )
2 sqrt2irrlem.2 
 |-  ( ph -> B e. NN )
3 sqrt2irrlem.3 
 |-  ( ph -> ( sqrt ` 2 ) = ( A / B ) )
4 2cnd 
 |-  ( ph -> 2 e. CC )
5 4 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` 2 ) ^ 2 ) = 2 )
6 3 oveq1d 
 |-  ( ph -> ( ( sqrt ` 2 ) ^ 2 ) = ( ( A / B ) ^ 2 ) )
7 5 6 eqtr3d 
 |-  ( ph -> 2 = ( ( A / B ) ^ 2 ) )
8 1 zcnd 
 |-  ( ph -> A e. CC )
9 2 nncnd 
 |-  ( ph -> B e. CC )
10 2 nnne0d 
 |-  ( ph -> B =/= 0 )
11 8 9 10 sqdivd 
 |-  ( ph -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )
12 7 11 eqtrd 
 |-  ( ph -> 2 = ( ( A ^ 2 ) / ( B ^ 2 ) ) )
13 12 oveq1d 
 |-  ( ph -> ( 2 x. ( B ^ 2 ) ) = ( ( ( A ^ 2 ) / ( B ^ 2 ) ) x. ( B ^ 2 ) ) )
14 8 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
15 2 nnsqcld 
 |-  ( ph -> ( B ^ 2 ) e. NN )
16 15 nncnd 
 |-  ( ph -> ( B ^ 2 ) e. CC )
17 15 nnne0d 
 |-  ( ph -> ( B ^ 2 ) =/= 0 )
18 14 16 17 divcan1d 
 |-  ( ph -> ( ( ( A ^ 2 ) / ( B ^ 2 ) ) x. ( B ^ 2 ) ) = ( A ^ 2 ) )
19 13 18 eqtrd 
 |-  ( ph -> ( 2 x. ( B ^ 2 ) ) = ( A ^ 2 ) )
20 19 oveq1d 
 |-  ( ph -> ( ( 2 x. ( B ^ 2 ) ) / 2 ) = ( ( A ^ 2 ) / 2 ) )
21 2ne0 
 |-  2 =/= 0
22 21 a1i 
 |-  ( ph -> 2 =/= 0 )
23 16 4 22 divcan3d 
 |-  ( ph -> ( ( 2 x. ( B ^ 2 ) ) / 2 ) = ( B ^ 2 ) )
24 20 23 eqtr3d 
 |-  ( ph -> ( ( A ^ 2 ) / 2 ) = ( B ^ 2 ) )
25 24 15 eqeltrd 
 |-  ( ph -> ( ( A ^ 2 ) / 2 ) e. NN )
26 25 nnzd 
 |-  ( ph -> ( ( A ^ 2 ) / 2 ) e. ZZ )
27 zesq 
 |-  ( A e. ZZ -> ( ( A / 2 ) e. ZZ <-> ( ( A ^ 2 ) / 2 ) e. ZZ ) )
28 1 27 syl 
 |-  ( ph -> ( ( A / 2 ) e. ZZ <-> ( ( A ^ 2 ) / 2 ) e. ZZ ) )
29 26 28 mpbird 
 |-  ( ph -> ( A / 2 ) e. ZZ )
30 4 sqvald 
 |-  ( ph -> ( 2 ^ 2 ) = ( 2 x. 2 ) )
31 30 oveq2d 
 |-  ( ph -> ( ( A ^ 2 ) / ( 2 ^ 2 ) ) = ( ( A ^ 2 ) / ( 2 x. 2 ) ) )
32 8 4 22 sqdivd 
 |-  ( ph -> ( ( A / 2 ) ^ 2 ) = ( ( A ^ 2 ) / ( 2 ^ 2 ) ) )
33 14 4 4 22 22 divdiv1d 
 |-  ( ph -> ( ( ( A ^ 2 ) / 2 ) / 2 ) = ( ( A ^ 2 ) / ( 2 x. 2 ) ) )
34 31 32 33 3eqtr4d 
 |-  ( ph -> ( ( A / 2 ) ^ 2 ) = ( ( ( A ^ 2 ) / 2 ) / 2 ) )
35 24 oveq1d 
 |-  ( ph -> ( ( ( A ^ 2 ) / 2 ) / 2 ) = ( ( B ^ 2 ) / 2 ) )
36 34 35 eqtrd 
 |-  ( ph -> ( ( A / 2 ) ^ 2 ) = ( ( B ^ 2 ) / 2 ) )
37 zsqcl 
 |-  ( ( A / 2 ) e. ZZ -> ( ( A / 2 ) ^ 2 ) e. ZZ )
38 29 37 syl 
 |-  ( ph -> ( ( A / 2 ) ^ 2 ) e. ZZ )
39 36 38 eqeltrrd 
 |-  ( ph -> ( ( B ^ 2 ) / 2 ) e. ZZ )
40 15 nnrpd 
 |-  ( ph -> ( B ^ 2 ) e. RR+ )
41 40 rphalfcld 
 |-  ( ph -> ( ( B ^ 2 ) / 2 ) e. RR+ )
42 41 rpgt0d 
 |-  ( ph -> 0 < ( ( B ^ 2 ) / 2 ) )
43 elnnz 
 |-  ( ( ( B ^ 2 ) / 2 ) e. NN <-> ( ( ( B ^ 2 ) / 2 ) e. ZZ /\ 0 < ( ( B ^ 2 ) / 2 ) ) )
44 39 42 43 sylanbrc 
 |-  ( ph -> ( ( B ^ 2 ) / 2 ) e. NN )
45 nnesq 
 |-  ( B e. NN -> ( ( B / 2 ) e. NN <-> ( ( B ^ 2 ) / 2 ) e. NN ) )
46 2 45 syl 
 |-  ( ph -> ( ( B / 2 ) e. NN <-> ( ( B ^ 2 ) / 2 ) e. NN ) )
47 44 46 mpbird 
 |-  ( ph -> ( B / 2 ) e. NN )
48 29 47 jca 
 |-  ( ph -> ( ( A / 2 ) e. ZZ /\ ( B / 2 ) e. NN ) )