Metamath Proof Explorer

Theorem prmdvdsfmtnof1lem2

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

Ref Expression
Assertion prmdvdsfmtnof1lem2 ( ( 𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo ) → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) )

Proof

Step Hyp Ref Expression
1 fmtnorn ⊢ ( 𝐹 ∈ ran FermatNo ↔ ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝐹 )
2 fmtnorn ⊢ ( 𝐺 ∈ ran FermatNo ↔ ∃ 𝑚 ∈ ℕ0 ( FermatNo ‘ 𝑚 ) = 𝐺 )
3 2a1 ⊢ ( 𝐹 = 𝐺 → ( ( FermatNo ‘ 𝑛 ) = 𝐹 → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) ) )
4 3 2a1d ⊢ ( 𝐹 = 𝐺 → ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( FermatNo ‘ 𝑚 ) = 𝐺 → ( ( FermatNo ‘ 𝑛 ) = 𝐹 → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) ) ) ) )
5 fmtnonn ⊢ ( 𝑛 ∈ ℕ0 → ( FermatNo ‘ 𝑛 ) ∈ ℕ )
6 5 ad2antrl ⊢ ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) → ( FermatNo ‘ 𝑛 ) ∈ ℕ )
7 6 adantr ⊢ ( ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) ∧ ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) ) → ( FermatNo ‘ 𝑛 ) ∈ ℕ )
8 eleq1 ⊢ ( ( FermatNo ‘ 𝑛 ) = 𝐹 → ( ( FermatNo ‘ 𝑛 ) ∈ ℕ ↔ 𝐹 ∈ ℕ ) )
9 8 ad2antll ⊢ ( ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) ∧ ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) ) → ( ( FermatNo ‘ 𝑛 ) ∈ ℕ ↔ 𝐹 ∈ ℕ ) )
10 7 9 mpbid ⊢ ( ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) ∧ ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) ) → 𝐹 ∈ ℕ )
11 fmtnonn ⊢ ( 𝑚 ∈ ℕ0 → ( FermatNo ‘ 𝑚 ) ∈ ℕ )
12 11 ad2antll ⊢ ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) → ( FermatNo ‘ 𝑚 ) ∈ ℕ )
13 12 adantr ⊢ ( ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) ∧ ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) ) → ( FermatNo ‘ 𝑚 ) ∈ ℕ )
14 eleq1 ⊢ ( ( FermatNo ‘ 𝑚 ) = 𝐺 → ( ( FermatNo ‘ 𝑚 ) ∈ ℕ ↔ 𝐺 ∈ ℕ ) )
15 14 ad2antrl ⊢ ( ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) ∧ ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) ) → ( ( FermatNo ‘ 𝑚 ) ∈ ℕ ↔ 𝐺 ∈ ℕ ) )
16 13 15 mpbid ⊢ ( ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) ∧ ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) ) → 𝐺 ∈ ℕ )
17 simpll ⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) ) → 𝑛 ∈ ℕ0 )
18 simplr ⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) ) → 𝑚 ∈ ℕ0 )
19 fveq2 ⊢ ( 𝑛 = 𝑚 → ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) )
20 19 con3i ⊢ ( ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) → ¬ 𝑛 = 𝑚 )
21 20 adantl ⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) ) → ¬ 𝑛 = 𝑚 )
22 21 neqned ⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) ) → 𝑛 ≠ 𝑚 )
23 goldbachth ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑛 ≠ 𝑚 ) → ( ( FermatNo ‘ 𝑛 ) gcd ( FermatNo ‘ 𝑚 ) ) = 1 )
24 17 18 22 23 syl3anc ⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) ) → ( ( FermatNo ‘ 𝑛 ) gcd ( FermatNo ‘ 𝑚 ) ) = 1 )
25 24 ex ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) → ( ( FermatNo ‘ 𝑛 ) gcd ( FermatNo ‘ 𝑚 ) ) = 1 ) )
26 eqeq12 ⊢ ( ( ( FermatNo ‘ 𝑛 ) = 𝐹 ∧ ( FermatNo ‘ 𝑚 ) = 𝐺 ) → ( ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) ↔ 𝐹 = 𝐺 ) )
27 26 notbid ⊢ ( ( ( FermatNo ‘ 𝑛 ) = 𝐹 ∧ ( FermatNo ‘ 𝑚 ) = 𝐺 ) → ( ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) ↔ ¬ 𝐹 = 𝐺 ) )
28 oveq12 ⊢ ( ( ( FermatNo ‘ 𝑛 ) = 𝐹 ∧ ( FermatNo ‘ 𝑚 ) = 𝐺 ) → ( ( FermatNo ‘ 𝑛 ) gcd ( FermatNo ‘ 𝑚 ) ) = ( 𝐹 gcd 𝐺 ) )
29 28 eqeq1d ⊢ ( ( ( FermatNo ‘ 𝑛 ) = 𝐹 ∧ ( FermatNo ‘ 𝑚 ) = 𝐺 ) → ( ( ( FermatNo ‘ 𝑛 ) gcd ( FermatNo ‘ 𝑚 ) ) = 1 ↔ ( 𝐹 gcd 𝐺 ) = 1 ) )
30 27 29 imbi12d ⊢ ( ( ( FermatNo ‘ 𝑛 ) = 𝐹 ∧ ( FermatNo ‘ 𝑚 ) = 𝐺 ) → ( ( ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) → ( ( FermatNo ‘ 𝑛 ) gcd ( FermatNo ‘ 𝑚 ) ) = 1 ) ↔ ( ¬ 𝐹 = 𝐺 → ( 𝐹 gcd 𝐺 ) = 1 ) ) )
31 30 ancoms ⊢ ( ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) → ( ( ¬ ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) → ( ( FermatNo ‘ 𝑛 ) gcd ( FermatNo ‘ 𝑚 ) ) = 1 ) ↔ ( ¬ 𝐹 = 𝐺 → ( 𝐹 gcd 𝐺 ) = 1 ) ) )
32 25 31 syl5ibcom ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) → ( ¬ 𝐹 = 𝐺 → ( 𝐹 gcd 𝐺 ) = 1 ) ) )
33 32 com23 ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ¬ 𝐹 = 𝐺 → ( ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) → ( 𝐹 gcd 𝐺 ) = 1 ) ) )
34 33 impcom ⊢ ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) → ( ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) → ( 𝐹 gcd 𝐺 ) = 1 ) )
35 34 imp ⊢ ( ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) ∧ ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) ) → ( 𝐹 gcd 𝐺 ) = 1 )
36 prmnn ⊢ ( 𝐼 ∈ ℙ → 𝐼 ∈ ℕ )
37 coprmdvds1 ⊢ ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) → ( ( 𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐼 = 1 ) )
38 37 imp ⊢ ( ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) ∧ ( 𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) → 𝐼 = 1 )
39 36 38 syl3anr1 ⊢ ( ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) ∧ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) → 𝐼 = 1 )
40 eleq1 ⊢ ( 𝐼 = 1 → ( 𝐼 ∈ ℙ ↔ 1 ∈ ℙ ) )
41 1nprm ⊢ ¬ 1 ∈ ℙ
42 41 pm2.21i ⊢ ( 1 ∈ ℙ → 𝐹 = 𝐺 )
43 40 42 syl6bi ⊢ ( 𝐼 = 1 → ( 𝐼 ∈ ℙ → 𝐹 = 𝐺 ) )
44 43 com12 ⊢ ( 𝐼 ∈ ℙ → ( 𝐼 = 1 → 𝐹 = 𝐺 ) )
45 44 a1d ⊢ ( 𝐼 ∈ ℙ → ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) → ( 𝐼 = 1 → 𝐹 = 𝐺 ) ) )
46 45 3ad2ant1 ⊢ ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) → ( 𝐼 = 1 → 𝐹 = 𝐺 ) ) )
47 46 impcom ⊢ ( ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) ∧ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) → ( 𝐼 = 1 → 𝐹 = 𝐺 ) )
48 39 47 mpd ⊢ ( ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) ∧ ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) → 𝐹 = 𝐺 )
49 48 ex ⊢ ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) )
50 10 16 35 49 syl3anc ⊢ ( ( ( ¬ 𝐹 = 𝐺 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) ) ∧ ( ( FermatNo ‘ 𝑚 ) = 𝐺 ∧ ( FermatNo ‘ 𝑛 ) = 𝐹 ) ) → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) )
51 50 exp43 ⊢ ( ¬ 𝐹 = 𝐺 → ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( FermatNo ‘ 𝑚 ) = 𝐺 → ( ( FermatNo ‘ 𝑛 ) = 𝐹 → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) ) ) ) )
52 4 51 pm2.61i ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( FermatNo ‘ 𝑚 ) = 𝐺 → ( ( FermatNo ‘ 𝑛 ) = 𝐹 → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) ) ) )
53 52 rexlimdva ⊢ ( 𝑛 ∈ ℕ0 → ( ∃ 𝑚 ∈ ℕ0 ( FermatNo ‘ 𝑚 ) = 𝐺 → ( ( FermatNo ‘ 𝑛 ) = 𝐹 → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) ) ) )
54 53 com23 ⊢ ( 𝑛 ∈ ℕ0 → ( ( FermatNo ‘ 𝑛 ) = 𝐹 → ( ∃ 𝑚 ∈ ℕ0 ( FermatNo ‘ 𝑚 ) = 𝐺 → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) ) ) )
55 54 rexlimiv ⊢ ( ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝐹 → ( ∃ 𝑚 ∈ ℕ0 ( FermatNo ‘ 𝑚 ) = 𝐺 → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) ) )
56 55 imp ⊢ ( ( ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝐹 ∧ ∃ 𝑚 ∈ ℕ0 ( FermatNo ‘ 𝑚 ) = 𝐺 ) → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) )
57 1 2 56 syl2anb ⊢ ( ( 𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo ) → ( ( 𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐹 = 𝐺 ) )