Step | Hyp | Ref
| Expression |
1 | | breq1 5109 |
. . . . . 6
β’ (π₯ = 1 β (π₯ β₯ (FermatNoβπ) β 1 β₯ (FermatNoβπ))) |
2 | 1 | anbi2d 630 |
. . . . 5
β’ (π₯ = 1 β ((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
(π β
(β€β₯β2) β§ 1 β₯ (FermatNoβπ)))) |
3 | | eqeq1 2737 |
. . . . . 6
β’ (π₯ = 1 β (π₯ = ((π Β· (2β(π + 2))) + 1) β 1 = ((π Β· (2β(π + 2))) + 1))) |
4 | 3 | rexbidv 3172 |
. . . . 5
β’ (π₯ = 1 β (βπ β β0
π₯ = ((π Β· (2β(π + 2))) + 1) β βπ β β0 1 =
((π Β· (2β(π + 2))) + 1))) |
5 | 2, 4 | imbi12d 345 |
. . . 4
β’ (π₯ = 1 β (((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
βπ β
β0 π₯ =
((π Β· (2β(π + 2))) + 1)) β ((π β
(β€β₯β2) β§ 1 β₯ (FermatNoβπ)) β βπ β β0 1 =
((π Β· (2β(π + 2))) + 1)))) |
6 | | breq1 5109 |
. . . . . 6
β’ (π₯ = π¦ β (π₯ β₯ (FermatNoβπ) β π¦ β₯ (FermatNoβπ))) |
7 | 6 | anbi2d 630 |
. . . . 5
β’ (π₯ = π¦ β ((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
(π β
(β€β₯β2) β§ π¦ β₯ (FermatNoβπ)))) |
8 | | eqeq1 2737 |
. . . . . 6
β’ (π₯ = π¦ β (π₯ = ((π Β· (2β(π + 2))) + 1) β π¦ = ((π Β· (2β(π + 2))) + 1))) |
9 | 8 | rexbidv 3172 |
. . . . 5
β’ (π₯ = π¦ β (βπ β β0 π₯ = ((π Β· (2β(π + 2))) + 1) β βπ β β0
π¦ = ((π Β· (2β(π + 2))) + 1))) |
10 | 7, 9 | imbi12d 345 |
. . . 4
β’ (π₯ = π¦ β (((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
βπ β
β0 π₯ =
((π Β· (2β(π + 2))) + 1)) β ((π β
(β€β₯β2) β§ π¦ β₯ (FermatNoβπ)) β βπ β β0 π¦ = ((π Β· (2β(π + 2))) + 1)))) |
11 | | breq1 5109 |
. . . . . 6
β’ (π₯ = π§ β (π₯ β₯ (FermatNoβπ) β π§ β₯ (FermatNoβπ))) |
12 | 11 | anbi2d 630 |
. . . . 5
β’ (π₯ = π§ β ((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
(π β
(β€β₯β2) β§ π§ β₯ (FermatNoβπ)))) |
13 | | eqeq1 2737 |
. . . . . 6
β’ (π₯ = π§ β (π₯ = ((π Β· (2β(π + 2))) + 1) β π§ = ((π Β· (2β(π + 2))) + 1))) |
14 | 13 | rexbidv 3172 |
. . . . 5
β’ (π₯ = π§ β (βπ β β0 π₯ = ((π Β· (2β(π + 2))) + 1) β βπ β β0
π§ = ((π Β· (2β(π + 2))) + 1))) |
15 | 12, 14 | imbi12d 345 |
. . . 4
β’ (π₯ = π§ β (((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
βπ β
β0 π₯ =
((π Β· (2β(π + 2))) + 1)) β ((π β
(β€β₯β2) β§ π§ β₯ (FermatNoβπ)) β βπ β β0 π§ = ((π Β· (2β(π + 2))) + 1)))) |
16 | | breq1 5109 |
. . . . . 6
β’ (π₯ = (π¦ Β· π§) β (π₯ β₯ (FermatNoβπ) β (π¦ Β· π§) β₯ (FermatNoβπ))) |
17 | 16 | anbi2d 630 |
. . . . 5
β’ (π₯ = (π¦ Β· π§) β ((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
(π β
(β€β₯β2) β§ (π¦ Β· π§) β₯ (FermatNoβπ)))) |
18 | | eqeq1 2737 |
. . . . . 6
β’ (π₯ = (π¦ Β· π§) β (π₯ = ((π Β· (2β(π + 2))) + 1) β (π¦ Β· π§) = ((π Β· (2β(π + 2))) + 1))) |
19 | 18 | rexbidv 3172 |
. . . . 5
β’ (π₯ = (π¦ Β· π§) β (βπ β β0 π₯ = ((π Β· (2β(π + 2))) + 1) β βπ β β0
(π¦ Β· π§) = ((π Β· (2β(π + 2))) + 1))) |
20 | 17, 19 | imbi12d 345 |
. . . 4
β’ (π₯ = (π¦ Β· π§) β (((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
βπ β
β0 π₯ =
((π Β· (2β(π + 2))) + 1)) β ((π β
(β€β₯β2) β§ (π¦ Β· π§) β₯ (FermatNoβπ)) β βπ β β0 (π¦ Β· π§) = ((π Β· (2β(π + 2))) + 1)))) |
21 | | breq1 5109 |
. . . . . 6
β’ (π₯ = π β (π₯ β₯ (FermatNoβπ) β π β₯ (FermatNoβπ))) |
22 | 21 | anbi2d 630 |
. . . . 5
β’ (π₯ = π β ((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
(π β
(β€β₯β2) β§ π β₯ (FermatNoβπ)))) |
23 | | eqeq1 2737 |
. . . . . 6
β’ (π₯ = π β (π₯ = ((π Β· (2β(π + 2))) + 1) β π = ((π Β· (2β(π + 2))) + 1))) |
24 | 23 | rexbidv 3172 |
. . . . 5
β’ (π₯ = π β (βπ β β0 π₯ = ((π Β· (2β(π + 2))) + 1) β βπ β β0
π = ((π Β· (2β(π + 2))) + 1))) |
25 | 22, 24 | imbi12d 345 |
. . . 4
β’ (π₯ = π β (((π β (β€β₯β2)
β§ π₯ β₯
(FermatNoβπ)) β
βπ β
β0 π₯ =
((π Β· (2β(π + 2))) + 1)) β ((π β
(β€β₯β2) β§ π β₯ (FermatNoβπ)) β βπ β β0 π = ((π Β· (2β(π + 2))) + 1)))) |
26 | | 0nn0 12433 |
. . . . . . 7
β’ 0 β
β0 |
27 | 26 | a1i 11 |
. . . . . 6
β’ (π β
(β€β₯β2) β 0 β
β0) |
28 | | oveq1 7365 |
. . . . . . . . 9
β’ (π = 0 β (π Β· (2β(π + 2))) = (0 Β· (2β(π + 2)))) |
29 | 28 | oveq1d 7373 |
. . . . . . . 8
β’ (π = 0 β ((π Β· (2β(π + 2))) + 1) = ((0 Β· (2β(π + 2))) + 1)) |
30 | 29 | eqeq2d 2744 |
. . . . . . 7
β’ (π = 0 β (1 = ((π Β· (2β(π + 2))) + 1) β 1 = ((0
Β· (2β(π + 2)))
+ 1))) |
31 | 30 | adantl 483 |
. . . . . 6
β’ ((π β
(β€β₯β2) β§ π = 0) β (1 = ((π Β· (2β(π + 2))) + 1) β 1 = ((0 Β·
(2β(π + 2))) +
1))) |
32 | | 2nn0 12435 |
. . . . . . . . . . . 12
β’ 2 β
β0 |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β 2 β
β0) |
34 | | eluzge2nn0 12817 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β2) β π β
β0) |
35 | 34, 33 | nn0addcld 12482 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β (π + 2) β
β0) |
36 | 33, 35 | nn0expcld 14155 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β (2β(π + 2)) β
β0) |
37 | 36 | nn0cnd 12480 |
. . . . . . . . 9
β’ (π β
(β€β₯β2) β (2β(π + 2)) β β) |
38 | 37 | mul02d 11358 |
. . . . . . . 8
β’ (π β
(β€β₯β2) β (0 Β· (2β(π + 2))) = 0) |
39 | 38 | oveq1d 7373 |
. . . . . . 7
β’ (π β
(β€β₯β2) β ((0 Β· (2β(π + 2))) + 1) = (0 + 1)) |
40 | | 0p1e1 12280 |
. . . . . . 7
β’ (0 + 1) =
1 |
41 | 39, 40 | eqtr2di 2790 |
. . . . . 6
β’ (π β
(β€β₯β2) β 1 = ((0 Β· (2β(π + 2))) + 1)) |
42 | 27, 31, 41 | rspcedvd 3582 |
. . . . 5
β’ (π β
(β€β₯β2) β βπ β β0 1 = ((π Β· (2β(π + 2))) + 1)) |
43 | 42 | adantr 482 |
. . . 4
β’ ((π β
(β€β₯β2) β§ 1 β₯ (FermatNoβπ)) β βπ β β0 1 =
((π Β· (2β(π + 2))) + 1)) |
44 | | simpl 484 |
. . . . . . 7
β’ ((π β
(β€β₯β2) β§ π₯ β₯ (FermatNoβπ)) β π β
(β€β₯β2)) |
45 | 44 | adantl 483 |
. . . . . 6
β’ ((π₯ β β β§ (π β
(β€β₯β2) β§ π₯ β₯ (FermatNoβπ))) β π β
(β€β₯β2)) |
46 | | simpl 484 |
. . . . . 6
β’ ((π₯ β β β§ (π β
(β€β₯β2) β§ π₯ β₯ (FermatNoβπ))) β π₯ β β) |
47 | | simprr 772 |
. . . . . 6
β’ ((π₯ β β β§ (π β
(β€β₯β2) β§ π₯ β₯ (FermatNoβπ))) β π₯ β₯ (FermatNoβπ)) |
48 | | nnssnn0 12421 |
. . . . . . 7
β’ β
β β0 |
49 | | fmtnoprmfac2 45845 |
. . . . . . 7
β’ ((π β
(β€β₯β2) β§ π₯ β β β§ π₯ β₯ (FermatNoβπ)) β βπ β β π₯ = ((π Β· (2β(π + 2))) + 1)) |
50 | | ssrexv 4012 |
. . . . . . 7
β’ (β
β β0 β (βπ β β π₯ = ((π Β· (2β(π + 2))) + 1) β βπ β β0
π₯ = ((π Β· (2β(π + 2))) + 1))) |
51 | 48, 49, 50 | mpsyl 68 |
. . . . . 6
β’ ((π β
(β€β₯β2) β§ π₯ β β β§ π₯ β₯ (FermatNoβπ)) β βπ β β0 π₯ = ((π Β· (2β(π + 2))) + 1)) |
52 | 45, 46, 47, 51 | syl3anc 1372 |
. . . . 5
β’ ((π₯ β β β§ (π β
(β€β₯β2) β§ π₯ β₯ (FermatNoβπ))) β βπ β β0 π₯ = ((π Β· (2β(π + 2))) + 1)) |
53 | 52 | ex 414 |
. . . 4
β’ (π₯ β β β ((π β
(β€β₯β2) β§ π₯ β₯ (FermatNoβπ)) β βπ β β0 π₯ = ((π Β· (2β(π + 2))) + 1))) |
54 | | fmtnofac2lem 45846 |
. . . 4
β’ ((π¦ β
(β€β₯β2) β§ π§ β (β€β₯β2))
β ((((π β
(β€β₯β2) β§ π¦ β₯ (FermatNoβπ)) β βπ β β0 π¦ = ((π Β· (2β(π + 2))) + 1)) β§ ((π β (β€β₯β2)
β§ π§ β₯
(FermatNoβπ)) β
βπ β
β0 π§ =
((π Β· (2β(π + 2))) + 1))) β ((π β
(β€β₯β2) β§ (π¦ Β· π§) β₯ (FermatNoβπ)) β βπ β β0 (π¦ Β· π§) = ((π Β· (2β(π + 2))) + 1)))) |
55 | 5, 10, 15, 20, 25, 43, 53, 54 | prmind 16567 |
. . 3
β’ (π β β β ((π β
(β€β₯β2) β§ π β₯ (FermatNoβπ)) β βπ β β0 π = ((π Β· (2β(π + 2))) + 1))) |
56 | 55 | expd 417 |
. 2
β’ (π β β β (π β
(β€β₯β2) β (π β₯ (FermatNoβπ) β βπ β β0 π = ((π Β· (2β(π + 2))) + 1)))) |
57 | 56 | 3imp21 1115 |
1
β’ ((π β
(β€β₯β2) β§ π β β β§ π β₯ (FermatNoβπ)) β βπ β β0 π = ((π Β· (2β(π + 2))) + 1)) |