Proof of Theorem 4sqlem15
Step | Hyp | Ref
| Expression |
1 | | 4sq.m |
. . . . . . . . . . . . 13
|
2 | | eluz2nn 11726 |
. . . . . . . . . . . . 13
|
3 | 1, 2 | syl 17 |
. . . . . . . . . . . 12
|
4 | 3 | nnred 11035 |
. . . . . . . . . . 11
|
5 | 4 | resqcld 13035 |
. . . . . . . . . 10
|
6 | 5 | rehalfcld 11279 |
. . . . . . . . 9
|
7 | 6 | rehalfcld 11279 |
. . . . . . . 8
|
8 | 7 | recnd 10068 |
. . . . . . 7
|
9 | | 4sq.a |
. . . . . . . . . . . 12
|
10 | | 4sq.e |
. . . . . . . . . . . 12
|
11 | 9, 3, 10 | 4sqlem5 15646 |
. . . . . . . . . . 11
|
12 | 11 | simpld 475 |
. . . . . . . . . 10
|
13 | | zsqcl 12934 |
. . . . . . . . . 10
|
14 | 12, 13 | syl 17 |
. . . . . . . . 9
|
15 | 14 | zred 11482 |
. . . . . . . 8
|
16 | 15 | recnd 10068 |
. . . . . . 7
|
17 | | 4sq.b |
. . . . . . . . . . . 12
|
18 | | 4sq.f |
. . . . . . . . . . . 12
|
19 | 17, 3, 18 | 4sqlem5 15646 |
. . . . . . . . . . 11
|
20 | 19 | simpld 475 |
. . . . . . . . . 10
|
21 | | zsqcl 12934 |
. . . . . . . . . 10
|
22 | 20, 21 | syl 17 |
. . . . . . . . 9
|
23 | 22 | zred 11482 |
. . . . . . . 8
|
24 | 23 | recnd 10068 |
. . . . . . 7
|
25 | 8, 8, 16, 24 | addsub4d 10439 |
. . . . . 6
|
26 | 6 | recnd 10068 |
. . . . . . . 8
|
27 | 26 | 2halvesd 11278 |
. . . . . . 7
|
28 | 27 | oveq1d 6665 |
. . . . . 6
|
29 | 25, 28 | eqtr3d 2658 |
. . . . 5
|
30 | 29 | adantr 481 |
. . . 4
|
31 | 5 | recnd 10068 |
. . . . . . . . . 10
|
32 | 31 | 2halvesd 11278 |
. . . . . . . . 9
|
33 | 32 | adantr 481 |
. . . . . . . 8
|
34 | 4 | recnd 10068 |
. . . . . . . . . . 11
|
35 | 34 | sqvald 13005 |
. . . . . . . . . 10
|
36 | 35 | adantr 481 |
. . . . . . . . 9
|
37 | | 4sq.r |
. . . . . . . . . . 11
|
38 | | simpr 477 |
. . . . . . . . . . 11
|
39 | 37, 38 | syl5eqr 2670 |
. . . . . . . . . 10
|
40 | 39 | oveq1d 6665 |
. . . . . . . . 9
|
41 | 15, 23 | readdcld 10069 |
. . . . . . . . . . . . 13
|
42 | | 4sq.c |
. . . . . . . . . . . . . . . . . 18
|
43 | | 4sq.g |
. . . . . . . . . . . . . . . . . 18
|
44 | 42, 3, 43 | 4sqlem5 15646 |
. . . . . . . . . . . . . . . . 17
|
45 | 44 | simpld 475 |
. . . . . . . . . . . . . . . 16
|
46 | | zsqcl 12934 |
. . . . . . . . . . . . . . . 16
|
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . 15
|
48 | 47 | zred 11482 |
. . . . . . . . . . . . . 14
|
49 | | 4sq.d |
. . . . . . . . . . . . . . . . . 18
|
50 | | 4sq.h |
. . . . . . . . . . . . . . . . . 18
|
51 | 49, 3, 50 | 4sqlem5 15646 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | simpld 475 |
. . . . . . . . . . . . . . . 16
|
53 | | zsqcl 12934 |
. . . . . . . . . . . . . . . 16
|
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . 15
|
55 | 54 | zred 11482 |
. . . . . . . . . . . . . 14
|
56 | 48, 55 | readdcld 10069 |
. . . . . . . . . . . . 13
|
57 | 41, 56 | readdcld 10069 |
. . . . . . . . . . . 12
|
58 | 57 | recnd 10068 |
. . . . . . . . . . 11
|
59 | 3 | nnne0d 11065 |
. . . . . . . . . . 11
|
60 | 58, 34, 59 | divcan1d 10802 |
. . . . . . . . . 10
|
61 | 60 | adantr 481 |
. . . . . . . . 9
|
62 | 36, 40, 61 | 3eqtr2rd 2663 |
. . . . . . . 8
|
63 | 33, 62 | oveq12d 6668 |
. . . . . . 7
|
64 | 41 | recnd 10068 |
. . . . . . . . 9
|
65 | 56 | recnd 10068 |
. . . . . . . . 9
|
66 | 26, 26, 64, 65 | addsub4d 10439 |
. . . . . . . 8
|
67 | 66 | adantr 481 |
. . . . . . 7
|
68 | 31 | subidd 10380 |
. . . . . . . 8
|
69 | 68 | adantr 481 |
. . . . . . 7
|
70 | 63, 67, 69 | 3eqtr3d 2664 |
. . . . . 6
|
71 | 6, 41 | resubcld 10458 |
. . . . . . . 8
|
72 | 9, 3, 10 | 4sqlem7 15648 |
. . . . . . . . . . 11
|
73 | 17, 3, 18 | 4sqlem7 15648 |
. . . . . . . . . . 11
|
74 | 15, 23, 7, 7, 72, 73 | le2addd 10646 |
. . . . . . . . . 10
|
75 | 74, 27 | breqtrd 4679 |
. . . . . . . . 9
|
76 | 6, 41 | subge0d 10617 |
. . . . . . . . 9
|
77 | 75, 76 | mpbird 247 |
. . . . . . . 8
|
78 | 6, 56 | resubcld 10458 |
. . . . . . . 8
|
79 | 42, 3, 43 | 4sqlem7 15648 |
. . . . . . . . . . 11
|
80 | 49, 3, 50 | 4sqlem7 15648 |
. . . . . . . . . . 11
|
81 | 48, 55, 7, 7, 79, 80 | le2addd 10646 |
. . . . . . . . . 10
|
82 | 81, 27 | breqtrd 4679 |
. . . . . . . . 9
|
83 | 6, 56 | subge0d 10617 |
. . . . . . . . 9
|
84 | 82, 83 | mpbird 247 |
. . . . . . . 8
|
85 | | add20 10540 |
. . . . . . . 8
|
86 | 71, 77, 78, 84, 85 | syl22anc 1327 |
. . . . . . 7
|
87 | 86 | biimpa 501 |
. . . . . 6
|
88 | 70, 87 | syldan 487 |
. . . . 5
|
89 | 88 | simpld 475 |
. . . 4
|
90 | 30, 89 | eqtrd 2656 |
. . 3
|
91 | 7, 15 | resubcld 10458 |
. . . . 5
|
92 | 7, 15 | subge0d 10617 |
. . . . . 6
|
93 | 72, 92 | mpbird 247 |
. . . . 5
|
94 | 7, 23 | resubcld 10458 |
. . . . 5
|
95 | 7, 23 | subge0d 10617 |
. . . . . 6
|
96 | 73, 95 | mpbird 247 |
. . . . 5
|
97 | | add20 10540 |
. . . . 5
|
98 | 91, 93, 94, 96, 97 | syl22anc 1327 |
. . . 4
|
99 | 98 | biimpa 501 |
. . 3
|
100 | 90, 99 | syldan 487 |
. 2
|
101 | 48 | recnd 10068 |
. . . . . . 7
|
102 | 55 | recnd 10068 |
. . . . . . 7
|
103 | 8, 8, 101, 102 | addsub4d 10439 |
. . . . . 6
|
104 | 27 | oveq1d 6665 |
. . . . . 6
|
105 | 103, 104 | eqtr3d 2658 |
. . . . 5
|
106 | 105 | adantr 481 |
. . . 4
|
107 | 88 | simprd 479 |
. . . 4
|
108 | 106, 107 | eqtrd 2656 |
. . 3
|
109 | 7, 48 | resubcld 10458 |
. . . . 5
|
110 | 7, 48 | subge0d 10617 |
. . . . . 6
|
111 | 79, 110 | mpbird 247 |
. . . . 5
|
112 | 7, 55 | resubcld 10458 |
. . . . 5
|
113 | 7, 55 | subge0d 10617 |
. . . . . 6
|
114 | 80, 113 | mpbird 247 |
. . . . 5
|
115 | | add20 10540 |
. . . . 5
|
116 | 109, 111,
112, 114, 115 | syl22anc 1327 |
. . . 4
|
117 | 116 | biimpa 501 |
. . 3
|
118 | 108, 117 | syldan 487 |
. 2
|
119 | 100, 118 | jca 554 |
1
|