Step | Hyp | Ref
| Expression |
1 | | 2sqnn 27288 |
. . 3
β’ ((π β β β§ (π mod 4) = 1) β βπ₯ β β βπ¦ β β π = ((π₯β2) + (π¦β2))) |
2 | | simpll 764 |
. . . . . . . . 9
β’ (((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2))) β π₯ β β) |
3 | 2 | adantl 481 |
. . . . . . . 8
β’ ((π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β π₯ β β) |
4 | | breq1 5141 |
. . . . . . . . . . 11
β’ (π = π₯ β (π β€ π β π₯ β€ π)) |
5 | | oveq1 7408 |
. . . . . . . . . . . . 13
β’ (π = π₯ β (πβ2) = (π₯β2)) |
6 | 5 | oveq1d 7416 |
. . . . . . . . . . . 12
β’ (π = π₯ β ((πβ2) + (πβ2)) = ((π₯β2) + (πβ2))) |
7 | 6 | eqeq1d 2726 |
. . . . . . . . . . 11
β’ (π = π₯ β (((πβ2) + (πβ2)) = π β ((π₯β2) + (πβ2)) = π)) |
8 | 4, 7 | anbi12d 630 |
. . . . . . . . . 10
β’ (π = π₯ β ((π β€ π β§ ((πβ2) + (πβ2)) = π) β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = π))) |
9 | 8 | reubidv 3386 |
. . . . . . . . 9
β’ (π = π₯ β (β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π) β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = π))) |
10 | 9 | adantl 481 |
. . . . . . . 8
β’ (((π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β§ π = π₯) β (β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π) β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = π))) |
11 | | simpr 484 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β) β π¦ β
β) |
12 | 11 | adantr 480 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β π¦ β β) |
13 | | breq2 5142 |
. . . . . . . . . . . . . . . . 17
β’ (π = π¦ β (π₯ β€ π β π₯ β€ π¦)) |
14 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π¦ β (πβ2) = (π¦β2)) |
15 | 14 | oveq2d 7417 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π¦ β ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) |
16 | 15 | eqeq1d 2726 |
. . . . . . . . . . . . . . . . 17
β’ (π = π¦ β (((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β ((π₯β2) + (π¦β2)) = ((π₯β2) + (π¦β2)))) |
17 | 13, 16 | anbi12d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = π¦ β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β (π₯ β€ π¦ β§ ((π₯β2) + (π¦β2)) = ((π₯β2) + (π¦β2))))) |
18 | | equequ1 2020 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π¦ β (π = π β π¦ = π)) |
19 | 18 | imbi2d 340 |
. . . . . . . . . . . . . . . . 17
β’ (π = π¦ β (((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π) β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π¦ = π))) |
20 | 19 | ralbidv 3169 |
. . . . . . . . . . . . . . . 16
β’ (π = π¦ β (βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π) β βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π¦ = π))) |
21 | 17, 20 | anbi12d 630 |
. . . . . . . . . . . . . . 15
β’ (π = π¦ β (((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π)) β ((π₯ β€ π¦ β§ ((π₯β2) + (π¦β2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π¦ = π)))) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β§ π = π¦) β (((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π)) β ((π₯ β€ π¦ β§ ((π₯β2) + (π¦β2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π¦ = π)))) |
23 | | simpr 484 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β π₯ β€ π¦) |
24 | | eqidd 2725 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β ((π₯β2) + (π¦β2)) = ((π₯β2) + (π¦β2))) |
25 | | nnre 12216 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β) |
26 | 25 | resqcld 14087 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (πβ2) β
β) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β§ π β β) β (πβ2) β β) |
28 | | nnre 12216 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β β β π¦ β
β) |
29 | 28 | resqcld 14087 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β β β (π¦β2) β
β) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β β β§ π¦ β β) β (π¦β2) β
β) |
31 | 30 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β§ π β β) β (π¦β2) β β) |
32 | | nnre 12216 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β β β π₯ β
β) |
33 | 32 | resqcld 14087 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β (π₯β2) β
β) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β β β§ π¦ β β) β (π₯β2) β
β) |
35 | 34 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β§ π β β) β (π₯β2) β β) |
36 | | readdcan 11385 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πβ2) β β β§
(π¦β2) β β
β§ (π₯β2) β
β) β (((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β (πβ2) = (π¦β2))) |
37 | 27, 31, 35, 36 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β§ π β β) β (((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β (πβ2) = (π¦β2))) |
38 | 28 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π₯ β
β β§ π¦ β
β) β§ π₯ β€ π¦) β§ π β β) β§ (πβ2) = (π¦β2)) β π¦ β β) |
39 | 25 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π₯ β
β β§ π¦ β
β) β§ π₯ β€ π¦) β§ π β β) β§ (πβ2) = (π¦β2)) β π β β) |
40 | | nnnn0 12476 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β β β π¦ β
β0) |
41 | 40 | nn0ge0d 12532 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β β β 0 β€
π¦) |
42 | 41 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π₯ β
β β§ π¦ β
β) β§ π₯ β€ π¦) β§ π β β) β§ (πβ2) = (π¦β2)) β 0 β€ π¦) |
43 | | nnnn0 12476 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β π β
β0) |
44 | 43 | nn0ge0d 12532 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β 0 β€
π) |
45 | 44 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π₯ β
β β§ π¦ β
β) β§ π₯ β€ π¦) β§ π β β) β§ (πβ2) = (π¦β2)) β 0 β€ π) |
46 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π₯ β
β β§ π¦ β
β) β§ π₯ β€ π¦) β§ π β β) β§ (πβ2) = (π¦β2)) β (πβ2) = (π¦β2)) |
47 | 46 | eqcomd 2730 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π₯ β
β β§ π¦ β
β) β§ π₯ β€ π¦) β§ π β β) β§ (πβ2) = (π¦β2)) β (π¦β2) = (πβ2)) |
48 | 38, 39, 42, 45, 47 | sq11d 14218 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π₯ β
β β§ π¦ β
β) β§ π₯ β€ π¦) β§ π β β) β§ (πβ2) = (π¦β2)) β π¦ = π) |
49 | 48 | ex 412 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β§ π β β) β ((πβ2) = (π¦β2) β π¦ = π)) |
50 | 37, 49 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β§ π β β) β (((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β π¦ = π)) |
51 | 50 | adantld 490 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β§ π β β) β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π¦ = π)) |
52 | 51 | ralrimiva 3138 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π¦ = π)) |
53 | 23, 24, 52 | jca31 514 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β ((π₯ β€ π¦ β§ ((π₯β2) + (π¦β2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π¦ = π))) |
54 | 12, 22, 53 | rspcedvd 3606 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π))) |
55 | | breq2 5142 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π₯ β€ π β π₯ β€ π)) |
56 | | oveq1 7408 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβ2) = (πβ2)) |
57 | 56 | oveq2d 7417 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π₯β2) + (πβ2)) = ((π₯β2) + (πβ2))) |
58 | 57 | eqeq1d 2726 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2)))) |
59 | 55, 58 | anbi12d 630 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
60 | 59 | reu8 3721 |
. . . . . . . . . . . . 13
β’
(β!π β
β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π))) |
61 | 54, 60 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π¦ β β) β§ π₯ β€ π¦) β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2)))) |
62 | 61 | ex 412 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β) β (π₯ β€ π¦ β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
63 | 62 | adantr 480 |
. . . . . . . . . 10
β’ (((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2))) β (π₯ β€ π¦ β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
64 | 63 | impcom 407 |
. . . . . . . . 9
β’ ((π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2)))) |
65 | | eqeq2 2736 |
. . . . . . . . . . . . 13
β’ (π = ((π₯β2) + (π¦β2)) β (((π₯β2) + (πβ2)) = π β ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2)))) |
66 | 65 | anbi2d 628 |
. . . . . . . . . . . 12
β’ (π = ((π₯β2) + (π¦β2)) β ((π₯ β€ π β§ ((π₯β2) + (πβ2)) = π) β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
67 | 66 | reubidv 3386 |
. . . . . . . . . . 11
β’ (π = ((π₯β2) + (π¦β2)) β (β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = π) β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
68 | 67 | adantl 481 |
. . . . . . . . . 10
β’ (((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2))) β (β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = π) β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
69 | 68 | adantl 481 |
. . . . . . . . 9
β’ ((π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β (β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = π) β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
70 | 64, 69 | mpbird 257 |
. . . . . . . 8
β’ ((π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β β!π β β (π₯ β€ π β§ ((π₯β2) + (πβ2)) = π)) |
71 | 3, 10, 70 | rspcedvd 3606 |
. . . . . . 7
β’ ((π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β βπ β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π)) |
72 | 11 | adantr 480 |
. . . . . . . . 9
β’ (((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2))) β π¦ β β) |
73 | 72 | adantl 481 |
. . . . . . . 8
β’ ((Β¬
π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β π¦ β β) |
74 | | breq1 5141 |
. . . . . . . . . . 11
β’ (π = π¦ β (π β€ π β π¦ β€ π)) |
75 | | oveq1 7408 |
. . . . . . . . . . . . 13
β’ (π = π¦ β (πβ2) = (π¦β2)) |
76 | 75 | oveq1d 7416 |
. . . . . . . . . . . 12
β’ (π = π¦ β ((πβ2) + (πβ2)) = ((π¦β2) + (πβ2))) |
77 | 76 | eqeq1d 2726 |
. . . . . . . . . . 11
β’ (π = π¦ β (((πβ2) + (πβ2)) = π β ((π¦β2) + (πβ2)) = π)) |
78 | 74, 77 | anbi12d 630 |
. . . . . . . . . 10
β’ (π = π¦ β ((π β€ π β§ ((πβ2) + (πβ2)) = π) β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = π))) |
79 | 78 | reubidv 3386 |
. . . . . . . . 9
β’ (π = π¦ β (β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π) β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = π))) |
80 | 79 | adantl 481 |
. . . . . . . 8
β’ (((Β¬
π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β§ π = π¦) β (β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π) β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = π))) |
81 | | simpll 764 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ π¦ β β) β§ Β¬
π₯ β€ π¦) β π₯ β β) |
82 | | breq2 5142 |
. . . . . . . . . . . . . . . . 17
β’ (π = π₯ β (π¦ β€ π β π¦ β€ π₯)) |
83 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π₯ β (πβ2) = (π₯β2)) |
84 | 83 | oveq2d 7417 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π₯ β ((π¦β2) + (πβ2)) = ((π¦β2) + (π₯β2))) |
85 | 84 | eqeq1d 2726 |
. . . . . . . . . . . . . . . . 17
β’ (π = π₯ β (((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β ((π¦β2) + (π₯β2)) = ((π₯β2) + (π¦β2)))) |
86 | 82, 85 | anbi12d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = π₯ β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β (π¦ β€ π₯ β§ ((π¦β2) + (π₯β2)) = ((π₯β2) + (π¦β2))))) |
87 | | equequ1 2020 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π₯ β (π = π β π₯ = π)) |
88 | 87 | imbi2d 340 |
. . . . . . . . . . . . . . . . 17
β’ (π = π₯ β (((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π) β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π₯ = π))) |
89 | 88 | ralbidv 3169 |
. . . . . . . . . . . . . . . 16
β’ (π = π₯ β (βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π) β βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π₯ = π))) |
90 | 86, 89 | anbi12d 630 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β (((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π)) β ((π¦ β€ π₯ β§ ((π¦β2) + (π₯β2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π₯ = π)))) |
91 | 90 | adantl 481 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β β) β§ Β¬
π₯ β€ π¦) β§ π = π₯) β (((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π)) β ((π¦ β€ π₯ β§ ((π¦β2) + (π₯β2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π₯ = π)))) |
92 | | ltnle 11290 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β β β§ π₯ β β) β (π¦ < π₯ β Β¬ π₯ β€ π¦)) |
93 | 28, 32, 92 | syl2anr 596 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π¦ β β) β (π¦ < π₯ β Β¬ π₯ β€ π¦)) |
94 | 28 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§ π¦ β β) β§ π¦ < π₯) β π¦ β β) |
95 | 32 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§ π¦ β β) β§ π¦ < π₯) β π₯ β β) |
96 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§ π¦ β β) β§ π¦ < π₯) β π¦ < π₯) |
97 | 94, 95, 96 | ltled 11359 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§ π¦ β β) β§ π¦ < π₯) β π¦ β€ π₯) |
98 | 97 | ex 412 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π¦ β β) β (π¦ < π₯ β π¦ β€ π₯)) |
99 | 93, 98 | sylbird 260 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π¦ β β) β (Β¬
π₯ β€ π¦ β π¦ β€ π₯)) |
100 | 99 | imp 406 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π¦ β β) β§ Β¬
π₯ β€ π¦) β π¦ β€ π₯) |
101 | 29 | recnd 11239 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β β β (π¦β2) β
β) |
102 | 101 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π¦ β β) β (π¦β2) β
β) |
103 | 33 | recnd 11239 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (π₯β2) β
β) |
104 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π¦ β β) β (π₯β2) β
β) |
105 | 102, 104 | addcomd 11413 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π¦ β β) β ((π¦β2) + (π₯β2)) = ((π₯β2) + (π¦β2))) |
106 | 105 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π¦ β β) β§ Β¬
π₯ β€ π¦) β ((π¦β2) + (π₯β2)) = ((π₯β2) + (π¦β2))) |
107 | 34 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π₯ β β β§ π¦ β β) β (π₯β2) β
β) |
108 | 107 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (π₯β2) β
β) |
109 | 30 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π₯ β β β§ π¦ β β) β (π¦β2) β
β) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (π¦β2) β
β) |
111 | 108, 110 | addcomd 11413 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β ((π₯β2) + (π¦β2)) = ((π¦β2) + (π₯β2))) |
112 | 111 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β ((π¦β2) + (πβ2)) = ((π¦β2) + (π₯β2)))) |
113 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (πβ2) β
β) |
114 | 33 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (π₯β2) β
β) |
115 | 29 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (π¦β2) β
β) |
116 | | readdcan 11385 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβ2) β β β§
(π₯β2) β β
β§ (π¦β2) β
β) β (((π¦β2) + (πβ2)) = ((π¦β2) + (π₯β2)) β (πβ2) = (π₯β2))) |
117 | 113, 114,
115, 116 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (((π¦β2) + (πβ2)) = ((π¦β2) + (π₯β2)) β (πβ2) = (π₯β2))) |
118 | 112, 117 | bitrd 279 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β (πβ2) = (π₯β2))) |
119 | 25 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π₯ β β β§ π¦ β β) β§ π β β) β§ (πβ2) = (π₯β2)) β π β β) |
120 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π₯ β β β§ π¦ β β) β π₯ β
β) |
121 | 120 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π₯ β β β§ π¦ β β) β§ π β β) β§ (πβ2) = (π₯β2)) β π₯ β β) |
122 | 44 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π₯ β β β§ π¦ β β) β§ π β β) β§ (πβ2) = (π₯β2)) β 0 β€ π) |
123 | | nnnn0 12476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β β β π₯ β
β0) |
124 | 123 | nn0ge0d 12532 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β β β 0 β€
π₯) |
125 | 124 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π₯ β β β§ π¦ β β) β 0 β€
π₯) |
126 | 125 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π₯ β β β§ π¦ β β) β§ π β β) β§ (πβ2) = (π₯β2)) β 0 β€ π₯) |
127 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π₯ β β β§ π¦ β β) β§ π β β) β§ (πβ2) = (π₯β2)) β (πβ2) = (π₯β2)) |
128 | 119, 121,
122, 126, 127 | sq11d 14218 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π₯ β β β§ π¦ β β) β§ π β β) β§ (πβ2) = (π₯β2)) β π = π₯) |
129 | 128 | eqcomd 2730 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π₯ β β β§ π¦ β β) β§ π β β) β§ (πβ2) = (π₯β2)) β π₯ = π) |
130 | 129 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β ((πβ2) = (π₯β2) β π₯ = π)) |
131 | 118, 130 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β π₯ = π)) |
132 | 131 | adantld 490 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π₯ = π)) |
133 | 132 | ralrimiva 3138 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π¦ β β) β
βπ β β
((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π₯ = π)) |
134 | 133 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π¦ β β) β§ Β¬
π₯ β€ π¦) β βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π₯ = π)) |
135 | 100, 106,
134 | jca31 514 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ π¦ β β) β§ Β¬
π₯ β€ π¦) β ((π¦ β€ π₯ β§ ((π¦β2) + (π₯β2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π₯ = π))) |
136 | 81, 91, 135 | rspcedvd 3606 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§ π¦ β β) β§ Β¬
π₯ β€ π¦) β βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π))) |
137 | | breq2 5142 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π¦ β€ π β π¦ β€ π)) |
138 | 56 | oveq2d 7417 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π¦β2) + (πβ2)) = ((π¦β2) + (πβ2))) |
139 | 138 | eqeq1d 2726 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2)) β ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2)))) |
140 | 137, 139 | anbi12d 630 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
141 | 140 | reu8 3721 |
. . . . . . . . . . . . 13
β’
(β!π β
β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β§ βπ β β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))) β π = π))) |
142 | 136, 141 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π¦ β β) β§ Β¬
π₯ β€ π¦) β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2)))) |
143 | 142 | ex 412 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β) β (Β¬
π₯ β€ π¦ β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
144 | 143 | adantr 480 |
. . . . . . . . . 10
β’ (((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2))) β (Β¬ π₯ β€ π¦ β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
145 | 144 | impcom 407 |
. . . . . . . . 9
β’ ((Β¬
π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2)))) |
146 | | eqeq2 2736 |
. . . . . . . . . . . . 13
β’ (π = ((π₯β2) + (π¦β2)) β (((π¦β2) + (πβ2)) = π β ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2)))) |
147 | 146 | anbi2d 628 |
. . . . . . . . . . . 12
β’ (π = ((π₯β2) + (π¦β2)) β ((π¦ β€ π β§ ((π¦β2) + (πβ2)) = π) β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
148 | 147 | reubidv 3386 |
. . . . . . . . . . 11
β’ (π = ((π₯β2) + (π¦β2)) β (β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = π) β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
149 | 148 | adantl 481 |
. . . . . . . . . 10
β’ (((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2))) β (β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = π) β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
150 | 149 | adantl 481 |
. . . . . . . . 9
β’ ((Β¬
π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β (β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = π) β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = ((π₯β2) + (π¦β2))))) |
151 | 145, 150 | mpbird 257 |
. . . . . . . 8
β’ ((Β¬
π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β β!π β β (π¦ β€ π β§ ((π¦β2) + (πβ2)) = π)) |
152 | 73, 80, 151 | rspcedvd 3606 |
. . . . . . 7
β’ ((Β¬
π₯ β€ π¦ β§ ((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2)))) β βπ β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π)) |
153 | 71, 152 | pm2.61ian 809 |
. . . . . 6
β’ (((π₯ β β β§ π¦ β β) β§ π = ((π₯β2) + (π¦β2))) β βπ β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π)) |
154 | 153 | ex 412 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β (π = ((π₯β2) + (π¦β2)) β βπ β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π))) |
155 | 154 | adantl 481 |
. . . 4
β’ (((π β β β§ (π mod 4) = 1) β§ (π₯ β β β§ π¦ β β)) β (π = ((π₯β2) + (π¦β2)) β βπ β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π))) |
156 | 155 | rexlimdvva 3203 |
. . 3
β’ ((π β β β§ (π mod 4) = 1) β
(βπ₯ β β
βπ¦ β β
π = ((π₯β2) + (π¦β2)) β βπ β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π))) |
157 | 1, 156 | mpd 15 |
. 2
β’ ((π β β β§ (π mod 4) = 1) β βπ β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π)) |
158 | | reurex 3372 |
. . . . 5
β’
(β!π β
β (π β€ π β§ ((πβ2) + (πβ2)) = π) β βπ β β (π β€ π β§ ((πβ2) + (πβ2)) = π)) |
159 | 158 | a1i 11 |
. . . 4
β’ (((π β β β§ (π mod 4) = 1) β§ π β β) β
(β!π β β
(π β€ π β§ ((πβ2) + (πβ2)) = π) β βπ β β (π β€ π β§ ((πβ2) + (πβ2)) = π))) |
160 | 159 | ralrimiva 3138 |
. . 3
β’ ((π β β β§ (π mod 4) = 1) β
βπ β β
(β!π β β
(π β€ π β§ ((πβ2) + (πβ2)) = π) β βπ β β (π β€ π β§ ((πβ2) + (πβ2)) = π))) |
161 | | 2sqmo 27286 |
. . . . 5
β’ (π β β β
β*π β
β0 βπ β β0 (π β€ π β§ ((πβ2) + (πβ2)) = π)) |
162 | | nnssnn0 12472 |
. . . . . 6
β’ β
β β0 |
163 | | nfcv 2895 |
. . . . . . 7
β’
β²πβ |
164 | | nfcv 2895 |
. . . . . . 7
β’
β²πβ0 |
165 | 163, 164 | ssrmof 4041 |
. . . . . 6
β’ (β
β β0 β (β*π β β0 βπ β β0
(π β€ π β§ ((πβ2) + (πβ2)) = π) β β*π β β βπ β β0 (π β€ π β§ ((πβ2) + (πβ2)) = π))) |
166 | 162, 165 | ax-mp 5 |
. . . . 5
β’
(β*π β
β0 βπ β β0 (π β€ π β§ ((πβ2) + (πβ2)) = π) β β*π β β βπ β β0 (π β€ π β§ ((πβ2) + (πβ2)) = π)) |
167 | | ssrexv 4043 |
. . . . . . 7
β’ (β
β β0 β (βπ β β (π β€ π β§ ((πβ2) + (πβ2)) = π) β βπ β β0 (π β€ π β§ ((πβ2) + (πβ2)) = π))) |
168 | 162, 167 | ax-mp 5 |
. . . . . 6
β’
(βπ β
β (π β€ π β§ ((πβ2) + (πβ2)) = π) β βπ β β0 (π β€ π β§ ((πβ2) + (πβ2)) = π)) |
169 | 168 | rmoimi 3730 |
. . . . 5
β’
(β*π β
β βπ β
β0 (π β€
π β§ ((πβ2) + (πβ2)) = π) β β*π β β βπ β β (π β€ π β§ ((πβ2) + (πβ2)) = π)) |
170 | 161, 166,
169 | 3syl 18 |
. . . 4
β’ (π β β β
β*π β β
βπ β β
(π β€ π β§ ((πβ2) + (πβ2)) = π)) |
171 | 170 | adantr 480 |
. . 3
β’ ((π β β β§ (π mod 4) = 1) β
β*π β β
βπ β β
(π β€ π β§ ((πβ2) + (πβ2)) = π)) |
172 | | rmoim 3728 |
. . 3
β’
(βπ β
β (β!π β
β (π β€ π β§ ((πβ2) + (πβ2)) = π) β βπ β β (π β€ π β§ ((πβ2) + (πβ2)) = π)) β (β*π β β βπ β β (π β€ π β§ ((πβ2) + (πβ2)) = π) β β*π β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π))) |
173 | 160, 171,
172 | sylc 65 |
. 2
β’ ((π β β β§ (π mod 4) = 1) β
β*π β β
β!π β β
(π β€ π β§ ((πβ2) + (πβ2)) = π)) |
174 | | reu5 3370 |
. 2
β’
(β!π β
β β!π β
β (π β€ π β§ ((πβ2) + (πβ2)) = π) β (βπ β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π) β§ β*π β β β!π β β (π β€ π β§ ((πβ2) + (πβ2)) = π))) |
175 | 157, 173,
174 | sylanbrc 582 |
1
β’ ((π β β β§ (π mod 4) = 1) β
β!π β β
β!π β β
(π β€ π β§ ((πβ2) + (πβ2)) = π)) |