Theorem flt4lem2

Description: If A is even, B is odd. (Contributed by SN, 22-Aug-2024)

	Ref	Expression
Hypotheses	flt4lem2.a	|- ( ph -> A e. NN )
	flt4lem2.b	|- ( ph -> B e. NN )
	flt4lem2.1	|- ( ph -> 2 || A )
	flt4lem2.2	|- ( ph -> ( A gcd B ) = 1 )
Assertion	flt4lem2	|- ( ph -> -. 2 || B )

Proof

Step	Hyp	Ref	Expression
1		flt4lem2.a	|- ( ph -> A e. NN )
2		flt4lem2.b	|- ( ph -> B e. NN )
3		flt4lem2.1	|- ( ph -> 2 || A )
4		flt4lem2.2	|- ( ph -> ( A gcd B ) = 1 )
5		breq1	|- ( i = 2 -> ( i || A <-> 2 || A ) )
6		breq1	|- ( i = 2 -> ( i || B <-> 2 || B ) )
7	5 6	anbi12d	|- ( i = 2 -> ( ( i || A /\ i || B ) <-> ( 2 || A /\ 2 || B ) ) )
8		2prm	|- 2 e. Prime
9	8	a1i	|- ( ( ph /\ 2 || B ) -> 2 e. Prime )
10	3	anim1i	|- ( ( ph /\ 2 || B ) -> ( 2 || A /\ 2 || B ) )
11	7 9 10	rspcedvdw	|- ( ( ph /\ 2 || B ) -> E. i e. Prime ( i || A /\ i || B ) )
12	1	adantr	|- ( ( ph /\ 2 || B ) -> A e. NN )
13	2	adantr	|- ( ( ph /\ 2 || B ) -> B e. NN )
14	12 13	prmdvdsncoprmbd	|- ( ( ph /\ 2 || B ) -> ( E. i e. Prime ( i || A /\ i || B ) <-> ( A gcd B ) =/= 1 ) )
15	11 14	mpbid	|- ( ( ph /\ 2 || B ) -> ( A gcd B ) =/= 1 )
16	15	ex	|- ( ph -> ( 2 || B -> ( A gcd B ) =/= 1 ) )
17	16	necon2bd	|- ( ph -> ( ( A gcd B ) = 1 -> -. 2 || B ) )
18	4 17	mpd	|- ( ph -> -. 2 || B )