Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: CRing_with_id x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ K_field_0 x0 x0.
Claim L2: ∀ x2 . nat_p x2 ⟶ 4a41c.. x0 x1 x2 ∈ K_field_0 x0 x0
Apply nat_ind with λ x2 . 4a41c.. x0 x1 x2 ∈ K_field_0 x0 x0 leaving 2 subgoals.
Apply unknownprop_4ab72f93767fc325730724758d3093e7af2a82217c4d5ee8a2692818e418bf07 with x0, x1, λ x2 x3 . x3 ∈ K_field_0 x0 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_1a3d25fd41b7c3c508a2fe54709eb7f884df8973d52168382e0bc01da2bfd1d5 with x0.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H2: nat_p x2.
Assume H3: 4a41c.. x0 x1 x2 ∈ K_field_0 x0 x0.
Apply unknownprop_99ced72b0a1cc72e56a6449ae7f85ace98b316636257ef59b14e002a0cde881d with x0, x1, x2, λ x3 x4 . x4 ∈ K_field_0 x0 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply nat_p_omega with x2.
The subproof is completed by applying H2.
Apply unknownprop_83ca4313fe8b0637c2e8068a8b92f4bb986f1989193702cbeb0baf134d146d34 with x0, x1, 4a41c.. x0 x1 x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H3: x2 ∈ omega.
Apply L2 with x2.
Apply omega_nat_p with x2.
The subproof is completed by applying H3.
■