Theorem flt4lem2

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

	Ref	Expression
Hypotheses	flt4lem2.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	flt4lem2.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	flt4lem2.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	flt4lem2.1	⊢ ( 𝜑 → 2 ∥ 𝐴 )
	flt4lem2.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
	flt4lem2.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
Assertion	flt4lem2	⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		flt4lem2.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2		flt4lem2.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		flt4lem2.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4		flt4lem2.1	⊢ ( 𝜑 → 2 ∥ 𝐴 )
5		flt4lem2.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
6		flt4lem2.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
7		breq1	⊢ ( 𝑖 = 2 → ( 𝑖 ∥ 𝐴 ↔ 2 ∥ 𝐴 ) )
8		breq1	⊢ ( 𝑖 = 2 → ( 𝑖 ∥ 𝐶 ↔ 2 ∥ 𝐶 ) )
9	7 8	anbi12d	⊢ ( 𝑖 = 2 → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ↔ ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐶 ) ) )
10		2z	⊢ 2 ∈ ℤ
11		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
12	10 11	ax-mp	⊢ 2 ∈ ( ℤ≥ ‘ 2 )
13	12	a1i	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∈ ( ℤ≥ ‘ 2 ) )
14	4	adantr	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∥ 𝐴 )
15	10	a1i	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∈ ℤ )
16		gcdnncl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
17	1 2 16	syl2anc	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
18	17	nnzd	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
20	3	adantr	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐶 ∈ ℕ )
21	20	nnzd	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐶 ∈ ℤ )
22		simpr	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∥ 𝐵 )
23	1	adantr	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐴 ∈ ℕ )
24	23	nnzd	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐴 ∈ ℤ )
25	2	nnzd	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
26	25	adantr	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 𝐵 ∈ ℤ )
27		dvdsgcd	⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 gcd 𝐵 ) ) )
28	15 24 26 27	syl3anc	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 gcd 𝐵 ) ) )
29	14 22 28	mp2and	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∥ ( 𝐴 gcd 𝐵 ) )
30		2nn	⊢ 2 ∈ ℕ
31	30	a1i	⊢ ( 𝜑 → 2 ∈ ℕ )
32	1 2 3 31 6	fltdvdsabdvdsc	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∥ 𝐶 )
33	32	adantr	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐶 )
34	15 19 21 29 33	dvdstrd	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → 2 ∥ 𝐶 )
35	14 34	jca	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 2 ∥ 𝐴 ∧ 2 ∥ 𝐶 ) )
36	9 13 35	rspcedvdw	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) )
37		ncoprmgcdne1b	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ↔ ( 𝐴 gcd 𝐶 ) ≠ 1 ) )
38	23 20 37	syl2anc	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶 ) ↔ ( 𝐴 gcd 𝐶 ) ≠ 1 ) )
39	36 38	mpbid	⊢ ( ( 𝜑 ∧ 2 ∥ 𝐵 ) → ( 𝐴 gcd 𝐶 ) ≠ 1 )
40	39	ex	⊢ ( 𝜑 → ( 2 ∥ 𝐵 → ( 𝐴 gcd 𝐶 ) ≠ 1 ) )
41	40	necon2bd	⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐶 ) = 1 → ¬ 2 ∥ 𝐵 ) )
42	5 41	mpd	⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )