| 1. | Nechť $p$ je prvek $\Natural$. | |
| 2. | $p$ je prvočíselné, právě tehdy, když $2 \leq p$ a pro všechny prvky $m$ $\Natural$, jestliže $\divides {m}{p}$, pak $m = 1$ nebo $m = p$. | Nat.prime_def |
| 3. | Nechť $x$ je prvek $\Natural$. | |
| 4. | Předpokládejme, že jestliže $\divides {x}{p}$, pak $x = 1$ nebo $x = p$. | |
| 5. | Předpokládejme, že $\divides {x}{p}$. | |
| 6. | $x = 1$ nebo $x = p$. | ifE 4, 5 |
| 7. | Předpokládejme, že $x < p$. | |
| 8. | $x \neq p$. | Nat.ne_of_lt 7 |
| 9. | $x = 1$. | Or.resolve_right 6, 8 |
| 10. | Jestliže $\divides {x}{p}$, pak $x = 1$. | ifI 9 [d] |
| 11. | Jestliže $x < p$, pak jestliže $\divides {x}{p}$, pak $x = 1$. | ifI 10 [l] |
| 12. | Předpokládejme, že jestliže $x < p$, pak jestliže $\divides {x}{p}$, pak $x = 1$. | |
| 13. | Předpokládejme, že $x < p$. | |
| 14. | Jestliže $\divides {x}{p}$, pak $x = 1$. | ifE 12, 13 |
| 15. | Předpokládejme, že $\divides {x}{p}$. | |
| 16. | $x = 1$. | ifE 14, 15 |
| 17. | Jestliže $x < p$, pak $x = 1$. | ifI 16 [l1] |
| 18. | Předpokládejme, že $2 \leq p$. | |
| 19. | Následník $0$ je menší nebo rovný než $p$. | Nat.le_of_succ_le 18 |
| 20. | $x \leq p$. | Nat.le_of_dvd 19, 15 |
| 21. | $x < p$ nebo $\EqtMACRoJ {x}{p}$. | LE.le.lt_or_eq_dec 20 |
| 22. | $x = 1$ nebo $x = p$. | Or.imp_left 17, 21 |
| 23. | Jestliže $\divides {x}{p}$, pak $x = 1$ nebo $x = p$. | ifI 22 [d2] |
| 24. | Jestliže $\divides {x}{p}$, pak $x = 1$ nebo $x = p$, právě tehdy, když jestliže $x < p$, pak jestliže $\divides {x}{p}$, pak $x = 1$. | iffI 11, 23 [h12, h13] |
| 25. | Pro všechny prvky $x$ $\Natural$, jestliže $\divides {x}{p}$, pak $x = 1$ nebo $x = p$, právě tehdy, když jestliže $x < p$, pak jestliže $\divides {x}{p}$, pak $x = 1$. | forallI 3, 24 [x] |
| 26. | Pro všechny prvky $m_{4}$ $\Natural$, jestliže $\divides {m_{4}}{p}$, pak $m_{4} = 1$ nebo $m_{4} = p$, právě tehdy, když pro všechny prvky $m_{5}$ $\Natural$, jestliže $m_{5} < p$, pak jestliže $\divides {m_{5}}{p}$, pak $m_{5} = 1$. | forall_congr' 25 |
| 27. | Jestliže $2 \leq p$, pak pro všechny prvky $a$ $\Natural$, jestliže $\divides {a}{p}$, pak $a = 1$ nebo $a = p$, právě tehdy, když pro všechny prvky $a_{1}$ $\Natural$, jestliže $a_{1} < p$, pak jestliže $\divides {a_{1}}{p}$, pak $a_{1} = 1$. | ifI 26 [p2] |
| 28. | $2 \leq p$ a pro všechny prvky $m_{2}$ $\Natural$, jestliže $\divides {m_{2}}{p}$, pak $m_{2} = 1$ nebo $m_{2} = p$, právě tehdy, když $2 \leq p$ a pro všechny prvky $m_{3}$ $\Natural$, jestliže $m_{3} < p$, pak jestliže $\divides {m_{3}}{p}$, pak $m_{3} = 1$. | and_congr_right 27 |
| 29. | $p$ je prvočíselné, právě tehdy, když $2 \leq p$ a pro všechny prvky $m_{1}$ $\Natural$, jestliže $m_{1} < p$, pak jestliže $\divides {m_{1}}{p}$, pak $m_{1} = 1$. | Iff.trans 2, 28 |