Metamath Proof Explorer


Theorem itscnhlinecirc02plem1

Description: Lemma 1 for itscnhlinecirc02p . (Contributed by AV, 6-Mar-2023)

Ref Expression
Hypotheses 2itscp.a φ A
2itscp.b φ B
2itscp.x φ X
2itscp.y φ Y
2itscp.d D = X A
2itscp.e E = B Y
2itscp.c C = D B + E A
2itscp.r φ R
2itscp.l φ A 2 + B 2 < R 2
itscnhlinecirc02plem1.n φ B Y
Assertion itscnhlinecirc02plem1 φ 0 < 2 D C 2 4 E 2 + D 2 C 2 E 2 R 2

Proof

Step Hyp Ref Expression
1 2itscp.a φ A
2 2itscp.b φ B
3 2itscp.x φ X
4 2itscp.y φ Y
5 2itscp.d D = X A
6 2itscp.e E = B Y
7 2itscp.c C = D B + E A
8 2itscp.r φ R
9 2itscp.l φ A 2 + B 2 < R 2
10 itscnhlinecirc02plem1.n φ B Y
11 4re 4
12 11 a1i φ 4
13 3 1 resubcld φ X A
14 5 13 eqeltrid φ D
15 14 resqcld φ D 2
16 14 2 remulcld φ D B
17 2 4 resubcld φ B Y
18 6 17 eqeltrid φ E
19 18 1 remulcld φ E A
20 16 19 readdcld φ D B + E A
21 7 20 eqeltrid φ C
22 21 resqcld φ C 2
23 15 22 remulcld φ D 2 C 2
24 18 resqcld φ E 2
25 24 15 readdcld φ E 2 + D 2
26 8 resqcld φ R 2
27 24 26 remulcld φ E 2 R 2
28 22 27 resubcld φ C 2 E 2 R 2
29 25 28 remulcld φ E 2 + D 2 C 2 E 2 R 2
30 23 29 resubcld φ D 2 C 2 E 2 + D 2 C 2 E 2 R 2
31 4pos 0 < 4
32 31 a1i φ 0 < 4
33 15 26 remulcld φ D 2 R 2
34 27 33 readdcld φ E 2 R 2 + D 2 R 2
35 34 22 resubcld φ E 2 R 2 + D 2 R 2 - C 2
36 6 a1i φ E = B Y
37 2 recnd φ B
38 4 recnd φ Y
39 37 38 10 subne0d φ B Y 0
40 36 39 eqnetrd φ E 0
41 18 40 sqgt0d φ 0 < E 2
42 10 orcd φ B Y A X
43 eqid E 2 + D 2 = E 2 + D 2
44 eqid R 2 E 2 + D 2 C 2 = R 2 E 2 + D 2 C 2
45 1 2 3 4 5 6 7 8 9 42 43 44 2itscp φ 0 < R 2 E 2 + D 2 C 2
46 24 recnd φ E 2
47 15 recnd φ D 2
48 26 recnd φ R 2
49 46 47 48 adddird φ E 2 + D 2 R 2 = E 2 R 2 + D 2 R 2
50 46 47 addcld φ E 2 + D 2
51 50 48 mulcomd φ E 2 + D 2 R 2 = R 2 E 2 + D 2
52 49 51 eqtr3d φ E 2 R 2 + D 2 R 2 = R 2 E 2 + D 2
53 52 oveq1d φ E 2 R 2 + D 2 R 2 - C 2 = R 2 E 2 + D 2 C 2
54 45 53 breqtrrd φ 0 < E 2 R 2 + D 2 R 2 - C 2
55 24 35 41 54 mulgt0d φ 0 < E 2 E 2 R 2 + D 2 R 2 - C 2
56 47 46 48 mul12d φ D 2 E 2 R 2 = E 2 D 2 R 2
57 56 oveq2d φ E 2 E 2 R 2 + D 2 E 2 R 2 = E 2 E 2 R 2 + E 2 D 2 R 2
58 46 48 mulcld φ E 2 R 2
59 47 48 mulcld φ D 2 R 2
60 46 58 59 adddid φ E 2 E 2 R 2 + D 2 R 2 = E 2 E 2 R 2 + E 2 D 2 R 2
61 57 60 eqtr4d φ E 2 E 2 R 2 + D 2 E 2 R 2 = E 2 E 2 R 2 + D 2 R 2
62 61 oveq1d φ E 2 E 2 R 2 + D 2 E 2 R 2 - E 2 C 2 = E 2 E 2 R 2 + D 2 R 2 E 2 C 2
63 58 59 addcld φ E 2 R 2 + D 2 R 2
64 22 recnd φ C 2
65 46 63 64 subdid φ E 2 E 2 R 2 + D 2 R 2 - C 2 = E 2 E 2 R 2 + D 2 R 2 E 2 C 2
66 62 65 eqtr4d φ E 2 E 2 R 2 + D 2 E 2 R 2 - E 2 C 2 = E 2 E 2 R 2 + D 2 R 2 - C 2
67 55 66 breqtrrd φ 0 < E 2 E 2 R 2 + D 2 E 2 R 2 - E 2 C 2
68 18 recnd φ E
69 68 sqcld φ E 2
70 14 recnd φ D
71 70 sqcld φ D 2
72 27 recnd φ E 2 R 2
73 mulsubaddmulsub E 2 D 2 C 2 E 2 R 2 D 2 C 2 E 2 + D 2 C 2 E 2 R 2 = E 2 E 2 R 2 + D 2 E 2 R 2 - E 2 C 2
74 69 71 64 72 73 syl22anc φ D 2 C 2 E 2 + D 2 C 2 E 2 R 2 = E 2 E 2 R 2 + D 2 E 2 R 2 - E 2 C 2
75 67 74 breqtrrd φ 0 < D 2 C 2 E 2 + D 2 C 2 E 2 R 2
76 12 30 32 75 mulgt0d φ 0 < 4 D 2 C 2 E 2 + D 2 C 2 E 2 R 2
77 4cn 4
78 77 a1i φ 4
79 21 recnd φ C
80 79 sqcld φ C 2
81 71 80 mulcld φ D 2 C 2
82 69 71 addcld φ E 2 + D 2
83 8 recnd φ R
84 83 sqcld φ R 2
85 69 84 mulcld φ E 2 R 2
86 80 85 subcld φ C 2 E 2 R 2
87 82 86 mulcld φ E 2 + D 2 C 2 E 2 R 2
88 78 81 87 subdid φ 4 D 2 C 2 E 2 + D 2 C 2 E 2 R 2 = 4 D 2 C 2 4 E 2 + D 2 C 2 E 2 R 2
89 76 88 breqtrd φ 0 < 4 D 2 C 2 4 E 2 + D 2 C 2 E 2 R 2
90 2cnd φ 2
91 70 79 mulcld φ D C
92 90 91 mulcld φ 2 D C
93 sqneg 2 D C 2 D C 2 = 2 D C 2
94 92 93 syl φ 2 D C 2 = 2 D C 2
95 90 91 sqmuld φ 2 D C 2 = 2 2 D C 2
96 sq2 2 2 = 4
97 96 a1i φ 2 2 = 4
98 70 79 sqmuld φ D C 2 = D 2 C 2
99 97 98 oveq12d φ 2 2 D C 2 = 4 D 2 C 2
100 94 95 99 3eqtrd φ 2 D C 2 = 4 D 2 C 2
101 100 oveq1d φ 2 D C 2 4 E 2 + D 2 C 2 E 2 R 2 = 4 D 2 C 2 4 E 2 + D 2 C 2 E 2 R 2
102 89 101 breqtrrd φ 0 < 2 D C 2 4 E 2 + D 2 C 2 E 2 R 2