Metamath Proof Explorer

Theorem flt4lem2

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

Ref Expression
Hypotheses flt4lem2.a ⊢φ→A∈ℕ
flt4lem2.b ⊢φ→B∈ℕ
flt4lem2.c ⊢φ→C∈ℕ
flt4lem2.1 ⊢φ→2∥A
flt4lem2.2 ⊢φ→AgcdC=1
flt4lem2.3 ⊢φ→A2+B2=C2
Assertion flt4lem2 ⊢φ→¬2∥B

Proof

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