Step | Hyp | Ref
| Expression |
1 | | 4sq.r |
. . 3
β’ π
= ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) |
2 | | 4sq.a |
. . . . . . . . . . . 12
β’ (π β π΄ β β€) |
3 | | 4sq.m |
. . . . . . . . . . . . 13
β’ (π β π β
(β€β₯β2)) |
4 | | eluz2nn 12738 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β2) β π β β) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β β) |
6 | | 4sq.e |
. . . . . . . . . . . 12
β’ πΈ = (((π΄ + (π / 2)) mod π) β (π / 2)) |
7 | 2, 5, 6 | 4sqlem5 16749 |
. . . . . . . . . . 11
β’ (π β (πΈ β β€ β§ ((π΄ β πΈ) / π) β β€)) |
8 | 7 | simpld 496 |
. . . . . . . . . 10
β’ (π β πΈ β β€) |
9 | | zsqcl 13962 |
. . . . . . . . . 10
β’ (πΈ β β€ β (πΈβ2) β
β€) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (π β (πΈβ2) β β€) |
11 | 10 | zred 12540 |
. . . . . . . 8
β’ (π β (πΈβ2) β β) |
12 | | 4sq.b |
. . . . . . . . . . . 12
β’ (π β π΅ β β€) |
13 | | 4sq.f |
. . . . . . . . . . . 12
β’ πΉ = (((π΅ + (π / 2)) mod π) β (π / 2)) |
14 | 12, 5, 13 | 4sqlem5 16749 |
. . . . . . . . . . 11
β’ (π β (πΉ β β€ β§ ((π΅ β πΉ) / π) β β€)) |
15 | 14 | simpld 496 |
. . . . . . . . . 10
β’ (π β πΉ β β€) |
16 | | zsqcl 13962 |
. . . . . . . . . 10
β’ (πΉ β β€ β (πΉβ2) β
β€) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
β’ (π β (πΉβ2) β β€) |
18 | 17 | zred 12540 |
. . . . . . . 8
β’ (π β (πΉβ2) β β) |
19 | 11, 18 | readdcld 11118 |
. . . . . . 7
β’ (π β ((πΈβ2) + (πΉβ2)) β β) |
20 | | 4sq.c |
. . . . . . . . . . . 12
β’ (π β πΆ β β€) |
21 | | 4sq.g |
. . . . . . . . . . . 12
β’ πΊ = (((πΆ + (π / 2)) mod π) β (π / 2)) |
22 | 20, 5, 21 | 4sqlem5 16749 |
. . . . . . . . . . 11
β’ (π β (πΊ β β€ β§ ((πΆ β πΊ) / π) β β€)) |
23 | 22 | simpld 496 |
. . . . . . . . . 10
β’ (π β πΊ β β€) |
24 | | zsqcl 13962 |
. . . . . . . . . 10
β’ (πΊ β β€ β (πΊβ2) β
β€) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊβ2) β β€) |
26 | 25 | zred 12540 |
. . . . . . . 8
β’ (π β (πΊβ2) β β) |
27 | | 4sq.d |
. . . . . . . . . . . 12
β’ (π β π· β β€) |
28 | | 4sq.h |
. . . . . . . . . . . 12
β’ π» = (((π· + (π / 2)) mod π) β (π / 2)) |
29 | 27, 5, 28 | 4sqlem5 16749 |
. . . . . . . . . . 11
β’ (π β (π» β β€ β§ ((π· β π») / π) β β€)) |
30 | 29 | simpld 496 |
. . . . . . . . . 10
β’ (π β π» β β€) |
31 | | zsqcl 13962 |
. . . . . . . . . 10
β’ (π» β β€ β (π»β2) β
β€) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
β’ (π β (π»β2) β β€) |
33 | 32 | zred 12540 |
. . . . . . . 8
β’ (π β (π»β2) β β) |
34 | 26, 33 | readdcld 11118 |
. . . . . . 7
β’ (π β ((πΊβ2) + (π»β2)) β β) |
35 | 5 | nnred 12102 |
. . . . . . . . 9
β’ (π β π β β) |
36 | 35 | resqcld 14079 |
. . . . . . . 8
β’ (π β (πβ2) β β) |
37 | 36 | rehalfcld 12334 |
. . . . . . 7
β’ (π β ((πβ2) / 2) β
β) |
38 | 37 | rehalfcld 12334 |
. . . . . . . . 9
β’ (π β (((πβ2) / 2) / 2) β
β) |
39 | 2, 5, 6 | 4sqlem7 16751 |
. . . . . . . . 9
β’ (π β (πΈβ2) β€ (((πβ2) / 2) / 2)) |
40 | 12, 5, 13 | 4sqlem7 16751 |
. . . . . . . . 9
β’ (π β (πΉβ2) β€ (((πβ2) / 2) / 2)) |
41 | 11, 18, 38, 38, 39, 40 | le2addd 11708 |
. . . . . . . 8
β’ (π β ((πΈβ2) + (πΉβ2)) β€ ((((πβ2) / 2) / 2) + (((πβ2) / 2) / 2))) |
42 | 37 | recnd 11117 |
. . . . . . . . 9
β’ (π β ((πβ2) / 2) β
β) |
43 | 42 | 2halvesd 12333 |
. . . . . . . 8
β’ (π β ((((πβ2) / 2) / 2) + (((πβ2) / 2) / 2)) = ((πβ2) / 2)) |
44 | 41, 43 | breqtrd 5130 |
. . . . . . 7
β’ (π β ((πΈβ2) + (πΉβ2)) β€ ((πβ2) / 2)) |
45 | 20, 5, 21 | 4sqlem7 16751 |
. . . . . . . . 9
β’ (π β (πΊβ2) β€ (((πβ2) / 2) / 2)) |
46 | 27, 5, 28 | 4sqlem7 16751 |
. . . . . . . . 9
β’ (π β (π»β2) β€ (((πβ2) / 2) / 2)) |
47 | 26, 33, 38, 38, 45, 46 | le2addd 11708 |
. . . . . . . 8
β’ (π β ((πΊβ2) + (π»β2)) β€ ((((πβ2) / 2) / 2) + (((πβ2) / 2) / 2))) |
48 | 47, 43 | breqtrd 5130 |
. . . . . . 7
β’ (π β ((πΊβ2) + (π»β2)) β€ ((πβ2) / 2)) |
49 | 19, 34, 37, 37, 44, 48 | le2addd 11708 |
. . . . . 6
β’ (π β (((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) β€ (((πβ2) / 2) + ((πβ2) / 2))) |
50 | 36 | recnd 11117 |
. . . . . . 7
β’ (π β (πβ2) β β) |
51 | 50 | 2halvesd 12333 |
. . . . . 6
β’ (π β (((πβ2) / 2) + ((πβ2) / 2)) = (πβ2)) |
52 | 49, 51 | breqtrd 5130 |
. . . . 5
β’ (π β (((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) β€ (πβ2)) |
53 | 35 | recnd 11117 |
. . . . . 6
β’ (π β π β β) |
54 | 53 | sqvald 13975 |
. . . . 5
β’ (π β (πβ2) = (π Β· π)) |
55 | 52, 54 | breqtrd 5130 |
. . . 4
β’ (π β (((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) β€ (π Β· π)) |
56 | 19, 34 | readdcld 11118 |
. . . . 5
β’ (π β (((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) β β) |
57 | 5 | nngt0d 12136 |
. . . . 5
β’ (π β 0 < π) |
58 | | ledivmul 11965 |
. . . . 5
β’
(((((πΈβ2) +
(πΉβ2)) + ((πΊβ2) + (π»β2))) β β β§ π β β β§ (π β β β§ 0 <
π)) β (((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) β€ π β (((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) β€ (π Β· π))) |
59 | 56, 35, 35, 57, 58 | syl112anc 1375 |
. . . 4
β’ (π β (((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) β€ π β (((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) β€ (π Β· π))) |
60 | 55, 59 | mpbird 257 |
. . 3
β’ (π β ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) β€ π) |
61 | 1, 60 | eqbrtrid 5139 |
. 2
β’ (π β π
β€ π) |
62 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π
= 0) β π
= 0) |
63 | 1, 62 | eqtr3id 2792 |
. . . . . . . . . . . 12
β’ ((π β§ π
= 0) β ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) = 0) |
64 | 56 | recnd 11117 |
. . . . . . . . . . . . . . 15
β’ (π β (((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) β β) |
65 | 5 | nnne0d 12137 |
. . . . . . . . . . . . . . 15
β’ (π β π β 0) |
66 | 64, 53, 65 | diveq0ad 11875 |
. . . . . . . . . . . . . 14
β’ (π β (((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) = 0 β (((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) = 0)) |
67 | | zsqcl2 13970 |
. . . . . . . . . . . . . . . . . 18
β’ (πΈ β β€ β (πΈβ2) β
β0) |
68 | 8, 67 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΈβ2) β
β0) |
69 | | zsqcl2 13970 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β β€ β (πΉβ2) β
β0) |
70 | 15, 69 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΉβ2) β
β0) |
71 | 68, 70 | nn0addcld 12411 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΈβ2) + (πΉβ2)) β
β0) |
72 | 71 | nn0ge0d 12410 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β€ ((πΈβ2) + (πΉβ2))) |
73 | | zsqcl2 13970 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ β β€ β (πΊβ2) β
β0) |
74 | 23, 73 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΊβ2) β
β0) |
75 | | zsqcl2 13970 |
. . . . . . . . . . . . . . . . . 18
β’ (π» β β€ β (π»β2) β
β0) |
76 | 30, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π»β2) β
β0) |
77 | 74, 76 | nn0addcld 12411 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΊβ2) + (π»β2)) β
β0) |
78 | 77 | nn0ge0d 12410 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β€ ((πΊβ2) + (π»β2))) |
79 | | add20 11601 |
. . . . . . . . . . . . . . 15
β’
(((((πΈβ2) +
(πΉβ2)) β β
β§ 0 β€ ((πΈβ2) +
(πΉβ2))) β§ (((πΊβ2) + (π»β2)) β β β§ 0 β€
((πΊβ2) + (π»β2)))) β ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) = 0 β (((πΈβ2) + (πΉβ2)) = 0 β§ ((πΊβ2) + (π»β2)) = 0))) |
80 | 19, 72, 34, 78, 79 | syl22anc 838 |
. . . . . . . . . . . . . 14
β’ (π β ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) = 0 β (((πΈβ2) + (πΉβ2)) = 0 β§ ((πΊβ2) + (π»β2)) = 0))) |
81 | 66, 80 | bitrd 279 |
. . . . . . . . . . . . 13
β’ (π β (((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) = 0 β (((πΈβ2) + (πΉβ2)) = 0 β§ ((πΊβ2) + (π»β2)) = 0))) |
82 | 81 | biimpa 478 |
. . . . . . . . . . . 12
β’ ((π β§ ((((πΈβ2) + (πΉβ2)) + ((πΊβ2) + (π»β2))) / π) = 0) β (((πΈβ2) + (πΉβ2)) = 0 β§ ((πΊβ2) + (π»β2)) = 0)) |
83 | 63, 82 | syldan 592 |
. . . . . . . . . . 11
β’ ((π β§ π
= 0) β (((πΈβ2) + (πΉβ2)) = 0 β§ ((πΊβ2) + (π»β2)) = 0)) |
84 | 83 | simpld 496 |
. . . . . . . . . 10
β’ ((π β§ π
= 0) β ((πΈβ2) + (πΉβ2)) = 0) |
85 | 68 | nn0ge0d 12410 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (πΈβ2)) |
86 | 70 | nn0ge0d 12410 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (πΉβ2)) |
87 | | add20 11601 |
. . . . . . . . . . . 12
β’ ((((πΈβ2) β β β§ 0
β€ (πΈβ2)) β§
((πΉβ2) β β
β§ 0 β€ (πΉβ2)))
β (((πΈβ2) +
(πΉβ2)) = 0 β
((πΈβ2) = 0 β§
(πΉβ2) =
0))) |
88 | 11, 85, 18, 86, 87 | syl22anc 838 |
. . . . . . . . . . 11
β’ (π β (((πΈβ2) + (πΉβ2)) = 0 β ((πΈβ2) = 0 β§ (πΉβ2) = 0))) |
89 | 88 | biimpa 478 |
. . . . . . . . . 10
β’ ((π β§ ((πΈβ2) + (πΉβ2)) = 0) β ((πΈβ2) = 0 β§ (πΉβ2) = 0)) |
90 | 84, 89 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π
= 0) β ((πΈβ2) = 0 β§ (πΉβ2) = 0)) |
91 | 90 | simpld 496 |
. . . . . . . 8
β’ ((π β§ π
= 0) β (πΈβ2) = 0) |
92 | 2, 5, 6, 91 | 4sqlem9 16753 |
. . . . . . 7
β’ ((π β§ π
= 0) β (πβ2) β₯ (π΄β2)) |
93 | 90 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π
= 0) β (πΉβ2) = 0) |
94 | 12, 5, 13, 93 | 4sqlem9 16753 |
. . . . . . 7
β’ ((π β§ π
= 0) β (πβ2) β₯ (π΅β2)) |
95 | 5 | nnsqcld 14073 |
. . . . . . . . . 10
β’ (π β (πβ2) β β) |
96 | 95 | nnzd 12539 |
. . . . . . . . 9
β’ (π β (πβ2) β β€) |
97 | | zsqcl 13962 |
. . . . . . . . . 10
β’ (π΄ β β€ β (π΄β2) β
β€) |
98 | 2, 97 | syl 17 |
. . . . . . . . 9
β’ (π β (π΄β2) β β€) |
99 | | zsqcl 13962 |
. . . . . . . . . 10
β’ (π΅ β β€ β (π΅β2) β
β€) |
100 | 12, 99 | syl 17 |
. . . . . . . . 9
β’ (π β (π΅β2) β β€) |
101 | | dvds2add 16107 |
. . . . . . . . 9
β’ (((πβ2) β β€ β§
(π΄β2) β β€
β§ (π΅β2) β
β€) β (((πβ2) β₯ (π΄β2) β§ (πβ2) β₯ (π΅β2)) β (πβ2) β₯ ((π΄β2) + (π΅β2)))) |
102 | 96, 98, 100, 101 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (((πβ2) β₯ (π΄β2) β§ (πβ2) β₯ (π΅β2)) β (πβ2) β₯ ((π΄β2) + (π΅β2)))) |
103 | 102 | adantr 482 |
. . . . . . 7
β’ ((π β§ π
= 0) β (((πβ2) β₯ (π΄β2) β§ (πβ2) β₯ (π΅β2)) β (πβ2) β₯ ((π΄β2) + (π΅β2)))) |
104 | 92, 94, 103 | mp2and 698 |
. . . . . 6
β’ ((π β§ π
= 0) β (πβ2) β₯ ((π΄β2) + (π΅β2))) |
105 | 83 | simprd 497 |
. . . . . . . . . 10
β’ ((π β§ π
= 0) β ((πΊβ2) + (π»β2)) = 0) |
106 | 74 | nn0ge0d 12410 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (πΊβ2)) |
107 | 76 | nn0ge0d 12410 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (π»β2)) |
108 | | add20 11601 |
. . . . . . . . . . . 12
β’ ((((πΊβ2) β β β§ 0
β€ (πΊβ2)) β§
((π»β2) β β
β§ 0 β€ (π»β2)))
β (((πΊβ2) +
(π»β2)) = 0 β
((πΊβ2) = 0 β§
(π»β2) =
0))) |
109 | 26, 106, 33, 107, 108 | syl22anc 838 |
. . . . . . . . . . 11
β’ (π β (((πΊβ2) + (π»β2)) = 0 β ((πΊβ2) = 0 β§ (π»β2) = 0))) |
110 | 109 | biimpa 478 |
. . . . . . . . . 10
β’ ((π β§ ((πΊβ2) + (π»β2)) = 0) β ((πΊβ2) = 0 β§ (π»β2) = 0)) |
111 | 105, 110 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π
= 0) β ((πΊβ2) = 0 β§ (π»β2) = 0)) |
112 | 111 | simpld 496 |
. . . . . . . 8
β’ ((π β§ π
= 0) β (πΊβ2) = 0) |
113 | 20, 5, 21, 112 | 4sqlem9 16753 |
. . . . . . 7
β’ ((π β§ π
= 0) β (πβ2) β₯ (πΆβ2)) |
114 | 111 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π
= 0) β (π»β2) = 0) |
115 | 27, 5, 28, 114 | 4sqlem9 16753 |
. . . . . . 7
β’ ((π β§ π
= 0) β (πβ2) β₯ (π·β2)) |
116 | | zsqcl 13962 |
. . . . . . . . . 10
β’ (πΆ β β€ β (πΆβ2) β
β€) |
117 | 20, 116 | syl 17 |
. . . . . . . . 9
β’ (π β (πΆβ2) β β€) |
118 | | zsqcl 13962 |
. . . . . . . . . 10
β’ (π· β β€ β (π·β2) β
β€) |
119 | 27, 118 | syl 17 |
. . . . . . . . 9
β’ (π β (π·β2) β β€) |
120 | | dvds2add 16107 |
. . . . . . . . 9
β’ (((πβ2) β β€ β§
(πΆβ2) β β€
β§ (π·β2) β
β€) β (((πβ2) β₯ (πΆβ2) β§ (πβ2) β₯ (π·β2)) β (πβ2) β₯ ((πΆβ2) + (π·β2)))) |
121 | 96, 117, 119, 120 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (((πβ2) β₯ (πΆβ2) β§ (πβ2) β₯ (π·β2)) β (πβ2) β₯ ((πΆβ2) + (π·β2)))) |
122 | 121 | adantr 482 |
. . . . . . 7
β’ ((π β§ π
= 0) β (((πβ2) β₯ (πΆβ2) β§ (πβ2) β₯ (π·β2)) β (πβ2) β₯ ((πΆβ2) + (π·β2)))) |
123 | 113, 115,
122 | mp2and 698 |
. . . . . 6
β’ ((π β§ π
= 0) β (πβ2) β₯ ((πΆβ2) + (π·β2))) |
124 | 98, 100 | zaddcld 12544 |
. . . . . . . 8
β’ (π β ((π΄β2) + (π΅β2)) β β€) |
125 | 117, 119 | zaddcld 12544 |
. . . . . . . 8
β’ (π β ((πΆβ2) + (π·β2)) β β€) |
126 | | dvds2add 16107 |
. . . . . . . 8
β’ (((πβ2) β β€ β§
((π΄β2) + (π΅β2)) β β€ β§
((πΆβ2) + (π·β2)) β β€) β
(((πβ2) β₯
((π΄β2) + (π΅β2)) β§ (πβ2) β₯ ((πΆβ2) + (π·β2))) β (πβ2) β₯ (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))))) |
127 | 96, 124, 125, 126 | syl3anc 1372 |
. . . . . . 7
β’ (π β (((πβ2) β₯ ((π΄β2) + (π΅β2)) β§ (πβ2) β₯ ((πΆβ2) + (π·β2))) β (πβ2) β₯ (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))))) |
128 | 127 | adantr 482 |
. . . . . 6
β’ ((π β§ π
= 0) β (((πβ2) β₯ ((π΄β2) + (π΅β2)) β§ (πβ2) β₯ ((πΆβ2) + (π·β2))) β (πβ2) β₯ (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))))) |
129 | 104, 123,
128 | mp2and 698 |
. . . . 5
β’ ((π β§ π
= 0) β (πβ2) β₯ (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2)))) |
130 | 96 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π
= π) β (πβ2) β β€) |
131 | 124 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π
= π) β ((π΄β2) + (π΅β2)) β β€) |
132 | 43 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β ((((πβ2) / 2) / 2) + (((πβ2) / 2) / 2)) = ((πβ2) / 2)) |
133 | | 4sq.1 |
. . . . . . . . . . . . . . . 16
β’ π = {π β£ βπ₯ β β€ βπ¦ β β€ βπ§ β β€ βπ€ β β€ π = (((π₯β2) + (π¦β2)) + ((π§β2) + (π€β2)))} |
134 | | 4sq.2 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
135 | | 4sq.3 |
. . . . . . . . . . . . . . . 16
β’ (π β π = ((2 Β· π) + 1)) |
136 | | 4sq.4 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
137 | | 4sq.5 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...(2 Β· π)) β π) |
138 | | 4sq.6 |
. . . . . . . . . . . . . . . 16
β’ π = {π β β β£ (π Β· π) β π} |
139 | | 4sq.7 |
. . . . . . . . . . . . . . . 16
β’ π = inf(π, β, < ) |
140 | | 4sq.p |
. . . . . . . . . . . . . . . 16
β’ (π β (π Β· π) = (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2)))) |
141 | 133, 134,
135, 136, 137, 138, 139, 3, 2, 12, 20, 27, 6, 13, 21, 28, 1, 140 | 4sqlem15 16766 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π
= π) β ((((((πβ2) / 2) / 2) β (πΈβ2)) = 0 β§ ((((πβ2) / 2) / 2) β
(πΉβ2)) = 0) β§
(((((πβ2) / 2) / 2)
β (πΊβ2)) = 0
β§ ((((πβ2) / 2) /
2) β (π»β2)) =
0))) |
142 | 141 | simpld 496 |
. . . . . . . . . . . . . 14
β’ ((π β§ π
= π) β (((((πβ2) / 2) / 2) β (πΈβ2)) = 0 β§ ((((πβ2) / 2) / 2) β
(πΉβ2)) =
0)) |
143 | 142 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((π β§ π
= π) β ((((πβ2) / 2) / 2) β (πΈβ2)) = 0) |
144 | 38 | recnd 11117 |
. . . . . . . . . . . . . . 15
β’ (π β (((πβ2) / 2) / 2) β
β) |
145 | 10 | zcnd 12541 |
. . . . . . . . . . . . . . 15
β’ (π β (πΈβ2) β β) |
146 | 144, 145 | subeq0ad 11456 |
. . . . . . . . . . . . . 14
β’ (π β (((((πβ2) / 2) / 2) β (πΈβ2)) = 0 β (((πβ2) / 2) / 2) = (πΈβ2))) |
147 | 146 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π
= π) β (((((πβ2) / 2) / 2) β (πΈβ2)) = 0 β (((πβ2) / 2) / 2) = (πΈβ2))) |
148 | 143, 147 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π
= π) β (((πβ2) / 2) / 2) = (πΈβ2)) |
149 | 10 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π
= π) β (πΈβ2) β β€) |
150 | 148, 149 | eqeltrd 2839 |
. . . . . . . . . . 11
β’ ((π β§ π
= π) β (((πβ2) / 2) / 2) β
β€) |
151 | 150, 150 | zaddcld 12544 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β ((((πβ2) / 2) / 2) + (((πβ2) / 2) / 2)) β
β€) |
152 | 132, 151 | eqeltrrd 2840 |
. . . . . . . . 9
β’ ((π β§ π
= π) β ((πβ2) / 2) β
β€) |
153 | 131, 152 | zsubcld 12545 |
. . . . . . . 8
β’ ((π β§ π
= π) β (((π΄β2) + (π΅β2)) β ((πβ2) / 2)) β
β€) |
154 | 125 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π
= π) β ((πΆβ2) + (π·β2)) β β€) |
155 | 154, 152 | zsubcld 12545 |
. . . . . . . 8
β’ ((π β§ π
= π) β (((πΆβ2) + (π·β2)) β ((πβ2) / 2)) β
β€) |
156 | 98 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π
= π) β (π΄β2) β β€) |
157 | 156, 150 | zsubcld 12545 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β ((π΄β2) β (((πβ2) / 2) / 2)) β
β€) |
158 | 100 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π
= π) β (π΅β2) β β€) |
159 | 158, 150 | zsubcld 12545 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β ((π΅β2) β (((πβ2) / 2) / 2)) β
β€) |
160 | 2, 5, 6, 143 | 4sqlem10 16754 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β (πβ2) β₯ ((π΄β2) β (((πβ2) / 2) / 2))) |
161 | 142 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ π
= π) β ((((πβ2) / 2) / 2) β (πΉβ2)) = 0) |
162 | 12, 5, 13, 161 | 4sqlem10 16754 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β (πβ2) β₯ ((π΅β2) β (((πβ2) / 2) / 2))) |
163 | 130, 157,
159, 160, 162 | dvds2addd 16109 |
. . . . . . . . 9
β’ ((π β§ π
= π) β (πβ2) β₯ (((π΄β2) β (((πβ2) / 2) / 2)) + ((π΅β2) β (((πβ2) / 2) / 2)))) |
164 | 98 | zcnd 12541 |
. . . . . . . . . . . 12
β’ (π β (π΄β2) β β) |
165 | 100 | zcnd 12541 |
. . . . . . . . . . . 12
β’ (π β (π΅β2) β β) |
166 | 164, 165,
144, 144 | addsub4d 11493 |
. . . . . . . . . . 11
β’ (π β (((π΄β2) + (π΅β2)) β ((((πβ2) / 2) / 2) + (((πβ2) / 2) / 2))) = (((π΄β2) β (((πβ2) / 2) / 2)) + ((π΅β2) β (((πβ2) / 2) / 2)))) |
167 | 43 | oveq2d 7366 |
. . . . . . . . . . 11
β’ (π β (((π΄β2) + (π΅β2)) β ((((πβ2) / 2) / 2) + (((πβ2) / 2) / 2))) = (((π΄β2) + (π΅β2)) β ((πβ2) / 2))) |
168 | 166, 167 | eqtr3d 2780 |
. . . . . . . . . 10
β’ (π β (((π΄β2) β (((πβ2) / 2) / 2)) + ((π΅β2) β (((πβ2) / 2) / 2))) = (((π΄β2) + (π΅β2)) β ((πβ2) / 2))) |
169 | 168 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π
= π) β (((π΄β2) β (((πβ2) / 2) / 2)) + ((π΅β2) β (((πβ2) / 2) / 2))) = (((π΄β2) + (π΅β2)) β ((πβ2) / 2))) |
170 | 163, 169 | breqtrd 5130 |
. . . . . . . 8
β’ ((π β§ π
= π) β (πβ2) β₯ (((π΄β2) + (π΅β2)) β ((πβ2) / 2))) |
171 | 117 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π
= π) β (πΆβ2) β β€) |
172 | 171, 150 | zsubcld 12545 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β ((πΆβ2) β (((πβ2) / 2) / 2)) β
β€) |
173 | 119 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π
= π) β (π·β2) β β€) |
174 | 173, 150 | zsubcld 12545 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β ((π·β2) β (((πβ2) / 2) / 2)) β
β€) |
175 | 141 | simprd 497 |
. . . . . . . . . . . 12
β’ ((π β§ π
= π) β (((((πβ2) / 2) / 2) β (πΊβ2)) = 0 β§ ((((πβ2) / 2) / 2) β
(π»β2)) =
0)) |
176 | 175 | simpld 496 |
. . . . . . . . . . 11
β’ ((π β§ π
= π) β ((((πβ2) / 2) / 2) β (πΊβ2)) = 0) |
177 | 20, 5, 21, 176 | 4sqlem10 16754 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β (πβ2) β₯ ((πΆβ2) β (((πβ2) / 2) / 2))) |
178 | 175 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ π
= π) β ((((πβ2) / 2) / 2) β (π»β2)) = 0) |
179 | 27, 5, 28, 178 | 4sqlem10 16754 |
. . . . . . . . . 10
β’ ((π β§ π
= π) β (πβ2) β₯ ((π·β2) β (((πβ2) / 2) / 2))) |
180 | 130, 172,
174, 177, 179 | dvds2addd 16109 |
. . . . . . . . 9
β’ ((π β§ π
= π) β (πβ2) β₯ (((πΆβ2) β (((πβ2) / 2) / 2)) + ((π·β2) β (((πβ2) / 2) / 2)))) |
181 | 117 | zcnd 12541 |
. . . . . . . . . . . 12
β’ (π β (πΆβ2) β β) |
182 | 119 | zcnd 12541 |
. . . . . . . . . . . 12
β’ (π β (π·β2) β β) |
183 | 181, 182,
144, 144 | addsub4d 11493 |
. . . . . . . . . . 11
β’ (π β (((πΆβ2) + (π·β2)) β ((((πβ2) / 2) / 2) + (((πβ2) / 2) / 2))) = (((πΆβ2) β (((πβ2) / 2) / 2)) + ((π·β2) β (((πβ2) / 2) / 2)))) |
184 | 43 | oveq2d 7366 |
. . . . . . . . . . 11
β’ (π β (((πΆβ2) + (π·β2)) β ((((πβ2) / 2) / 2) + (((πβ2) / 2) / 2))) = (((πΆβ2) + (π·β2)) β ((πβ2) / 2))) |
185 | 183, 184 | eqtr3d 2780 |
. . . . . . . . . 10
β’ (π β (((πΆβ2) β (((πβ2) / 2) / 2)) + ((π·β2) β (((πβ2) / 2) / 2))) = (((πΆβ2) + (π·β2)) β ((πβ2) / 2))) |
186 | 185 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π
= π) β (((πΆβ2) β (((πβ2) / 2) / 2)) + ((π·β2) β (((πβ2) / 2) / 2))) = (((πΆβ2) + (π·β2)) β ((πβ2) / 2))) |
187 | 180, 186 | breqtrd 5130 |
. . . . . . . 8
β’ ((π β§ π
= π) β (πβ2) β₯ (((πΆβ2) + (π·β2)) β ((πβ2) / 2))) |
188 | 130, 153,
155, 170, 187 | dvds2addd 16109 |
. . . . . . 7
β’ ((π β§ π
= π) β (πβ2) β₯ ((((π΄β2) + (π΅β2)) β ((πβ2) / 2)) + (((πΆβ2) + (π·β2)) β ((πβ2) / 2)))) |
189 | 124 | zcnd 12541 |
. . . . . . . . . 10
β’ (π β ((π΄β2) + (π΅β2)) β β) |
190 | 125 | zcnd 12541 |
. . . . . . . . . 10
β’ (π β ((πΆβ2) + (π·β2)) β β) |
191 | 189, 190,
42, 42 | addsub4d 11493 |
. . . . . . . . 9
β’ (π β ((((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (((πβ2) / 2) + ((πβ2) / 2))) = ((((π΄β2) + (π΅β2)) β ((πβ2) / 2)) + (((πΆβ2) + (π·β2)) β ((πβ2) / 2)))) |
192 | 51 | oveq2d 7366 |
. . . . . . . . 9
β’ (π β ((((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (((πβ2) / 2) + ((πβ2) / 2))) = ((((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (πβ2))) |
193 | 191, 192 | eqtr3d 2780 |
. . . . . . . 8
β’ (π β ((((π΄β2) + (π΅β2)) β ((πβ2) / 2)) + (((πΆβ2) + (π·β2)) β ((πβ2) / 2))) = ((((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (πβ2))) |
194 | 193 | adantr 482 |
. . . . . . 7
β’ ((π β§ π
= π) β ((((π΄β2) + (π΅β2)) β ((πβ2) / 2)) + (((πΆβ2) + (π·β2)) β ((πβ2) / 2))) = ((((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (πβ2))) |
195 | 188, 194 | breqtrd 5130 |
. . . . . 6
β’ ((π β§ π
= π) β (πβ2) β₯ ((((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (πβ2))) |
196 | 124, 125 | zaddcld 12544 |
. . . . . . . 8
β’ (π β (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β β€) |
197 | 196 | adantr 482 |
. . . . . . 7
β’ ((π β§ π
= π) β (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β β€) |
198 | | dvdssubr 16122 |
. . . . . . 7
β’ (((πβ2) β β€ β§
(((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β β€) β ((πβ2) β₯ (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (πβ2) β₯ ((((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (πβ2)))) |
199 | 130, 197,
198 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π
= π) β ((πβ2) β₯ (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (πβ2) β₯ ((((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2))) β (πβ2)))) |
200 | 195, 199 | mpbird 257 |
. . . . 5
β’ ((π β§ π
= π) β (πβ2) β₯ (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2)))) |
201 | 129, 200 | jaodan 957 |
. . . 4
β’ ((π β§ (π
= 0 β¨ π
= π)) β (πβ2) β₯ (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2)))) |
202 | 140 | adantr 482 |
. . . 4
β’ ((π β§ (π
= 0 β¨ π
= π)) β (π Β· π) = (((π΄β2) + (π΅β2)) + ((πΆβ2) + (π·β2)))) |
203 | 201, 202 | breqtrrd 5132 |
. . 3
β’ ((π β§ (π
= 0 β¨ π
= π)) β (πβ2) β₯ (π Β· π)) |
204 | 203 | ex 414 |
. 2
β’ (π β ((π
= 0 β¨ π
= π) β (πβ2) β₯ (π Β· π))) |
205 | 61, 204 | jca 513 |
1
β’ (π β (π
β€ π β§ ((π
= 0 β¨ π
= π) β (πβ2) β₯ (π Β· π)))) |