pellexlem6

Description: Lemma for pellex . Doing a field division between near solutions get us to norm 1, and the modularity constraint ensures we still have an integer. Returning NN guarantees that we are not returning the trivial solution (1,0). We are not explicitly defining the Pell-field, Pell-ring, and Pell-norm explicitly because after this construction is done we will never use them. This is mostly basic algebraic number theory and could be simplified if a generic framework for that were in place. (Contributed by Stefan O'Rear, 19-Oct-2014)

	Ref	Expression
Hypotheses	pellex.ann	$⊢ φ \to A \in ℕ$
	pellex.bnn	$⊢ φ \to B \in ℕ$
	pellex.cz	$⊢ φ \to C \in ℤ$
	pellex.dnn	$⊢ φ \to D \in ℕ$
	pellex.irr	$⊢ φ \to \neg \sqrt{D} \in ℚ$
	pellex.enn	$⊢ φ \to E \in ℕ$
	pellex.fnn	$⊢ φ \to F \in ℕ$
	pellex.neq	$⊢ φ \to \neg (A = E \land B = F)$
	pellex.cn0	$⊢ φ \to C \neq 0$
	pellex.no1	$⊢ φ \to A^{2} - D B^{2} = C$
	pellex.no2	$⊢ φ \to E^{2} - D F^{2} = C$
	pellex.xcg	$⊢ φ \to A \mod \|C\| = E \mod \|C\|$
	pellex.ycg	$⊢ φ \to B \mod \|C\| = F \mod \|C\|$
Assertion	pellexlem6	$⊢ φ \to \exists a \in ℕ \exists b \in ℕ a^{2} - D b^{2} = 1$

Proof

Step	Hyp	Ref	Expression
1		pellex.ann	$⊢ φ \to A \in ℕ$
2		pellex.bnn	$⊢ φ \to B \in ℕ$
3		pellex.cz	$⊢ φ \to C \in ℤ$
4		pellex.dnn	$⊢ φ \to D \in ℕ$
5		pellex.irr	$⊢ φ \to \neg \sqrt{D} \in ℚ$
6		pellex.enn	$⊢ φ \to E \in ℕ$
7		pellex.fnn	$⊢ φ \to F \in ℕ$
8		pellex.neq	$⊢ φ \to \neg (A = E \land B = F)$
9		pellex.cn0	$⊢ φ \to C \neq 0$
10		pellex.no1	$⊢ φ \to A^{2} - D B^{2} = C$
11		pellex.no2	$⊢ φ \to E^{2} - D F^{2} = C$
12		pellex.xcg	$⊢ φ \to A \mod \|C\| = E \mod \|C\|$
13		pellex.ycg	$⊢ φ \to B \mod \|C\| = F \mod \|C\|$
14	1	nncnd	$⊢ φ \to A \in ℂ$
15	6	nncnd	$⊢ φ \to E \in ℂ$
16	14 15	mulcld	$⊢ φ \to A E \in ℂ$
17	4	nncnd	$⊢ φ \to D \in ℂ$
18	2	nncnd	$⊢ φ \to B \in ℂ$
19	7	nncnd	$⊢ φ \to F \in ℂ$
20	18 19	mulcld	$⊢ φ \to B F \in ℂ$
21	17 20	mulcld	$⊢ φ \to D B F \in ℂ$
22	16 21	subcld	$⊢ φ \to A E - D B F \in ℂ$
23	3	zcnd	$⊢ φ \to C \in ℂ$
24	22 23 9	absdivd	$⊢ φ \to \|\frac{A E - D B F}{C}\| = \frac{\|A E - D B F\|}{\|C\|}$
25	16 21	negsubd	$⊢ φ \to A E + (- D B F) = A E - D B F$
26	25	eqcomd	$⊢ φ \to A E - D B F = A E + (- D B F)$
27	26	oveq1d	$⊢ φ \to (A E - D B F) \mod \|C\| = (A E + (- D B F)) \mod \|C\|$
28	1	nnred	$⊢ φ \to A \in ℝ$
29	6	nnred	$⊢ φ \to E \in ℝ$
30	28 29	remulcld	$⊢ φ \to A E \in ℝ$
31	4	nnred	$⊢ φ \to D \in ℝ$
32	2	nnred	$⊢ φ \to B \in ℝ$
33	7	nnred	$⊢ φ \to F \in ℝ$
34	32 33	remulcld	$⊢ φ \to B F \in ℝ$
35	31 34	remulcld	$⊢ φ \to D B F \in ℝ$
36	35	renegcld	$⊢ φ \to - D B F \in ℝ$
37	23 9	absrpcld	$⊢ φ \to \|C\| \in ℝ^{+}$
38	6	nnzd	$⊢ φ \to E \in ℤ$
39		modmul1	$⊢ ((A \in ℝ \land E \in ℝ) \land (E \in ℤ \land \|C\| \in ℝ^{+}) \land A \mod \|C\| = E \mod \|C\|) \to A E \mod \|C\| = E E \mod \|C\|$
40	28 29 38 37 12 39	syl221anc	$⊢ φ \to A E \mod \|C\| = E E \mod \|C\|$
41	15	sqcld	$⊢ φ \to E^{2} \in ℂ$
42	19	sqcld	$⊢ φ \to F^{2} \in ℂ$
43	17 42	mulcld	$⊢ φ \to D F^{2} \in ℂ$
44	41 43	npcand	$⊢ φ \to E^{2} - D F^{2} + D F^{2} = E^{2}$
45	15	sqvald	$⊢ φ \to E^{2} = E E$
46	44 45	eqtr2d	$⊢ φ \to E E = E^{2} - D F^{2} + D F^{2}$
47	46	oveq1d	$⊢ φ \to E E \mod \|C\| = (E^{2} - D F^{2} + D F^{2}) \mod \|C\|$
48	29	resqcld	$⊢ φ \to E^{2} \in ℝ$
49	33	resqcld	$⊢ φ \to F^{2} \in ℝ$
50	31 49	remulcld	$⊢ φ \to D F^{2} \in ℝ$
51	48 50	resubcld	$⊢ φ \to E^{2} - D F^{2} \in ℝ$
52		0red	$⊢ φ \to 0 \in ℝ$
53	23	abscld	$⊢ φ \to \|C\| \in ℝ$
54	53	recnd	$⊢ φ \to \|C\| \in ℂ$
55	23 9	absne0d	$⊢ φ \to \|C\| \neq 0$
56	54 55	dividd	$⊢ φ \to \frac{\|C\|}{\|C\|} = 1$
57		1zzd	$⊢ φ \to 1 \in ℤ$
58	56 57	eqeltrd	$⊢ φ \to \frac{\|C\|}{\|C\|} \in ℤ$
59		mod0	$⊢ (\|C\| \in ℝ \land \|C\| \in ℝ^{+}) \to (\|C\| \mod \|C\| = 0 \leftrightarrow \frac{\|C\|}{\|C\|} \in ℤ)$
60	53 37 59	syl2anc	$⊢ φ \to (\|C\| \mod \|C\| = 0 \leftrightarrow \frac{\|C\|}{\|C\|} \in ℤ)$
61	58 60	mpbird	$⊢ φ \to \|C\| \mod \|C\| = 0$
62	3	zred	$⊢ φ \to C \in ℝ$
63		absmod0	$⊢ (C \in ℝ \land \|C\| \in ℝ^{+}) \to (C \mod \|C\| = 0 \leftrightarrow \|C\| \mod \|C\| = 0)$
64	62 37 63	syl2anc	$⊢ φ \to (C \mod \|C\| = 0 \leftrightarrow \|C\| \mod \|C\| = 0)$
65	61 64	mpbird	$⊢ φ \to C \mod \|C\| = 0$
66	11	oveq1d	$⊢ φ \to (E^{2} - D F^{2}) \mod \|C\| = C \mod \|C\|$
67		0mod	$⊢ \|C\| \in ℝ^{+} \to 0 \mod \|C\| = 0$
68	37 67	syl	$⊢ φ \to 0 \mod \|C\| = 0$
69	65 66 68	3eqtr4d	$⊢ φ \to (E^{2} - D F^{2}) \mod \|C\| = 0 \mod \|C\|$
70		modadd1	$⊢ ((E^{2} - D F^{2} \in ℝ \land 0 \in ℝ) \land (D F^{2} \in ℝ \land \|C\| \in ℝ^{+}) \land (E^{2} - D F^{2}) \mod \|C\| = 0 \mod \|C\|) \to (E^{2} - D F^{2} + D F^{2}) \mod \|C\| = (0 + D F^{2}) \mod \|C\|$
71	51 52 50 37 69 70	syl221anc	$⊢ φ \to (E^{2} - D F^{2} + D F^{2}) \mod \|C\| = (0 + D F^{2}) \mod \|C\|$
72	43	addid2d	$⊢ φ \to 0 + D F^{2} = D F^{2}$
73	19	sqvald	$⊢ φ \to F^{2} = F F$
74	73	oveq2d	$⊢ φ \to D F^{2} = D F F$
75	17 19 19	mul12d	$⊢ φ \to D F F = F D F$
76	72 74 75	3eqtrd	$⊢ φ \to 0 + D F^{2} = F D F$
77	76	oveq1d	$⊢ φ \to (0 + D F^{2}) \mod \|C\| = F D F \mod \|C\|$
78	47 71 77	3eqtrd	$⊢ φ \to E E \mod \|C\| = F D F \mod \|C\|$
79	4	nnzd	$⊢ φ \to D \in ℤ$
80	7	nnzd	$⊢ φ \to F \in ℤ$
81	79 80	zmulcld	$⊢ φ \to D F \in ℤ$
82	13	eqcomd	$⊢ φ \to F \mod \|C\| = B \mod \|C\|$
83		modmul1	$⊢ ((F \in ℝ \land B \in ℝ) \land (D F \in ℤ \land \|C\| \in ℝ^{+}) \land F \mod \|C\| = B \mod \|C\|) \to F D F \mod \|C\| = B D F \mod \|C\|$
84	33 32 81 37 82 83	syl221anc	$⊢ φ \to F D F \mod \|C\| = B D F \mod \|C\|$
85	18 17 19	mul12d	$⊢ φ \to B D F = D B F$
86	85	oveq1d	$⊢ φ \to B D F \mod \|C\| = D B F \mod \|C\|$
87	84 86	eqtrd	$⊢ φ \to F D F \mod \|C\| = D B F \mod \|C\|$
88	40 78 87	3eqtrd	$⊢ φ \to A E \mod \|C\| = D B F \mod \|C\|$
89		modadd1	$⊢ ((A E \in ℝ \land D B F \in ℝ) \land (- D B F \in ℝ \land \|C\| \in ℝ^{+}) \land A E \mod \|C\| = D B F \mod \|C\|) \to (A E + (- D B F)) \mod \|C\| = (D B F + (- D B F)) \mod \|C\|$
90	30 35 36 37 88 89	syl221anc	$⊢ φ \to (A E + (- D B F)) \mod \|C\| = (D B F + (- D B F)) \mod \|C\|$
91	21	negidd	$⊢ φ \to D B F + (- D B F) = 0$
92	91	oveq1d	$⊢ φ \to (D B F + (- D B F)) \mod \|C\| = 0 \mod \|C\|$
93	27 90 92	3eqtrd	$⊢ φ \to (A E - D B F) \mod \|C\| = 0 \mod \|C\|$
94	93 68	eqtrd	$⊢ φ \to (A E - D B F) \mod \|C\| = 0$
95	30 35	resubcld	$⊢ φ \to A E - D B F \in ℝ$
96		absmod0	$⊢ (A E - D B F \in ℝ \land \|C\| \in ℝ^{+}) \to ((A E - D B F) \mod \|C\| = 0 \leftrightarrow \|A E - D B F\| \mod \|C\| = 0)$
97	95 37 96	syl2anc	$⊢ φ \to ((A E - D B F) \mod \|C\| = 0 \leftrightarrow \|A E - D B F\| \mod \|C\| = 0)$
98	94 97	mpbid	$⊢ φ \to \|A E - D B F\| \mod \|C\| = 0$
99	22	abscld	$⊢ φ \to \|A E - D B F\| \in ℝ$
100		mod0	$⊢ (\|A E - D B F\| \in ℝ \land \|C\| \in ℝ^{+}) \to (\|A E - D B F\| \mod \|C\| = 0 \leftrightarrow \frac{\|A E - D B F\|}{\|C\|} \in ℤ)$
101	99 37 100	syl2anc	$⊢ φ \to (\|A E - D B F\| \mod \|C\| = 0 \leftrightarrow \frac{\|A E - D B F\|}{\|C\|} \in ℤ)$
102	98 101	mpbid	$⊢ φ \to \frac{\|A E - D B F\|}{\|C\|} \in ℤ$
103	24 102	eqeltrd	$⊢ φ \to \|\frac{A E - D B F}{C}\| \in ℤ$
104	95 62 9	redivcld	$⊢ φ \to \frac{A E - D B F}{C} \in ℝ$
105		absz	$⊢ \frac{A E - D B F}{C} \in ℝ \to (\frac{A E - D B F}{C} \in ℤ \leftrightarrow \|\frac{A E - D B F}{C}\| \in ℤ)$
106	104 105	syl	$⊢ φ \to (\frac{A E - D B F}{C} \in ℤ \leftrightarrow \|\frac{A E - D B F}{C}\| \in ℤ)$
107	103 106	mpbird	$⊢ φ \to \frac{A E - D B F}{C} \in ℤ$
108		0lt1	$⊢ 0 < 1$
109		0re	$⊢ 0 \in ℝ$
110		1re	$⊢ 1 \in ℝ$
111	109 110	ltnlei	$⊢ 0 < 1 \leftrightarrow \neg 1 \leq 0$
112	108 111	mpbi	$⊢ \neg 1 \leq 0$
113	18 15	mulcld	$⊢ φ \to B E \in ℂ$
114	14 19	mulcld	$⊢ φ \to A F \in ℂ$
115	113 114	subcld	$⊢ φ \to B E - A F \in ℂ$
116	115 23 9	divcld	$⊢ φ \to \frac{B E - A F}{C} \in ℂ$
117	116	abscld	$⊢ φ \to \|\frac{B E - A F}{C}\| \in ℝ$
118	117	resqcld	$⊢ φ \to {\|\frac{B E - A F}{C}\|}^{2} \in ℝ$
119	4	nnnn0d	$⊢ φ \to D \in ℕ_{0}$
120	119	nn0ge0d	$⊢ φ \to 0 \leq D$
121	117	sqge0d	$⊢ φ \to 0 \leq {\|\frac{B E - A F}{C}\|}^{2}$
122	31 118 120 121	mulge0d	$⊢ φ \to 0 \leq D {\|\frac{B E - A F}{C}\|}^{2}$
123	31 118	remulcld	$⊢ φ \to D {\|\frac{B E - A F}{C}\|}^{2} \in ℝ$
124	52 123	suble0d	$⊢ φ \to (0 - D {\|\frac{B E - A F}{C}\|}^{2} \leq 0 \leftrightarrow 0 \leq D {\|\frac{B E - A F}{C}\|}^{2})$
125	122 124	mpbird	$⊢ φ \to 0 - D {\|\frac{B E - A F}{C}\|}^{2} \leq 0$
126		breq1	$⊢ 1 = 0 - D {\|\frac{B E - A F}{C}\|}^{2} \to (1 \leq 0 \leftrightarrow 0 - D {\|\frac{B E - A F}{C}\|}^{2} \leq 0)$
127	125 126	syl5ibrcom	$⊢ φ \to (1 = 0 - D {\|\frac{B E - A F}{C}\|}^{2} \to 1 \leq 0)$
128	112 127	mtoi	$⊢ φ \to \neg 1 = 0 - D {\|\frac{B E - A F}{C}\|}^{2}$
129		absresq	$⊢ \frac{A E - D B F}{C} \in ℝ \to {\|\frac{A E - D B F}{C}\|}^{2} = {(\frac{A E - D B F}{C})}^{2}$
130	104 129	syl	$⊢ φ \to {\|\frac{A E - D B F}{C}\|}^{2} = {(\frac{A E - D B F}{C})}^{2}$
131	22 23 9	sqdivd	$⊢ φ \to {(\frac{A E - D B F}{C})}^{2} = \frac{{(A E - D B F)}^{2}}{C^{2}}$
132	22	sqvald	$⊢ φ \to {(A E - D B F)}^{2} = (A E - D B F) (A E - D B F)$
133	132	oveq1d	$⊢ φ \to \frac{{(A E - D B F)}^{2}}{C^{2}} = \frac{(A E - D B F) (A E - D B F)}{C^{2}}$
134	130 131 133	3eqtrd	$⊢ φ \to {\|\frac{A E - D B F}{C}\|}^{2} = \frac{(A E - D B F) (A E - D B F)}{C^{2}}$
135	32 29	remulcld	$⊢ φ \to B E \in ℝ$
136	28 33	remulcld	$⊢ φ \to A F \in ℝ$
137	135 136	resubcld	$⊢ φ \to B E - A F \in ℝ$
138	137 62 9	redivcld	$⊢ φ \to \frac{B E - A F}{C} \in ℝ$
139		absresq	$⊢ \frac{B E - A F}{C} \in ℝ \to {\|\frac{B E - A F}{C}\|}^{2} = {(\frac{B E - A F}{C})}^{2}$
140	138 139	syl	$⊢ φ \to {\|\frac{B E - A F}{C}\|}^{2} = {(\frac{B E - A F}{C})}^{2}$
141	115 23 9	sqdivd	$⊢ φ \to {(\frac{B E - A F}{C})}^{2} = \frac{{(B E - A F)}^{2}}{C^{2}}$
142	140 141	eqtrd	$⊢ φ \to {\|\frac{B E - A F}{C}\|}^{2} = \frac{{(B E - A F)}^{2}}{C^{2}}$
143	142	oveq2d	$⊢ φ \to D {\|\frac{B E - A F}{C}\|}^{2} = D (\frac{{(B E - A F)}^{2}}{C^{2}})$
144	115	sqcld	$⊢ φ \to {(B E - A F)}^{2} \in ℂ$
145	23	sqcld	$⊢ φ \to C^{2} \in ℂ$
146		sqne0	$⊢ C \in ℂ \to (C^{2} \neq 0 \leftrightarrow C \neq 0)$
147	23 146	syl	$⊢ φ \to (C^{2} \neq 0 \leftrightarrow C \neq 0)$
148	9 147	mpbird	$⊢ φ \to C^{2} \neq 0$
149	17 144 145 148	divassd	$⊢ φ \to \frac{D {(B E - A F)}^{2}}{C^{2}} = D (\frac{{(B E - A F)}^{2}}{C^{2}})$
150	115	sqvald	$⊢ φ \to {(B E - A F)}^{2} = (B E - A F) (B E - A F)$
151	150	oveq2d	$⊢ φ \to D {(B E - A F)}^{2} = D (B E - A F) (B E - A F)$
152	151	oveq1d	$⊢ φ \to \frac{D {(B E - A F)}^{2}}{C^{2}} = \frac{D (B E - A F) (B E - A F)}{C^{2}}$
153	143 149 152	3eqtr2d	$⊢ φ \to D {\|\frac{B E - A F}{C}\|}^{2} = \frac{D (B E - A F) (B E - A F)}{C^{2}}$
154	134 153	oveq12d	$⊢ φ \to {\|\frac{A E - D B F}{C}\|}^{2} - D {\|\frac{B E - A F}{C}\|}^{2} = (\frac{(A E - D B F) (A E - D B F)}{C^{2}}) - (\frac{D (B E - A F) (B E - A F)}{C^{2}})$
155	22 22	mulcld	$⊢ φ \to (A E - D B F) (A E - D B F) \in ℂ$
156	115 115	mulcld	$⊢ φ \to (B E - A F) (B E - A F) \in ℂ$
157	17 156	mulcld	$⊢ φ \to D (B E - A F) (B E - A F) \in ℂ$
158	155 157 145 148	divsubdird	$⊢ φ \to \frac{(A E - D B F) (A E - D B F) - D (B E - A F) (B E - A F)}{C^{2}} = (\frac{(A E - D B F) (A E - D B F)}{C^{2}}) - (\frac{D (B E - A F) (B E - A F)}{C^{2}})$
159	16 21 16 21	mulsubd	$⊢ φ \to (A E - D B F) (A E - D B F) = A E A E + D B F D B F - (A E D B F + A E D B F)$
160	113 114 113 114	mulsubd	$⊢ φ \to (B E - A F) (B E - A F) = B E B E + A F A F - (B E A F + B E A F)$
161	160	oveq2d	$⊢ φ \to D (B E - A F) (B E - A F) = D (B E B E + A F A F - (B E A F + B E A F))$
162	113 113	mulcld	$⊢ φ \to B E B E \in ℂ$
163	114 114	mulcld	$⊢ φ \to A F A F \in ℂ$
164	162 163	addcld	$⊢ φ \to B E B E + A F A F \in ℂ$
165	113 114	mulcld	$⊢ φ \to B E A F \in ℂ$
166	165 165	addcld	$⊢ φ \to B E A F + B E A F \in ℂ$
167	17 164 166	subdid	$⊢ φ \to D (B E B E + A F A F - (B E A F + B E A F)) = D (B E B E + A F A F) - D (B E A F + B E A F)$
168	17 162 163	adddid	$⊢ φ \to D (B E B E + A F A F) = D B E B E + D A F A F$
169	17 165 165	adddid	$⊢ φ \to D (B E A F + B E A F) = D B E A F + D B E A F$
170	168 169	oveq12d	$⊢ φ \to D (B E B E + A F A F) - D (B E A F + B E A F) = D B E B E + D A F A F - (D B E A F + D B E A F)$
171	161 167 170	3eqtrd	$⊢ φ \to D (B E - A F) (B E - A F) = D B E B E + D A F A F - (D B E A F + D B E A F)$
172	159 171	oveq12d	$⊢ φ \to (A E - D B F) (A E - D B F) - D (B E - A F) (B E - A F) = (A E A E + D B F D B F) - (A E D B F + A E D B F) - (D B E B E + D A F A F - (D B E A F + D B E A F))$
173	172	oveq1d	$⊢ φ \to \frac{(A E - D B F) (A E - D B F) - D (B E - A F) (B E - A F)}{C^{2}} = \frac{(A E A E + D B F D B F) - (A E D B F + A E D B F) - (D B E B E + D A F A F - (D B E A F + D B E A F))}{C^{2}}$
174	16 21	mulcomd	$⊢ φ \to A E D B F = D B F A E$
175	17 20 16	mulassd	$⊢ φ \to D B F A E = D B F A E$
176	14 15	mulcomd	$⊢ φ \to A E = E A$
177	176	oveq2d	$⊢ φ \to B F A E = B F E A$
178	18 19 15 14	mul4d	$⊢ φ \to B F E A = B E F A$
179	19 14	mulcomd	$⊢ φ \to F A = A F$
180	179	oveq2d	$⊢ φ \to B E F A = B E A F$
181	177 178 180	3eqtrd	$⊢ φ \to B F A E = B E A F$
182	181	oveq2d	$⊢ φ \to D B F A E = D B E A F$
183	174 175 182	3eqtrd	$⊢ φ \to A E D B F = D B E A F$
184	183 183	oveq12d	$⊢ φ \to A E D B F + A E D B F = D B E A F + D B E A F$
185	184	oveq2d	$⊢ φ \to A E A E + D B F D B F - (A E D B F + A E D B F) = A E A E + D B F D B F - (D B E A F + D B E A F)$
186	185	oveq1d	$⊢ φ \to (A E A E + D B F D B F) - (A E D B F + A E D B F) - (D B E B E + D A F A F - (D B E A F + D B E A F)) = (A E A E + D B F D B F) - (D B E A F + D B E A F) - (D B E B E + D A F A F - (D B E A F + D B E A F))$
187	16 16	mulcld	$⊢ φ \to A E A E \in ℂ$
188	21 21	mulcld	$⊢ φ \to D B F D B F \in ℂ$
189	187 188	addcld	$⊢ φ \to A E A E + D B F D B F \in ℂ$
190	17 162	mulcld	$⊢ φ \to D B E B E \in ℂ$
191	17 163	mulcld	$⊢ φ \to D A F A F \in ℂ$
192	190 191	addcld	$⊢ φ \to D B E B E + D A F A F \in ℂ$
193	17 165	mulcld	$⊢ φ \to D B E A F \in ℂ$
194	193 193	addcld	$⊢ φ \to D B E A F + D B E A F \in ℂ$
195	189 192 194	nnncan2d	$⊢ φ \to (A E A E + D B F D B F) - (D B E A F + D B E A F) - (D B E B E + D A F A F - (D B E A F + D B E A F)) = A E A E + D B F D B F - (D B E B E + D A F A F)$
196	187 188 190 191	addsub4d	$⊢ φ \to A E A E + D B F D B F - (D B E B E + D A F A F) = (A E A E - D B E B E) + D B F D B F - D A F A F$
197	16	sqvald	$⊢ φ \to {A E}^{2} = A E A E$
198	113	sqvald	$⊢ φ \to {B E}^{2} = B E B E$
199	198	oveq2d	$⊢ φ \to D {B E}^{2} = D B E B E$
200	197 199	oveq12d	$⊢ φ \to {A E}^{2} - D {B E}^{2} = A E A E - D B E B E$
201	21	sqvald	$⊢ φ \to {D B F}^{2} = D B F D B F$
202	114	sqvald	$⊢ φ \to {A F}^{2} = A F A F$
203	202	oveq2d	$⊢ φ \to D {A F}^{2} = D A F A F$
204	201 203	oveq12d	$⊢ φ \to {D B F}^{2} - D {A F}^{2} = D B F D B F - D A F A F$
205	200 204	oveq12d	$⊢ φ \to ({A E}^{2} - D {B E}^{2}) + {D B F}^{2} - D {A F}^{2} = (A E A E - D B E B E) + D B F D B F - D A F A F$
206	14 15	sqmuld	$⊢ φ \to {A E}^{2} = A^{2} E^{2}$
207	18 15	sqmuld	$⊢ φ \to {B E}^{2} = B^{2} E^{2}$
208	207	oveq2d	$⊢ φ \to D {B E}^{2} = D B^{2} E^{2}$
209	18	sqcld	$⊢ φ \to B^{2} \in ℂ$
210	17 209 41	mulassd	$⊢ φ \to D B^{2} E^{2} = D B^{2} E^{2}$
211	208 210	eqtr4d	$⊢ φ \to D {B E}^{2} = D B^{2} E^{2}$
212	206 211	oveq12d	$⊢ φ \to {A E}^{2} - D {B E}^{2} = A^{2} E^{2} - D B^{2} E^{2}$
213	17	sqvald	$⊢ φ \to D^{2} = D D$
214	18 19	sqmuld	$⊢ φ \to {B F}^{2} = B^{2} F^{2}$
215	213 214	oveq12d	$⊢ φ \to D^{2} {B F}^{2} = D D B^{2} F^{2}$
216	17 20	sqmuld	$⊢ φ \to {D B F}^{2} = D^{2} {B F}^{2}$
217	17 17	mulcld	$⊢ φ \to D D \in ℂ$
218	217 209 42	mulassd	$⊢ φ \to D D B^{2} F^{2} = D D B^{2} F^{2}$
219	215 216 218	3eqtr4d	$⊢ φ \to {D B F}^{2} = D D B^{2} F^{2}$
220	14 19	sqmuld	$⊢ φ \to {A F}^{2} = A^{2} F^{2}$
221	220	oveq2d	$⊢ φ \to D {A F}^{2} = D A^{2} F^{2}$
222	14	sqcld	$⊢ φ \to A^{2} \in ℂ$
223	17 222 42	mulassd	$⊢ φ \to D A^{2} F^{2} = D A^{2} F^{2}$
224	221 223	eqtr4d	$⊢ φ \to D {A F}^{2} = D A^{2} F^{2}$
225	219 224	oveq12d	$⊢ φ \to {D B F}^{2} - D {A F}^{2} = D D B^{2} F^{2} - D A^{2} F^{2}$
226	212 225	oveq12d	$⊢ φ \to ({A E}^{2} - D {B E}^{2}) + {D B F}^{2} - D {A F}^{2} = (A^{2} E^{2} - D B^{2} E^{2}) + D D B^{2} F^{2} - D A^{2} F^{2}$
227	17 209	mulcld	$⊢ φ \to D B^{2} \in ℂ$
228	222 227 41	subdird	$⊢ φ \to (A^{2} - D B^{2}) E^{2} = A^{2} E^{2} - D B^{2} E^{2}$
229	10	oveq1d	$⊢ φ \to (A^{2} - D B^{2}) E^{2} = C E^{2}$
230	228 229	eqtr3d	$⊢ φ \to A^{2} E^{2} - D B^{2} E^{2} = C E^{2}$
231	17 17 209	mulassd	$⊢ φ \to D D B^{2} = D D B^{2}$
232	231	oveq1d	$⊢ φ \to D D B^{2} - D A^{2} = D D B^{2} - D A^{2}$
233	232	oveq1d	$⊢ φ \to (D D B^{2} - D A^{2}) F^{2} = (D D B^{2} - D A^{2}) F^{2}$
234	217 209	mulcld	$⊢ φ \to D D B^{2} \in ℂ$
235	17 222	mulcld	$⊢ φ \to D A^{2} \in ℂ$
236	234 235 42	subdird	$⊢ φ \to (D D B^{2} - D A^{2}) F^{2} = D D B^{2} F^{2} - D A^{2} F^{2}$
237		subdi	$⊢ (D \in ℂ \land D B^{2} \in ℂ \land A^{2} \in ℂ) \to D (D B^{2} - A^{2}) = D D B^{2} - D A^{2}$
238	237	eqcomd	$⊢ (D \in ℂ \land D B^{2} \in ℂ \land A^{2} \in ℂ) \to D D B^{2} - D A^{2} = D (D B^{2} - A^{2})$
239	17 227 222 238	syl3anc	$⊢ φ \to D D B^{2} - D A^{2} = D (D B^{2} - A^{2})$
240		negsubdi2	$⊢ (A^{2} \in ℂ \land D B^{2} \in ℂ) \to - (A^{2} - D B^{2}) = D B^{2} - A^{2}$
241	240	eqcomd	$⊢ (A^{2} \in ℂ \land D B^{2} \in ℂ) \to D B^{2} - A^{2} = - (A^{2} - D B^{2})$
242	222 227 241	syl2anc	$⊢ φ \to D B^{2} - A^{2} = - (A^{2} - D B^{2})$
243	10	negeqd	$⊢ φ \to - (A^{2} - D B^{2}) = - C$
244	242 243	eqtrd	$⊢ φ \to D B^{2} - A^{2} = - C$
245	244	oveq2d	$⊢ φ \to D (D B^{2} - A^{2}) = D (- C)$
246	17 23	mulneg2d	$⊢ φ \to D (- C) = - D C$
247	239 245 246	3eqtrd	$⊢ φ \to D D B^{2} - D A^{2} = - D C$
248	247	oveq1d	$⊢ φ \to (D D B^{2} - D A^{2}) F^{2} = (- D C) F^{2}$
249	233 236 248	3eqtr3d	$⊢ φ \to D D B^{2} F^{2} - D A^{2} F^{2} = (- D C) F^{2}$
250	230 249	oveq12d	$⊢ φ \to (A^{2} E^{2} - D B^{2} E^{2}) + D D B^{2} F^{2} - D A^{2} F^{2} = C E^{2} + (- D C) F^{2}$
251	17 23	mulcld	$⊢ φ \to D C \in ℂ$
252	251 42	mulneg1d	$⊢ φ \to (- D C) F^{2} = - D C F^{2}$
253	17 23	mulcomd	$⊢ φ \to D C = C D$
254	253	oveq1d	$⊢ φ \to D C F^{2} = C D F^{2}$
255	23 17 42	mulassd	$⊢ φ \to C D F^{2} = C D F^{2}$
256	254 255	eqtrd	$⊢ φ \to D C F^{2} = C D F^{2}$
257	256	negeqd	$⊢ φ \to - D C F^{2} = - C D F^{2}$
258	252 257	eqtrd	$⊢ φ \to (- D C) F^{2} = - C D F^{2}$
259	258	oveq2d	$⊢ φ \to C E^{2} + (- D C) F^{2} = C E^{2} + (- C D F^{2})$
260	23 41	mulcld	$⊢ φ \to C E^{2} \in ℂ$
261	23 43	mulcld	$⊢ φ \to C D F^{2} \in ℂ$
262	260 261	negsubd	$⊢ φ \to C E^{2} + (- C D F^{2}) = C E^{2} - C D F^{2}$
263	11	oveq2d	$⊢ φ \to C (E^{2} - D F^{2}) = C C$
264		subdi	$⊢ (C \in ℂ \land E^{2} \in ℂ \land D F^{2} \in ℂ) \to C (E^{2} - D F^{2}) = C E^{2} - C D F^{2}$
265	264	eqcomd	$⊢ (C \in ℂ \land E^{2} \in ℂ \land D F^{2} \in ℂ) \to C E^{2} - C D F^{2} = C (E^{2} - D F^{2})$
266	23 41 43 265	syl3anc	$⊢ φ \to C E^{2} - C D F^{2} = C (E^{2} - D F^{2})$
267	23	sqvald	$⊢ φ \to C^{2} = C C$
268	263 266 267	3eqtr4d	$⊢ φ \to C E^{2} - C D F^{2} = C^{2}$
269	259 262 268	3eqtrd	$⊢ φ \to C E^{2} + (- D C) F^{2} = C^{2}$
270	226 250 269	3eqtrd	$⊢ φ \to ({A E}^{2} - D {B E}^{2}) + {D B F}^{2} - D {A F}^{2} = C^{2}$
271	196 205 270	3eqtr2d	$⊢ φ \to A E A E + D B F D B F - (D B E B E + D A F A F) = C^{2}$
272	186 195 271	3eqtrd	$⊢ φ \to (A E A E + D B F D B F) - (A E D B F + A E D B F) - (D B E B E + D A F A F - (D B E A F + D B E A F)) = C^{2}$
273	272	oveq1d	$⊢ φ \to \frac{(A E A E + D B F D B F) - (A E D B F + A E D B F) - (D B E B E + D A F A F - (D B E A F + D B E A F))}{C^{2}} = \frac{C^{2}}{C^{2}}$
274	145 148	dividd	$⊢ φ \to \frac{C^{2}}{C^{2}} = 1$
275	173 273 274	3eqtrd	$⊢ φ \to \frac{(A E - D B F) (A E - D B F) - D (B E - A F) (B E - A F)}{C^{2}} = 1$
276	154 158 275	3eqtr2d	$⊢ φ \to {\|\frac{A E - D B F}{C}\|}^{2} - D {\|\frac{B E - A F}{C}\|}^{2} = 1$
277	276	adantr	$⊢ (φ \land A E - D B F = 0) \to {\|\frac{A E - D B F}{C}\|}^{2} - D {\|\frac{B E - A F}{C}\|}^{2} = 1$
278		simpr	$⊢ (φ \land A E - D B F = 0) \to A E - D B F = 0$
279	278	fvoveq1d	$⊢ (φ \land A E - D B F = 0) \to \|\frac{A E - D B F}{C}\| = \|\frac{0}{C}\|$
280	23 9	div0d	$⊢ φ \to \frac{0}{C} = 0$
281	280	abs00bd	$⊢ φ \to \|\frac{0}{C}\| = 0$
282	281	adantr	$⊢ (φ \land A E - D B F = 0) \to \|\frac{0}{C}\| = 0$
283	279 282	eqtrd	$⊢ (φ \land A E - D B F = 0) \to \|\frac{A E - D B F}{C}\| = 0$
284	283	sq0id	$⊢ (φ \land A E - D B F = 0) \to {\|\frac{A E - D B F}{C}\|}^{2} = 0$
285	284	oveq1d	$⊢ (φ \land A E - D B F = 0) \to {\|\frac{A E - D B F}{C}\|}^{2} - D {\|\frac{B E - A F}{C}\|}^{2} = 0 - D {\|\frac{B E - A F}{C}\|}^{2}$
286	277 285	eqtr3d	$⊢ (φ \land A E - D B F = 0) \to 1 = 0 - D {\|\frac{B E - A F}{C}\|}^{2}$
287	128 286	mtand	$⊢ φ \to \neg A E - D B F = 0$
288	287	neqned	$⊢ φ \to A E - D B F \neq 0$
289	22 23 288 9	divne0d	$⊢ φ \to \frac{A E - D B F}{C} \neq 0$
290		nnabscl	$⊢ (\frac{A E - D B F}{C} \in ℤ \land \frac{A E - D B F}{C} \neq 0) \to \|\frac{A E - D B F}{C}\| \in ℕ$
291	107 289 290	syl2anc	$⊢ φ \to \|\frac{A E - D B F}{C}\| \in ℕ$
292	115 23 9	absdivd	$⊢ φ \to \|\frac{B E - A F}{C}\| = \frac{\|B E - A F\|}{\|C\|}$
293		negsub	$⊢ (B E \in ℂ \land A F \in ℂ) \to B E + (- A F) = B E - A F$
294	293	eqcomd	$⊢ (B E \in ℂ \land A F \in ℂ) \to B E - A F = B E + (- A F)$
295	113 114 294	syl2anc	$⊢ φ \to B E - A F = B E + (- A F)$
296	295	oveq1d	$⊢ φ \to (B E - A F) \mod \|C\| = (B E + (- A F)) \mod \|C\|$
297	136	renegcld	$⊢ φ \to - A F \in ℝ$
298	19 15	mulcomd	$⊢ φ \to F E = E F$
299	298	oveq1d	$⊢ φ \to F E \mod \|C\| = E F \mod \|C\|$
300		modmul1	$⊢ ((B \in ℝ \land F \in ℝ) \land (E \in ℤ \land \|C\| \in ℝ^{+}) \land B \mod \|C\| = F \mod \|C\|) \to B E \mod \|C\| = F E \mod \|C\|$
301	32 33 38 37 13 300	syl221anc	$⊢ φ \to B E \mod \|C\| = F E \mod \|C\|$
302		modmul1	$⊢ ((A \in ℝ \land E \in ℝ) \land (F \in ℤ \land \|C\| \in ℝ^{+}) \land A \mod \|C\| = E \mod \|C\|) \to A F \mod \|C\| = E F \mod \|C\|$
303	28 29 80 37 12 302	syl221anc	$⊢ φ \to A F \mod \|C\| = E F \mod \|C\|$
304	299 301 303	3eqtr4d	$⊢ φ \to B E \mod \|C\| = A F \mod \|C\|$
305		modadd1	$⊢ ((B E \in ℝ \land A F \in ℝ) \land (- A F \in ℝ \land \|C\| \in ℝ^{+}) \land B E \mod \|C\| = A F \mod \|C\|) \to (B E + (- A F)) \mod \|C\| = (A F + (- A F)) \mod \|C\|$
306	135 136 297 37 304 305	syl221anc	$⊢ φ \to (B E + (- A F)) \mod \|C\| = (A F + (- A F)) \mod \|C\|$
307	114	negidd	$⊢ φ \to A F + (- A F) = 0$
308	307	oveq1d	$⊢ φ \to (A F + (- A F)) \mod \|C\| = 0 \mod \|C\|$
309	296 306 308	3eqtrd	$⊢ φ \to (B E - A F) \mod \|C\| = 0 \mod \|C\|$
310	309 68	eqtrd	$⊢ φ \to (B E - A F) \mod \|C\| = 0$
311		absmod0	$⊢ (B E - A F \in ℝ \land \|C\| \in ℝ^{+}) \to ((B E - A F) \mod \|C\| = 0 \leftrightarrow \|B E - A F\| \mod \|C\| = 0)$
312	137 37 311	syl2anc	$⊢ φ \to ((B E - A F) \mod \|C\| = 0 \leftrightarrow \|B E - A F\| \mod \|C\| = 0)$
313	310 312	mpbid	$⊢ φ \to \|B E - A F\| \mod \|C\| = 0$
314	115	abscld	$⊢ φ \to \|B E - A F\| \in ℝ$
315		mod0	$⊢ (\|B E - A F\| \in ℝ \land \|C\| \in ℝ^{+}) \to (\|B E - A F\| \mod \|C\| = 0 \leftrightarrow \frac{\|B E - A F\|}{\|C\|} \in ℤ)$
316	314 37 315	syl2anc	$⊢ φ \to (\|B E - A F\| \mod \|C\| = 0 \leftrightarrow \frac{\|B E - A F\|}{\|C\|} \in ℤ)$
317	313 316	mpbid	$⊢ φ \to \frac{\|B E - A F\|}{\|C\|} \in ℤ$
318	292 317	eqeltrd	$⊢ φ \to \|\frac{B E - A F}{C}\| \in ℤ$
319		absz	$⊢ \frac{B E - A F}{C} \in ℝ \to (\frac{B E - A F}{C} \in ℤ \leftrightarrow \|\frac{B E - A F}{C}\| \in ℤ)$
320	138 319	syl	$⊢ φ \to (\frac{B E - A F}{C} \in ℤ \leftrightarrow \|\frac{B E - A F}{C}\| \in ℤ)$
321	318 320	mpbird	$⊢ φ \to \frac{B E - A F}{C} \in ℤ$
322	7	nnne0d	$⊢ φ \to F \neq 0$
323	6	nnne0d	$⊢ φ \to E \neq 0$
324	18 19 14 15 322 323	divmuleqd	$⊢ φ \to (\frac{B}{F} = \frac{A}{E} \leftrightarrow B E = A F)$
325	11	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to E^{2} - D F^{2} = C$
326	325	eqcomd	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to C = E^{2} - D F^{2}$
327	326	oveq2d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} C = {(\frac{B}{F})}^{2} (E^{2} - D F^{2})$
328	18 19 322	divcld	$⊢ φ \to \frac{B}{F} \in ℂ$
329	328	sqcld	$⊢ φ \to {(\frac{B}{F})}^{2} \in ℂ$
330	329	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} \in ℂ$
331	41	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to E^{2} \in ℂ$
332	43	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to D F^{2} \in ℂ$
333	330 331 332	subdid	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} (E^{2} - D F^{2}) = {(\frac{B}{F})}^{2} E^{2} - {(\frac{B}{F})}^{2} D F^{2}$
334		oveq1	$⊢ \frac{B}{F} = \frac{A}{E} \to {(\frac{B}{F})}^{2} = {(\frac{A}{E})}^{2}$
335	334	oveq1d	$⊢ \frac{B}{F} = \frac{A}{E} \to {(\frac{B}{F})}^{2} E^{2} = {(\frac{A}{E})}^{2} E^{2}$
336	335	adantl	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} E^{2} = {(\frac{A}{E})}^{2} E^{2}$
337	14	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to A \in ℂ$
338	15	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to E \in ℂ$
339	323	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to E \neq 0$
340	337 338 339	sqdivd	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{A}{E})}^{2} = \frac{A^{2}}{E^{2}}$
341	340	oveq1d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{A}{E})}^{2} E^{2} = (\frac{A^{2}}{E^{2}}) E^{2}$
342	222	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to A^{2} \in ℂ$
343		sqne0	$⊢ E \in ℂ \to (E^{2} \neq 0 \leftrightarrow E \neq 0)$
344	15 343	syl	$⊢ φ \to (E^{2} \neq 0 \leftrightarrow E \neq 0)$
345	323 344	mpbird	$⊢ φ \to E^{2} \neq 0$
346	345	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to E^{2} \neq 0$
347	342 331 346	divcan1d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to (\frac{A^{2}}{E^{2}}) E^{2} = A^{2}$
348	336 341 347	3eqtrd	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} E^{2} = A^{2}$
349	17	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to D \in ℂ$
350	42	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to F^{2} \in ℂ$
351	330 349 350	mul12d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} D F^{2} = D {(\frac{B}{F})}^{2} F^{2}$
352	18	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to B \in ℂ$
353	19	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to F \in ℂ$
354	322	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to F \neq 0$
355	352 353 354	sqdivd	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} = \frac{B^{2}}{F^{2}}$
356	355	oveq1d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} F^{2} = (\frac{B^{2}}{F^{2}}) F^{2}$
357	356	oveq2d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to D {(\frac{B}{F})}^{2} F^{2} = D (\frac{B^{2}}{F^{2}}) F^{2}$
358	209	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to B^{2} \in ℂ$
359		sqne0	$⊢ F \in ℂ \to (F^{2} \neq 0 \leftrightarrow F \neq 0)$
360	19 359	syl	$⊢ φ \to (F^{2} \neq 0 \leftrightarrow F \neq 0)$
361	322 360	mpbird	$⊢ φ \to F^{2} \neq 0$
362	361	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to F^{2} \neq 0$
363	358 350 362	divcan1d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to (\frac{B^{2}}{F^{2}}) F^{2} = B^{2}$
364	363	oveq2d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to D (\frac{B^{2}}{F^{2}}) F^{2} = D B^{2}$
365	351 357 364	3eqtrd	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} D F^{2} = D B^{2}$
366	348 365	oveq12d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} E^{2} - {(\frac{B}{F})}^{2} D F^{2} = A^{2} - D B^{2}$
367	327 333 366	3eqtrd	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} C = A^{2} - D B^{2}$
368	10	eqcomd	$⊢ φ \to C = A^{2} - D B^{2}$
369	368	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to C = A^{2} - D B^{2}$
370	367 369	oveq12d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to \frac{{(\frac{B}{F})}^{2} C}{C} = \frac{A^{2} - D B^{2}}{A^{2} - D B^{2}}$
371	23	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to C \in ℂ$
372	9	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to C \neq 0$
373	330 371 372	divcan4d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to \frac{{(\frac{B}{F})}^{2} C}{C} = {(\frac{B}{F})}^{2}$
374	10 10	oveq12d	$⊢ φ \to \frac{A^{2} - D B^{2}}{A^{2} - D B^{2}} = \frac{C}{C}$
375	23 9	dividd	$⊢ φ \to \frac{C}{C} = 1$
376	374 375	eqtrd	$⊢ φ \to \frac{A^{2} - D B^{2}}{A^{2} - D B^{2}} = 1$
377	376	adantr	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to \frac{A^{2} - D B^{2}}{A^{2} - D B^{2}} = 1$
378	370 373 377	3eqtr3d	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to {(\frac{B}{F})}^{2} = 1$
379	32 33 322	redivcld	$⊢ φ \to \frac{B}{F} \in ℝ$
380	2	nnnn0d	$⊢ φ \to B \in ℕ_{0}$
381	380	nn0ge0d	$⊢ φ \to 0 \leq B$
382	7	nngt0d	$⊢ φ \to 0 < F$
383		divge0	$⊢ ((B \in ℝ \land 0 \leq B) \land (F \in ℝ \land 0 < F)) \to 0 \leq \frac{B}{F}$
384	32 381 33 382 383	syl22anc	$⊢ φ \to 0 \leq \frac{B}{F}$
385	379 384	sqrtsqd	$⊢ φ \to \sqrt{{(\frac{B}{F})}^{2}} = \frac{B}{F}$
386	385	eqcomd	$⊢ φ \to \frac{B}{F} = \sqrt{{(\frac{B}{F})}^{2}}$
387	386	ad2antrr	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land {(\frac{B}{F})}^{2} = 1) \to \frac{B}{F} = \sqrt{{(\frac{B}{F})}^{2}}$
388		fveq2	$⊢ {(\frac{B}{F})}^{2} = 1 \to \sqrt{{(\frac{B}{F})}^{2}} = \sqrt{1}$
389	388	adantl	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land {(\frac{B}{F})}^{2} = 1) \to \sqrt{{(\frac{B}{F})}^{2}} = \sqrt{1}$
390		sqrt1	$⊢ \sqrt{1} = 1$
391	390	a1i	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land {(\frac{B}{F})}^{2} = 1) \to \sqrt{1} = 1$
392	387 389 391	3eqtrd	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land {(\frac{B}{F})}^{2} = 1) \to \frac{B}{F} = 1$
393	392	ex	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to ({(\frac{B}{F})}^{2} = 1 \to \frac{B}{F} = 1)$
394		simplr	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to \frac{B}{F} = \frac{A}{E}$
395		simpr	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to \frac{B}{F} = 1$
396	394 395	eqtr3d	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to \frac{A}{E} = 1$
397	396	oveq1d	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to (\frac{A}{E}) E = 1 E$
398	14 15 323	divcan1d	$⊢ φ \to (\frac{A}{E}) E = A$
399	398	ad2antrr	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to (\frac{A}{E}) E = A$
400	15	mulid2d	$⊢ φ \to 1 E = E$
401	400	ad2antrr	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to 1 E = E$
402	397 399 401	3eqtr3d	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to A = E$
403	395	oveq1d	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to (\frac{B}{F}) F = 1 F$
404	18 19 322	divcan1d	$⊢ φ \to (\frac{B}{F}) F = B$
405	404	ad2antrr	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to (\frac{B}{F}) F = B$
406	19	mulid2d	$⊢ φ \to 1 F = F$
407	406	ad2antrr	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to 1 F = F$
408	403 405 407	3eqtr3d	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to B = F$
409	402 408	jca	$⊢ ((φ \land \frac{B}{F} = \frac{A}{E}) \land \frac{B}{F} = 1) \to (A = E \land B = F)$
410	409	ex	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to (\frac{B}{F} = 1 \to (A = E \land B = F))$
411	393 410	syld	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to ({(\frac{B}{F})}^{2} = 1 \to (A = E \land B = F))$
412	378 411	mpd	$⊢ (φ \land \frac{B}{F} = \frac{A}{E}) \to (A = E \land B = F)$
413	412	ex	$⊢ φ \to (\frac{B}{F} = \frac{A}{E} \to (A = E \land B = F))$
414	324 413	sylbird	$⊢ φ \to (B E = A F \to (A = E \land B = F))$
415	8 414	mtod	$⊢ φ \to \neg B E = A F$
416	415	neqned	$⊢ φ \to B E \neq A F$
417	113 114 416	subne0d	$⊢ φ \to B E - A F \neq 0$
418	115 23 417 9	divne0d	$⊢ φ \to \frac{B E - A F}{C} \neq 0$
419		nnabscl	$⊢ (\frac{B E - A F}{C} \in ℤ \land \frac{B E - A F}{C} \neq 0) \to \|\frac{B E - A F}{C}\| \in ℕ$
420	321 418 419	syl2anc	$⊢ φ \to \|\frac{B E - A F}{C}\| \in ℕ$
421		oveq1	$⊢ a = \|\frac{A E - D B F}{C}\| \to a^{2} = {\|\frac{A E - D B F}{C}\|}^{2}$
422	421	oveq1d	$⊢ a = \|\frac{A E - D B F}{C}\| \to a^{2} - D b^{2} = {\|\frac{A E - D B F}{C}\|}^{2} - D b^{2}$
423	422	eqeq1d	$⊢ a = \|\frac{A E - D B F}{C}\| \to (a^{2} - D b^{2} = 1 \leftrightarrow {\|\frac{A E - D B F}{C}\|}^{2} - D b^{2} = 1)$
424		oveq1	$⊢ b = \|\frac{B E - A F}{C}\| \to b^{2} = {\|\frac{B E - A F}{C}\|}^{2}$
425	424	oveq2d	$⊢ b = \|\frac{B E - A F}{C}\| \to D b^{2} = D {\|\frac{B E - A F}{C}\|}^{2}$
426	425	oveq2d	$⊢ b = \|\frac{B E - A F}{C}\| \to {\|\frac{A E - D B F}{C}\|}^{2} - D b^{2} = {\|\frac{A E - D B F}{C}\|}^{2} - D {\|\frac{B E - A F}{C}\|}^{2}$
427	426	eqeq1d	$⊢ b = \|\frac{B E - A F}{C}\| \to ({\|\frac{A E - D B F}{C}\|}^{2} - D b^{2} = 1 \leftrightarrow {\|\frac{A E - D B F}{C}\|}^{2} - D {\|\frac{B E - A F}{C}\|}^{2} = 1)$
428	423 427	rspc2ev	$⊢ (\|\frac{A E - D B F}{C}\| \in ℕ \land \|\frac{B E - A F}{C}\| \in ℕ \land {\|\frac{A E - D B F}{C}\|}^{2} - D {\|\frac{B E - A F}{C}\|}^{2} = 1) \to \exists a \in ℕ \exists b \in ℕ a^{2} - D b^{2} = 1$
429	291 420 276 428	syl3anc	$⊢ φ \to \exists a \in ℕ \exists b \in ℕ a^{2} - D b^{2} = 1$

Metamath Proof Explorer

Theorem pellexlem6

Proof