Step | Hyp | Ref
| Expression |
1 | | 2sqreulem1 26810 |
. 2
โข ((๐ โ โ โง (๐ mod 4) = 1) โ
โ!๐ โ
โ0 โ!๐ โ โ0 (๐ โค ๐ โง ((๐โ2) + (๐โ2)) = ๐)) |
2 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐โ2) = (๐โ2)) |
3 | 2 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((๐โ2) + (๐โ2)) = ((๐โ2) + (๐โ2))) |
4 | 3 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ = ๐ โง (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0) โง ๐ โ โ0))
โ ((๐โ2) + (๐โ2)) = ((๐โ2) + (๐โ2))) |
5 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ ๐ โ
โ) |
6 | 5 | sqcld 14056 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ (๐โ2) โ
โ) |
7 | | 2times 12296 |
. . . . . . . . . . . . . . . . 17
โข ((๐โ2) โ โ โ
(2 ยท (๐โ2)) =
((๐โ2) + (๐โ2))) |
8 | 7 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
โข ((๐โ2) โ โ โ
((๐โ2) + (๐โ2)) = (2 ยท (๐โ2))) |
9 | 6, 8 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ ((๐โ2) + (๐โ2)) = (2 ยท (๐โ2))) |
10 | 9 | adantl 483 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0)
โ ((๐โ2) + (๐โ2)) = (2 ยท (๐โ2))) |
11 | 10 | ad2antrl 727 |
. . . . . . . . . . . . 13
โข ((๐ = ๐ โง (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0) โง ๐ โ โ0))
โ ((๐โ2) + (๐โ2)) = (2 ยท (๐โ2))) |
12 | 4, 11 | eqtrd 2777 |
. . . . . . . . . . . 12
โข ((๐ = ๐ โง (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0) โง ๐ โ โ0))
โ ((๐โ2) + (๐โ2)) = (2 ยท (๐โ2))) |
13 | 12 | eqeq1d 2739 |
. . . . . . . . . . 11
โข ((๐ = ๐ โง (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0) โง ๐ โ โ0))
โ (((๐โ2) +
(๐โ2)) = ๐ โ (2 ยท (๐โ2)) = ๐)) |
14 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (2 ยท (๐โ2)) โ (๐ mod 4) = ((2 ยท (๐โ2)) mod
4)) |
15 | 14 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (2 ยท (๐โ2)) โ ((๐ mod 4) = 1 โ ((2 ยท
(๐โ2)) mod 4) =
1)) |
16 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (2 ยท (๐โ2)) โ (๐ โ โ โ (2
ยท (๐โ2)) โ
โ)) |
17 | 15, 16 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (2 ยท (๐โ2)) โ (((๐ mod 4) = 1 โง ๐ โ โ) โ (((2
ยท (๐โ2)) mod 4)
= 1 โง (2 ยท (๐โ2)) โ โ))) |
18 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ0
โ ๐ โ
โค) |
19 | | 2nn0 12437 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 2 โ
โ0 |
20 | | zexpcl 13989 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โค โง 2 โ
โ0) โ (๐โ2) โ โค) |
21 | 18, 19, 20 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ0
โ (๐โ2) โ
โค) |
22 | | 2mulprm 16576 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐โ2) โ โค โ
((2 ยท (๐โ2))
โ โ โ (๐โ2) = 1)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ0
โ ((2 ยท (๐โ2)) โ โ โ (๐โ2) = 1)) |
24 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐โ2) = 1 โ (2 ยท
(๐โ2)) = (2 ยท
1)) |
25 | | 2t1e2 12323 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (2
ยท 1) = 2 |
26 | 24, 25 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐โ2) = 1 โ (2 ยท
(๐โ2)) =
2) |
27 | 26 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐โ2) = 1 โ ((2 ยท
(๐โ2)) mod 4) = (2 mod
4)) |
28 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 2 โ
โ |
29 | | 4nn 12243 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข 4 โ
โ |
30 | | nnrp 12933 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (4 โ
โ โ 4 โ โ+) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 4 โ
โ+ |
32 | | 0le2 12262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 0 โค
2 |
33 | | 2lt4 12335 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 2 <
4 |
34 | | modid 13808 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((2
โ โ โง 4 โ โ+) โง (0 โค 2 โง 2 <
4)) โ (2 mod 4) = 2) |
35 | 28, 31, 32, 33, 34 | mp4an 692 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (2 mod 4)
= 2 |
36 | 27, 35 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐โ2) = 1 โ ((2 ยท
(๐โ2)) mod 4) =
2) |
37 | 36 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐โ2) = 1 โ (((2
ยท (๐โ2)) mod 4)
= 1 โ 2 = 1)) |
38 | | 1ne2 12368 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 1 โ
2 |
39 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (2 = 1
โ 1 = 2) |
40 | | eqneqall 2955 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (1 = 2
โ (1 โ 2 โ (๐
โค ๐ โ ๐ โ ๐))) |
41 | 40 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (1 โ 2
โ (1 = 2 โ (๐
โค ๐ โ ๐ โ ๐))) |
42 | 39, 41 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (1 โ 2
โ (2 = 1 โ (๐
โค ๐ โ ๐ โ ๐))) |
43 | 38, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (2 = 1
โ (๐ โค ๐ โ ๐ โ ๐)) |
44 | 37, 43 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐โ2) = 1 โ (((2
ยท (๐โ2)) mod 4)
= 1 โ (๐ โค ๐ โ ๐ โ ๐))) |
45 | 23, 44 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ0
โ ((2 ยท (๐โ2)) โ โ โ (((2 ยท
(๐โ2)) mod 4) = 1
โ (๐ โค ๐ โ ๐ โ ๐)))) |
46 | 45 | impcomd 413 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ0
โ ((((2 ยท (๐โ2)) mod 4) = 1 โง (2 ยท (๐โ2)) โ โ) โ
(๐ โค ๐ โ ๐ โ ๐))) |
47 | 46 | com12 32 |
. . . . . . . . . . . . . . . . . 18
โข ((((2
ยท (๐โ2)) mod 4)
= 1 โง (2 ยท (๐โ2)) โ โ) โ (๐ โ โ0
โ (๐ โค ๐ โ ๐ โ ๐))) |
48 | 17, 47 | syl6bi 253 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (2 ยท (๐โ2)) โ (((๐ mod 4) = 1 โง ๐ โ โ) โ (๐ โ โ0
โ (๐ โค ๐ โ ๐ โ ๐)))) |
49 | 48 | expd 417 |
. . . . . . . . . . . . . . . 16
โข (๐ = (2 ยท (๐โ2)) โ ((๐ mod 4) = 1 โ (๐ โ โ โ (๐ โ โ0
โ (๐ โค ๐ โ ๐ โ ๐))))) |
50 | 49 | com34 91 |
. . . . . . . . . . . . . . 15
โข (๐ = (2 ยท (๐โ2)) โ ((๐ mod 4) = 1 โ (๐ โ โ0
โ (๐ โ โ
โ (๐ โค ๐ โ ๐ โ ๐))))) |
51 | 50 | eqcoms 2745 |
. . . . . . . . . . . . . 14
โข ((2
ยท (๐โ2)) =
๐ โ ((๐ mod 4) = 1 โ (๐ โ โ0
โ (๐ โ โ
โ (๐ โค ๐ โ ๐ โ ๐))))) |
52 | 51 | com14 96 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐ mod 4) = 1 โ (๐ โ โ0
โ ((2 ยท (๐โ2)) = ๐ โ (๐ โค ๐ โ ๐ โ ๐))))) |
53 | 52 | imp31 419 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0)
โ ((2 ยท (๐โ2)) = ๐ โ (๐ โค ๐ โ ๐ โ ๐))) |
54 | 53 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((๐ = ๐ โง (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0) โง ๐ โ โ0))
โ ((2 ยท (๐โ2)) = ๐ โ (๐ โค ๐ โ ๐ โ ๐))) |
55 | 13, 54 | sylbid 239 |
. . . . . . . . . 10
โข ((๐ = ๐ โง (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0) โง ๐ โ โ0))
โ (((๐โ2) +
(๐โ2)) = ๐ โ (๐ โค ๐ โ ๐ โ ๐))) |
56 | 55 | expimpd 455 |
. . . . . . . . 9
โข (๐ = ๐ โ (((((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0) โง ๐ โ โ0)
โง ((๐โ2) + (๐โ2)) = ๐) โ (๐ โค ๐ โ ๐ โ ๐))) |
57 | | 2a1 28 |
. . . . . . . . 9
โข (๐ โ ๐ โ (((((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0) โง ๐ โ โ0)
โง ((๐โ2) + (๐โ2)) = ๐) โ (๐ โค ๐ โ ๐ โ ๐))) |
58 | 56, 57 | pm2.61ine 3029 |
. . . . . . . 8
โข
(((((๐ โ
โ โง (๐ mod 4) =
1) โง ๐ โ
โ0) โง ๐ โ โ0) โง ((๐โ2) + (๐โ2)) = ๐) โ (๐ โค ๐ โ ๐ โ ๐)) |
59 | 58 | pm4.71d 563 |
. . . . . . 7
โข
(((((๐ โ
โ โง (๐ mod 4) =
1) โง ๐ โ
โ0) โง ๐ โ โ0) โง ((๐โ2) + (๐โ2)) = ๐) โ (๐ โค ๐ โ (๐ โค ๐ โง ๐ โ ๐))) |
60 | | nn0re 12429 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โ) |
61 | 60 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0)
โ ๐ โ
โ) |
62 | | nn0re 12429 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ๐ โ
โ) |
63 | | ltlen 11263 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ < ๐ โ (๐ โค ๐ โง ๐ โ ๐))) |
64 | 61, 62, 63 | syl2an 597 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ < ๐ โ (๐ โค ๐ โง ๐ โ ๐))) |
65 | 64 | bibi2d 343 |
. . . . . . . 8
โข ((((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ โค ๐ โ ๐ < ๐) โ (๐ โค ๐ โ (๐ โค ๐ โง ๐ โ ๐)))) |
66 | 65 | adantr 482 |
. . . . . . 7
โข
(((((๐ โ
โ โง (๐ mod 4) =
1) โง ๐ โ
โ0) โง ๐ โ โ0) โง ((๐โ2) + (๐โ2)) = ๐) โ ((๐ โค ๐ โ ๐ < ๐) โ (๐ โค ๐ โ (๐ โค ๐ โง ๐ โ ๐)))) |
67 | 59, 66 | mpbird 257 |
. . . . . 6
โข
(((((๐ โ
โ โง (๐ mod 4) =
1) โง ๐ โ
โ0) โง ๐ โ โ0) โง ((๐โ2) + (๐โ2)) = ๐) โ (๐ โค ๐ โ ๐ < ๐)) |
68 | 67 | ex 414 |
. . . . 5
โข ((((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0)
โง ๐ โ
โ0) โ (((๐โ2) + (๐โ2)) = ๐ โ (๐ โค ๐ โ ๐ < ๐))) |
69 | 68 | pm5.32rd 579 |
. . . 4
โข ((((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ โค ๐ โง ((๐โ2) + (๐โ2)) = ๐) โ (๐ < ๐ โง ((๐โ2) + (๐โ2)) = ๐))) |
70 | 69 | reubidva 3372 |
. . 3
โข (((๐ โ โ โง (๐ mod 4) = 1) โง ๐ โ โ0)
โ (โ!๐ โ
โ0 (๐ โค
๐ โง ((๐โ2) + (๐โ2)) = ๐) โ โ!๐ โ โ0 (๐ < ๐ โง ((๐โ2) + (๐โ2)) = ๐))) |
71 | 70 | reubidva 3372 |
. 2
โข ((๐ โ โ โง (๐ mod 4) = 1) โ
(โ!๐ โ
โ0 โ!๐ โ โ0 (๐ โค ๐ โง ((๐โ2) + (๐โ2)) = ๐) โ โ!๐ โ โ0 โ!๐ โ โ0
(๐ < ๐ โง ((๐โ2) + (๐โ2)) = ๐))) |
72 | 1, 71 | mpbid 231 |
1
โข ((๐ โ โ โง (๐ mod 4) = 1) โ
โ!๐ โ
โ0 โ!๐ โ โ0 (๐ < ๐ โง ((๐โ2) + (๐โ2)) = ๐)) |