Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ u. ∀ m. ∀ n. ∀ v. ∀ r. ∀ s. ∀ h. ¬u = 0 → ¬n = 0 → Coprime(r,s) → m = u · u → n = 2 · (v · v) → m = r · r + s · s → n = 2 · (r · s) → h = m · m + n · n → ∃ x. ∃ y. SmallerFermatFourCounterexample(x,y,u,h)Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
Exact expanded first-order statement
forall u m n v r s h. ~(u = 0) -> ~(n = 0) -> (forall pff_divisor_ffd_second_parameters. (exists pff_left_ffd_second_parameters. (r) = pff_divisor_ffd_second_parameters * pff_left_ffd_second_parameters) -> (exists pff_right_ffd_second_parameters. (s) = pff_divisor_ffd_second_parameters * pff_right_ffd_second_parameters) -> pff_divisor_ffd_second_parameters = 1) -> m = u * u -> n = 2 * (v * v) -> m = r * r + s * s -> n = 2 * (r * s) -> h = m * m + n * n -> exists A B. ((((~((A) = 0) /\ (~((B) = 0) /\ (~((u) = 0) /\ ((A) * (A) * (A) * (A) + (B) * (B) * (B) * (B) = (u) * (u)))))) /\ (exists ffd_gap_second_result. ffd_gap_second_result + S u = h)))Proof neighborhood
Direct theorem prerequisites
PF001E coprime_square_product_factors factor_nonzero_left · Stable closed factor_nonzero_right · Alpha closed fourth_power_regroup · Stable closed PF002B fermat_four_root_lt_normDirect theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–15
03Establish hproductL16–25
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul left cancel nonzero.
04Calculate and transport equalitiesL26–26
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L26
symm
05Use earlier factsL27–28
06Establish hsquaresL29–35
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply coprime square product factors.
07Separate the logical casesL36–38
08Establish hrspositiveL39–47
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero right.
09Establish hrL48–56
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero left.
10Establish hsL57–65
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero right.
11Construct an explicit witnessL66–67
12Separate the logical casesL68–69
13Fix variables and assumptionsL70–70
Work with arbitrary variables or the premises of the current implication.
- L70
intro hzero
14Use earlier factsL71–77
15Separate the logical casesL78–78
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L78
split
16Fix variables and assumptionsL79–79
Work with arbitrary variables or the premises of the current implication.
- L79
intro hzero
17Use earlier factsL80–86
18Separate the logical casesL87–87
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L87
split
19Use earlier factsL88–88
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L88
exact hu
20Calculate and transport equalitiesL89–90
21Use earlier factsL91–92
22Calculate and transport equalitiesL93–96
23Use earlier factsL97–97
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L97
exact hsquares_witness_witness_left
24Calculate and transport equalitiesL98–98
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L98
symm
25Use earlier factsL99–99
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L99
exact hsquares_witness_witness_left
26Calculate and transport equalitiesL100–101
27Use earlier factsL102–102
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L102
exact hsquares_witness_witness_right
28Calculate and transport equalitiesL103–103
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L103
symm
29Use earlier factsL104–104
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L104
exact hsquares_witness_witness_right
30Calculate and transport equalitiesL105–106
31Use earlier factsL107–116
Instantiate or apply named facts and discharge the corresponding proof obligations.
32Use earlier factsL117–117
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L117
exact hh
Original defined command ledger · 117 lines
- 0001
intro u - 0002
intro m - 0003
intro n - 0004
intro v - 0005
intro r - 0006
intro s - 0007
intro h - 0008
intro hu - 0009
intro hn - 0010
intro hcoprime - 0011
intro hm - 0012
intro hnv - 0013
intro hmrs - 0014
intro hnrs - 0015
intro hh - 0016
have hproduct : r * s = v * v - 0017
specialize mul_left_cancel_nonzero (2) - 0018
specialize mul_left_cancel_nonzero (r * s) - 0019
specialize mul_left_cancel_nonzero (v * v) - 0020
apply mul_left_cancel_nonzero - 0021
intro hzero - 0022
specialize succ_ne_zero 1 - 0023
apply succ_ne_zero - 0024
exact hzero - 0025
trans n - 0026
symm - 0027
exact hnrs - 0028
exact hnv - 0029
have hsquares : exists A B. (r = A * A /\ s = B * B) - 0030
specialize coprime_square_product_factors (r) - 0031
specialize coprime_square_product_factors (s) - 0032
specialize coprime_square_product_factors (v) - 0033
apply coprime_square_product_factors - 0034
exact hcoprime - 0035
exact hproduct - 0036
cases hsquares - 0037
cases hsquares_witness - 0038
cases hsquares_witness_witness - 0039
have hrspositive : ~(r * s = 0) - 0040
intro hzero - 0041
specialize factor_nonzero_right (n) - 0042
specialize factor_nonzero_right (2) - 0043
specialize factor_nonzero_right (r * s) - 0044
apply factor_nonzero_right - 0045
exact hn - 0046
exact hnrs - 0047
exact hzero - 0048
have hr : ~(r = 0) - 0049
intro hzero - 0050
specialize factor_nonzero_left (r * s) - 0051
specialize factor_nonzero_left (r) - 0052
specialize factor_nonzero_left (s) - 0053
apply factor_nonzero_left - 0054
exact hrspositive - 0055
refl - 0056
exact hzero - 0057
have hs : ~(s = 0) - 0058
intro hzero - 0059
specialize factor_nonzero_right (r * s) - 0060
specialize factor_nonzero_right (r) - 0061
specialize factor_nonzero_right (s) - 0062
apply factor_nonzero_right - 0063
exact hrspositive - 0064
refl - 0065
exact hzero - 0066
exists x - 0067
exists x1 - 0068
split - 0069
split - 0070
intro hzero - 0071
specialize factor_nonzero_left (r) - 0072
specialize factor_nonzero_left (x) - 0073
specialize factor_nonzero_left (x) - 0074
apply factor_nonzero_left - 0075
exact hr - 0076
exact hsquares_witness_witness_left - 0077
exact hzero - 0078
split - 0079
intro hzero - 0080
specialize factor_nonzero_left (s) - 0081
specialize factor_nonzero_left (x1) - 0082
specialize factor_nonzero_left (x1) - 0083
apply factor_nonzero_left - 0084
exact hs - 0085
exact hsquares_witness_witness_right - 0086
exact hzero - 0087
split - 0088
exact hu - 0089
trans (x * x) * (x * x) + (x1 * x1) * (x1 * x1) - 0090
congr - 0091
apply fourth_power_regroup - 0092
apply fourth_power_regroup - 0093
trans r * r + s * s - 0094
congr - 0095
congr - 0096
symm - 0097
exact hsquares_witness_witness_left - 0098
symm - 0099
exact hsquares_witness_witness_left - 0100
congr - 0101
symm - 0102
exact hsquares_witness_witness_right - 0103
symm - 0104
exact hsquares_witness_witness_right - 0105
trans m - 0106
symm - 0107
exact hmrs - 0108
exact hm - 0109
specialize fermat_four_root_lt_norm (u) - 0110
specialize fermat_four_root_lt_norm (m) - 0111
specialize fermat_four_root_lt_norm (n) - 0112
specialize fermat_four_root_lt_norm (h) - 0113
apply fermat_four_root_lt_norm - 0114
exact hu - 0115
exact hn - 0116
exact hm - 0117
exact hh