Theorem flt4lem2

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

	Ref	Expression
Hypotheses	flt4lem2.a	$$⊢\phi \to A\in \mathbb{N}$$
	flt4lem2.b	$$⊢\phi \to B\in \mathbb{N}$$
	flt4lem2.1	$$⊢\phi \to 2\parallel A$$
	flt4lem2.2	$$⊢\phi \to A\gcd B=1$$
Assertion	flt4lem2	$$⊢\phi \to \neg 2\parallel B$$

Proof

Step	Hyp	Ref	Expression
1		flt4lem2.a	$$⊢\phi \to A\in \mathbb{N}$$
2		flt4lem2.b	$$⊢\phi \to B\in \mathbb{N}$$
3		flt4lem2.1	$$⊢\phi \to 2\parallel A$$
4		flt4lem2.2	$$⊢\phi \to A\gcd B=1$$
5		breq1	$$⊢i=2\to \left(i\parallel A\leftrightarrow 2\parallel A\right)$$
6		breq1	$$⊢i=2\to \left(i\parallel B\leftrightarrow 2\parallel B\right)$$
7	5 6	anbi12d	$$⊢i=2\to \left(\left(i\parallel A\wedge i\parallel B\right)\leftrightarrow \left(2\parallel A\wedge 2\parallel B\right)\right)$$
8		2prm	$$⊢2\in \mathbb{P}$$
9	8	a1i	$$⊢\left(\phi \wedge 2\parallel B\right)\to 2\in \mathbb{P}$$
10	3	anim1i	$$⊢\left(\phi \wedge 2\parallel B\right)\to \left(2\parallel A\wedge 2\parallel B\right)$$
11	7 9 10	rspcedvdw	$$⊢\left(\phi \wedge 2\parallel B\right)\to \exists i\in \mathbb{P}\left(i\parallel A\wedge i\parallel B\right)$$
12	1	adantr	$$⊢\left(\phi \wedge 2\parallel B\right)\to A\in \mathbb{N}$$
13	2	adantr	$$⊢\left(\phi \wedge 2\parallel B\right)\to B\in \mathbb{N}$$
14	12 13	prmdvdsncoprmbd	$$⊢\left(\phi \wedge 2\parallel B\right)\to \left(\exists i\in \mathbb{P}\left(i\parallel A\wedge i\parallel B\right)\leftrightarrow A\gcd B\ne 1\right)$$
15	11 14	mpbid	$$⊢\left(\phi \wedge 2\parallel B\right)\to A\gcd B\ne 1$$
16	15	ex	$$⊢\phi \to \left(2\parallel B\to A\gcd B\ne 1\right)$$
17	16	necon2bd	$$⊢\phi \to \left(A\gcd B=1\to \neg 2\parallel B\right)$$
18	4 17	mpd	$$⊢\phi \to \neg 2\parallel B$$