Metamath Proof Explorer

Theorem prmdvdsfmtnof1lem2

Description: Lemma 2 for prmdvdsfmtnof1 . (Contributed by AV, 3-Aug-2021)

Ref Expression
Assertion prmdvdsfmtnof1lem2 
|- ( ( F e. ran FermatNo /\ G e. ran FermatNo ) -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) )

Proof

Step Hyp Ref Expression
1 fmtnorn 
 |-  ( F e. ran FermatNo <-> E. n e. NN0 ( FermatNo ` n ) = F )
2 fmtnorn 
 |-  ( G e. ran FermatNo <-> E. m e. NN0 ( FermatNo ` m ) = G )
3 2a1 
 |-  ( F = G -> ( ( FermatNo ` n ) = F -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) ) )
4 3 2a1d 
 |-  ( F = G -> ( ( n e. NN0 /\ m e. NN0 ) -> ( ( FermatNo ` m ) = G -> ( ( FermatNo ` n ) = F -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) ) ) ) )
5 fmtnonn 
 |-  ( n e. NN0 -> ( FermatNo ` n ) e. NN )
6 5 ad2antrl 
 |-  ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) -> ( FermatNo ` n ) e. NN )
7 6 adantr 
 |-  ( ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) /\ ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) ) -> ( FermatNo ` n ) e. NN )
8 eleq1 
 |-  ( ( FermatNo ` n ) = F -> ( ( FermatNo ` n ) e. NN <-> F e. NN ) )
9 8 ad2antll 
 |-  ( ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) /\ ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) ) -> ( ( FermatNo ` n ) e. NN <-> F e. NN ) )
10 7 9 mpbid 
 |-  ( ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) /\ ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) ) -> F e. NN )
11 fmtnonn 
 |-  ( m e. NN0 -> ( FermatNo ` m ) e. NN )
12 11 ad2antll 
 |-  ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) -> ( FermatNo ` m ) e. NN )
13 12 adantr 
 |-  ( ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) /\ ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) ) -> ( FermatNo ` m ) e. NN )
14 eleq1 
 |-  ( ( FermatNo ` m ) = G -> ( ( FermatNo ` m ) e. NN <-> G e. NN ) )
15 14 ad2antrl 
 |-  ( ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) /\ ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) ) -> ( ( FermatNo ` m ) e. NN <-> G e. NN ) )
16 13 15 mpbid 
 |-  ( ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) /\ ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) ) -> G e. NN )
17 simpll 
 |-  ( ( ( n e. NN0 /\ m e. NN0 ) /\ -. ( FermatNo ` n ) = ( FermatNo ` m ) ) -> n e. NN0 )
18 simplr 
 |-  ( ( ( n e. NN0 /\ m e. NN0 ) /\ -. ( FermatNo ` n ) = ( FermatNo ` m ) ) -> m e. NN0 )
19 fveq2 
 |-  ( n = m -> ( FermatNo ` n ) = ( FermatNo ` m ) )
20 19 con3i 
 |-  ( -. ( FermatNo ` n ) = ( FermatNo ` m ) -> -. n = m )
21 20 adantl 
 |-  ( ( ( n e. NN0 /\ m e. NN0 ) /\ -. ( FermatNo ` n ) = ( FermatNo ` m ) ) -> -. n = m )
22 21 neqned 
 |-  ( ( ( n e. NN0 /\ m e. NN0 ) /\ -. ( FermatNo ` n ) = ( FermatNo ` m ) ) -> n =/= m )
23 goldbachth 
 |-  ( ( n e. NN0 /\ m e. NN0 /\ n =/= m ) -> ( ( FermatNo ` n ) gcd ( FermatNo ` m ) ) = 1 )
24 17 18 22 23 syl3anc 
 |-  ( ( ( n e. NN0 /\ m e. NN0 ) /\ -. ( FermatNo ` n ) = ( FermatNo ` m ) ) -> ( ( FermatNo ` n ) gcd ( FermatNo ` m ) ) = 1 )
25 24 ex 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( -. ( FermatNo ` n ) = ( FermatNo ` m ) -> ( ( FermatNo ` n ) gcd ( FermatNo ` m ) ) = 1 ) )
26 eqeq12 
 |-  ( ( ( FermatNo ` n ) = F /\ ( FermatNo ` m ) = G ) -> ( ( FermatNo ` n ) = ( FermatNo ` m ) <-> F = G ) )
27 26 notbid 
 |-  ( ( ( FermatNo ` n ) = F /\ ( FermatNo ` m ) = G ) -> ( -. ( FermatNo ` n ) = ( FermatNo ` m ) <-> -. F = G ) )
28 oveq12 
 |-  ( ( ( FermatNo ` n ) = F /\ ( FermatNo ` m ) = G ) -> ( ( FermatNo ` n ) gcd ( FermatNo ` m ) ) = ( F gcd G ) )
29 28 eqeq1d 
 |-  ( ( ( FermatNo ` n ) = F /\ ( FermatNo ` m ) = G ) -> ( ( ( FermatNo ` n ) gcd ( FermatNo ` m ) ) = 1 <-> ( F gcd G ) = 1 ) )
30 27 29 imbi12d 
 |-  ( ( ( FermatNo ` n ) = F /\ ( FermatNo ` m ) = G ) -> ( ( -. ( FermatNo ` n ) = ( FermatNo ` m ) -> ( ( FermatNo ` n ) gcd ( FermatNo ` m ) ) = 1 ) <-> ( -. F = G -> ( F gcd G ) = 1 ) ) )
31 30 ancoms 
 |-  ( ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) -> ( ( -. ( FermatNo ` n ) = ( FermatNo ` m ) -> ( ( FermatNo ` n ) gcd ( FermatNo ` m ) ) = 1 ) <-> ( -. F = G -> ( F gcd G ) = 1 ) ) )
32 25 31 syl5ibcom 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) -> ( -. F = G -> ( F gcd G ) = 1 ) ) )
33 32 com23 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( -. F = G -> ( ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) -> ( F gcd G ) = 1 ) ) )
34 33 impcom 
 |-  ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) -> ( ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) -> ( F gcd G ) = 1 ) )
35 34 imp 
 |-  ( ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) /\ ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) ) -> ( F gcd G ) = 1 )
36 prmnn 
 |-  ( I e. Prime -> I e. NN )
37 coprmdvds1 
 |-  ( ( F e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) -> ( ( I e. NN /\ I || F /\ I || G ) -> I = 1 ) )
38 37 imp 
 |-  ( ( ( F e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) /\ ( I e. NN /\ I || F /\ I || G ) ) -> I = 1 )
39 36 38 syl3anr1 
 |-  ( ( ( F e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) /\ ( I e. Prime /\ I || F /\ I || G ) ) -> I = 1 )
40 eleq1 
 |-  ( I = 1 -> ( I e. Prime <-> 1 e. Prime ) )
41 1nprm 
 |-  -. 1 e. Prime
42 41 pm2.21i 
 |-  ( 1 e. Prime -> F = G )
43 40 42 syl6bi 
 |-  ( I = 1 -> ( I e. Prime -> F = G ) )
44 43 com12 
 |-  ( I e. Prime -> ( I = 1 -> F = G ) )
45 44 a1d 
 |-  ( I e. Prime -> ( ( F e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) -> ( I = 1 -> F = G ) ) )
46 45 3ad2ant1 
 |-  ( ( I e. Prime /\ I || F /\ I || G ) -> ( ( F e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) -> ( I = 1 -> F = G ) ) )
47 46 impcom 
 |-  ( ( ( F e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) /\ ( I e. Prime /\ I || F /\ I || G ) ) -> ( I = 1 -> F = G ) )
48 39 47 mpd 
 |-  ( ( ( F e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) /\ ( I e. Prime /\ I || F /\ I || G ) ) -> F = G )
49 48 ex 
 |-  ( ( F e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) )
50 10 16 35 49 syl3anc 
 |-  ( ( ( -. F = G /\ ( n e. NN0 /\ m e. NN0 ) ) /\ ( ( FermatNo ` m ) = G /\ ( FermatNo ` n ) = F ) ) -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) )
51 50 exp43 
 |-  ( -. F = G -> ( ( n e. NN0 /\ m e. NN0 ) -> ( ( FermatNo ` m ) = G -> ( ( FermatNo ` n ) = F -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) ) ) ) )
52 4 51 pm2.61i 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( FermatNo ` m ) = G -> ( ( FermatNo ` n ) = F -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) ) ) )
53 52 rexlimdva 
 |-  ( n e. NN0 -> ( E. m e. NN0 ( FermatNo ` m ) = G -> ( ( FermatNo ` n ) = F -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) ) ) )
54 53 com23 
 |-  ( n e. NN0 -> ( ( FermatNo ` n ) = F -> ( E. m e. NN0 ( FermatNo ` m ) = G -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) ) ) )
55 54 rexlimiv 
 |-  ( E. n e. NN0 ( FermatNo ` n ) = F -> ( E. m e. NN0 ( FermatNo ` m ) = G -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) ) )
56 55 imp 
 |-  ( ( E. n e. NN0 ( FermatNo ` n ) = F /\ E. m e. NN0 ( FermatNo ` m ) = G ) -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) )
57 1 2 56 syl2anb 
 |-  ( ( F e. ran FermatNo /\ G e. ran FermatNo ) -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) )