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
forall n m. n + m = m + nEvery purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
0 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall n m. n + m = m + nProof neighborhood
Direct theorem prerequisites
Direct theorem dependents
BT0005 mul_succ_left BT000V add_left_cancel BT0013 le_add_right BT0015 add_le_add_left BT001N mul_lt_mul_succ_left_nonzero BT001R division_block_upper BT001S positive_quotient_gap_impossible BT001X add_eq_zero_left BT002G factor_difference BT0032 add_permute_outer BT0033 balanced_bezout_euclid_step BT0037 common_divisor_divides_balanced_result BT003Q mod_eq_trans BT003R mod_eq_add BT003W mod_eq_bounded_unique BT003X mod_eq_to_remainder_decomposition BT004C bezout_mod_left BT004E mod_eq_predecessor_cancel BT004O beta_moduli_coprime_of_lt_bounded_common_multiple BT00K5 beta_sum_pointwise_add BT00MY add_shuffle_middle BT00QK power_divides_exponent_antitone BT00R0 ceil_div_six_shift BT00R1 ceil_div_six_total BT00RD mul_le_cancel_left_nonzero BT00RG double_triple_remainder_complement_budget BT00SN pow_exponent_monotone_from_total BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00TL choose_symmetry BT00U0 four_power_central_recurrence_step BT00VG primorial_even_interval_divides_central BT00VH primorial_odd_interval_divides_middle BT00W4 pow_three_five_le_pow_four_four_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total BT00W7 linear_square_budget BT00W8 bertrand_scaled_budget_root_32 BT00WC bertrand_scaled_budget_root_36 BT00WD bertrand_scaled_budget_root_37 BT00X1 six_block_window_decomposition_above_thirty_two BT00XC add_lt_cancel_left BT00XG division_double_quotient_bit BT00XJ pow_le_pow_of_exponent_le BT00XQ power_quotient_prefix_sum_extend_zero BT00Y2 division_successor_quotient_divisor_le BT00Y3 beta_sum_double_carry_exact BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds BT00YB division_first_two_of_two_three_range BT010G floor_sqrt_third_quotient_gap_exists BT010I third_quotient_double_gap_exists BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval BT0112 no_bertrand_high_contribution_interval_eq_one BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one BT011O bertrand_add_swap_nested BT0120 bertrand_cover_eighty_three_one_hundred_sixty_three BT0121 bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen BT0122 bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one BT0123 bertrand_cutoff_lt_final_primeDefinition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
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.
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro n