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

Metamath Proof Explorer

Theorem flt4lem2

Description: If A is even, B is odd. (Contributed by SN, 22-Aug-2024)

Ref Expression
Hypotheses flt4lem2.a 
|- ( ph -> A e. NN )
flt4lem2.b 
|- ( ph -> B e. NN )
flt4lem2.c 
|- ( ph -> C e. NN )
flt4lem2.1 
|- ( ph -> 2 || A )
flt4lem2.2 
|- ( ph -> ( A gcd C ) = 1 )
flt4lem2.3 
|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
Assertion flt4lem2 
|- ( ph -> -. 2 || B )

Proof

Step Hyp Ref Expression
1 flt4lem2.a 
 |-  ( ph -> A e. NN )
2 flt4lem2.b 
 |-  ( ph -> B e. NN )
3 flt4lem2.c 
 |-  ( ph -> C e. NN )
4 flt4lem2.1 
 |-  ( ph -> 2 || A )
5 flt4lem2.2 
 |-  ( ph -> ( A gcd C ) = 1 )
6 flt4lem2.3 
 |-  ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
7 breq1 
 |-  ( i = 2 -> ( i || A <-> 2 || A ) )
8 breq1 
 |-  ( i = 2 -> ( i || C <-> 2 || C ) )
9 7 8 anbi12d 
 |-  ( i = 2 -> ( ( i || A /\ i || C ) <-> ( 2 || A /\ 2 || C ) ) )
10 2z 
 |-  2 e. ZZ
11 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
12 10 11 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
13 12 a1i 
 |-  ( ( ph /\ 2 || B ) -> 2 e. ( ZZ>= ` 2 ) )
14 4 adantr 
 |-  ( ( ph /\ 2 || B ) -> 2 || A )
15 10 a1i 
 |-  ( ( ph /\ 2 || B ) -> 2 e. ZZ )
16 gcdnncl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
17 1 2 16 syl2anc 
 |-  ( ph -> ( A gcd B ) e. NN )
18 17 nnzd 
 |-  ( ph -> ( A gcd B ) e. ZZ )
19 18 adantr 
 |-  ( ( ph /\ 2 || B ) -> ( A gcd B ) e. ZZ )
20 3 adantr 
 |-  ( ( ph /\ 2 || B ) -> C e. NN )
21 20 nnzd 
 |-  ( ( ph /\ 2 || B ) -> C e. ZZ )
22 simpr 
 |-  ( ( ph /\ 2 || B ) -> 2 || B )
23 1 adantr 
 |-  ( ( ph /\ 2 || B ) -> A e. NN )
24 23 nnzd 
 |-  ( ( ph /\ 2 || B ) -> A e. ZZ )
25 2 nnzd 
 |-  ( ph -> B e. ZZ )
26 25 adantr 
 |-  ( ( ph /\ 2 || B ) -> B e. ZZ )
27 dvdsgcd 
 |-  ( ( 2 e. ZZ /\ A e. ZZ /\ B e. ZZ ) -> ( ( 2 || A /\ 2 || B ) -> 2 || ( A gcd B ) ) )
28 15 24 26 27 syl3anc 
 |-  ( ( ph /\ 2 || B ) -> ( ( 2 || A /\ 2 || B ) -> 2 || ( A gcd B ) ) )
29 14 22 28 mp2and 
 |-  ( ( ph /\ 2 || B ) -> 2 || ( A gcd B ) )
30 2nn 
 |-  2 e. NN
31 30 a1i 
 |-  ( ph -> 2 e. NN )
32 1 2 3 31 6 fltdvdsabdvdsc 
 |-  ( ph -> ( A gcd B ) || C )
33 32 adantr 
 |-  ( ( ph /\ 2 || B ) -> ( A gcd B ) || C )
34 15 19 21 29 33 dvdstrd 
 |-  ( ( ph /\ 2 || B ) -> 2 || C )
35 14 34 jca 
 |-  ( ( ph /\ 2 || B ) -> ( 2 || A /\ 2 || C ) )
36 9 13 35 rspcedvdw 
 |-  ( ( ph /\ 2 || B ) -> E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || C ) )
37 ncoprmgcdne1b 
 |-  ( ( A e. NN /\ C e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || C ) <-> ( A gcd C ) =/= 1 ) )
38 23 20 37 syl2anc 
 |-  ( ( ph /\ 2 || B ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || C ) <-> ( A gcd C ) =/= 1 ) )
39 36 38 mpbid 
 |-  ( ( ph /\ 2 || B ) -> ( A gcd C ) =/= 1 )
40 39 ex 
 |-  ( ph -> ( 2 || B -> ( A gcd C ) =/= 1 ) )
41 40 necon2bd 
 |-  ( ph -> ( ( A gcd C ) = 1 -> -. 2 || B ) )
42 5 41 mpd 
 |-  ( ph -> -. 2 || B )