flt4lem6

Description: Remove shared factors in a solution to A ^ 4 + B ^ 4 = C ^ 2 . (Contributed by SN, 24-Jul-2024)

	Ref	Expression
Hypotheses	flt4lem6.a	$⊢ φ \to A \in ℕ$
	flt4lem6.b	$⊢ φ \to B \in ℕ$
	flt4lem6.c	$⊢ φ \to C \in ℕ$
	flt4lem6.1	$⊢ φ \to A^{4} + B^{4} = C^{2}$
Assertion	flt4lem6	$⊢ φ \to ((\frac{A}{A \gcd B} \in ℕ \land \frac{B}{A \gcd B} \in ℕ \land \frac{C}{{(A \gcd B)}^{2}} \in ℕ) \land {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} = {(\frac{C}{{(A \gcd B)}^{2}})}^{2})$

Proof

Step	Hyp	Ref	Expression
1		flt4lem6.a	$⊢ φ \to A \in ℕ$
2		flt4lem6.b	$⊢ φ \to B \in ℕ$
3		flt4lem6.c	$⊢ φ \to C \in ℕ$
4		flt4lem6.1	$⊢ φ \to A^{4} + B^{4} = C^{2}$
5	2	nnzd	$⊢ φ \to B \in ℤ$
6		divgcdnn	$⊢ (A \in ℕ \land B \in ℤ) \to \frac{A}{A \gcd B} \in ℕ$
7	1 5 6	syl2anc	$⊢ φ \to \frac{A}{A \gcd B} \in ℕ$
8	1	nnzd	$⊢ φ \to A \in ℤ$
9		divgcdnnr	$⊢ (B \in ℕ \land A \in ℤ) \to \frac{B}{A \gcd B} \in ℕ$
10	2 8 9	syl2anc	$⊢ φ \to \frac{B}{A \gcd B} \in ℕ$
11		gcdnncl	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℕ$
12	1 2 11	syl2anc	$⊢ φ \to A \gcd B \in ℕ$
13	12	nncnd	$⊢ φ \to A \gcd B \in ℂ$
14	13	flt4lem	$⊢ φ \to {(A \gcd B)}^{4} = {({(A \gcd B)}^{2})}^{2}$
15	4 14	oveq12d	$⊢ φ \to \frac{A^{4} + B^{4}}{{(A \gcd B)}^{4}} = \frac{C^{2}}{{({(A \gcd B)}^{2})}^{2}}$
16	1	nncnd	$⊢ φ \to A \in ℂ$
17	12	nnne0d	$⊢ φ \to A \gcd B \neq 0$
18		4nn0	$⊢ 4 \in ℕ_{0}$
19	18	a1i	$⊢ φ \to 4 \in ℕ_{0}$
20	16 13 17 19	expdivd	$⊢ φ \to {(\frac{A}{A \gcd B})}^{4} = \frac{A^{4}}{{(A \gcd B)}^{4}}$
21	2	nncnd	$⊢ φ \to B \in ℂ$
22	21 13 17 19	expdivd	$⊢ φ \to {(\frac{B}{A \gcd B})}^{4} = \frac{B^{4}}{{(A \gcd B)}^{4}}$
23	20 22	oveq12d	$⊢ φ \to {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} = (\frac{A^{4}}{{(A \gcd B)}^{4}}) + (\frac{B^{4}}{{(A \gcd B)}^{4}})$
24	16 19	expcld	$⊢ φ \to A^{4} \in ℂ$
25	21 19	expcld	$⊢ φ \to B^{4} \in ℂ$
26	13 19	expcld	$⊢ φ \to {(A \gcd B)}^{4} \in ℂ$
27	12 19	nnexpcld	$⊢ φ \to {(A \gcd B)}^{4} \in ℕ$
28	27	nnne0d	$⊢ φ \to {(A \gcd B)}^{4} \neq 0$
29	24 25 26 28	divdird	$⊢ φ \to \frac{A^{4} + B^{4}}{{(A \gcd B)}^{4}} = (\frac{A^{4}}{{(A \gcd B)}^{4}}) + (\frac{B^{4}}{{(A \gcd B)}^{4}})$
30	23 29	eqtr4d	$⊢ φ \to {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} = \frac{A^{4} + B^{4}}{{(A \gcd B)}^{4}}$
31	3	nncnd	$⊢ φ \to C \in ℂ$
32	12	nnsqcld	$⊢ φ \to {(A \gcd B)}^{2} \in ℕ$
33	32	nncnd	$⊢ φ \to {(A \gcd B)}^{2} \in ℂ$
34	32	nnne0d	$⊢ φ \to {(A \gcd B)}^{2} \neq 0$
35	31 33 34	sqdivd	$⊢ φ \to {(\frac{C}{{(A \gcd B)}^{2}})}^{2} = \frac{C^{2}}{{({(A \gcd B)}^{2})}^{2}}$
36	15 30 35	3eqtr4d	$⊢ φ \to {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} = {(\frac{C}{{(A \gcd B)}^{2}})}^{2}$
37	7 19	nnexpcld	$⊢ φ \to {(\frac{A}{A \gcd B})}^{4} \in ℕ$
38	10 19	nnexpcld	$⊢ φ \to {(\frac{B}{A \gcd B})}^{4} \in ℕ$
39	37 38	nnaddcld	$⊢ φ \to {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} \in ℕ$
40	39	nnzd	$⊢ φ \to {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} \in ℤ$
41	36 40	eqeltrrd	$⊢ φ \to {(\frac{C}{{(A \gcd B)}^{2}})}^{2} \in ℤ$
42	3	nnzd	$⊢ φ \to C \in ℤ$
43		znq	$⊢ (C \in ℤ \land {(A \gcd B)}^{2} \in ℕ) \to \frac{C}{{(A \gcd B)}^{2}} \in ℚ$
44	42 32 43	syl2anc	$⊢ φ \to \frac{C}{{(A \gcd B)}^{2}} \in ℚ$
45	3	nnred	$⊢ φ \to C \in ℝ$
46	32	nnred	$⊢ φ \to {(A \gcd B)}^{2} \in ℝ$
47	3	nngt0d	$⊢ φ \to 0 < C$
48	32	nngt0d	$⊢ φ \to 0 < {(A \gcd B)}^{2}$
49	45 46 47 48	divgt0d	$⊢ φ \to 0 < \frac{C}{{(A \gcd B)}^{2}}$
50	41 44 49	posqsqznn	$⊢ φ \to \frac{C}{{(A \gcd B)}^{2}} \in ℕ$
51	7 10 50	3jca	$⊢ φ \to (\frac{A}{A \gcd B} \in ℕ \land \frac{B}{A \gcd B} \in ℕ \land \frac{C}{{(A \gcd B)}^{2}} \in ℕ)$
52	51 36	jca	$⊢ φ \to ((\frac{A}{A \gcd B} \in ℕ \land \frac{B}{A \gcd B} \in ℕ \land \frac{C}{{(A \gcd B)}^{2}} \in ℕ) \land {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} = {(\frac{C}{{(A \gcd B)}^{2}})}^{2})$

Metamath Proof Explorer

Theorem flt4lem6

Proof