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 ) )