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

Metamath Proof Explorer

Theorem flt4lem5elem

Description: Version of fltaccoprm and fltbccoprm where M is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd , dvds2addd , and prmdvdsexp , we can show that if two variables are coprime, the third is also coprime to the two. (Contributed by SN, 24-Aug-2024)

Ref Expression
Hypotheses flt4lem5elem.m 
|- ( ph -> M e. NN )
flt4lem5elem.r 
|- ( ph -> R e. NN )
flt4lem5elem.s 
|- ( ph -> S e. NN )
flt4lem5elem.1 
|- ( ph -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) )
flt4lem5elem.2 
|- ( ph -> ( R gcd S ) = 1 )
Assertion flt4lem5elem 
|- ( ph -> ( ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) )

Proof

Step Hyp Ref Expression
1 flt4lem5elem.m 
 |-  ( ph -> M e. NN )
2 flt4lem5elem.r 
 |-  ( ph -> R e. NN )
3 flt4lem5elem.s 
 |-  ( ph -> S e. NN )
4 flt4lem5elem.1 
 |-  ( ph -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) )
5 flt4lem5elem.2 
 |-  ( ph -> ( R gcd S ) = 1 )
6 2 3 prmdvdsncoprmbd 
 |-  ( ph -> ( E. p e. Prime ( p || R /\ p || S ) <-> ( R gcd S ) =/= 1 ) )
7 6 necon2bbid 
 |-  ( ph -> ( ( R gcd S ) = 1 <-> -. E. p e. Prime ( p || R /\ p || S ) ) )
8 5 7 mpbid 
 |-  ( ph -> -. E. p e. Prime ( p || R /\ p || S ) )
9 simprl 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || R )
10 simplr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p e. Prime )
11 prmz 
 |-  ( p e. Prime -> p e. ZZ )
12 10 11 syl 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p e. ZZ )
13 1 nnzd 
 |-  ( ph -> M e. ZZ )
14 13 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> M e. ZZ )
15 2 nnsqcld 
 |-  ( ph -> ( R ^ 2 ) e. NN )
16 15 nnzd 
 |-  ( ph -> ( R ^ 2 ) e. ZZ )
17 16 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( R ^ 2 ) e. ZZ )
18 simprr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || M )
19 2 nnzd 
 |-  ( ph -> R e. ZZ )
20 19 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> R e. ZZ )
21 prmdvdssq 
 |-  ( ( p e. Prime /\ R e. ZZ ) -> ( p || R <-> p || ( R ^ 2 ) ) )
22 10 20 21 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( p || R <-> p || ( R ^ 2 ) ) )
23 9 22 mpbid 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || ( R ^ 2 ) )
24 12 14 17 18 23 dvds2subd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || ( M - ( R ^ 2 ) ) )
25 15 nncnd 
 |-  ( ph -> ( R ^ 2 ) e. CC )
26 25 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( R ^ 2 ) e. CC )
27 3 nnsqcld 
 |-  ( ph -> ( S ^ 2 ) e. NN )
28 27 nncnd 
 |-  ( ph -> ( S ^ 2 ) e. CC )
29 28 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( S ^ 2 ) e. CC )
30 4 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) )
31 26 29 30 mvrladdd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( M - ( R ^ 2 ) ) = ( S ^ 2 ) )
32 24 31 breqtrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || ( S ^ 2 ) )
33 3 nnzd 
 |-  ( ph -> S e. ZZ )
34 33 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> S e. ZZ )
35 prmdvdssq 
 |-  ( ( p e. Prime /\ S e. ZZ ) -> ( p || S <-> p || ( S ^ 2 ) ) )
36 10 34 35 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( p || S <-> p || ( S ^ 2 ) ) )
37 32 36 mpbird 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> p || S )
38 9 37 jca 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || R /\ p || M ) ) -> ( p || R /\ p || S ) )
39 38 ex 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p || R /\ p || M ) -> ( p || R /\ p || S ) ) )
40 39 reximdva 
 |-  ( ph -> ( E. p e. Prime ( p || R /\ p || M ) -> E. p e. Prime ( p || R /\ p || S ) ) )
41 8 40 mtod 
 |-  ( ph -> -. E. p e. Prime ( p || R /\ p || M ) )
42 2 1 prmdvdsncoprmbd 
 |-  ( ph -> ( E. p e. Prime ( p || R /\ p || M ) <-> ( R gcd M ) =/= 1 ) )
43 42 necon2bbid 
 |-  ( ph -> ( ( R gcd M ) = 1 <-> -. E. p e. Prime ( p || R /\ p || M ) ) )
44 41 43 mpbird 
 |-  ( ph -> ( R gcd M ) = 1 )
45 simplr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p e. Prime )
46 45 11 syl 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p e. ZZ )
47 13 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> M e. ZZ )
48 27 nnzd 
 |-  ( ph -> ( S ^ 2 ) e. ZZ )
49 48 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( S ^ 2 ) e. ZZ )
50 simprr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || M )
51 simprl 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || S )
52 33 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> S e. ZZ )
53 45 52 35 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( p || S <-> p || ( S ^ 2 ) ) )
54 51 53 mpbid 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || ( S ^ 2 ) )
55 46 47 49 50 54 dvds2subd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || ( M - ( S ^ 2 ) ) )
56 25 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( R ^ 2 ) e. CC )
57 28 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( S ^ 2 ) e. CC )
58 4 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) )
59 56 57 58 mvrraddd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( M - ( S ^ 2 ) ) = ( R ^ 2 ) )
60 55 59 breqtrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || ( R ^ 2 ) )
61 19 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> R e. ZZ )
62 45 61 21 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( p || R <-> p || ( R ^ 2 ) ) )
63 60 62 mpbird 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> p || R )
64 63 51 jca 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p || S /\ p || M ) ) -> ( p || R /\ p || S ) )
65 64 ex 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p || S /\ p || M ) -> ( p || R /\ p || S ) ) )
66 65 reximdva 
 |-  ( ph -> ( E. p e. Prime ( p || S /\ p || M ) -> E. p e. Prime ( p || R /\ p || S ) ) )
67 8 66 mtod 
 |-  ( ph -> -. E. p e. Prime ( p || S /\ p || M ) )
68 3 1 prmdvdsncoprmbd 
 |-  ( ph -> ( E. p e. Prime ( p || S /\ p || M ) <-> ( S gcd M ) =/= 1 ) )
69 68 necon2bbid 
 |-  ( ph -> ( ( S gcd M ) = 1 <-> -. E. p e. Prime ( p || S /\ p || M ) ) )
70 67 69 mpbird 
 |-  ( ph -> ( S gcd M ) = 1 )
71 44 70 jca 
 |-  ( ph -> ( ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) )