Metamath Proof Explorer

Theorem goldbachthlem1

Description: Lemma 1 for goldbachth . (Contributed by AV, 1-Aug-2021)

Ref Expression
Assertion goldbachthlem1 
|- ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( FermatNo ` M ) || ( ( FermatNo ` N ) - 2 ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> M e. NN0 )
2 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
3 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
4 znnsub 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( N - M ) e. NN ) )
5 2 3 4 syl2anr 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( M < N <-> ( N - M ) e. NN ) )
6 5 biimp3a 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( N - M ) e. NN )
7 fmtnodvds 
 |-  ( ( M e. NN0 /\ ( N - M ) e. NN ) -> ( FermatNo ` M ) || ( ( FermatNo ` ( M + ( N - M ) ) ) - 2 ) )
8 1 6 7 syl2anc 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( FermatNo ` M ) || ( ( FermatNo ` ( M + ( N - M ) ) ) - 2 ) )
9 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
10 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
11 9 10 anim12ci 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( M e. CC /\ N e. CC ) )
12 11 3adant3 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( M e. CC /\ N e. CC ) )
13 pncan3 
 |-  ( ( M e. CC /\ N e. CC ) -> ( M + ( N - M ) ) = N )
14 12 13 syl 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( M + ( N - M ) ) = N )
15 14 eqcomd 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> N = ( M + ( N - M ) ) )
16 15 fveq2d 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( FermatNo ` N ) = ( FermatNo ` ( M + ( N - M ) ) ) )
17 16 oveq1d 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` N ) - 2 ) = ( ( FermatNo ` ( M + ( N - M ) ) ) - 2 ) )
18 8 17 breqtrrd 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( FermatNo ` M ) || ( ( FermatNo ` N ) - 2 ) )